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.
|