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