portfolio merge

4 files changed, 79 insertions, 5 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 09e072370..7f1456639 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -43,8 +43,9 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace prop {
 
-CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) :
+CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar, bool fullLitToNodeMap) :
   d_satSolver(satSolver),
+  d_fullLitToNodeMap(fullLitToNodeMap),
   d_registrar(registrar) {
 }
 
@@ -129,7 +130,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
                 n.toString().c_str(),
                 n.getType().toString().c_str());
 
-  bool negated = false;
+  bool negated CVC4_UNUSED = false;
   SatLiteral lit;
 
   if(n.getKind() == kind::NOT) {
@@ -178,7 +179,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   d_translationCache[node.notNode()].level = level;
 
   // If it's a theory literal, need to store it for back queries
-  if ( theoryLiteral ||
+  if ( theoryLiteral || d_fullLitToNodeMap ||
        ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ||
        Dump.isOn("clauses") ) {
     d_nodeCache[lit] = node;
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 5eaeeef94..c9fd4a08b 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -69,6 +69,13 @@ protected:
   TranslationCache d_translationCache;
   NodeCache d_nodeCache;
 
+  /**
+   * True if the lit-to-Node map should be kept for all lits, not just
+   * theory lits.  This is true if e.g. replay logging is on, which
+   * dumps the Nodes corresponding to decision literals.
+   */
+  const bool d_fullLitToNodeMap;
+
   /** The "registrar" for pre-registration of terms */
   theory::Registrar d_registrar;
 
@@ -179,8 +186,10 @@ public:
    * set of clauses and sends them to the given sat solver.
    * @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.
    */
-  CnfStream(SatInputInterface* satSolver, theory::Registrar registrar);
+  CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -283,7 +292,7 @@ public:
 private:
 
   /**
-   * Same as above, except that removable is rememebered.
+   * Same as above, except that removable is remembered.
    */
   void convertAndAssert(TNode node, bool negated);
 
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 36f411df4..7df7535dd 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -22,6 +22,7 @@
 #include "prop/sat.h"
 #include "context/context.h"
 #include "theory/theory_engine.h"
+#include "theory/rewriter.h"
 #include "expr/expr_stream.h"
 
 namespace CVC4 {
@@ -89,6 +90,55 @@ TNode SatSolver::getNode(SatLiteral lit) {
 void SatSolver::notifyRestart() {
   d_propEngine->checkTime();
   d_theoryEngine->notifyRestart();
+
+  static uint32_t lemmaCount = 0;
+
+  if(Options::current()->lemmaInputChannel != NULL) {
+    while(Options::current()->lemmaInputChannel->hasNewLemma()) {
+      Debug("shared") << "shared" << std::endl;
+      Expr lemma = Options::current()->lemmaInputChannel->getNewLemma();
+      Node asNode = lemma.getNode();
+      asNode = theory::Rewriter::rewrite(asNode);
+
+      if(d_shared.find(asNode) == d_shared.end()) {
+        d_shared.insert(asNode);
+        if(asNode.getKind() == kind::OR) {
+          ++lemmaCount;
+          if(lemmaCount % 1 == 0) {
+            Debug("shared") << "=) " << asNode << std::endl;
+          }
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true);
+        } else {
+          Debug("shared") << "=(" << asNode << std::endl;
+        }
+      } else {
+        Debug("shared") <<"drop shared " << asNode << std::endl;
+      }
+    }
+  }
+}
+
+void SatSolver::notifyNewLemma(SatClause& lemma) {
+  Assert(lemma.size() > 0);
+  if(Options::current()->lemmaOutputChannel != NULL) {
+    if(lemma.size() == 1) {
+      // cannot share units yet
+      //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
+    } else {
+      NodeBuilder<> b(kind::OR);
+      for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) {
+        b << d_cnfStream->getNode(lemma[i]);
+      }
+      Node n = b;
+
+      if(d_shared.find(n) == d_shared.end()) {
+        d_shared.insert(n);
+        Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr());
+      } else {
+        Debug("shared") <<"drop new " << n << std::endl;
+      }
+    }
+  }
 }
 
 SatLiteral SatSolver::getNextReplayDecision() {
diff --git a/src/prop/sat.h b/src/prop/sat.h
index be3ed244b..e86443827 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -137,6 +137,12 @@ class SatSolver : public SatInputInterface {
   /** Context we will be using to synchronzie the sat solver */
   context::Context* d_context;
 
+  /**
+   * Set of all lemmas that have been "shared" in the portfolio---i.e.,
+   * all imported and exported lemmas.
+   */
+  std::hash_set<Node, NodeHashFunction> d_shared;
+
   /* Pointer to the concrete SAT solver. Including this via the
      preprocessor saves us a level of indirection vs, e.g., defining a
      sub-class for each solver. */
@@ -263,6 +269,8 @@ public:
 
   void notifyRestart();
 
+  void notifyNewLemma(SatClause& lemma);
+
   SatLiteral getNextReplayDecision();
 
   void logDecision(SatLiteral lit);
@@ -294,6 +302,12 @@ inline SatSolver::SatSolver(PropEngine* propEngine,
   d_minisat->random_var_freq = Options::current()->satRandomFreq;
   d_minisat->random_seed = Options::current()->satRandomSeed;
 
+  // Give access to all possible options in the sat solver
+  d_minisat->var_decay = Options::current()->satVarDecay;
+  d_minisat->clause_decay = Options::current()->satClauseDecay;
+  d_minisat->restart_first = Options::current()->satRestartFirst;
+  d_minisat->restart_inc = Options::current()->satRestartInc;
+
   d_statistics.init(d_minisat);
 }