package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Egraph
Ground terms
Different Object
Fix the models
Custom Environment and data-structures
Events
Choices
Helpers
For schedulers

Package contains no libraries

Colibri2 core: define basic types and the solver

Egraph

The Egraph contains all the context of a state of the analysis. Moreover it handles:

the consolidation of the unique domain for each equivalence class
execute callbacks when some events happens

The Egraph is piloted by a scheduler which distinguished four different phases:

Propagation phase
Decision phase
LastEffort phase
FixingModel phase

Each phase starts when there is nothing more to do in the previous phase, but a later phase can add work to a previous phase. A decision adds new possible propagations

module Egraph : sig ... end

Ground terms

The main representations of constraints are the ground terms. Each ground terms is associated to a node in the Egraph. The terms are simplified from the input syntax by substituting let bindings and separate the other bindings:

Ground.Term.t for the total application of a known symbol Builtin.t
Ground.ClosedQuantifier.t for close quantified formula
Ground.NotTotallyApplied.t for partial applications and anonymous lambdas

This separation allows to consider most of the time only Ground.Term.t terms.

module Ground : sig ... end

Different Object

The different kind of terms are reunited as Node.t by being indexed into theory terms ThTerm.t. Predefined theory terms are:

the theory term of Ground.s is Ground.t;
for Ground.ClosedQuantifier.s is Ground.ClosedQuantifier.t
for Ground.NotTotallyApplied.s is Ground.NotTotallyApplied.t

The theory terms can be transformed without cost directly as Node.t. New kind of theory terms are obtained by applying the functor ThTerm.Register

module Node : sig ... end

The nodes form equivalence class inside the Egraph

module ThTerm : sig ... end

ThTerm allows to associates an OCaml type to a uniq Node.t using an indexing table

Another kind of nodes are values. They are disjoint but similar to theory terms. The goal of the solver is to find one Value.t for each expression of the input problem. They are registered using Value.Register.

module Value : sig ... end

One Value.t can be associated to an equivalence class and a Value.t is associated to an uniq Node.t

Domains are additional informations associated to each equivalence class inside the _Egraph.t. They can be registered using Dom.register or when the domain is simple by Dom.Lattice

module Dom : sig ... end

module Expr : sig ... end

The module Expr corresponds to the typed expression parsed and typed by Dolmen. It is generally not useful.

module Builtin = Dolmen_std.Builtin

Fix the models

The module Interp handles:

Checking the model before answering SAT, the interpretation of the application are provided using Interp.Register.check
Enumerating the possible values for each node Interp.Register.node
Otherwise enumerating the possible values of each type Interp.Register.ty

module Interp : sig ... end

Custom Environment and data-structures

module Env : sig ... end

Theory specific environment

module Datastructure : sig ... end