Module Solving.UtilsSource

module B = Kernel.Basic
Sourcemodule M = Api.Meta

This module declares all the types and signatures needed to implement an smt solver.

Sourcetype logic = [
  1. | `Qfuf
  2. | `Lra
]

Qfuf is a logic with non-interpreted symbols, can be slow. Lra is linear arithmetic. Fast, but it requires an interpretation of CTS specification into linear arithmetic.

Sourcemodule type LOGIC = sig ... end

Any SMT Logic

Sourcetype env = {
  1. mk_theory : int -> Common.Oracle.theory;
    (*

    Compute a theory related to the target CTS specification.

    *)
  2. min : int;
    (*

    minimum number of universes to check

    *)
  3. max : int;
    (*

    maximum number of universes to check

    *)
  4. print : bool;
    (*

    print the problem in a file

    *)
}

configures the SMT solver

Sourcetype model = B.name -> Common.Universes.univ

model is a function that associate to each fresh universe a concrete universe.

Sourcemodule type SMTSOLVER = sig ... end

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

Sourcemodule type SOLVER = sig ... end

Generic solver for Universo

Sourceexception NoSolution