Class type Solver_api.theory

class type theory = object .. end

method owns_constant : Term.term -> bool

owns_constant t holds when the solver responsible for reasoning about the constant t.

• Require Term.is_constant t

method proxy : Term.term -> Term.term

A proxy for a pure term.

method add_interface_variable : Term.term -> unit

add_interface_variable v treats the variable v and its negation as an interface literal.

• Require Term.is_variable v
• Require Term_set.mem v Solver_api.theory.variables

method variables : Term.Term_set.t

Set of all variables known to this solver.

• Ensure Term_set.for_all Term.is_variable variables

method decision_level : int

Decision level of the solver.

• Ensure decision_level >= 0

method inference_possible : bool

Might an inference be made?

method get_literal_possible : bool

Is there a literal that has been inferred, but not dispatched by Solver_api.theory.get_literal?

method get_lemma_possible : bool

Is there a lemma that has been inferred, but not dispatched by Solver_api.theory.get_lemma?

method conflict_detected : bool

Has a conflict been detected in the current solver state?

method is_interface_literal : Term.term -> bool

Is the literal l an interface literal for the solver.

• Require Term_literal.is_literal l
• Ensure is_interface_literal l = Term_set.mem (Term_literal.variable l) Solver_api.theory.variables

method is_true : Term.term -> bool

Is the literal l assigned true in the solver state?

• Require Solver_api.theory.is_interface_literal l

method infer : unit

Attempt to make inferences from currently assigned literals.

• Require not Solver_api.theory.conflict_detected
• Require Solver_api.theory.inference_possible

method set_literal : Term.term -> unit

set_literal l attempts to make a variable assignment inferred by an external agent.

• Require Solver_api.theory.is_interface_literal l
• Require not Solver_api.theory.conflict_detected

method get_literal : Term.term

Choose an inferred literal that has not been dispatched before.

• Require Solver_api.theory.get_literal_possible
• Ensure Solver_api.theory.is_true get_literal

method get_lemma : Term.term list

Choose an inferred lemma that has not been dispatched before.

• Require Solver_api.theory.get_lemma_possible
• Ensure List.for_all Solver_api.theory.is_interface_literal ls

method final_check : unit

Check consistency before the solver confirms satisfiability.

method increment_level : unit

Increment decision_level.

• Require not Solver_api.theory.conflict_detected
• Require not Solver_api.theory.inference_possible
• Require not Solver_api.theory.get_literal_possible
• Ensure not Solver_api.theory.conflict_detected
• Ensure not Solver_api.theory.inference_possible
• Ensure not Solver_api.theory.get_literal_possible
• Ensure Solver_api.theory.decision_level > 0

method backjump : int -> unit

Backjumps to the given level.

For backjump level:

• Require 0 <= level
• Require level < Solver_api.theory.decision_level
• Ensure level = Solver_api.theory.decision_level
• Ensure (not Solver_api.theory.conflict_detected)

method restart : unit

Backjumps to level 0 if not already there.

• Require not Solver_api.theory.conflict_detected
• Ensure Solver_api.theory.decision_level = 0
• Ensure not Solver_api.theory.conflict_detected

method conflict_clause : Term.term list

An explanation for a conflict. The explanation clause consists of interface literals that have been set in the solver.

• Require Solver_api.theory.conflict_detected
• Ensure List.for_all (fun l -> Solver_api.theory.is_true (Term_literal.negation l)) conflict_clause
• Ensure conflict_clause != []

method literal_explanation : Term.term -> Term.term list

An explanation clause for a literal. The explanation clause consists of literals that were given to Solver_api.theory.set_literal.

let cls = literal_explanation l

• Ensure List.for_all Solver_api.theory.is_interface_literal cls
• Ensure List.mem l cls
• Ensure List.for_all (fun m -> Solver_api.theory.is_true (Term_literal.negation m) || Term.term_equal l m) cls