Parameter Make.ZL

type t = Z3.Expr.expr

Type for formulas

type smt_model = Z3.Model.model

Model returns by the solver

type ctx = Z3.context

Meta informations needed by the solver

val logic : Utils.logic

Specify the logic implemented

val mk_name : Solving.Utils.B.name -> string

mk_name n returns a SMT string from a Dedukti name n

val mk_var : ctx -> string -> t

mk_var ctx s returns a variable expression as to the name s

val mk_univ : ctx -> Common.Universes.univ -> t

mk_univ ctx u returns an expression associated to the universe u

val mk_axiom : ctx -> t -> t -> t

mk_axiom ctx s s' returns an expression encoding the predicate A(s,s')

val mk_cumul : ctx -> t -> t -> t

mk_cumul ctx s s' returns an expression encoding the predicate C(s,s')

val mk_rule : ctx -> t -> t -> t -> t

mk_rule ctx s s' s'' returns an expression encoding the predicate R(s,s',s'')

val mk_bounds : ctx -> string -> int -> t

mk_bound ctx s i returns an expression encoding that a variable cannot be higher that the ith universe

val solution_of_var : ctx -> int -> smt_model -> string -> Common.Universes.univ

solution_of_var ctx i model s returns the universe found by the SMT solver