diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/prop/prop_engine.cpp | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
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(); |