Adding debugging code in PropEngine/CnfStream

6 files changed, 84 insertions, 7 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 233032706..eb77b0d54 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -47,12 +47,14 @@ void CnfStream::assertClause(SatLiteral a) {
   clause[0] = a;
   assertClause(clause);
 }
+
 void CnfStream::assertClause(SatLiteral a, SatLiteral b) {
   SatClause clause(2);
   clause[0] = a;
   clause[1] = b;
   assertClause(clause);
 }
+
 void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) {
   SatClause clause(3);
   clause[0] = a;
@@ -104,6 +106,14 @@ SatLiteral CnfStream::getLiteral(TNode node) {
   return literal;
 }
 
+const CnfStream::NodeCache& CnfStream::getNodeCache() const {
+  return d_nodeCache;
+}
+
+const CnfStream::TranslationCache& CnfStream::getTranslationCache() const {
+  return d_translationCache;
+}
+
 SatLiteral TseitinCnfStream::handleAtom(TNode node) {
   Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom");
   Assert(!isCached(node), "atom already mapped!");
@@ -285,6 +295,8 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   Assert(iteNode.getKind() == ITE);
   Assert(iteNode.getNumChildren() == 3);
 
+  Debug("cnf") << "handlIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
+
   SatLiteral condLit = toCNF(iteNode[0]);
   SatLiteral thenLit = toCNF(iteNode[1]);
   SatLiteral elseLit = toCNF(iteNode[2]);
@@ -293,20 +305,30 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
 
   // If ITE is true then one of the branches is true and the condition
   // implies which one
+  // lit -> (ite b t e)
+  // lit -> (t | e) & (b -> t) & (!b -> e)
+  // lit -> (t | e) & (!b | t) & (b | e)
+  // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
+  assertClause(~iteLit, thenLit, elseLit);
   assertClause(~iteLit, ~condLit, thenLit);
   assertClause(~iteLit, condLit, elseLit);
-  assertClause(~iteLit, elseLit, thenLit);
 
   // If ITE is false then one of the branches is false and the condition
   // implies which one
+  // !lit -> !(ite b t e)
+  // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
+  // !lit -> (!t | !e) & (!b | !t) & (b | !e)
+  // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
+  assertClause(iteLit, ~thenLit, ~elseLit);
   assertClause(iteLit, ~condLit, ~thenLit);
   assertClause(iteLit, condLit, ~elseLit);
-  assertClause(iteLit, ~thenLit, ~elseLit);
 
   return iteLit;
 }
 
 Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
+  Debug("cnf") << "handleNonAtomicNode(" << node << ")" << endl;
+
   /* Our main goal here is to tease out any ITE's sitting under a theory operator. */
   Node rewrite;
   NodeManager *nodeManager = NodeManager::currentNM();
@@ -347,6 +369,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
 }
 
 SatLiteral TseitinCnfStream::toCNF(TNode node) {
+  Debug("cnf") << "toCNF(" << node << ")" << endl;
 
   // If the node has already been translated, return the previous translation
   if(isCached(node)) {
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index ae4582d6f..7546a8880 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -39,18 +39,19 @@ class PropEngine;
  * @author Tim King <taking@cs.nyu.edu>
  */
 class CnfStream {
+public:
+  /** Cache of what nodes have been registered to a literal. */
+  typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
+
+  /** Cache of what literals have been registered to a node. */
+  typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache;
 
 private:
 
   /** The SAT solver we will be using */
   SatInputInterface *d_satSolver;
 
-  /** Cache of what literals have been registered to a node. */
-  typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache;
   TranslationCache d_translationCache;
-
-  /** Cache of what nodes have been registered to a literal. */
-  typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
   NodeCache d_nodeCache;
 
 protected:
@@ -153,6 +154,8 @@ public:
    */
   SatLiteral getLiteral(TNode node);
 
+  const TranslationCache& getTranslationCache() const;
+  const NodeCache& getNodeCache() const;
 }; /* class CnfStream */
 
 /**
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 6b28e6f99..ec0e2dfbc 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -25,6 +25,7 @@
 
 #include <utility>
 #include <map>
+#include <iomanip>
 
 using namespace std;
 using namespace CVC4::context;
@@ -65,6 +66,26 @@ void PropEngine::assertLemma(TNode node) {
   d_cnfStream->convertAndAssert(node);
 }
 
+
+void PropEngine::printSatisfyingAssignment(){
+  const CnfStream::TranslationCache& transCache = d_cnfStream->getTranslationCache();
+  Debug("prop-value") << "Literal | Value | Expr" << endl
+                      << "---------------------------------------------------------" << endl;
+  for(CnfStream::TranslationCache::const_iterator i = transCache.begin(),
+      end = transCache.end();
+      i != end;
+      ++i) {
+    pair<Node, SatLiteral> curr = *i;
+    SatLiteral l = curr.second;
+    if(!sign(l)) {
+      Node n = curr.first;
+      SatLiteralValue value = d_satSolver->value(l);
+      Debug("prop-value") << /*setw(4) << */ "'" << l << "' " /*<< setw(4)*/ << value << " " << n
+            << endl;
+    }
+  }
+}
+
 Result PropEngine::checkSat() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "PropEngine::checkSat()" << endl;
