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.

4 files changed, 4 insertions, 131 deletions

diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index a73ec44f4..7615325b7 100644
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -163,31 +163,4 @@ void ManagedDiagnosticOutputChannel::addSpecialCases(OstreamOpener* opener)
   opener->addSpecialCase("stderr", &std::cerr);
 }
 
-
-ManagedReplayLogOstream::ManagedReplayLogOstream() : d_replayLog(NULL) {}
-ManagedReplayLogOstream::~ManagedReplayLogOstream(){
-  if(d_replayLog != NULL) {
-    (*d_replayLog) << std::flush;
-  }
-}
-
-std::string ManagedReplayLogOstream::defaultSource() const {
-  return options::replayLogFilename();
-}
-
-void ManagedReplayLogOstream::initialize(std::ostream* outStream) {
-  if(outStream != NULL){
-    *outStream << language::SetLanguage(options::outputLanguage())
-               << expr::ExprSetDepth(-1);
-  }
-  /* Do this regardless of managing the memory. */
-  d_replayLog = outStream;
-}
-
-/** Adds special cases to an ostreamopener. */
-void ManagedReplayLogOstream::addSpecialCases(OstreamOpener* opener) const {
-  opener->addSpecialCase("-", &std::cout);
-}
-
-
 }/* CVC4 namespace */
diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index f495f8e72..bc12bbe39 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -156,27 +156,6 @@ class ManagedDiagnosticOutputChannel : public ManagedOstream {
   void addSpecialCases(OstreamOpener* opener) const override;
 };/* class ManagedRegularOutputChannel */
 
-/** This controls the memory associated with replay-log. */
-class ManagedReplayLogOstream : public ManagedOstream {
- public:
-  ManagedReplayLogOstream();
-  ~ManagedReplayLogOstream();
-
-  std::ostream* getReplayLog() const { return d_replayLog; }
-  const char* getName() const override { return "replay-log"; }
-  std::string defaultSource() const override;
-
- protected:
-  /** Initializes an output stream. Not necessarily managed. */
-  void initialize(std::ostream* outStream) override;
-
-  /** Adds special cases to an ostreamopener. */
-  void addSpecialCases(OstreamOpener* opener) const override;
-
- private:
-  std::ostream* d_replayLog;
-};/* class ManagedRegularOutputChannel */
-
 }/* CVC4 namespace */
 
 #endif /* CVC4__MANAGED_OSTREAMS_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 30c1cd0f5..10fc76bf7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -294,40 +294,6 @@ class BeforeSearchListener : public Listener {
   SmtEngine* d_smt;
 }; /* class BeforeSearchListener */
 
