package universo

  1. Overview
  2. Docs

Parameters

Signature

type t = Z3.Expr.expr
type smt_model = Z3.Model.model
type ctx = Z3.context
val logic : [> `Lra ]
val mk_name : B.name -> string
val int_sort : Z3.context -> Z3.Sort.sort
val mk_var : ctx -> string -> t
val to_int : ctx -> int -> t
val mk_univ : ctx -> U.univ -> t
val mk_max : ctx -> t -> t -> t
val mk_imax : ctx -> t -> t -> t
val mk : (ctx, t) L.k
val mk_axiom : ctx -> t -> t -> t
val mk_rule : ctx -> t -> t -> t -> t
val mk_cumul : ctx -> t -> t -> t
val mk_bounds : ctx -> string -> int -> Z3.Expr.expr
val solution_of_var : ctx -> int -> Z3.Model.model -> string -> U.univ
val mk_theory : bool