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

1 files changed, 7 insertions, 0 deletions

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();