diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 702a530cf..f3904549f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -126,6 +126,24 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) { d_cnfStream->convertAndAssert(node, removable, negated); } +void PropEngine::requirePhase(TNode n, bool phase) { + Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl; + + Assert(n.getType().isBoolean()); + SatLiteral lit = d_cnfStream->getLiteral(n); + d_satSolver->requirePhase(phase ? lit : ~lit); +} + +bool PropEngine::flipDecision() { + Debug("prop") << "flipDecision()" << endl; + return d_satSolver->flipDecision(); +} + +bool PropEngine::isDecision(Node lit) const { + Assert(isTranslatedSatLiteral(lit)); + return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable()); +} + void PropEngine::printSatisfyingAssignment(){ const CnfStream::TranslationCache& transCache = d_cnfStream->getTranslationCache(); |