ensureLiteral() in CNF stream to support Andy's quantifiers work; an update to model gen on booleans; and a little cleanup

9 files changed, 181 insertions, 64 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index c211a9c71..6810d3a94 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -22,6 +22,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "theory/theory_engine.h"
+#include "theory/theory.h"
 #include "expr/node.h"
 #include "util/Assert.h"
 #include "util/output.h"
@@ -100,17 +101,59 @@ void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral
 
 bool CnfStream::isTranslated(TNode n) const {
   TranslationCache::const_iterator find = d_translationCache.find(n);
-  return find != d_translationCache.end() && find->second.level >= 0;
+  return find != d_translationCache.end() && (*find).second.level >= 0;
 }
 
-bool CnfStream::hasEverHadLiteral(TNode n) const {
+bool CnfStream::hasLiteral(TNode n) const {
   TranslationCache::const_iterator find = d_translationCache.find(n);
   return find != d_translationCache.end();
 }
 
-bool CnfStream::currentlyHasLiteral(TNode n) const {
-  TranslationCache::const_iterator find = d_translationCache.find(n);
-  return find != d_translationCache.end() && (*find).second.level != -1;
+void TseitinCnfStream::ensureLiteral(TNode n) {
+  if(hasLiteral(n)) {
+    // Already a literal!
+    SatLiteral lit = getLiteral(n);
+    NodeCache::iterator i = d_nodeCache.find(lit);
+    if(i == d_nodeCache.end()) {
+      // Store backward-mappings
+      d_nodeCache[lit] = n;
+      d_nodeCache[~lit] = n.notNode();
+    }
+    return;
+  }
+
+  CheckArgument(n.getType().isBoolean(), n,
+                "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
+                "got node: %s\n"
+                "its type: %s\n",
+                n.toString().c_str(),
+                n.getType().toString().c_str());
+
+  bool negated = false;
+  SatLiteral lit;
+
+  if(n.getKind() == kind::NOT) {
+    negated = true;
+    n = n[0];
+  }
+
+  if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL &&
+      n.getMetaKind() != kind::metakind::VARIABLE ) {
+    // If we were called with something other than a theory atom (or
+    // Boolean variable), we get a SatLiteral that is definitionally
+    // equal to it.
+    lit = toCNF(n, false);
+
+    // Store backward-mappings
+    d_nodeCache[lit] = n;
+    d_nodeCache[~lit] = n.notNode();
+  } else {
+    // We have a theory atom or variable.
+    lit = convertAtom(n);
+  }
+
+  Assert(hasLiteral(n) && getNode(lit) == n);
+  Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit << std::endl;
 }
 
 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
@@ -118,7 +161,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 
   // Get the literal for this node
   SatLiteral lit;
-  if (!hasEverHadLiteral(node)) {
+  if (!hasLiteral(node)) {
     // If no literal, well make one
     lit = variableToLiteral(d_satSolver->newVar(theoryLiteral));
     d_translationCache[node].literal = lit;
@@ -605,7 +648,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
   /*
-  if(currentlyHasLiteral(node)) {
+  if(isTranslated(node)) {
     Debug("cnf") << "==> fortunate literal detected!" << endl;
     ++d_fortunateLiterals;
     SatLiteral lit = getLiteral(node);
@@ -739,7 +782,6 @@ void CnfStream::moveToBaseLevel(TNode node) {
     moveToBaseLevel(*child);
     ++ child;
   }
-
 }
 
 }/* CVC4::prop namespace */
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 3ef636811..5eaeeef94 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -61,7 +61,7 @@ public:
   /** Cache of what literals have been registered to a node. */
   typedef __gnu_cxx::hash_map<Node, TranslationInfo, NodeHashFunction> TranslationCache;
 
-private:
+protected:
 
   /** The SAT solver we will be using */
   SatInputInterface *d_satSolver;
@@ -69,8 +69,6 @@ private:
   TranslationCache d_translationCache;
   NodeCache d_nodeCache;
 
-protected:
-
   /** The "registrar" for pre-registration of terms */
   theory::Registrar d_registrar;
 
@@ -155,13 +153,6 @@ protected:
   void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
 
   /**
-   * Returns true if the node has been cached in the translation cache.
-   * @param node the node
-   * @return true if the node has been cached
-   */
-  bool isTranslated(TNode node) const;
-
-  /**
    * Acquires a new variable from the SAT solver to represent the node
    * and inserts the necessary data it into the mapping tables.
    * @param node a formula
@@ -203,7 +194,7 @@ public:
    * Converts and asserts a formula.
    * @param node node to convert and assert
    * @param removable whether the sat solver can choose to remove the clauses
-   * @param negated wheather we are asserting the node negated
+   * @param negated whether we are asserting the node negated
    */
   virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0;
 
@@ -215,16 +206,26 @@ public:
   TNode getNode(const SatLiteral& literal);
 
   /**
-   * Returns true iff the node has an assigned literal (it might not be translated).
+   * Returns true if the node has been cached in the translation cache.
    * @param node the node
+   * @return true if the node has been cached
    */
-  bool hasEverHadLiteral(TNode node) const;
+  bool isTranslated(TNode node) const;
 
   /**
-   * Returns true iff the node has an assigned literal and it's translated.
+   * Returns true iff the node has an assigned literal (it might not be translated).
    * @param node the node
    */
-  bool currentlyHasLiteral(TNode node) const;
+  bool hasLiteral(TNode node) const;
+
+  /**
+   * Ensure that the given node will have a designated SAT literal
+   * that is definitionally equal to it.  The result of this function
+   * is that the Node can be queried via getSatValue().  Essentially,
+   * this is like a "convert-but-don't-assert" version of
+   * convertAndAssert().
+   */
+  virtual void ensureLiteral(TNode n) = 0;
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
@@ -319,6 +320,8 @@ private:
    */
   SatLiteral toCNF(TNode node, bool negated = false);
 
+  void ensureLiteral(TNode n);
+
 };/* class TseitinCnfStream */
 
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 7b4155bde..e123db0ed 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -167,7 +167,7 @@ Node PropEngine::getValue(TNode node) {
 }
 
 bool PropEngine::isSatLiteral(TNode node) {
-  return d_cnfStream->hasEverHadLiteral(node);
+  return d_cnfStream->hasLiteral(node);
 }
 
 bool PropEngine::hasValue(TNode node, bool& value) {
@@ -187,6 +187,9 @@ bool PropEngine::hasValue(TNode node, bool& value) {
   }
 }
 
+void PropEngine::ensureLiteral(TNode n) {
+  d_cnfStream->ensureLiteral(n);
+}
 
 void PropEngine::push() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index bb8ed86e1..16cb34e04 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -127,6 +127,13 @@ public:
   bool hasValue(TNode node, bool& value);
 
   /**
+   * Ensure that the given node will have a designated SAT literal
+   * that is definitionally equal to it.  The result of this function
+   * is that the Node can be queried via getSatValue().
+   */
+  void ensureLiteral(TNode n);
+
+  /**
    * Push the context level.
    */
   void push();
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 2be1dac55..229a40532 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -45,52 +45,89 @@ Node TheoryBool::getValue(TNode n) {
     // should be handled by IFF
     Unreachable();
 
-  case kind::NOT: // 1 arg
-    return nodeManager->mkConst(! d_valuation.getValue(n[0]).getConst<bool>());
+  case kind::NOT: { // 1 arg
+    Node v = d_valuation.getValue(n[0]);
+    return v.isNull() ? Node::null() : nodeManager->mkConst(! v.getConst<bool>());
+  }
 
   case kind::AND: { // 2+ args
+    bool foundNull = false;
     for(TNode::iterator i = n.begin(),
             iend = n.end();
           i != iend;
           ++i) {
-      if(! d_valuation.getValue(*i).getConst<bool>()) {
+      Node v = d_valuation.getValue(*i);
+      if(v.isNull()) {
+        foundNull = true;
+      } else if(! v.getConst<bool>()) {
         return nodeManager->mkConst(false);
       }
     }
-    return nodeManager->mkConst(true);
+    return foundNull ? Node::null() : nodeManager->mkConst(true);
   }
 
-  case kind::IFF: // 2 args
-    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ==
-                                 d_valuation.getValue(n[1]).getConst<bool>() );
+  case kind::IFF: { // 2 args
+    Node v0 = d_valuation.getValue(n[0]);
+    Node v1 = d_valuation.getValue(n[1]);
+    if(v0.isNull() || v1.isNull()) {
+      return Node::null();
+    }
+    return nodeManager->mkConst( v0.getConst<bool>() == v1.getConst<bool>() );
+  }
 
-  case kind::IMPLIES: // 2 args
-    return nodeManager->mkConst( (! d_valuation.getValue(n[0]).getConst<bool>()) ||
-                                 d_valuation.getValue(n[1]).getConst<bool>() );
+  case kind::IMPLIES: { // 2 args
+    Node v0 = d_valuation.getValue(n[0]);
+    Node v1 = d_valuation.getValue(n[1]);
+    if(v0.isNull() && v1.isNull()) {
+      return Node::null();
+    }
+    bool value = false;
+    if(! v0.isNull()) {
+      value = value || (! v0.getConst<bool>());
+    }
+    if(! v1.isNull()) {
+      value = value || v1.getConst<bool>();
+    }
+    return nodeManager->mkConst(value);
+  }
 
   case kind::OR: { // 2+ args
+    bool foundNull = false;
     for(TNode::iterator i = n.begin(),
             iend = n.end();
           i != iend;
           ++i) {
-      if(d_valuation.getValue(*i).getConst<bool>()) {
+      Node v = d_valuation.getValue(*i);
+      if(v.isNull()) {
+        foundNull = true;
+      } else if(v.getConst<bool>()) {
         return nodeManager->mkConst(true);
       }
     }
-    return nodeManager->mkConst(false);
+    return foundNull ? Node::null() : nodeManager->mkConst(false);
   }
 
-  case kind::XOR: // 2 args
-    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() !=
-                                 d_valuation.getValue(n[1]).getConst<bool>() );
+  case kind::XOR: { // 2 args
+    Node v0 = d_valuation.getValue(n[0]);
+    Node v1 = d_valuation.getValue(n[1]);
+    if(v0.isNull() || v1.isNull()) {
+      return Node::null();
+    }
+    return nodeManager->mkConst( v0.getConst<bool>() != v1.getConst<bool>() );
+  }
 
-  case kind::ITE: // 3 args
+  case kind::ITE: { // 3 args
     // all ITEs should be gone except (bool,bool,bool) ones
     Assert( n[1].getType() == nodeManager->booleanType() &&
             n[2].getType() == nodeManager->booleanType() );
-    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ?
-                                 d_valuation.getValue(n[1]).getConst<bool>() :
-                                 d_valuation.getValue(n[2]).getConst<bool>() );
+    Node v0 = d_valuation.getValue(n[0]);
+    Node v1 = d_valuation.getValue(n[1]);
+    Node v2 = d_valuation.getValue(n[2]);
+    if(v0.isNull()) {
+      return v1 == v2 ? v1 : Node::null();
+    }
+    return nodeManager->mkConst( v0.getConst<bool>() ? v1.getConst<bool>() : v2.getConst<bool>() );
+  }
 
   default:
     Unhandled(n.getKind());
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a3b91c132..2d4672776 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -298,6 +298,7 @@ Node TheoryEngine::getValue(TNode node) {
 
   // otherwise ask the theory-in-charge
   return theoryOf(node)->getValue(node);
+
 }/* TheoryEngine::getValue(TNode node) */
 
 bool TheoryEngine::presolve() {
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 9375998f9..148b95632 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -19,6 +19,7 @@
 #include "expr/node.h"
 #include "theory/valuation.h"
 #include "theory/theory_engine.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
@@ -49,5 +50,15 @@ bool Valuation::hasSatValue(TNode n, bool& value) const {
   return d_engine->getPropEngine()->hasValue(n, value);
 }
 
+Node Valuation::ensureLiteral(TNode n) {
+  Debug("ensureLiteral") << "rewriting: " << n << std::endl;
+  Node rewritten = Rewriter::rewrite(n);
+  Debug("ensureLiteral") << "      got: " << rewritten << std::endl;
+  Node preprocessed = d_engine->preprocess(rewritten);
+  Debug("ensureLiteral") << "preproced: " << preprocessed << std::endl;
+  d_engine->getPropEngine()->ensureLiteral(preprocessed);
+  return preprocessed;
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index f819eff9d..71b194905 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -69,6 +69,17 @@ public:
    */
   bool hasSatValue(TNode n, bool& value) const;
 
+  /**
+   * Ensure that the given node will have a designated SAT literal
+   * that is definitionally equal to it.  The result of this function
+   * is a Node that can be queried via getSatValue().
+   *
+   * @return the actual node that's been "literalized," which may
+   * differ from the input due to theory-rewriting and preprocessing,
+   * as well as CNF conversion
+   */
+  Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT;
+
 };/* class Valuation */
 
 }/* CVC4::theory namespace */
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 62117d4c1..26b490d2d 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -144,8 +144,7 @@ public:
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(
-                                  d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
@@ -157,22 +156,18 @@ public:
     Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(
-                                  d_nodeManager->mkNode(
-                                                        kind::IMPLIES,
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES,
                                                         d_nodeManager->mkNode(kind::AND, a, b),
-                                                        d_nodeManager->mkNode(
-                                                                              kind::IFF,
+                                                        d_nodeManager->mkNode(kind::IFF,
                                                                               d_nodeManager->mkNode(kind::OR, c, d),
-                                                                              d_nodeManager->mkNode(
-                                                                                                    kind::NOT,
+                                                                              d_nodeManager->mkNode(kind::NOT,
                                                                                                     d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
   void testFalse() {
     NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
+    d_cnfStream->convertAndAssert(  d_nodeManager->mkConst(false), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
@@ -180,8 +175,7 @@ public:
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(
-                                  d_nodeManager->mkNode(kind::IFF, a, b), false, false );
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
@@ -189,8 +183,7 @@ public:
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(
-                                  d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
@@ -214,8 +207,7 @@ public:
   void testNot() {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(
-                                  d_nodeManager->mkNode(kind::NOT, a), false, false );
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
@@ -224,14 +216,13 @@ public:
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(
-                                  d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
   void testTrue() {
     NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
+    d_cnfStream->convertAndAssert(  d_nodeManager->mkConst(true), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
@@ -250,8 +241,19 @@ public:
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(
-                                  d_nodeManager->mkNode(kind::XOR, a, b), false, false );
+    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
+
+  void testEnsureLiteral() {
+    NodeManagerScope nms(d_nodeManager);
+    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+    Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
+    d_cnfStream->ensureLiteral(a_and_b);
+    // Clauses are necessary to "literal-ize" a_and_b; this perhaps
+    // doesn't belong in a black-box test though...
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+    TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
+  }
 };