-class UseTheoryListListener : public Listener {
- public:
-  UseTheoryListListener(TheoryEngine* theoryEngine)
-      : d_theoryEngine(theoryEngine)
-  {}
-
-  void notify() override
-  {
-    std::stringstream commaList(options::useTheoryList());
-    std::string token;
-
-    Debug("UseTheoryListListener") << "UseTheoryListListener::notify() "
-                                   << options::useTheoryList() << std::endl;
-
-    while(std::getline(commaList, token, ',')){
-      if(token == "help") {
-        puts(theory::useTheoryHelp);
-        exit(1);
-      }
-      if(theory::useTheoryValidate(token)) {
-        d_theoryEngine->enableTheoryAlternative(token);
-      } else {
-        throw OptionException(
-            std::string("unknown option for --use-theory : `") + token +
-            "'.  Try --use-theory=help.");
-      }
-    }
-  }
-
- private:
-  TheoryEngine* d_theoryEngine;
-}; /* class UseTheoryListListener */
-
-
 class SetDefaultExprDepthListener : public Listener {
  public:
   void notify() override
@@ -433,15 +399,11 @@ class SmtEnginePrivate : public NodeManagerListener {
   /** Manager for the memory of --dump-to. */
   ManagedDumpOStream d_managedDumpChannel;
 
-  /** Manager for --replay-log. */
-  ManagedReplayLogOstream d_managedReplayLog;
-
   /**
    * This list contains:
    *  softResourceOut
    *  hardResourceOut
    *  beforeSearchListener
-   *  UseTheoryListListener
    *
    * This needs to be deleted before both NodeManager's Options,
    * SmtEngine, d_resourceManager, and TheoryEngine.
@@ -554,7 +516,6 @@ class SmtEnginePrivate : public NodeManagerListener {
         d_managedRegularChannel(),
         d_managedDiagnosticChannel(),
         d_managedDumpChannel(),
-        d_managedReplayLog(),
         d_listenerRegistrations(new ListenerRegistrationList()),
         d_propagator(true, true),
         d_assertions(),
@@ -618,9 +579,6 @@ class SmtEnginePrivate : public NodeManagerListener {
       d_listenerRegistrations->add(
           nodeManagerOptions.registerDumpToFileNameListener(
               new SetToDefaultSourceListener(&d_managedDumpChannel), true));
-      d_listenerRegistrations->add(
-          nodeManagerOptions.registerSetReplayLogFilename(
-              new SetToDefaultSourceListener(&d_managedReplayLog), true));
     }
     catch (OptionException& e)
     {
@@ -814,17 +772,6 @@ class SmtEnginePrivate : public NodeManagerListener {
     return retval;
   }
 
-  void addUseTheoryListListener(TheoryEngine* theoryEngine){
-    Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
-    d_listenerRegistrations->add(
-        nodeManagerOptions.registerUseTheoryListListener(
-            new UseTheoryListListener(theoryEngine), true));
-  }
-
-  std::ostream* getReplayLog() const {
-    return d_managedReplayLog.getReplayLog();
-  }
-
   //------------------------------- expression names
   // implements setExpressionName, as described in smt_engine.h
   void setExpressionName(Expr e, std::string name) {
@@ -874,7 +821,6 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_status(),
       d_expectedStatus(),
       d_smtMode(SMT_MODE_START),
-      d_replayStream(nullptr),
       d_private(nullptr),
       d_statisticsRegistry(nullptr),
       d_stats(nullptr)
@@ -923,8 +869,6 @@ void SmtEngine::finishInit()
 #endif
   }
 
-  d_private->addUseTheoryListListener(getTheoryEngine());
-
   // set the random seed
   Random::getRandom().setSeed(options::seed());
 
@@ -938,11 +882,8 @@ void SmtEngine::finishInit()
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(getTheoryEngine(),
-                                    getContext(),
-                                    getUserContext(),
-                                    d_private->getReplayLog(),
-                                    d_replayStream));
+  d_propEngine.reset(
+      new PropEngine(getTheoryEngine(), getContext(), getUserContext()));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -4337,11 +4278,8 @@ void SmtEngine::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(getTheoryEngine(),
-                                    getContext(),
-                                    getUserContext(),
-                                    d_private->getReplayLog(),
-                                    d_replayStream));
+  d_propEngine.reset(
+      new PropEngine(getTheoryEngine(), getContext(), getUserContext()));
   d_theoryEngine->setPropEngine(getPropEngine());
 }
 
@@ -4534,12 +4472,6 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
   return SExpr::parseAtom(nodeManagerOptions.getOption(key));
 }
 
-void SmtEngine::setReplayStream(ExprStream* replayStream) {
-  AlwaysAssert(!d_fullyInited)
-      << "Cannot set replay stream once fully initialized";
-  d_replayStream = replayStream;
-}
-
 bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
   return d_private->getExpressionName(e, name);
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f5abda1b0..2cb227fc9 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,7 +28,6 @@
 #include "context/cdlist_forward.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "expr/expr_stream.h"
 #include "options/options.h"
 #include "proof/unsat_core.h"
 #include "smt/logic_exception.h"
@@ -800,13 +799,6 @@ class CVC4_PUBLIC SmtEngine
   void beforeSearch();
 
   /**
-   * Expermintal feature: Sets the sequence of decisions.
-   * This currently requires very fine grained knowledge about literal
-   * translation.
-   */
-  void setReplayStream(ExprStream* exprStream);
-
-  /**
    * Get expression name.
    *
    * Return true if given expressoion has a name in the current context.
@@ -1243,9 +1235,6 @@ class CVC4_PUBLIC SmtEngine
    */
   std::map<std::string, Integer> d_commandVerbosity;
 
-  /** ReplayStream for the solver. */
-  ExprStream* d_replayStream;
-
   /**
    * A private utility class to SmtEngine.
    */