merge from replay branch

5 files changed, 80 insertions, 13 deletions

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.