Module SrkZ3

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