merge from replay branch

5 files changed, 65 insertions, 14 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index fc7fa600a..6732b09bc 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -31,11 +31,18 @@
 using namespace std;
 using namespace CVC4::kind;
 
+#ifdef CVC4_REPLAY
+#  define CVC4_USE_REPLAY true
+#else /* CVC4_REPLAY */
+#  define CVC4_USE_REPLAY false
+#endif /* CVC4_REPLAY */
+
 namespace CVC4 {
 namespace prop {
 
 CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) :
-  d_satSolver(satSolver), d_registrar(registrar) {
+  d_satSolver(satSolver),
+  d_registrar(registrar) {
 }
 
 void CnfStream::recordTranslation(TNode node) {
@@ -46,7 +53,6 @@ void CnfStream::recordTranslation(TNode node) {
   }
 }
 
-
 TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar) :
   CnfStream(satSolver, registrar) {
 }
@@ -88,7 +94,7 @@ bool CnfStream::hasLiteral(TNode n) const {
 }
 
 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
-  Debug("cnf") << "newLiteral(" << node << ")" << endl;
+  Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
 
   // Get the literal for this node
   SatLiteral lit;
@@ -108,14 +114,16 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   d_translationCache[node].level = level;
   d_translationCache[node.notNode()].level = level;
 
-  // If it's a theory literal, store it for back queries
-  if (theoryLiteral) {
+  // If it's a theory literal, need to store it for back queries
+  if ( theoryLiteral ||
+       ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ) {
     d_nodeCache[lit] = node;
     d_nodeCache[~lit] = node.notNode();
   }
 
   // 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;
@@ -155,6 +163,7 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 
 SatLiteral CnfStream::getLiteral(TNode node) {
   TranslationCache::iterator find = d_translationCache.find(node);
+  Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
   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;
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 28b2cfb03..ef75e635b 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -180,6 +180,7 @@ public:
    * Constructs a CnfStream that sends constructs an equi-satisfiable
    * 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
    */
   CnfStream(SatInputInterface* satSolver, theory::Registrar registrar);
 
@@ -255,6 +256,7 @@ 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
    */
   TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar);
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index fd4b18222..10cd02f94 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -395,6 +395,13 @@ void Solver::popTrail() {
 
 Lit Solver::pickBranchLit()
 {
+#ifdef CVC4_REPLAY
+    Lit nextLit = proxy->getNextReplayDecision();
+    if (nextLit != lit_Undef) {
+      return nextLit;
+    }
+#endif /* CVC4_REPLAY */
+
     Var next = var_Undef;
 
     // Random decision:
@@ -1051,6 +1058,10 @@ lbool Solver::search(int nof_conflicts)
                     check_type = CHECK_WITHOUTH_PROPAGATION_FINAL;
                     continue;
                 }
+
+#ifdef CVC4_REPLAY
+                proxy->logDecision(next);
+#endif /* CVC4_REPLAY */
             }
 
             // Increase decision level and enqueue 'next'
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 1db7bf446..a6adecb1d 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -2,10 +2,10 @@
 /*! \file sat.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters, taking
- ** Minor contributors (to current version): dejan
+ ** Major contributors: dejan, mdeters, taking
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -17,11 +17,12 @@
  ** \todo document this file
  **/
 
-#include "cnf_stream.h"
-#include "prop_engine.h"
-#include "sat.h"
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/sat.h"
 #include "context/context.h"
 #include "theory/theory_engine.h"
+#include "expr/expr_stream.h"
 
 namespace CVC4 {
 namespace prop {
@@ -106,5 +107,28 @@ void SatSolver::notifyRestart() {
   d_theoryEngine->notifyRestart();
 }
 
+SatLiteral SatSolver::getNextReplayDecision() {
+#ifdef CVC4_REPLAY
+  if(Options::current()->replayStream != NULL) {
+    Expr e = Options::current()->replayStream->nextExpr();
+    if(!e.isNull()) { // we get null node when out of decisions to replay
+      // convert & return
+      return d_cnfStream->getLiteral(e);
+    }
+  }
+  return Minisat::lit_Undef;
+#endif /* CVC4_REPLAY */
+}
+
+void SatSolver::logDecision(SatLiteral lit) {
+#ifdef CVC4_REPLAY
+  if(Options::current()->replayLog != NULL) {
+    Assert(lit != Minisat::lit_Undef, "logging an `undef' decision ?!");
+    *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl;
+  }
+#endif /* CVC4_REPLAY */
+}
+
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index b80b0f705..c00115cd8 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -5,7 +5,7 @@
  ** Major contributors: taking, cconway, dejan
  ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -250,14 +250,19 @@ public:
 
   void notifyRestart();
 
+  SatLiteral getNextReplayDecision();
+
+  void logDecision(SatLiteral lit);
+
 };/* class SatSolver */
 
 /* Functions that delegate to the concrete SAT solver. */
 
 #ifdef __CVC4_USE_MINISAT
 
-inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
-                     context::Context* context) :
+inline SatSolver::SatSolver(PropEngine* propEngine,
+                            TheoryEngine* theoryEngine,
+                            context::Context* context) :
   d_propEngine(propEngine),
   d_cnfStream(NULL),
   d_theoryEngine(theoryEngine),