merge from replay branch

19 files changed, 398 insertions, 88 deletions

diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h
new file mode 100644
index 000000000..a6b99fb73
--- /dev/null
+++ b/src/expr/expr_stream.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file expr_stream.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A stream interface for expressions
+ **
+ ** A stream interface for expressions.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__EXPR_STREAM_H
+#define __CVC4__EXPR_STREAM_H
+
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+/**
+ * A pure-virtual stream interface for expressions.  Can be used to
+ * communicate streams of expressions between different parts of CVC4.
+ */
+class CVC4_PUBLIC ExprStream {
+public:
+  /** Virtual destructor; this implementation does nothing. */
+  virtual ~ExprStream() {}
+
+  /**
+   * Get the next expression in the stream (advancing the stream
+   * pointer as a side effect.)
+   */
+  virtual Expr nextExpr() = 0;
+};/* class ExprStream */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_STREAM_H */
+
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 2e27b4f66..ba695355e 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking, cconway
  ** 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
@@ -432,6 +432,7 @@ protected:
   friend class ExprManager;
   friend class TypeCheckingException;
   friend std::ostream& operator<<(std::ostream& out, const Expr& e);
+  template <bool ref_count> friend class NodeTemplate;
 
 };/* class Expr */
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 03840e670..d67bc2e2b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** Minor contributors (to current version): taking, cconway
  ** 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
@@ -225,6 +225,14 @@ public:
   NodeTemplate(const NodeTemplate& node);
 
   /**
+   * Allow Exprs to become Nodes.  This permits flexible translation of
+   * Exprs -> Nodes inside the CVC4 library without exposing a toNode()
+   * function in the public interface, or requiring lots of "friend"
+   * relationships.
+   */
+  NodeTemplate(const Expr& e);
+
+  /**
    * Assignment operator for nodes, copies the relevant information from node
    * to this node.
    * @param node the node to copy
@@ -915,6 +923,18 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
 }
 
 template <bool ref_count>
+NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
+  Assert(e.d_node != NULL, "Expecting a non-NULL expression value!");
+  Assert(e.d_node->d_nv != NULL, "Expecting a non-NULL expression value!");
+  d_nv = e.d_node->d_nv;
+  // shouldn't ever fail
+  Assert(d_nv->d_rc > 0, "Node constructed from Expr with rc == 0");
+  if(ref_count) {
+    d_nv->inc();
+  }
+}
+
+template <bool ref_count>
 NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   if(ref_count) {
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index f99eef4a1..dc9d0604d 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -40,7 +40,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
    ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options);
    /* Create parser with bogus input. */
    d_parser = parserBuilder.withStringInput("").build();
-}
+}/* InteractiveShell::InteractiveShell() */
 
 
 Command* InteractiveShell::readCommand() {
@@ -139,6 +139,7 @@ Command* InteractiveShell::readCommand() {
   // d_lastParser = parser;
 
   return cmd_seq;
-}
+}/* InteractiveShell::readCommand() */
+
+}/* CVC4 namespace */
 
-} // CVC4 namespace
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index faa80fb84..a08e2cbb4 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -2,10 +2,10 @@
 /*! \file interactive_shell.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: 
- ** Minor contributors (to current version): 
+ ** Major contributors: none
+ ** 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
@@ -24,13 +24,13 @@
 
 namespace CVC4 {
 
-  class Command;
-  class ExprManager;
-  class Options;
+class Command;
+class ExprManager;
+class Options;
 
-  namespace parser {
-    class Parser;
-  }
+namespace parser {
+  class Parser;
+}/* CVC4::parser namespace */
 
 class CVC4_PUBLIC InteractiveShell {
   std::istream& d_in;
@@ -41,14 +41,24 @@ class CVC4_PUBLIC InteractiveShell {
   static const std::string INPUT_FILENAME;
 
 public:
-  InteractiveShell(ExprManager& exprManager,
-                   const Options& options);
+  InteractiveShell(ExprManager& exprManager, const Options& options);
+
+  /**
+   * Read a command from the interactive shell. This will read as
+   * many lines as necessary to parse a well-formed command.
+   */
+  Command* readCommand();
+
+  /**
+   * Return the internal parser being used.
+   */
+  parser::Parser* getParser() {
+    return d_parser;
+  }
+
+};/* class InteractiveShell */
 
-  /** Read a command from the interactive shell. This will read as
-      many lines as necessary to parse a well-formed command. */
-  Command *readCommand();
-};
+}/* CVC4 namespace */
 
