Fixes to the cnf converter. Also a barebones utility for printing out a satisifying...

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 78c4f9186fdc2c958db607f15d1e12318c646ddc..cd61b257fc751113696d17d9645c6b2718c38c30 100644 (file)
--- 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 17ae6031333bc0ab8c68ca0862d9d550ac3bc779..e758301d4f7789f11870fecb42ca12c07a6126f1 100644 (file)
--- 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 <queue>
 
@@ -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<Lit> & c) {
+  out << "clause :";  
+  for(int i=0;i<c.size();i++){
+    out << " ";
+    printLit(out, c[i]) ;
+  }
+  out << ";" << endl;
+}
+
 void CnfStream::insertClauseIntoStream(vec<Lit> & 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<Lit> & 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<Lit> c;
-  c.push(~e);
+  vec<Lit> 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<Lit> c;
-  c.push(e);
+  vec<Lit> 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 3455b845e6f50393077005e5e9e3f70fd7e83e3d..8485a6e32c603defe24e505b7db564218c6d70fe 100644 (file)
--- 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);
 }