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