package universo

  1. Overview
  2. Docs

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.

OCaml

Innovation. Community. Security.