module type Statement = sig .. end
type
The type of statements.
type
The type of identifiers.
type
The type of terms.
type
The type of locations.
val pop : ?loc:location -> int -> t
Pop the given number of level on the stack of assertions.
val push : ?loc:location -> int -> t
Push the given number of new level on the stack of assertions.
val assert_ : ?loc:location ->
term -> t
Add a proposition to the current set of assertions.
val check_sat : ?loc:location -> unit -> t
Solve the current set of assertions for satisfiability.
val set_logic : ?loc:location -> string -> t
Set the problem logic.
val get_info : ?loc:location -> string -> t
Get information (see smtlib manual).
val set_info : ?loc:location ->
string * term option -> t
Set information (see smtlib manual).
val get_option : ?loc:location -> string -> t
Get the value of a prover option.
val set_option : ?loc:location ->
string * term option -> t
Set the value of a prover option.
val type_decl : ?loc:location ->
id -> int -> t
Declares a new type constructor with given arity.
val type_def : ?loc:location ->
id ->
id list ->
term -> t
Defines an alias for types. type_def f args body is such that
later occurences of f applied to a list of arguments l should
be replaced by body where the args have been substituted by
their value in l.
val fun_decl : ?loc:location ->
id ->
term list ->
term -> t
Declares a new term symbol, and its type. fun_decl f args ret
declares f as a new function symbol which takes arguments of types
described in args, and with return type ret.
val fun_def : ?loc:location ->
id ->
term list ->
term ->
term -> t
Defines a new function. fun_def f args ret body is such that
applications of f are equal to body (module substitution of the arguments),
which should be of type ret.
val get_proof : ?loc:location -> unit -> t
Return the proof of the lastest check_sat if it returned unsat, else
is undefined.
val get_unsat_core : ?loc:location -> unit -> t
Return the unsat core of the latest check_sat if it returned unsat,
else is undefined.
val get_value : ?loc:location ->
term list -> t
Return the value of the given terms in the current model of the solver.
val get_assignment : ?loc:location -> unit -> t
Return the values of asserted propositions which have been labelled using
the ":named" attribute.
val get_assertions : ?loc:location -> unit -> t
Return the current set of assertions.
val exit : ?loc:location -> unit -> t
Exit the interactive loop.