YicesNative.CreateThe functor Create creates a new instance of the SMT solver with paramters passed as its arguments. The parameter argument P conataints a unique identifier id, initialized to the logic l and produces models if the optional labelled argument produce_models is true, proofs if produce_proofs is true, unsatisfiable cores if produce_unsat_cores is true, and unsatisfiable sets of assumptions if produce_unsat_assumptions is true
module P : SolverSig.Paramsmodule Conv : SMTExpr.ConvKill the underlying solver process without interacting with it. Unlike delete_instance this is safe to call from a different domain, to unblock an engine stuck in a solver call.
val declare_sort : SMTExpr.sort -> SolverResponse.decl_responseDeclare a new sort symbol
val declare_fun :
string ->
SMTExpr.sort list ->
SMTExpr.sort ->
SolverResponse.decl_responseDeclare a new function symbol
val define_fun :
string ->
SMTExpr.var list ->
SMTExpr.sort ->
SMTExpr.t ->
SolverResponse.decl_responseDefine a new function symbol as an abbreviation for an expression
val define_funs_rec :
(string * SMTExpr.var list * SMTExpr.sort * SMTExpr.t) list ->
SolverResponse.decl_responseDefine a group of (mutually) recursive function symbols, each given with its formal parameters, its result sort and its body, which may apply any symbol of the group
val assert_expr : SMTExpr.t -> SolverResponse.decl_responseAssert the expression
val assert_soft_expr : SMTExpr.t -> int -> SolverResponse.decl_responseval push : int -> SolverResponse.decl_responsePush a number of empty assertion sets to the stack
val pop : int -> SolverResponse.decl_responsePop a number of assertion sets from the stack
val check_sat : ?timeout:int -> unit -> SolverResponse.check_sat_responseCheck satisfiability of the asserted expressions
The optional parameter timeout limits the maximum runtime to the given number of milliseconds
val check_sat_assuming : SMTExpr.t list -> SolverResponse.check_sat_responseCheck satisfiability of the asserted expressions assuming the input literals.
Indicates whether the solver supports the check-sat-assuming command.
val get_value : SMTExpr.t list -> SolverResponse.get_value_responseGet the assigned values of expressions in the current model
val get_model : unit -> SolverResponse.get_model_responseGet the assigned values of expressions in the current model
val get_unsat_core : unit -> SolverResponse.get_unsat_core_responseGet an unsatisfiable core of named expressions
val get_unsat_assumptions : unit -> SolverResponse.get_unsat_core_responseGet an unsatisfiable subset of assumptions
val execute_custom_command :
string ->
SMTExpr.custom_arg list ->
int ->
SolverResponse.custom_responseExecute a custom command and return its result
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