Class DecisionStack¶
- Defined in File stack.h
Class Documentation¶
-
class
DecisionStack
: public std::vector<StackLevel>¶ Vector based decision stack. It is also used during implicit BCP (i.e., failed literal testing).
Public Functions
-
DecisionStack
()¶
-
void
startFailedLitTest
()¶ Sets a flag to begin implicit BCP
-
void
stopFailedLitTest
()¶ Sets a flag to halt implicit BCP.
-
StackLevel &
top
()¶ Accessor for the top of the decision stack.
- Return
- Top of the decision stack.
-
const StackLevel &
top_const
() const¶ Accessor for the top of the decision stack.
- Return
- Top of the decision stack.
-
StackLevel &
on_deck
()¶ Get the element below the top, making it on deck in baseball parlance (i.e., it would be up next after the top).
- Return
- One below the top of the stack.
-
DecisionLevel
get_decision_level
() const¶ Height of the decision stack. This represents “d” in CDCL.
If a failed literal test is underway, a failed literal is pushed onto the stack during testing.
- Return
- Height of the stack.
-