package universo

You can search for identifiers within the package.

in-package search v0.2.0

package universo

universo.api
- Universo_api
universo.checking
- Checking
  - Checker
    
    MakeRE
    
    Conv
    
    RE
    
    Typing
universo.common
- Common
  - Constraints
  - Files
  - Log
  - Logic
    
    LRA_REIFICATION
    
    LRA_SPECIFICATION
    
    MakeLraSpecif
    
    Lra
    
    QFUF_SPECIFICATION
  - Oracle
    
    Util
  - Universes
    
    C
universo.elaboration
- Elaboration
  - Elaborate
  - Var
universo.solving
- Solving
  - Solver
    
    Make
    
    S
    
    MakeUF
    
    S
  - Utils
    
    LOGIC
    
    SMTSOLVER
    
    SOLVER
  - Z3arith
    
    Make
    
    Spec
  - Z3cfg
    
    Arith
    
    S
    
    Make
    
    ZL
    
    Syn
    
    Z3LOGIC
  - Z3syn

Legend:
Library
Module
Module type
Parameter
Class
Class type

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.