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/Utils/module-type-SMTSOLVER/index.html

Module type `Utils.SMTSOLVER`Source

An SMT solver is a solver specific to one SMT such as Z3

val add : Common.Universes.cstr -> unit

add pred add the predicate cstr to the solver

val solve : env -> int * model

solve mk_theory call the solver and returns the mimimum number of universes needed to solve the constraints as long as the model. The theory used by solver depends on the number of universes needed. Hence one needs to provide a function mk_theory that builds a theory when at most i are used.