package universo

  1. Overview
  2. Docs
module B = Kernel.Basic
module L = Common.Logic
module O = Common.Oracle
module U = Common.Universes
module Z = Z3
type t = Z.Expr.expr
type smt_model = Z.Model.model
type ctx = Z.context
val logic : [> `Qfuf ]
val sort : Z3.context -> Z.Sort.sort
val mk_name : B.name -> string

var_of_name name returns a variable string for Z3.

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

mk_univ ctx u construct a Z3 expression from a universe.

val bool_sort : Z3.context -> Z3.Sort.sort

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

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

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

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

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

OCaml

Innovation. Community. Security.