diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 6 | ||||
-rw-r--r-- | src/prop/sat.h | 8 |
2 files changed, 12 insertions, 2 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index d64aadc96..44709630d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -104,7 +104,7 @@ void PropEngine::printSatisfyingAssignment(){ SatLiteral l = curr.second.literal; if(!sign(l)) { Node n = curr.first; - SatLiteralValue value = d_satSolver->value(l); + SatLiteralValue value = d_satSolver->modelValue(l); Debug("prop-value") << "'" << l << "' " << value << " " << n << endl; } } @@ -138,7 +138,9 @@ Result PropEngine::checkSat() { Node PropEngine::getValue(TNode node) { Assert(node.getType().isBoolean()); - SatLiteralValue v = d_satSolver->value(d_cnfStream->getLiteral(node)); + SatLiteral lit = d_cnfStream->getLiteral(node); + + SatLiteralValue v = d_satSolver->value(lit); if(v == l_True) { return NodeManager::currentNM()->mkConst(true); } else if(v == l_False) { diff --git a/src/prop/sat.h b/src/prop/sat.h index 88df366e2..f9e135c0d 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -232,8 +232,12 @@ public: void setCnfStream(CnfStream* cnfStream); + /** Call value() during the search.*/ SatLiteralValue value(SatLiteral l); + /** Call value() when the search is done.*/ + SatLiteralValue modelValue(SatLiteral l); + int getLevel() const; void push(); @@ -294,6 +298,10 @@ inline SatVariable SatSolver::newVar(bool theoryAtom) { } inline SatLiteralValue SatSolver::value(SatLiteral l) { + return d_minisat->value(l); +} + +inline SatLiteralValue SatSolver::modelValue(SatLiteral l) { return d_minisat->modelValue(l); } |