Remove replay and use-theory options and idl (#4186)

Towards disentangling Options / NodeManager / SmtEngine.

This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.

The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.

The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.

It also removes the solver in src/theory/idl, which cannot be enabled after this commit.

3 files changed, 1 insertions, 44 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 9db704621..323f24492 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -53,8 +53,7 @@ CommandExecutor::CommandExecutor(Options& options)
       d_smtEngine(d_solver->getSmtEngine()),
       d_options(options),
       d_stats("driver"),
-      d_result(),
-      d_replayStream(nullptr)
+      d_result()
 {
 }
 
@@ -72,12 +71,6 @@ void CommandExecutor::safeFlushStatistics(int fd) const
   d_stats.safeFlushInformation(fd);
 }
 
-void CommandExecutor::setReplayStream(ExprStream* replayStream) {
-  assert(d_replayStream == NULL);
-  d_replayStream = replayStream;
-  d_smtEngine->setReplayStream(d_replayStream);
-}
-
 bool CommandExecutor::doCommand(Command* cmd)
 {
   if( d_options.getParseOnly() ) {
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 3fc971f5b..a9b6d9077 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -44,17 +44,12 @@ class CommandExecutor
   Options& d_options;
   StatisticsRegistry d_stats;
   Result d_result;
-  ExprStream* d_replayStream;
 
  public:
   CommandExecutor(Options& options);
 
   virtual ~CommandExecutor()
   {
-    if (d_replayStream != NULL)
-    {
-      delete d_replayStream;
-    }
   }
 
   /**
@@ -92,8 +87,6 @@ class CommandExecutor
 
   void flushOutputStreams();
 
-  void setReplayStream(ExprStream* replayStream);
-
 protected:
   /** Executes treating cmd as a singleton */
   virtual bool doCommandSingleton(CVC4::Command* cmd);
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index be2d0a0f8..92368148b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -184,23 +184,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   // Create the command executor to execute the parsed commands
   pExecutor = new CommandExecutor(opts);
 
-  std::unique_ptr<Parser> replayParser;
-  if (opts.getReplayInputFilename() != "")
-  {
-    std::string replayFilename = opts.getReplayInputFilename();
-    ParserBuilder replayParserBuilder(
-        pExecutor->getSolver(), replayFilename, opts);
-
-    if( replayFilename == "-") {
-      if( inputFromStdin ) {
-        throw OptionException("Replay file and input file can't both be stdin.");
-      }
-      replayParserBuilder.withStreamInput(cin);
-    }
-    replayParser.reset(replayParserBuilder.build());
-    pExecutor->setReplayStream(new Parser::ExprStream(replayParser.get()));
-  }
-
   int returnValue = 0;
   {
     // Timer statistic
@@ -241,10 +224,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
                   << endl << endl;
         Message() << Configuration::copyright() << endl;
       }
-      if(replayParser) {
-        // have the replay parser use the declarations input interactively
-        replayParser->useDeclarationsFrom(shell.getParser());
-      }
 
       while(true) {
         try {
@@ -294,10 +273,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       vector< vector<Command*> > allCommands;
       allCommands.push_back(vector<Command*>());
       std::unique_ptr<Parser> parser(parserBuilder.build());
-      if(replayParser) {
-        // have the replay parser use the file's declarations
-        replayParser->useDeclarationsFrom(parser.get());
-      }
       int needReset = 0;
       // true if one of the commands was interrupted
       bool interrupted = false;
@@ -453,10 +428,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       }
 
       std::unique_ptr<Parser> parser(parserBuilder.build());
-      if(replayParser) {
-        // have the replay parser use the file's declarations
-        replayParser->useDeclarationsFrom(parser.get());
-      }
       bool interrupted = false;
       while (status)
       {