package universo

You can search for identifiers within the package.

in-package search v0.2.0

A tool for Dedukti to play with universes

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

D

dedukti-dev@inria.fr

Maintainers

D

dedukti-dev@inria.fr

Sources

v2.7.tar.gz

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/universo.solving/Solving/Z3syn/index.html

Module `Solving.Z3syn`Source

module B = Kernel.Basic

module L = Common.Logic

module O = Common.Oracle

module U = Common.Universes

module Z = Z3

Sourcetype t = Z.Expr.expr

Sourcetype smt_model = Z.Model.model

Sourcetype ctx = Z.context

Sourceval logic : [> `Qfuf ]

Sourceval sort : Z3.context -> Z.Sort.sort

Sourceval mk_name : B.name -> string

var_of_name name returns a variable string for Z3.

Sourceval mk_enum : Z3.context -> int -> Z.Expr.expr

Sourceval mk_var : Z3.context -> string -> Z.Expr.expr

Sourceval mk_sinf : Z3.context -> Z.Expr.expr

Sourceval mk_univ : Z3.context -> U.univ -> Z.Expr.expr

mk_univ ctx u construct a Z3 expression from a universe.

Sourceval bool_sort : Z3.context -> Z3.Sort.sort

Sourceval mk_axiom : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z.Expr.expr

mk_axiom s s' construct the Z3 predicate associated to the Axiom Predicate

Sourceval mk_cumul : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z.Expr.expr

mk_cumul s s' construct the Z3 predicate associated to the Cumul Predicate

Source

val mk_rule : 
  Z3.context ->
  Z3.Expr.expr ->
  Z3.Expr.expr ->
  Z3.Expr.expr ->
  Z.Expr.expr

mk_rule s s' s'' construct the Z3 predicate associated to the Rule Predicate

Sourceval mk_bounds : Z3.context -> string -> int -> Z3.Expr.expr

register_vars vars i give bound for each variable var between 0 and i

Sourceval solution_of_var : Z3.context -> int -> Z.Model.model -> string -> U.univ

solution_of_var univs model var looks for the concrete universe associated to var in the model. Such universe satisfy that model(univ) = model(var).