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.

1 files changed, 0 insertions, 33 deletions

diff --git a/src/options/options.h b/src/options/options.h
index ad2729205..3d1e67aba 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -67,9 +67,6 @@ class CVC4_PUBLIC Options {
   /** Listeners for options::tlimit-per. */
   ListenerCollection d_rlimitPerListeners;
 
-  /** Listeners for options::useTheoryList. */
-  ListenerCollection d_useTheoryListListeners;
-
   /** Listeners for options::defaultExprDepth. */
   ListenerCollection d_setDefaultExprDepthListeners;
 
@@ -94,10 +91,6 @@ class CVC4_PUBLIC Options {
   /** Listeners for options::diagnosticChannelName. */
   ListenerCollection d_setDiagnosticChannelListeners;
 
-  /** Listeners for options::replayFilename. */
-  ListenerCollection d_setReplayFilenameListeners;
-
-
   static ListenerCollection::Registration* registerAndNotify(
       ListenerCollection& collection, Listener* listener, bool notify);
 
@@ -231,7 +224,6 @@ public:
   std::ostream* getOut();
   std::ostream* getOutConst() const; // TODO: Remove this.
   std::string getBinaryName() const;
-  std::string getReplayInputFilename() const;
   unsigned getParseStep() const;
 
   // TODO: Document these.
@@ -382,19 +374,6 @@ public:
       Listener* listener, bool notifyIfSet);
 
   /**
-   * Registers a listener for options::useTheoryList being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerUseTheoryListListener(
-      Listener* listener, bool notifyIfSet);
-
-
-  /**
    * Registers a listener for options::defaultExprDepth being set.
    *
    * If notifyIfSet is true, this calls notify on the listener
@@ -490,18 +469,6 @@ public:
   ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener(
       Listener* listener, bool notifyIfSet);
 
-  /**
-   * Registers a listener for options::replayLogFilename being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetReplayLogFilename(
-      Listener* listener, bool notifyIfSet);
-
   /** Sends a std::flush to getErr(). */
   void flushErr();