Z3syn (p.universo.2.7.doc.universo.solving.Solving.Z3syn)

module B = Kernel.Basic

module L = Common.Logic

module O = Common.Oracle

module U = Common.Universes

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

Source

val 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).