merge from replay branch

24 files changed, 435 insertions, 97 deletions

diff --git a/COPYING b/COPYING
index 857ebf32f..8c0b74c43 100644
--- a/COPYING
+++ b/COPYING
@@ -1,5 +1,5 @@
-CVC4 is copyright (C) 2009, 2010 the ACSys research group at the Courant
-Institute for Mathematical Sciences, New York University.
+CVC4 is copyright (C) 2009, 2010, 2011 the ACSys research group at the
+Courant Institute for Mathematical Sciences, New York University.
 All rights reserved.
 
 CVC4 is open-source; distribution is under the terms of the modified BSD
@@ -20,7 +20,7 @@ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 04 Mar 2010 20:46:40 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  Fri, 04 Feb 2011 14:56:41 -0500
 
 CVC4 incorporates MiniSat code, excluded from the above copyright.
 See src/sat/minisat.  Its copyright:
diff --git a/Makefile b/Makefile
index 4b731cb04..d79e03f46 100644
--- a/Makefile
+++ b/Makefile
@@ -32,6 +32,6 @@ submission:
 	if [ ! -e configure ]; then ./autogen.sh; fi
 	./configure competition --disable-shared --enable-static-binary
 	$(MAKE)
-	mkdir -p cvc4-smtcomp-2010
-	cp -p $(top_builddir)/bin/cvc4 cvc4-smtcomp-2010/run
-	tar cfz cvc4-smtcomp-2010.tgz cvc4-smtcomp-2010
+	mkdir -p cvc4-smtcomp-2011
+	cp -p $(top_builddir)/bin/cvc4 cvc4-smtcomp-2011/run
+	tar cfz cvc4-smtcomp-2011.tgz cvc4-smtcomp-2011
diff --git a/config/build-type b/config/build-type
index 266ba2ca5..91a88faa6 100755
--- a/config/build-type
+++ b/config/build-type
@@ -52,7 +52,7 @@ while [ $# -gt 0 ]; do
 done
 
 build_type_suffix=
-for arg in cln staticbinary optimized debugsymbols statistics assertions tracing muzzle coverage profiling; do
+for arg in cln staticbinary optimized debugsymbols statistics replay assertions tracing muzzle coverage profiling; do
   if eval [ -n '"${'$arg'+set}"' ]; then
     if eval [ '"${'$arg'}"' -eq 0 ]; then
       build_type_suffix=$build_type_suffix-no$arg
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index 27efb8718..c58d976b5 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -23,7 +23,7 @@ do
       ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
       ac_cvc4_build_profile_set=yes
       AC_MSG_NOTICE([CVC4: building profile $ac_option_build])
-      for x in optimized statistics assertions tracing muzzle coverage profiling; do
+      for x in optimized statistics replay assertions tracing muzzle coverage profiling; do
         if expr "$ac_option" : '.*-no'$x'$' >/dev/null || expr "$ac_option" : '.*-no'$x'-' >/dev/null; then
           eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""'
         fi
diff --git a/configure.ac b/configure.ac
index 975d032b8..8ab087a22 100644
--- a/configure.ac
+++ b/configure.ac
@@ -90,7 +90,7 @@ AC_ARG_WITH([build],
 if test -z "${with_build+set}" -o "$with_build" = default; then
   with_build=default
 fi
-if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}"; then
+if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}"; then
   custom_build_profile=no
 else
   custom_build_profile=yes
@@ -159,6 +159,13 @@ if test -n "${enable_statistics+set}"; then
     btargs="$btargs nostatistics"
   fi
 fi
+if test -n "${enable_replay+set}"; then
+  if test "$enable_replay" = yes; then
+    btargs="$btargs replay"
+  else
+    btargs="$btargs noreplay"
+  fi
+fi
 AC_MSG_RESULT([$with_build])
 
 AM_INIT_AUTOMAKE([1.11 no-define parallel-tests color-tests])
@@ -333,6 +340,7 @@ case "$with_build" in
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
+    if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
@@ -346,6 +354,7 @@ case "$with_build" in
     if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
+    if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
@@ -360,6 +369,7 @@ case "$with_build" in
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
+    if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
@@ -374,6 +384,7 @@ case "$with_build" in
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
     if test -z "${enable_statistics+set}"   ; then enable_statistics=no             ; fi
+    if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
@@ -459,6 +470,22 @@ if test "$enable_statistics" = yes; then
   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
 fi
 
+AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
+
+AC_ARG_ENABLE([replay],
+  [AS_HELP_STRING([--disable-replay],
+     [turn off the replay feature in libcvc4])])
+
+if test -z "${enable_replay+set}"; then
+  enable_replay=yes
+fi
+
+AC_MSG_RESULT([$enable_replay])
+
+if test "$enable_replay" = yes; then
+  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
+fi
+
 AC_MSG_CHECKING([whether to include assertions in build])
 
 AC_ARG_ENABLE([assertions],
@@ -869,6 +896,7 @@ Build ID     : $build_type
 Optimized    : $optimized
 Debug symbols: $enable_debug_symbols
 Statistics   : $enable_statistics
+Replay       : $enable_replay
 Assertions   : $enable_assertions
 Tracing      : $enable_tracing
 Muzzle       : $enable_muzzle
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.