module type Inst =sig
..end
module Conv:SMTExpr.Conv
val delete_instance : unit -> unit
val declare_sort : SMTExpr.sort -> SolverResponse.decl_response
val declare_fun : string -> SMTExpr.sort list -> SMTExpr.sort -> SolverResponse.decl_response
val define_fun : string ->
SMTExpr.var list -> SMTExpr.sort -> SMTExpr.t -> SolverResponse.decl_response
val assert_expr : SMTExpr.t -> SolverResponse.decl_response
val push : int -> SolverResponse.decl_response
val pop : int -> SolverResponse.decl_response
val check_sat : ?timeout:int -> unit -> SolverResponse.check_sat_response
The optional parameter timeout
limits the maximum runtime to the given
number of milliseconds
val check_sat_assuming : SMTExpr.t list -> SolverResponse.check_sat_response
val check_sat_assuming_supported : unit -> bool
val get_value : SMTExpr.t list -> SolverResponse.get_value_response
val get_model : unit -> SolverResponse.get_model_response
val get_unsat_core : unit -> SolverResponse.get_unsat_core_response
val execute_custom_command : string -> SMTExpr.custom_arg list -> int -> SolverResponse.custom_response
execute_custom_command s c a r
sends a custom command s
with
the arguments a
to the solver instance s
. The command
expects r
S-expressions as result in case of success and
returns a pair of the success response and a list of
S-expressions.
val execute_custom_check_sat_command : string -> SolverResponse.check_sat_response
val trace_comment : string -> unit