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();