From: Tim King Date: Thu, 4 Feb 2010 00:47:45 +0000 (+0000) Subject: Fixes to the cnf converter. Also a barebones utility for printing out a satisifying... X-Git-Tag: cvc5-1.0.0~9295 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7329c1f1e3603c86c7ad88cbdefe2393d9740d98;p=cvc5.git Fixes to the cnf converter. Also a barebones utility for printing out a satisifying model. --- diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 78c4f9186..cd61b257f 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -116,7 +116,7 @@ Node Node::xorExpr(const Node& right) const { return NodeManager::currentNM()->mkNode(XOR, *this, right); } -void indent(ostream & o, int indent){ +static void indent(ostream & o, int indent){ for(int i=0; i < indent; i++) o << ' '; } @@ -130,8 +130,10 @@ void Node::printAst(ostream & o, int ind) const{ }else if(getNumChildren() >= 1){ for(Node::iterator child = begin(); child != end(); ++child){ + o << endl; (*child).printAst(o, ind+1); } + o << endl; indent(o, ind); } o << ')'; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 17ae60313..e758301d4 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -18,6 +18,7 @@ #include "prop/prop_engine.h" #include "expr/node.h" #include "util/Assert.h" +#include "util/output.h" #include @@ -27,6 +28,8 @@ using namespace std; namespace CVC4 { namespace prop { +bool atomic(const Node & n); + CnfStream::CnfStream(PropEngine *pe) : d_propEngine(pe) { } @@ -35,7 +38,25 @@ TseitinCnfStream::TseitinCnfStream(PropEngine *pe) : CnfStream(pe) { } +static void printLit(ostream & out, Lit l) { + const char * s = (sign(l))?"~":" "; + out << s << var(l); + +} + +static void printClause(ostream & out, vec & c) { + out << "clause :"; + for(int i=0;i & c) { + Debug("cnf") << "Inserting into stream "; + printClause(Debug("cnf"),c); + d_propEngine->assertClause(c); } @@ -64,15 +85,22 @@ bool CnfStream::isCached(const Node & n) const { } Lit CnfStream::lookupInCache(const Node & n) const { - Assert(isCached(n)); + Assert(isCached(n), + "Node is not in cnf translation cache"); return d_translationCache.find(n)->second; } void CnfStream::flushCache() { + Debug("cnf") << "flushing the translation cache" << endl; d_translationCache.clear(); } void CnfStream::registerMapping(const Node & node, Lit lit, bool atom) { + + Debug("cnf") << "Mapping Node "<< node << " to "; + printLit(Debug("cnf"),lit); + Debug("cnf") << endl; + //Prop engine does not need to know this mapping d_translationCache.insert(make_pair(node, lit)); if(atom) @@ -96,6 +124,10 @@ Lit CnfStream::aquireAndRegister(const Node & node, bool atom) { /***********************************************/ Lit TseitinCnfStream::handleAtom(const Node & n) { + Assert(atomic(n), "handleAtom(n) expects n to be an atom"); + + Debug("cnf") << "handling atom" << endl; + Lit l = aquireAndRegister(n, true); switch(n.getKind()) { /* TRUE and FALSE are handled specially. */ case TRUE: @@ -131,7 +163,8 @@ Lit TseitinCnfStream::handleXor(const Node & n) { */ void TseitinCnfStream::mapRecTransformOverChildren(const Node& n, vec & target) { - Assert(target.size() == n.getNumChildren()); + Assert(target.size() == n.getNumChildren(), + "Size of the children must be the same the constructed clause"); int i = 0; Node::iterator subExprIter = n.begin(); @@ -162,14 +195,15 @@ Lit TseitinCnfStream::handleOr(const Node& n) { * : (e | ~a1) & (e |~a2) & (e & ~a3) & ... */ - vec c; - c.push(~e); + vec c(1 + lits.size()); + for(int index = 0; index < lits.size(); ++index) { Lit a = lits[index]; - c.push(a); + c[index] = a; insertClauseIntoStream(e, ~a); } + c[lits.size()] = ~e; insertClauseIntoStream(c); return e; @@ -226,13 +260,14 @@ Lit TseitinCnfStream::handleAnd(const Node& n) { * : e | ~a1 | ~a2 | ~a3 | ... */ - vec c; - c.push(e); + vec c(lits.size()+1); for(int index = 0; index < lits.size(); ++index) { Lit a = lits[index]; - c.push(~a); + c[index] = (~a); insertClauseIntoStream(~e, a); } + c[lits.size()] = e; + insertClauseIntoStream(c); return e; @@ -274,9 +309,11 @@ Lit TseitinCnfStream::handleNot(const Node & n) { Node m = n[0]; Lit equivM = recTransform(m); - registerMapping(n, ~equivM, false); + Lit equivN = ~equivM; + + registerMapping(n, equivN, false); - return equivM; + return equivN; } //FIXME: This function is a major hack! Should be changed ASAP @@ -325,6 +362,7 @@ bool atomic(const Node & n) { case XOR: case ITE: case IFF: + case IMPLIES: case OR: case AND: return false; @@ -353,6 +391,8 @@ Lit TseitinCnfStream::recTransform(const Node & n) { return handleIte(n); case IFF: return handleIff(n); + case IMPLIES: + return handleImplies(n); case OR: return handleOr(n); case AND: 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::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); }