-} // CVC4 namespace
+#endif /* __CVC4__INTERACTIVE_SHELL_H */
 
-#endif // __CVC4__INTERACTIVE_SHELL_H
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 655562512..56c4bb422 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -2,10 +2,10 @@
 /*! \file main.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking, cconway
- ** Minor contributors (to current version): barrett, dejan
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): barrett, dejan, taking
  ** 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
@@ -228,20 +228,60 @@ int runCvc4(int argc, char* argv[]) {
     }
   }
 
-  if(!Configuration::isMuzzledBuild()) {
-    OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
-    Debug.getStream() << Expr::setlanguage(language);
-    Trace.getStream() << Expr::setlanguage(language);
-    Notice.getStream() << Expr::setlanguage(language);
-    Chat.getStream() << Expr::setlanguage(language);
-    Message.getStream() << Expr::setlanguage(language);
-    Warning.getStream() << Expr::setlanguage(language);
+  OutputLanguage outLang = language::toOutputLanguage(options.inputLanguage);
+  // Determine which messages to show based on smtcomp_mode and verbosity
+  if(Configuration::isMuzzledBuild()) {
+    Debug.setStream(CVC4::null_os);
+    Trace.setStream(CVC4::null_os);
+    Notice.setStream(CVC4::null_os);
+    Chat.setStream(CVC4::null_os);
+    Message.setStream(CVC4::null_os);
+    Warning.setStream(CVC4::null_os);
+  } else {
+    if(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+
+    Debug.getStream() << Expr::setlanguage(outLang);
+    Trace.getStream() << Expr::setlanguage(outLang);
+    Notice.getStream() << Expr::setlanguage(outLang);
+    Chat.getStream() << Expr::setlanguage(outLang);
+    Message.getStream() << Expr::setlanguage(outLang);
+    Warning.getStream() << Expr::setlanguage(outLang);
+  }
+
+  Parser* replayParser = NULL;
+  if( options.replayFilename != "" ) {
+    ParserBuilder replayParserBuilder(exprMgr, options.replayFilename, options);
+
+    if( options.replayFilename == "-") {
+      if( inputFromStdin ) {
+        throw OptionException("Replay file and input file can't both be stdin.");
+      }
+      replayParserBuilder.withStreamInput(cin);
+    }
+    replayParser = replayParserBuilder.build();
+    options.replayStream = new Parser::ExprStream(replayParser);
+  }
+  if( options.replayLog != NULL ) {
+    *options.replayLog << Expr::setlanguage(outLang) << Expr::setdepth(-1);
   }
 
   // Parse and execute commands until we are done
   Command* cmd;
   if( options.interactive ) {
-    InteractiveShell shell(exprMgr,options);
+    InteractiveShell shell(exprMgr, options);
+    if(replayParser != NULL) {
+      // have the replay parser use the declarations input interactively
+      replayParser->useDeclarationsFrom(shell.getParser());
+    }
     while((cmd = shell.readCommand())) {
       doCommand(smt,cmd);
       delete cmd;
@@ -255,6 +295,10 @@ int runCvc4(int argc, char* argv[]) {
     }
 
     Parser *parser = parserBuilder.build();
+    if(replayParser != NULL) {
+      // have the replay parser use the file's declarations
+      replayParser->useDeclarationsFrom(parser);
+    }
     while((cmd = parser->nextCommand())) {
       doCommand(smt, cmd);
       delete cmd;
@@ -263,6 +307,12 @@ int runCvc4(int argc, char* argv[]) {
     delete parser;
   }
 
+  if( options.replayStream != NULL ) {
+    // this deletes the expression parser too
+    delete options.replayStream;
+    options.replayStream = NULL;
+  }
+
   string result = smt.getInfo(":status").getValue();
   int returnValue;
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 90e13022c..0ebccf720 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -2,10 +2,10 @@
 /*! \file parser.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters, cconway
+ ** Major contributors: cconway, mdeters
  ** 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
@@ -42,6 +42,8 @@ namespace parser {
 Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode) :
   d_exprManager(exprManager),
   d_input(input),
+  d_declScopeAllocated(),
+  d_declScope(&d_declScopeAllocated),
   d_done(false),
   d_checksEnabled(true),
   d_strictMode(strictMode) {
@@ -54,7 +56,7 @@ Expr Parser::getSymbol(const std::string& name, SymbolType type) {
   switch( type ) {
 
   case SYM_VARIABLE: // Functions share var namespace
-    return d_declScope.lookup(name);
+    return d_declScope->lookup(name);
 
   default:
     Unhandled(type);
@@ -80,14 +82,14 @@ Parser::getType(const std::string& var_name,
 
 Type Parser::getSort(const std::string& name) {
   Assert( isDeclared(name, SYM_SORT) );
-  Type t = d_declScope.lookupType(name);
+  Type t = d_declScope->lookupType(name);
   return t;
 }
 
 Type Parser::getSort(const std::string& name,
                      const std::vector<Type>& params) {
   Assert( isDeclared(name, SYM_SORT) );
-  Type t = d_declScope.lookupType(name, params);
+  Type t = d_declScope->lookupType(name, params);
   return t;
 }
 
@@ -105,7 +107,7 @@ bool Parser::isFunction(const std::string& name) {
 bool Parser::isDefinedFunction(const std::string& name) {
   // more permissive in type than isFunction(), because defined
   // functions can be zero-ary and declared functions cannot.
-  return d_declScope.isBoundDefinedFunction(name);
+  return d_declScope->isBoundDefinedFunction(name);
 }
 
 /* Returns true if name is bound to a function returning boolean. */
