fix sharing issue for portfolio (full lit-to-node map wasn't being kept in my previou...

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 7f1456639db92919db21c83048a6f58ad24ffa42..681e42a99d1ce4196969210e545dc1d5f96c0edd 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -55,8 +55,8 @@ void CnfStream::recordTranslation(TNode node) {
   }
 }
 
-TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar) :
-  CnfStream(satSolver, registrar) {
+TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap) :
+  CnfStream(satSolver, registrar, fullLitToNodeMap) {
 }
 
 void CnfStream::assertClause(TNode node, SatClause& c) {

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index c9fd4a08ba0f2c1f860833b604d76f6959028d0a..4b16a02b9acb867a84093e7554bda1c0c48682aa 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -187,7 +187,7 @@ public:
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of preregistration of Nodes
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
-   * even for non-theory literals.
+   * even for non-theory literals
    */
   CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false);
 
@@ -286,8 +286,10 @@ public:
    * Constructs the stream to use the given sat solver.
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of pre-registration of Nodes
+   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
+   * even for non-theory literals
    */
-  TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar);
+  TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false);
 
 private:
 

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 9b0b93f78b0dc268e2657cfc0aadc762d65f260b..3430fd7c65c1672522eec1094fd2bf856d923d25 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -73,7 +73,7 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) :
   d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
 
   theory::Registrar registrar(d_theoryEngine);
-  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
+  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1);
 
   d_satSolver->setCnfStream(d_cnfStream);
 }