A  
add_clause [Solver_api.solver] 
Adds the clause (disjunction of pure Boolean terms) to the
solver.

add_clause [Solver_api.dpll] 
Adds the clause (disjunction of pure Boolean terms) to the
solver.

add_interface_variable [Solver_api.dpll]  add_interface_variables v treats the variable v and its
negation as an interface literal.

add_interface_variable [Solver_api.theory]  add_interface_variable v treats the variable v and its
negation as an interface literal.

B  
backjump [Solver_api.dpll] 
Resolve a conflict by backjumping to undo conflicting
assignments from the current partial model.

backjump [Solver_api.theory] 
Backjumps to the given level.

backjump_possible [Solver_api.dpll] 
Might a backjump be used to resolve a conflict?

C  
conflict_clause [Solver_api.theory] 
An explanation for a conflict.

conflict_detected [Solver_api.dpll] 
Has the solver deduced that the current (partial) model cannot
be (extended to) a satisfying variable assignment?

conflict_detected [Solver_api.theory] 
Has a conflict been detected in the current solver state?

D  
decide [Solver_api.dpll] 
Makes an arbitrary assignment to an unassigned variable.

decision_level [Solver_api.dpll] 
Decision level of the solver.

decision_level [Solver_api.theory] 
Decision level of the solver.

decision_possible [Solver_api.dpll] 
Might further arbitrary variable assignment decisions be
attempted?

F  
final_check [Solver_api.theory] 
Check consistency before the solver confirms satisfiability.

forget_some_learned_clauses [Solver_api.dpll] 
Forget some clauses learned by the solver though conflict
analysis.

G  
get_lemma [Solver_api.theory] 
Choose an inferred lemma that has not been dispatched before.

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

get_literal [Solver_api.dpll] 
Choose an interface literal assigned true in the current
partial model that has not been dispatched since it was
assigned.

get_literal [Solver_api.theory] 
Choose an inferred literal that has not been dispatched
before.

get_literal_possible [Solver_api.dpll] 
Is there an interface literal in the current partial model
that has not been dispatched by
Solver_api.dpll.get_literal since it was
assigned?

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

I  
increment_level [Solver_api.theory] 
Increment decision_level.

infer [Solver_api.dpll] 
Attempt to infer a unit propagation or a conflict.

infer [Solver_api.theory] 
Attempt to make inferences from currently assigned literals.

inference_possible [Solver_api.dpll] 
Might an inference be made?

inference_possible [Solver_api.theory] 
Might an inference be made?

is_interface_literal [Solver_api.dpll] 
Is the literal
l an interface literal for the solver.

is_interface_literal [Solver_api.theory] 
Is the literal
l an interface literal for the solver.

is_true [Solver_api.dpll] 
Is the literal
l assigned true in the solver state?

is_true [Solver_api.theory] 
Is the literal
l assigned true in the solver state?

L  
level [Solver_api.dpll] 
The decision level at which literal
l was assigned true.

literal_explanation [Solver_api.theory] 
An explanation clause for a literal.

literal_to_explain [Solver_api.dpll] 
Returns the next conflict literal to explain for conflict
resolution.

N  
num_clauses [Solver_api.dpll] 
Number of added clauses that are tracked in current state.

num_conflicts [Solver_api.dpll] 
Number of conflicts encountered.

num_decisions [Solver_api.dpll] 
Number of arbitrary variable assignment ever tried.

num_externally_set [Solver_api.dpll] 
Number of variable assignments ever made by
Solver_api.dpll.set_literal .

num_inferences [Solver_api.dpll] 
Number of variable assignment ever made by unit propagation.

num_learneds [Solver_api.dpll] 
Number of clauses learned through conflict analysis in current
state.

num_vars [Solver_api.dpll] 
Number of variables created.

O  
owns_constant [Solver_api.dpll]  owns_constant c holds when c is a boolean constant or
connective.

owns_constant [Solver_api.theory]  owns_constant t holds when the solver responsible for
reasoning about the constant t .

P  
proxy [Solver_api.dpll] 
A proxy for a pure boolean term.

proxy [Solver_api.theory] 
A proxy for a pure term.

R  
restart [Solver_api.dpll] 
Undo all arbitrary variable assignment decisions.

restart [Solver_api.theory] 
Backjumps to level 0 if not already there.

S  
satisfied [Solver_api.dpll] 
Has the solver deduced that the current model is a satisfying
assignment for every variable?

set_conflict_clause [Solver_api.dpll]  set_conflict_clause ls initializes the conflict clause with
the disjoined literals.

set_literal [Solver_api.dpll]  set_literal l attempts to make a variable assignment
inferred by an external agent.

set_literal [Solver_api.theory]  set_literal l attempts to make a variable assignment
inferred by an external agent.

set_literal_explanation [Solver_api.dpll]  set_literal_explanation ls removes Solver_api.dpll.literal_to_explain
from the set of conflict literals using the provided
explanation ls .

solve [Solver_api.solver] 
Determines the satisfiability of the conjunction of clauses
added to the solver.

U  
unsatisfiable [Solver_api.dpll] 
Has the solver deduced that the problem is unsatisfiable?

V  
variables [Solver_api.dpll] 
Set of all variables known to this solver.

variables [Solver_api.theory] 
Set of all variables known to this solver.