@@ -141,19 +143,19 @@ Parser::mkVars(const std::vector<std::string> names,
 
 void
 Parser::defineVar(const std::string& name, const Expr& val) {
-  d_declScope.bind(name, val);
+  d_declScope->bind(name, val);
   Assert( isDeclared(name) );
 }
 
 void
 Parser::defineFunction(const std::string& name, const Expr& val) {
-  d_declScope.bindDefinedFunction(name, val);
+  d_declScope->bindDefinedFunction(name, val);
   Assert( isDeclared(name) );
 }
 
 void
 Parser::defineType(const std::string& name, const Type& type) {
-  d_declScope.bindType(name, type);
+  d_declScope->bindType(name, type);
   Assert( isDeclared(name, SYM_SORT) );
 }
 
@@ -161,7 +163,7 @@ void
 Parser::defineType(const std::string& name,
                    const std::vector<Type>& params,
                    const Type& type) {
-  d_declScope.bindType(name, params, type);
+  d_declScope->bindType(name, params, type);
   Assert( isDeclared(name, SYM_SORT) );
 }
 
@@ -210,9 +212,9 @@ Parser::mkSorts(const std::vector<std::string>& names) {
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
-    return d_declScope.isBound(name);
+    return d_declScope->isBound(name);
   case SYM_SORT:
-    return d_declScope.isBoundType(name);
+    return d_declScope->isBoundType(name);
   default:
     Unhandled(type);
   }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 9765f352b..15fe5126c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -2,10 +2,10 @@
 /*! \file parser.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
  ** 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
@@ -25,16 +25,17 @@
 #include <set>
 #include <list>
 
-#include "input.h"
-#include "parser_exception.h"
+#include "parser/input.h"
+#include "parser/parser_exception.h"
+#include "expr/expr.h"
 #include "expr/declaration_scope.h"
 #include "expr/kind.h"
+#include "expr/expr_stream.h"
 
 namespace CVC4 {
 
 // Forward declarations
 class BooleanType;
-class Expr;
 class ExprManager;
 class Command;
 class FunctionType;
@@ -106,8 +107,19 @@ class CVC4_PUBLIC Parser {
   /** The input that we're parsing. */
   Input *d_input;
 
-  /** The symbol table */
-  DeclarationScope d_declScope;
+  /**
+   * The declaration scope that is "owned" by this parser.  May or
+   * may not be the current declaration scope in use.
+   */
+  DeclarationScope d_declScopeAllocated;
+
+  /**
+   * This current symbol table used by this parser.  Initially points
+   * to d_declScopeAllocated, but can be changed (making this parser
+   * delegate its definitions and lookups to another parser).
+   * See useDeclarationsFrom().
+   */
+  DeclarationScope* d_declScope;
 
   /** The name of the input file. */
 //  std::string d_filename;
@@ -361,12 +373,60 @@ public:
     d_input->parseError(msg);
   }
 
