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

1 files changed, 11 insertions, 0 deletions

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