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

1 files changed, 18 insertions, 15 deletions

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 */