Class DecisionStack

Inheritance Relationships

Base Type

  • public std::vector< StackLevel >

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.