diff options
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r-- | src/prop/prop_engine.h | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 603cdb0e6..dcfc5a9df 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -194,6 +194,37 @@ public: void assertLemma(TNode node, bool negated, bool removable); /** + * If ever n is decided upon, it must be in the given phase. This + * occurs *globally*, i.e., even if the literal is untranslated by + * user pop and retranslated, it keeps this phase. The associated + * variable will _always_ be phase-locked. + * + * @param n the node in question; must have an associated SAT literal + * @param phase the phase to use + */ + void requirePhase(TNode n, bool phase); + + /** + * Backtracks to and flips the most recent unflipped decision, and + * returns TRUE. If the decision stack is nonempty but all + * decisions have been flipped already, the state is backtracked to + * the root decision, which is re-flipped to the original phase (and + * FALSE is returned). If the decision stack is empty, the state is + * unchanged and FALSE is returned. + * + * @return true if a decision was flipped as requested; false if the + * root decision was reflipped, or if no decisions are on the stack. + */ + bool flipDecision(); + + /** + * Return whether the given literal is a SAT decision. Either phase + * is permitted; that is, if "lit" is a SAT decision, this function + * returns true for both lit and the negation of lit. + */ + bool isDecision(Node lit) const; + + /** * Checks the current context for satisfiability. * * @param millis the time limit for this call in milliseconds |