-  inline void pushScope() { d_declScope.pushScope(); }
-  inline void popScope() { d_declScope.popScope(); }
-}; // class Parser
+  inline void pushScope() { d_declScope->pushScope(); }
+  inline void popScope() { d_declScope->popScope(); }
 
-} // namespace parser
+  /**
+   * Set the current symbol table used by this parser.
+   * From now on, this parser will perform its definitions and
+   * lookups in the declaration scope of the "parser" argument
+   * (but doesn't re-delegate if the other parser's declaration scope
+   * changes later).  A NULL argument restores this parser's
+   * "primordial" declaration scope assigned at its creation.  Calling
+   * p->useDeclarationsFrom(p) is a no-op.
+   *
+   * This feature is useful when e.g. reading out-of-band expression data:
+   * 1. Parsing --replay log files produced with --replay-log.
+   * 2. Perhaps a multi-query benchmark file is being single-stepped
+   *    with intervening queries on stdin that must reference
+   *
+   * However, the feature must be used carefully.  Pushes and pops
+   * should be performed with the correct current declaration scope.
+   * Care must be taken to match up declaration scopes, of course;
+   * If variables in the deferred-to parser go out of scope, the
+   * secondary parser will give errors that they are undeclared.
+   * Also, an outer-scope variable shadowed by an inner-scope one of
+   * the same name may be temporarily inaccessible.
+   *
+   * In short, caveat emptor.
+   */
+  void useDeclarationsFrom(Parser* parser) {
+    if(parser == NULL) {
+      d_declScope = &d_declScopeAllocated;
+    } else {
+      d_declScope = parser->d_declScope;
+    }
+  }
 
-} // namespace CVC4
+  /**
+   * An expression stream interface for a parser.  This stream simply
+   * pulls expressions from the given Parser object.
+   *
+   * Here, the ExprStream base class allows a Parser (from the parser
+   * library) and core components of CVC4 (in the core library) to
+   * communicate without polluting the public interface or having them
+   * reach into private (undocumented) interfaces.
+   */
+  class ExprStream : public CVC4::ExprStream {
+    Parser* d_parser;
+  public:
+    ExprStream(Parser* parser) : d_parser(parser) {}
+    ~ExprStream() { delete d_parser; }
+    Expr nextExpr() { return d_parser->nextExpression(); }
+  };/* class Parser::ExprStream */
+};/* class Parser */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__PARSER__PARSER_STATE_H */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1e36b211d..91a529bc2 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** 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
@@ -173,6 +173,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     if(toDepth != 0) {
       n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
                                types, language::output::LANG_SMTLIB_V2);
+      out << " ";
     } else {
       out << "(...)";
     }
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),
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 94ade5a52..afd30bba9 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): acsys, cconway
  ** 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
@@ -40,6 +40,10 @@ bool Configuration::isStatisticsBuild() {
   return IS_STATISTICS_BUILD;
 }
 
+bool Configuration::isReplayBuild() {
+  return IS_REPLAY_BUILD;
+}
+
 bool Configuration::isTracingBuild() {
   return IS_TRACING_BUILD;
 }
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 150354c29..3aae370d9 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): acsys
  ** 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
@@ -43,6 +43,8 @@ public:
 
   static bool isStatisticsBuild();
 
+  static bool isReplayBuild();
+
   static bool isTracingBuild();
 
   static bool isMuzzledBuild();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index c0ce86c97..4f7501a08 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -2,10 +2,10 @@
 /*! \file configuration_private.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway, acsys
- ** Minor contributors (to current version): none
+ ** Major contributors: acsys
+ ** Minor contributors (to current version): cconway
  ** 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
@@ -34,6 +34,12 @@ namespace CVC4 {
 #  define IS_STATISTICS_BUILD false
 #endif /* CVC4_STATISTICS_ON */
 