@@ -74,6 +95,11 @@ Result PropEngine::checkSat() {
   bool result = d_satSolver->solve();
   // Not in checkSat any more
   d_inCheckSat = false;
+
+  if( result && debugTagIsOn("prop") ) {
+    printSatisfyingAssignment();
+  }
+
   Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl;
   return Result(result ? Result::SAT : Result::UNSAT);
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 36f6cb0cb..4d25e9bc0 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -63,6 +63,8 @@ class PropEngine {
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
+  void printSatisfyingAssignment();
+
 public:
 
   /**
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index c578cf361..46d2182a9 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -28,6 +28,7 @@ void SatSolver::theoryCheck(SatClause& conflict) {
 
 void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
   Node literalNode = d_cnfStream->getNode(l);
+  Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
   // We can get null from the prop engine if the literal is useless (i.e.)
   // the expression is not in context anyomore
   if(!literalNode.isNull()) {
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 33ab674c9..42f454820 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -54,6 +54,8 @@ typedef minisat::Lit SatLiteral;
 /** Type of the SAT clauses */
 typedef minisat::vec<SatLiteral> SatClause;
 
+typedef minisat::lbool SatLiteralValue;
+
 /**
  * Returns the variable of the literal.
  * @param lit the literal
@@ -71,6 +73,15 @@ hashSatLiteral(const SatLiteral& literal) {
   return (size_t) minisat::toInt(literal);
 }
 
+inline std::string stringOfLiteralValue(SatLiteralValue val) {
+  if( val == minisat::l_False ) {
+    return "0";
+  } else if (val == minisat::l_True ) {
+    return "1";
+  } else { // unknown
+    return "_";
+  }
+}
 #endif /* __CVC4_USE_MINISAT */
 
 /** Interface encapsulating the "input" to the solver, e.g., from the 
@@ -146,6 +157,8 @@ public:
   void enqueueTheoryLiteral(const SatLiteral& l);
   
   void setCnfStream(CnfStream* cnfStream);
+
+  SatLiteralValue value(SatLiteral l);
 };
 
 /* Functions that delegate to the concrete SAT solver. */
@@ -185,6 +198,10 @@ inline SatVariable SatSolver::newVar(bool theoryAtom) {
   return d_minisat->newVar(true, true, theoryAtom);
 }
 
+inline SatLiteralValue SatSolver::value(SatLiteral l) {
+  return d_minisat->modelValue(l);
+}
+
 #endif /* __CVC4_USE_MINISAT */
 
 inline size_t
@@ -207,6 +224,11 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
   return out;
 }
 
+inline std::ostream& operator <<(std::ostream& out, const SatLiteralValue& val) {
+  out << stringOfLiteralValue(val);
+  return out;
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */