diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-03-31 18:35:45 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-03-31 18:35:45 +0000 |
| commit | ceca24424da629db2e133f7864b0bac03ad44829 (patch) | |
| tree | 6b50c8337f6617ee11718cede5fbaf35a21d6a6c /src/prop/prop_engine.cpp | |
| parent | b04d7ee960729bcde8677be3682a2d64789f825b (diff) | |
Fixes to Valuation.
Diffstat (limited to 'src/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 6 |
1 files changed, 4 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) { |