module B = Kernel.Basicmodule L = Common.Logicmodule O = Common.Oraclemodule U = Common.Universesmodule Z = Z3type t = Z.Expr.exprtype smt_model = Z.Model.modeltype ctx = Z.contextval sort : Z3.context -> Z.Sort.sortval mk_name : B.name -> stringvar_of_name name returns a variable string for Z3.
val mk_enum : Z3.context -> int -> Z.Expr.exprval mk_var : Z3.context -> string -> Z.Expr.exprval mk_sinf : Z3.context -> Z.Expr.exprval mk_univ : Z3.context -> U.univ -> Z.Expr.exprmk_univ ctx u construct a Z3 expression from a universe.
val bool_sort : Z3.context -> Z3.Sort.sortval mk_axiom : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z.Expr.exprmk_axiom s s' construct the Z3 predicate associated to the Axiom Predicate
val mk_cumul : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z.Expr.exprmk_cumul s s' construct the Z3 predicate associated to the Cumul Predicate
val mk_rule :
Z3.context ->
Z3.Expr.expr ->
Z3.Expr.expr ->
Z3.Expr.expr ->
Z.Expr.exprmk_rule s s' s'' construct the Z3 predicate associated to the Rule Predicate
val mk_bounds : Z3.context -> string -> int -> Z3.Expr.exprregister_vars vars i give bound for each variable var between 0 and i
val solution_of_var : Z3.context -> int -> Z.Model.model -> string -> U.univsolution_of_var univs model var looks for the concrete universe associated to var in the model. Such universe satisfy that model(univ) = model(var).