package universo

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

Any SMT Logic

type t

Type for formulas

type smt_model

Model returns by the solver

type ctx

Meta informations needed by the solver

val logic : logic

Specify the logic implemented

val mk_name : 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