Module Z3cfg.SynSource

Sourcetype t = Z3.Expr.expr

Type for formulas

Sourcetype smt_model = Z3.Model.model

Model returns by the solver

Sourcetype ctx = Z3.context

Meta informations needed by the solver

Sourceval logic : Utils.logic

Specify the logic implemented

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

mk_name n returns a SMT string from a Dedukti name n

Sourceval mk_var : ctx -> string -> t

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

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

mk_univ ctx u returns an expression associated to the universe u

Sourceval mk_axiom : ctx -> t -> t -> t

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

Sourceval mk_cumul : ctx -> t -> t -> t

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

Sourceval mk_rule : ctx -> t -> t -> t -> t

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

Sourceval 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

Sourceval 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