Module Cc_core

module Cc_core: sig .. end
Congruence-closure solver for EUF.

Congruence closure solver core for equality and updatable, uninterpreted functions based on the algorithms described in:

Solver Creation, Problem Setup and Solution

type solver 
Type of Congruence closure-based solver for Equality and Uninterpreted Functions.
val new_solver : unit -> solver
A new solver.

let s = new_solver ()

val fresh_variable : solver -> Cc_literal.Variable.t
A fresh variable in the given solver.
val proxy_app : solver ->
Cc_literal.Variable.t -> Cc_literal.Variable.t -> Cc_literal.Variable.t
proxy_app s f x returns a proxy y for the application of f to x.

val proxy_u : solver ->
Cc_literal.Variable.t ->
Cc_literal.Variable.t -> Cc_literal.Variable.t -> Cc_literal.Variable.t
proxy_u s a i x returns a proxy b for the update of a at i with x .

val proxy_k : solver -> Cc_literal.Variable.t -> Cc_literal.Variable.t
proxy_k s x returns a proxy a for the constant function evaluating to x.

val add_interface_literal : solver -> Cc_literal.Variable.t * Cc_literal.Variable.t -> unit
add_interface_literal s (x, y) records an interest in the literals x = y and x != y. Only interface literals are available via Cc_core.get_literal.

Solver Status

val decision_level : solver -> int
Decision level of the solver.

val inference_possible : solver -> bool
Might an inference be made?
val conflict_detected : solver -> bool
Has a conflict been detected in the current solver state?

Literal Status

val is_true : solver -> Cc_literal.literal -> bool
Is the literal assigned true in the solver state?
val is_inferred : solver -> Cc_literal.literal -> bool
Can the solver produce an explanation for a literal?


val infer : solver -> unit
Attempt to make inferences from currently assigned literals.

val final_check : solver -> unit
Determine consistency before we declare satisfiability.

val set_literal : solver -> Cc_literal.literal -> unit
Make a literal assignment obtained from another solver.

val get_literal_possible : solver -> bool
Are there any inferred interface literals waiting to be dispatched?
val get_literal : solver -> Cc_literal.literal
Choose an inferred interface literal that has not been chosen before.

val get_lemma_possible : solver -> bool
Are there any lemmas waiting to be dispatched?
val get_lemma : solver -> Cc_literal.lemma
Choose an inferred lemma that has not been chosen before.

val literal_explanation : solver -> Cc_literal.literal -> Cc_literal.literal list
An explanation clause for an assigned interface literal. The explanation clause consists of literals that were given to the solver.

let cls = literal_explanation l s in

val increment_level : solver -> unit
Increment decision_level.

Conflict Resolution

val backjump : solver -> int -> unit
Backjumps to the given level.

For backjump s k:

val restart : solver -> unit
Backjumps to level 0 if not already there.

val conflict_clause : solver -> Cc_literal.literal list
An explanation for a conflict. The explanation clause consists of interface literals that have been set in the solver.

let cls = conflict_clause s in

Hosted by the Logo* web site.
*Other names and brands may be claimed as the property of others.