+#ifdef CVC4_REPLAY
+#  define IS_REPLAY_BUILD true
+#else /* CVC4_REPLAY */
+#  define IS_REPLAY_BUILD false
+#endif /* CVC4_REPLAY */
+
 #ifdef CVC4_TRACING
 #  define IS_TRACING_BUILD true
 #else /* CVC4_TRACING */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 88c8a2958..03dedfe00 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -2,10 +2,10 @@
 /*! \file options.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway
- ** Minor contributors (to current version): dejan, barrett
+ ** Major contributors: taking, cconway
+ ** Minor contributors (to current version): barrett, dejan
  ** 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
@@ -77,6 +77,9 @@ Options::Options() :
   typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
   earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
   incrementalSolving(false),
+  replayFilename(""),
+  replayStream(NULL),
+  replayLog(NULL),
   rewriteArithEqualities(false),
   satRandomFreq(0.0),
   satRandomSeed(91648253), //Minisat's default value
@@ -111,6 +114,8 @@ static const string optionsDescription = "\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
    --lazy-definition-expansion expand define-fun lazily\n\
+   --replay file          replay decisions from file\n\
+   --replay-log file      log decisions and propagations to file\n\
    --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
    --random-freq=P        sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
    --random-seed=S        sets the random seed for the sat solver\n\
@@ -169,6 +174,8 @@ enum OptionValue {
   LAZY_TYPE_CHECKING,
   EAGER_TYPE_CHECKING,
   INCREMENTAL,
+  REPLAY,
+  REPLAY_LOG,
   PIVOT_RULE,
   RANDOM_FREQUENCY,
   RANDOM_SEED,
@@ -219,16 +226,23 @@ static struct option cmdlineOptions[] = {
   { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
   { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
-  { "uf"         , required_argument, NULL, UF_THEORY },
+  { "uf"         , required_argument, NULL, UF_THEORY   },
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, PRODUCE_MODELS },
   { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
+  { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
+  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
+  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
+  { "incremental", no_argument      , NULL, INCREMENTAL },
+  { "replay"     , required_argument, NULL, REPLAY      },
+  { "replay-log" , required_argument, NULL, REPLAY_LOG  },
+  { "produce-models", no_argument   , NULL, PRODUCE_MODELS },
+  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
   { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING },
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
   { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
-  { "incremental", no_argument, NULL, INCREMENTAL },
   { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
   { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY  },
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
@@ -430,6 +444,35 @@ throw(OptionException) {
       incrementalSolving = true;
       break;
 
+    case REPLAY:
+#ifdef CVC4_REPLAY
+      if(optarg == NULL || *optarg == '\0') {
+        throw OptionException(string("Bad file name for --replay"));
+      } else {
+        replayFilename = optarg;
+      }
+#else /* CVC4_REPLAY */
+      throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+      break;
+
+    case REPLAY_LOG:
+#ifdef CVC4_REPLAY
+      if(optarg == NULL || *optarg == '\0') {
+        throw OptionException(string("Bad file name for --replay-log"));
+      } else if(!strcmp(optarg, "-")) {
+        replayLog = &cout;
+      } else {
+        replayLog = new ofstream(optarg, ofstream::out | ofstream::trunc);
+        if(!*replayLog) {
+          throw OptionException(string("Cannot open replay-log file: `") + optarg + "'");
+        }
+      }
+#else /* CVC4_REPLAY */
+      throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+      break;
+
     case REWRITE_ARITHMETIC_EQUALITIES:
       rewriteArithEqualities = true;
       break;
@@ -480,6 +523,7 @@ throw(OptionException) {
       printf("\n");
       printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
       printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
+      printf("replay     : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
       printf("tracing    : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
       printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
       printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
diff --git a/src/util/options.h b/src/util/options.h
index dc0d231bd..8273db458 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: cconway
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): dejan, taking
  ** 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
@@ -22,6 +22,7 @@
 #define __CVC4__OPTIONS_H
 
 #include <iostream>
+#include <fstream>
 #include <string>
 
 #include "util/exception.h"
@@ -30,6 +31,8 @@
 
 namespace CVC4 {
 
+class ExprStream;
+
 /** Class representing an option-parsing exception. */
 class OptionException : public CVC4::Exception {
 public:
@@ -128,10 +131,18 @@ struct CVC4_PUBLIC Options {
   /** Whether incemental solving (push/pop) */
   bool incrementalSolving;
 
+  /** Replay file to use (for decisions); empty if no replay file. */
+  std::string replayFilename;
+
+  /** Replay stream to use (for decisions); NULL if no replay file. */
+  ExprStream* replayStream;
+
+  /** Log to write replay instructions to; NULL if not logging. */
+  std::ostream* replayLog;
+
   /** Whether to rewrite equalities in arithmetic theory */
   bool rewriteArithEqualities;
 
-
   /**
    * Frequency for the sat solver to make random decisions.
    * Should be between 0 and 1.