Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
(* Smtlib2 printing *)(* ************************************************************************* *)
module type Smtlib2 = sig
type env type sexpr type ty type ty_var type ty_cst type term type term_var type term_cst
(** {2 Env} *)
val add_named : env -> term_cst -> term -> env (** Add a `:named` definition to the env. *)
val set_split_dec : env -> (string -> ([ `Pos | `Neg ] * string * string) option) -> env (** Set a splitting function for decimals. *)
(** {2 Helpers} *)
val match_prop_literal : term -> [ | `Cst of term_cst | `Neg of term_cst | `Not_a_prop_literal ] (** Match against prop literals. *)
(** {2 Types and terms} *)
val ty : env -> Format.formatter -> ty -> unit (** Printer for types *)
val term : env -> Format.formatter -> term -> unit (** Printer for terms *)
(** {2 Statements} *)
val echo : env -> Format.formatter -> string -> unit (** *)
val set_logic : env -> Format.formatter -> string -> unit (** Print a set-logic statement. *)
val set_info : env -> Format.formatter -> sexpr -> unit (** *)
val set_option : env -> Format.formatter-> sexpr -> unit (** *)
val get_info : env -> Format.formatter -> sexpr -> unit (** *)
val get_option : env -> Format.formatter -> sexpr -> unit (** *)
val get_value : env -> Format.formatter -> term list -> unit (** *)
val pop : env -> Format.formatter -> int -> unit (** [pop fmt n] prints a statement that pops `n` levels. @raise Cannot_print if the provided level is non-positive *)
val push : env -> Format.formatter -> int -> unit (** [push fmt n] prints a statement that pushes `n` levels. @raise Cannot_print if the provided level is non-positive *)
val declare_sort : env -> Format.formatter -> ty_cst -> unit (** Declare a sort, i.e. a type constant. *)
val declare_datatype : env -> Format.formatter -> ty_cst * ty_var list * (term_cst * (ty * term_cst) list) list -> unit (** Declare a single datatype. *)
val declare_datatypes : env -> Format.formatter -> (ty_cst * ty_var list * (term_cst * (ty * term_cst) list) list) list -> unit (** Declare multiple mutually recursive datatypes. *)
val declare_fun : env -> Format.formatter -> term_cst -> unit (** Declare a function, i.e. a term constant. This will use either the `declare-fun` or the `declare-const` statement depending on the actualy type of the function. *)
val define_sort : env -> Format.formatter -> (ty_cst * ty_var list * ty) -> unit (** *)
val define_fun : env -> Format.formatter -> (term_cst * ty_var list * term_var list * term) -> unit (** *)
val define_fun_rec : env -> Format.formatter -> (term_cst * ty_var list * term_var list * term) -> unit (** *)
val define_funs_rec : env -> Format.formatter -> (term_cst * ty_var list * term_var list * term) list -> unit (** *)
val assert_ : env -> Format.formatter -> term -> unit (** *)
val check_sat : env -> Format.formatter -> unit -> unit (** *)
val check_sat_assuming : env -> Format.formatter -> term list -> unit (** *)
val reset : env -> Format.formatter -> unit -> unit (** Print a `reset` statement. *)
val reset_assertions : env -> Format.formatter -> unit -> unit (** Print a `reset-assertion` statement. *)
val get_unsat_core : env -> Format.formatter -> unit -> unit (** Print a `get-unsat-core` statement. *)
val get_unsat_assumptions : env -> Format.formatter -> unit -> unit (** Print a `get-unsat-assumptions` statement. *)
val get_proof : env -> Format.formatter -> unit -> unit (** Print a `get-proof` statement. *)
val get_model : env -> Format.formatter -> unit -> unit (** Print a `get-model` statement. *)
val get_assertions : env -> Format.formatter -> unit -> unit (** Print a `get-assertions` statement. *)
val get_assignment : env -> Format.formatter -> unit -> unit (** Print a `get-assignment` statement. *)
val exit : env -> Format.formatter -> unit -> unit (** Print an `exit` statement. *)
end