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:

Robert Nieuwenhuis, Albert Oliveras. Fast congruence closure and extensions. Information and Computation, 205(4):557-580, 2007.

Amit Goel, Sava Krstic. Deciding Array Formulas using Frugal Axiom Instantiation. Submitted for publication.

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 ()

Ensure Cc_core.decision_level s = 0
Ensure not (Cc_core.conflict_detected s)
Ensure not (Cc_core.get_literal_possible s)
Ensure not (Cc_core.inference_possible s)

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.

Require not (Cc_core.conflict_detected s)
Ensure not (Cc_core.conflict_detected s)

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 .

Require not (Cc_core.conflict_detected s)
Ensure not (Cc_core.conflict_detected s)

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.

Require not (Cc_core.conflict_detected s)
Ensure not (Cc_core.conflict_detected s)

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.

Require not (Cc_core.conflict_detected s)
Ensure not (Cc_core.conflict_detected s)

Solver Status

val decision_level : solver -> int

Decision level of the solver.

Ensure 0 <= decision_level s

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?

Require Cc_core.is_true s l

Inference

val infer : solver -> unit

Attempt to make inferences from currently assigned literals.

Require not (Cc_core.conflict_detected s)
Require Cc_core.inference_possible s

val final_check : solver -> unit

Determine consistency before we declare satisfiability.

Require not (Cc_core.conflict_detected s)
Require not (Cc_core.inference_possible s)
Require not (Cc_core.get_literal_possible s)
Require not (Cc_core.get_lemma_possible s)

val set_literal : solver -> Cc_literal.literal -> unit

Make a literal assignment obtained from another solver.

Require not (Cc_core.conflict_detected s)

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.

Require Cc_core.get_literal_possible s
Ensure Cc_core.is_true s l

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.

Require Cc_core.get_lemma_possible s

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

Require Cc_core.is_inferred s l
Ensure List.for_all (fun m -> m = l || Cc_core.is_true s (Cc_literal.negation m)) cls
Ensure List.mem l cls
Ensure List.length cls >= 2

val increment_level : solver -> unit

Increment decision_level.

Require not (Cc_core.conflict_detected s)
Require not (Cc_core.inference_possible s)
Require not (Cc_core.get_literal_possible s)
Ensure not (Cc_core.conflict_detected s)
Ensure not (Cc_core.inference_possible s)
Ensure not (Cc_core.get_literal_possible s)
Ensure Cc_core.decision_level s > 0

Conflict Resolution

val backjump : solver -> int -> unit

Backjumps to the given level.

For backjump s k:

Require 0 <= k && k < Cc_core.decision_level s
Ensure k = Cc_core.decision_level s
Ensure not (Cc_core.conflict_detected s)
Ensure not (Cc_core.inference_possible s)

val restart : solver -> unit

Backjumps to level 0 if not already there.

Require not (Cc_core.conflict_detected s)
Ensure not (Cc_core.conflict_detected s)
Ensure Cc_core.decision_level s = 0

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

Require Cc_core.conflict_detected s
Ensure List.for_all (fun l -> is_true s (Cc_literal.negation l)) cls
Ensure cls != []

Hosted by the

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