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

4 files changed, 79 insertions, 24 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();