sig
type solver
type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
val string_of_status : Z3.Solver.status -> string
module Statistics :
sig
type statistics
module Entry :
sig
type statistics_entry
val get_key : Z3.Solver.Statistics.Entry.statistics_entry -> string
val get_int : Z3.Solver.Statistics.Entry.statistics_entry -> int
val get_float :
Z3.Solver.Statistics.Entry.statistics_entry -> float
val is_int : Z3.Solver.Statistics.Entry.statistics_entry -> bool
val is_float : Z3.Solver.Statistics.Entry.statistics_entry -> bool
val to_string_value :
Z3.Solver.Statistics.Entry.statistics_entry -> string
val to_string :
Z3.Solver.Statistics.Entry.statistics_entry -> string
end
val to_string : Z3.Solver.Statistics.statistics -> string
val get_size : Z3.Solver.Statistics.statistics -> int
val get_entries :
Z3.Solver.Statistics.statistics ->
Z3.Solver.Statistics.Entry.statistics_entry list
val get_keys : Z3.Solver.Statistics.statistics -> string list
val get :
Z3.Solver.Statistics.statistics ->
string -> Z3.Solver.Statistics.Entry.statistics_entry option
end
val get_help : Z3.Solver.solver -> string
val set_parameters : Z3.Solver.solver -> Z3.Params.params -> unit
val get_param_descrs :
Z3.Solver.solver -> Z3.Params.ParamDescrs.param_descrs
val get_num_scopes : Z3.Solver.solver -> int
val push : Z3.Solver.solver -> unit
val pop : Z3.Solver.solver -> int -> unit
val reset : Z3.Solver.solver -> unit
val add : Z3.Solver.solver -> Z3.Expr.expr list -> unit
val assert_and_track_l :
Z3.Solver.solver -> Z3.Expr.expr list -> Z3.Expr.expr list -> unit
val assert_and_track :
Z3.Solver.solver -> Z3.Expr.expr -> Z3.Expr.expr -> unit
val get_num_assertions : Z3.Solver.solver -> int
val get_assertions : Z3.Solver.solver -> Z3.Expr.expr list
val check : Z3.Solver.solver -> Z3.Expr.expr list -> Z3.Solver.status
val get_model : Z3.Solver.solver -> Z3.Model.model option
val get_proof : Z3.Solver.solver -> Z3.Expr.expr option
val get_unsat_core : Z3.Solver.solver -> Z3.AST.ast list
val get_reason_unknown : Z3.Solver.solver -> string
val get_statistics : Z3.Solver.solver -> Z3.Solver.Statistics.statistics
val mk_solver : Z3.context -> Z3.Symbol.symbol option -> Z3.Solver.solver
val mk_solver_s : Z3.context -> string -> Z3.Solver.solver
val mk_simple_solver : Z3.context -> Z3.Solver.solver
val mk_solver_t : Z3.context -> Z3.Tactic.tactic -> Z3.Solver.solver
val to_string : Z3.Solver.solver -> string
end