Module Solving.Z3synSource

module Z = Z3
Sourcetype t = Z.Expr.expr
Sourcetype smt_model = Z.Model.model
Sourcetype ctx = Z.context
Sourceval logic : [> `Qfuf ]
Sourceval sort : Z3.context -> Z.Sort.sort
Sourceval mk_name : B.name -> string

var_of_name name returns a variable string for Z3.

Sourceval mk_enum : Z3.context -> int -> Z.Expr.expr
Sourceval mk_var : Z3.context -> string -> Z.Expr.expr
Sourceval mk_sinf : Z3.context -> Z.Expr.expr
Sourceval mk_univ : Z3.context -> U.univ -> Z.Expr.expr

mk_univ ctx u construct a Z3 expression from a universe.

Sourceval bool_sort : Z3.context -> Z3.Sort.sort
Sourceval mk_axiom : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z.Expr.expr

mk_axiom s s' construct the Z3 predicate associated to the Axiom Predicate

Sourceval mk_cumul : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z.Expr.expr

mk_cumul s s' construct the Z3 predicate associated to the Cumul Predicate

Sourceval mk_rule : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z.Expr.expr

mk_rule s s' s'' construct the Z3 predicate associated to the Rule Predicate

Sourceval mk_bounds : Z3.context -> string -> int -> Z3.Expr.expr

register_vars vars i give bound for each variable var between 0 and i

Sourceval solution_of_var : Z3.context -> int -> Z.Model.model -> string -> U.univ

solution_of_var univs model var looks for the concrete universe associated to var in the model. Such universe satisfy that model(univ) = model(var).