Module Z3arith.MakeSource

Parameters

Signature

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