diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 34 |
1 files changed, 33 insertions, 1 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 3455b845e..8485a6e32 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -70,6 +70,11 @@ Lit PropEngine::requestFreshLit(){ } void PropEngine::assertFormula(const Node& node) { + + Debug("prop") << "Asserting "; + node.printAst(Debug("prop")); + Debug("prop") << endl; + d_cnfStream->convertAndAssert(node); d_assertionList.push_back(node); } @@ -87,6 +92,12 @@ void PropEngine::restart(){ } } +static void printLit(ostream & out, Lit l) { + const char * s = (sign(l))?"~":" "; + out << s << var(l); + +} + Result PropEngine::solve() { if(d_restartMayBeNeeded) restart(); @@ -98,7 +109,28 @@ Result PropEngine::solve() { d_restartMayBeNeeded = true; } - Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl; + Message() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl; + + if(result){ + for(map<Node,Lit>::iterator atomIter = d_atom2lit.begin(); + atomIter != d_atom2lit.end(); + ++atomIter){ + Node n = (*atomIter).first; + Lit l = (*atomIter).second; + + lbool lb = d_sat->modelValue(l); + + Notice() << n << "->" << lb.toInt() << endl; + } + }else{ + // unsat case + Notice() << "Conflict {"; + for(int i=0; i< d_sat->conflict.size(); i++){ + Notice() << endl << " "; + printLit(Notice(), d_sat->conflict[i]); + } + Notice() << endl << "}" << endl; + } return Result(result ? Result::SAT : Result::UNSAT); } |