sig
type z3_context = Z3.context
type z3_expr = Z3.Expr.expr
type z3_func_decl = Z3.FuncDecl.func_decl
type 'a open_expr =
[ `Add of 'a list
| `And of 'a list
| `App of SrkZ3.z3_func_decl * 'a list
| `Atom of [ `Eq | `Leq | `Lt ] * 'a * 'a
| `Binop of [ `Div | `Mod ] * 'a * 'a
| `Fls
| `Ite of 'a * 'a * 'a
| `Mul of 'a list
| `Not of 'a
| `Or of 'a list
| `Quantify of [ `Exists | `Forall ] * string * Syntax.typ_fo * 'a
| `Real of QQ.t
| `Tru
| `Unop of [ `Floor | `Neg ] * 'a
| `Var of int * Syntax.typ_fo ]
val z3_of_term :
'a Syntax.context -> SrkZ3.z3_context -> 'a Syntax.term -> SrkZ3.z3_expr
val z3_of_formula :
'a Syntax.context ->
SrkZ3.z3_context -> 'a Syntax.formula -> SrkZ3.z3_expr
val z3_of_expr :
'a Syntax.context ->
SrkZ3.z3_context -> ('a, Syntax.typ_fo) Syntax.expr -> SrkZ3.z3_expr
val term_of_z3 : 'a Syntax.context -> SrkZ3.z3_expr -> 'a Syntax.term
val formula_of_z3 : 'a Syntax.context -> SrkZ3.z3_expr -> 'a Syntax.formula
val expr_of_z3 :
'a Syntax.context -> SrkZ3.z3_expr -> ('a, Syntax.typ_fo) Syntax.expr
module Solver :
sig
type 'a t
val add : 'a SrkZ3.Solver.t -> 'a Syntax.formula list -> unit
val push : 'a SrkZ3.Solver.t -> unit
val pop : 'a SrkZ3.Solver.t -> int -> unit
val reset : 'a SrkZ3.Solver.t -> unit
val check :
'a SrkZ3.Solver.t ->
'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
val to_string : 'a SrkZ3.Solver.t -> string
val get_model :
?symbols:Syntax.symbol list ->
'a SrkZ3.Solver.t ->
[ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
val get_concrete_model :
'a SrkZ3.Solver.t ->
Syntax.symbol list ->
[ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
val get_unsat_core :
'a SrkZ3.Solver.t ->
'a Syntax.formula list ->
[ `Sat | `Unknown | `Unsat of 'a Syntax.formula list ]
end
val mk_solver :
?context:SrkZ3.z3_context ->
?theory:string -> 'a Syntax.context -> 'a SrkZ3.Solver.t
val optimize_box :
?context:SrkZ3.z3_context ->
'a Syntax.context ->
'a Syntax.formula ->
'a Syntax.term list -> [ `Sat of Interval.t list | `Unknown | `Unsat ]
val qe :
?context:SrkZ3.z3_context ->
'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
val load_smtlib2 :
?context:SrkZ3.z3_context ->
'a Syntax.context -> string -> 'a Syntax.formula
val interpolate_seq :
?context:SrkZ3.z3_context ->
'a Syntax.context ->
'a Syntax.formula list ->
[ `Sat of 'a Interpretation.interpretation
| `Unknown
| `Unsat of 'a Syntax.formula list ]
module CHC :
sig
type 'a solver
val mk_solver :
?context:SrkZ3.z3_context -> 'a Syntax.context -> 'a SrkZ3.CHC.solver
val register_relation : 'a SrkZ3.CHC.solver -> Syntax.symbol -> unit
val add_rule :
'a SrkZ3.CHC.solver -> 'a Syntax.formula -> 'a Syntax.formula -> unit
val add : 'a SrkZ3.CHC.solver -> 'a Syntax.formula list -> unit
val check :
'a SrkZ3.CHC.solver ->
'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
val get_solution :
'a SrkZ3.CHC.solver -> Syntax.symbol -> 'a Syntax.formula
val to_string : 'a SrkZ3.CHC.solver -> string
val push : 'a SrkZ3.CHC.solver -> unit
val pop : 'a SrkZ3.CHC.solver -> unit
end
end