Merging the satliteral-before-prereg branch into trunk. Theory preregistration is...

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index e278c81753bfffaaaa42ec12342068073b211c5a..65ed6caf69ddcb4807aa2c60e24cc8d75b15f88a 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -21,6 +21,7 @@
 #include "sat.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
+#include "theory/theory_engine.h"
 #include "expr/node.h"
 #include "util/Assert.h"
 #include "util/output.h"
@@ -33,8 +34,8 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace prop {
 
-CnfStream::CnfStream(SatInputInterface *satSolver) :
-  d_satSolver(satSolver) {
+CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar reg) :
+  d_satSolver(satSolver), d_registrar(reg) {
 }
 
 void CnfStream::recordTranslation(TNode node) {
@@ -45,8 +46,9 @@ void CnfStream::recordTranslation(TNode node) {
   }
 }
 
-TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) :
-  CnfStream(satSolver) {
+
+TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar reg) :
+  CnfStream(satSolver, reg) {
 }
 
 void CnfStream::assertClause(TNode node, SatClause& c) {
@@ -114,6 +116,12 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 
   // Here, you can have it
   Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl;
+  // have to keep track of this, because with the call to preRegister(),
+  // the cnf stream is re-entrant!
+  bool wasAssertingLemma = d_assertingLemma;
+  d_registrar.preRegister(node);
+  d_assertingLemma = wasAssertingLemma;
+
   return lit;
 }
 
@@ -147,7 +155,7 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 
 SatLiteral CnfStream::getLiteral(TNode node) {
   TranslationCache::iterator find = d_translationCache.find(node);
-  Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: %s", node.toString().c_str());
+  Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
   SatLiteral literal = find->second.literal;
   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
   return literal;

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 9d152a9159d13791262bed97dcdcea7f397858d8..929cae34669061628e7a97b6b8a3553a3438d900 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -29,6 +29,7 @@
 
 #include "expr/node.h"
 #include "prop/sat.h"
+#include "theory/registrar.h"
 
 #include <ext/hash_map>
 
@@ -70,6 +71,8 @@ private:
 
 protected:
 
+  theory::Registrar d_registrar;
+
   /** Top level nodes that we translated */
   std::vector<TNode> d_translationTrail;
 
@@ -177,7 +180,7 @@ public:
    * set of clauses and sends them to the given sat solver.
    * @param satSolver the sat solver to use
    */
-  CnfStream(SatInputInterface* satSolver);
+  CnfStream(SatInputInterface* satSolver, theory::Registrar r);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -252,7 +255,7 @@ public:
    * Constructs the stream to use the given sat solver.
    * @param satSolver the sat solver to use
    */
-  TseitinCnfStream(SatInputInterface* satSolver);
+  TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar reg);
 
 private:
 

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 4da3aa842c4ce1f2b9655038283294ce3f000fed..84e51d1d9898ca0ceee6b23915b6d26f6857950f 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -21,6 +21,7 @@
 #include "sat.h"
 
 #include "theory/theory_engine.h"
+#include "theory/registrar.h"
 #include "util/Assert.h"
 #include "util/options.h"
 #include "util/output.h"
@@ -62,7 +63,8 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) :
   d_context(context) {
   Debug("prop") << "Constructing the PropEngine" << endl;
   d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
-  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
+  theory::Registrar reg(d_theoryEngine);
+  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, reg);
   d_satSolver->setCnfStream(d_cnfStream);
 }
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cb6dd3460aabde800649883663539f1ca7f5a05c..6ea9de45eab5a57bd5a000b0470c65c6fe9bf749 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -463,7 +463,8 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
   throw(NoSuchFunctionException, AssertionException) {
   Debug("smt") << "push_back assertion " << n << endl;
   smt.d_haveAdditions = true;
-  smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n));
+  Node node = SmtEnginePrivate::preprocess(smt, n);
+  smt.d_propEngine->assertFormula(node);
 }
 
 void SmtEngine::ensureBoolean(const BoolExpr& e) {

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index a9ff5376d7f98209eb96029fc3cea72246c72623..b72502eca2ed1a5a3c733ecf7e872382b577289c 100644 (file)
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -19,6 +19,7 @@ libtheory_la_SOURCES = \
        shared_term_manager.cpp \
        shared_data.h \
        shared_data.cpp \
+       registrar.h \
        rewriter.h \
        rewriter_attributes.h \
        rewriter.cpp \

diff --git a/src/theory/registrar.h b/src/theory/registrar.h
new file mode 100644 (file)
index 0000000..ce3a301
--- /dev/null
+++ b/src/theory/registrar.h
@@ -0,0 +1,31 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_REGISTRAR_H
+#define __CVC4__THEORY_REGISTRAR_H
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+class Registrar {
+private:
+  TheoryEngine* d_theoryEngine;
+
+public:
+  Registrar() : d_theoryEngine(NULL){ }
+
+  Registrar(TheoryEngine* te) : d_theoryEngine(te){ }
+
+  void preRegister(Node n){
+    if(d_theoryEngine != NULL){
+      d_theoryEngine->preRegister(n);
+    }
+  }
+
+};/* class Registrar */
+
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY_REGISTRAR_H */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d1040e6fccbd89a41952a743cc652afa0d712399..aa70a9bda82f74fafda432806fa6049c869dc42e 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -162,13 +162,15 @@ struct preprocess_stack_element {
 };
 
 Node TheoryEngine::preprocess(TNode node) {
-
   // Remove ITEs and rewrite the node
   Node preprocessed = Rewriter::rewrite(removeITEs(node));
+  return preprocessed;
+}
 
+void TheoryEngine::preRegister(TNode preprocessed) {
   // If we are pre-registered already we are done
   if (preprocessed.getAttribute(PreRegistered())) {
-    return preprocessed;
+    return;
   }
 
   // Do a topological sort of the subexpressions and preregister them
@@ -223,8 +225,6 @@ Node TheoryEngine::preprocess(TNode node) {
       }
     }
   }
-
-  return preprocessed;
 }
 
 /**

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index be2e6e271b34ed3c971f74c2f739eff560c7971f..2e12d3a16d0b38a215a919defea4f0c2eb9a6148 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -247,6 +247,7 @@ public:
    * @param n the node to preprocess
    */
   Node preprocess(TNode n);
+  void preRegister(TNode preprocessed);
 
   /**
    * Assert the formula to the appropriate theory.

diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 7258e630d762ef94b2ef0b4e43cfa8f1f6cb69ec..d2f86d9692bb81515b023db3bfeee80810ceade4 100644 (file)
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -30,6 +30,7 @@
 #include "prop/prop_engine.h"
 #include "prop/sat.h"
 #include "smt/smt_engine.h"
+#include "theory/registrar.h"
 
 using namespace CVC4;
 using namespace CVC4::context;
@@ -91,7 +92,7 @@ void setUp() {
   d_context = new Context;
   d_nodeManager = new NodeManager(d_context);
   d_satSolver = new FakeSatSolver;
-  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
+  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, theory::Registrar());
 }
 
 void tearDown() {