module SrkZ3: sig
.. end
Interface to
Z3 SMT solver
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 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 -> z3_context -> 'a Syntax.term -> z3_expr
val z3_of_formula : 'a Syntax.context -> z3_context -> 'a Syntax.formula -> z3_expr
val z3_of_expr : 'a Syntax.context ->
z3_context -> ('a, Syntax.typ_fo) Syntax.expr -> z3_expr
val term_of_z3 : 'a Syntax.context -> z3_expr -> 'a Syntax.term
Convert a Z3 expression into a term. Raises Invalid_argument on
failure.
val formula_of_z3 : 'a Syntax.context -> z3_expr -> 'a Syntax.formula
Convert a Z3 expression into a formula. Raises Invalid_argument on
failure.
val expr_of_z3 : 'a Syntax.context -> z3_expr -> ('a, Syntax.typ_fo) Syntax.expr
Convert a Z3 expression into an expression. Raises Invalid_argument on
failure.
module Solver: sig
.. end
val mk_solver : ?context:z3_context ->
?theory:string -> 'a Syntax.context -> 'a Solver.t
val optimize_box : ?context:z3_context ->
'a Syntax.context ->
'a Syntax.formula ->
'a Syntax.term list -> [ `Sat of Interval.t list | `Unknown | `Unsat ]
Given a formula phi and a list of objectives o1,...,on
, find the least
bounding interval for each objective within the feasible region defined by
the formula.
val qe : ?context:z3_context ->
'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
Quantifier elimination
val load_smtlib2 : ?context:z3_context -> 'a Syntax.context -> string -> 'a Syntax.formula
Parse a SMTLIB2-formatted string
val interpolate_seq : ?context:z3_context ->
'a Syntax.context ->
'a Syntax.formula list ->
[ `Sat of 'a Interpretation.interpretation
| `Unknown
| `Unsat of 'a Syntax.formula list ]
Sequence interpolation. Returns either a model of the formula or a
sequence of interpolants if there is no model.
module CHC: sig
.. end
Constrained Horn Clauses