package universo

  1. Overview
  2. Docs

Parameters

module ZL : Z3LOGIC

Signature

val add : Common.Universes.cstr -> unit

add pred add the predicate cstr to the solver

val solve : Utils.env -> int * Utils.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.