From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 31 Mar 2020 19:27:04 +0000 (-0500)
Subject: Remove replay and use-theory options and idl (#4186)
X-Git-Tag: cvc5-1.0.0~3419
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=63f887783e003546bf8de4501774a79dbcf8d4b0;p=cvc5.git

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.
---

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 945f71d36..c535890e1 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -121,7 +121,6 @@ cvc4_option(ENABLE_DEBUG_SYMBOLS  "Enable debug symbols")
 cvc4_option(ENABLE_DUMPING        "Enable dumping")
 cvc4_option(ENABLE_MUZZLE         "Suppress ALL non-result output")
 cvc4_option(ENABLE_PROOFS         "Enable proof support")
-cvc4_option(ENABLE_REPLAY         "Enable the replay feature")
 cvc4_option(ENABLE_STATISTICS     "Enable statistics")
 cvc4_option(ENABLE_TRACING        "Enable tracing")
 cvc4_option(ENABLE_UNIT_TESTING   "Enable unit testing")
@@ -429,10 +428,6 @@ if(ENABLE_PROOFS)
   add_definitions(-DCVC4_PROOF)
 endif()
 
-if(ENABLE_REPLAY)
-  add_definitions(-DCVC4_REPLAY)
-endif()
-
 if(ENABLE_TRACING)
   add_definitions(-DCVC4_TRACING)
 endif()
@@ -608,7 +603,6 @@ message("")
 print_config("Dumping                   :" ENABLE_DUMPING)
 print_config("Muzzle                    :" ENABLE_MUZZLE)
 print_config("Proofs                    :" ENABLE_PROOFS)
-print_config("Replay                    :" ENABLE_REPLAY)
 print_config("Statistics                :" ENABLE_STATISTICS)
 print_config("Tracing                   :" ENABLE_TRACING)
 message("")
diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake
index 6bd846d0c..e18d2b2f1 100644
--- a/cmake/ConfigCompetition.cmake
+++ b/cmake/ConfigCompetition.cmake
@@ -8,8 +8,6 @@ set(OPTIMIZATION_LEVEL 9)
 cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF)
 # enable_statistics=no
 cvc4_set_option(ENABLE_STATISTICS OFF)
-# enable_replay=no
-cvc4_set_option(ENABLE_REPLAY OFF)
 # enable_assertions=no
 cvc4_set_option(ENABLE_ASSERTIONS OFF)
 # enable_proof=no
diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake
index 31b142ffc..1ee78a602 100644
--- a/cmake/ConfigDebug.cmake
+++ b/cmake/ConfigDebug.cmake
@@ -7,8 +7,6 @@ add_c_cxx_flag("-Og")
 cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON)
 # enable_statistics=yes
 cvc4_set_option(ENABLE_STATISTICS ON)
-# enable_replay=yes
-cvc4_set_option(ENABLE_REPLAY ON)
 # enable_assertions=yes
 cvc4_set_option(ENABLE_ASSERTIONS ON)
 # enable_proof=yes
diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake
index 49e338abf..503f5d58f 100644
--- a/cmake/ConfigProduction.cmake
+++ b/cmake/ConfigProduction.cmake
@@ -4,8 +4,6 @@ set(OPTIMIZATION_LEVEL 3)
 cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF)
 # enable_statistics=yes
 cvc4_set_option(ENABLE_STATISTICS ON)
-# enable_replay=no
-cvc4_set_option(ENABLE_REPLAY OFF)
 # enable_assertions=no
 cvc4_set_option(ENABLE_ASSERTIONS OFF)
 # enable_proof=yes
diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake
index 40366495d..cdc9e3af8 100644
--- a/cmake/ConfigTesting.cmake
+++ b/cmake/ConfigTesting.cmake
@@ -4,8 +4,6 @@ set(OPTIMIZATION_LEVEL 2)
 cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON)
 # enable_statistics=yes
 cvc4_set_option(ENABLE_STATISTICS ON)
-# enable_replay=yes
-cvc4_set_option(ENABLE_REPLAY ON)
 # enable_assertions=yes
 cvc4_set_option(ENABLE_ASSERTIONS ON)
 # enable_proof=yes
diff --git a/configure.sh b/configure.sh
index ae9b275aa..bd95e38ed 100755
--- a/configure.sh
+++ b/configure.sh
@@ -34,7 +34,6 @@ The following flags enable optional features (disable with --no-<option name>).
   --valgrind               Valgrind instrumentation
   --debug-context-mm       use the debug context memory manager
   --statistics             include statistics
-  --replay                 turn on the replay feature
   --assertions             turn on assertions
   --tracing                include tracing code
   --dumping                include dumping code
@@ -130,7 +129,6 @@ lfsc=default
 muzzle=default
 optimized=default
 proofs=default
-replay=default
 shared=default
 static_binary=default
 statistics=default
@@ -248,9 +246,6 @@ do
     --proofs) proofs=ON;;
     --no-proofs) proofs=OFF;;
 
-    --replay) replay=ON;;
-    --no-replay) replay=OFF;;
-
     --static) shared=OFF; static_binary=ON;;
     --no-static) shared=ON;;
 
@@ -387,8 +382,6 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized"
 [ $proofs != default ] \
   && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs"
-[ $replay != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_REPLAY=$replay"
 [ $shared != default ] \
   && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
 [ $static_binary != default ] \
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 912df8b82..c1c8c15e0 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -427,14 +427,6 @@ libcvc4_add_sources(
   theory/fp/theory_fp_rewriter.h
   theory/fp/theory_fp_type_rules.h
   theory/fp/type_enumerator.h
-  theory/idl/idl_assertion.cpp
-  theory/idl/idl_assertion.h
-  theory/idl/idl_assertion_db.cpp
-  theory/idl/idl_assertion_db.h
-  theory/idl/idl_model.cpp
-  theory/idl/idl_model.h
-  theory/idl/theory_idl.cpp
-  theory/idl/theory_idl.h
   theory/interrupted.h
   theory/logic_info.cpp
   theory/logic_info.h
@@ -769,8 +761,7 @@ set(KINDS_FILES
   ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/idl/kinds)
+  ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds)
 
 #-----------------------------------------------------------------------------#
 # Add subdirectories
@@ -905,7 +896,6 @@ install(FILES
           expr/datatype.h
           expr/emptyset.h
           expr/expr_iomanip.h
-          expr/expr_stream.h
           expr/record.h
           expr/symbol_table.h
           expr/type.h
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index f907f212f..aed835f3f 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -50,10 +50,6 @@ 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/base/configuration.h b/src/base/configuration.h
index 60cdd5a9c..72ccb2301 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -47,8 +47,6 @@ public:
 
   static bool isStatisticsBuild();
 
-  static bool isReplayBuild();
-
   static bool isTracingBuild();
 
   static bool isDumpingBuild();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index f3e76d53b..77db0b51c 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -36,12 +36,6 @@ 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/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index c6034d0aa..c5abf9b27 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -65,7 +65,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/ExprHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/ExprManager.java
   ${CMAKE_CURRENT_BINARY_DIR}/ExprManagerMapCollection.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ExprStream.java
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPoint.java
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointConvertSort.java
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointSize.java
diff --git a/src/cvc4.i b/src/cvc4.i
index 42713ce40..01fd088a8 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -301,7 +301,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 // The remainder of the includes:
 %include "expr/expr.i"
 %include "expr/expr_manager.i"
-%include "expr/expr_stream.i"
 %include "expr/variable_type_map.i"
 %include "options/option_exception.i"
 %include "options/options.i"
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 00bd121cb..a308e536c 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -12,7 +12,6 @@ libcvc4_add_sources(
   expr_iomanip.cpp
   expr_iomanip.h
   expr_manager_scope.h
-  expr_stream.h
   kind_map.h
   match_trie.cpp
   match_trie.h
diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h
deleted file mode 100644
index d31e8e4fc..000000000
--- a/src/expr/expr_stream.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/*********************                                                        */
-/*! \file expr_stream.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A stream interface for expressions
- **
- ** A stream interface for expressions.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__EXPR_STREAM_H
-#define CVC4__EXPR_STREAM_H
-
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-/**
- * A pure-virtual stream interface for expressions.  Can be used to
- * communicate streams of expressions between different parts of CVC4.
- */
-class CVC4_PUBLIC ExprStream {
-public:
-  /** Virtual destructor; this implementation does nothing. */
-  virtual ~ExprStream() {}
-
-  /**
-   * Get the next expression in the stream (advancing the stream
-   * pointer as a side effect.)
-   */
-  virtual Expr nextExpr() = 0;
-};/* class ExprStream */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__EXPR_STREAM_H */
-
diff --git a/src/expr/expr_stream.i b/src/expr/expr_stream.i
deleted file mode 100644
index f1144623b..000000000
--- a/src/expr/expr_stream.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "expr/expr_stream.h"
-%}
-
-%include "expr/expr_stream.h"
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index c4d35b7dc..fb1626adb 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -203,20 +203,6 @@ Kind operatorToKind(::CVC4::expr::NodeValue* nv);
 
 #line 205 "${template}"
 
-namespace theory {
-
-static inline bool useTheoryValidate(std::string theory) {
-${use_theory_validations}
-  return false;
-}
-
-static const char *const useTheoryHelp = "\
-The following options are valid alternate implementations for use with\n\
-the --use-theory option:\n\
-\n\
-${theory_alternate_doc}";
-
-}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
 #endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index fe8a152df..e2a733ec8 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -50,9 +50,6 @@ metakind_ubchildren=
 metakind_lbchildren=
 metakind_operatorKinds=
 
-use_theory_validations=
-theory_alternate_doc=
-
 seen_theory=false
 seen_theory_builtin=false
 
@@ -108,13 +105,6 @@ function alternate {
   theory_header="$4"
   theory_includes="${theory_includes}#include \"$theory_header\"
 "
-
-  use_theory_validations="${use_theory_validations}
-  if(theory == \"$name\") {
-    return true;
-  }"
-  theory_alternate_doc="$theory_alternate_doc$name - alternate implementation for $theory_id\\n\\
-"
 }
 
 function properties {
@@ -410,10 +400,6 @@ check_builtin_theory_seen
 nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
   awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
 
-if [ -z "$theory_alternate_doc" ]; then
-  theory_alternate_doc="[none defined]"
-fi
-
 text=$(cat "$template")
 for var in \
     metakind_includes \
@@ -428,8 +414,6 @@ for var in \
     metakind_ubchildren \
     metakind_lbchildren \
     metakind_operatorKinds \
-    use_theory_validations \
-    theory_alternate_doc \
     template \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
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)
       {
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 4fb331e50..4909d7d43 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -47,7 +47,6 @@ set(options_toml_files
   decision_options.toml
   expr_options.toml
   fp_options.toml
-  idl_options.toml
   main_options.toml
   parser_options.toml
   printer_options.toml
diff --git a/src/options/idl_options.toml b/src/options/idl_options.toml
deleted file mode 100644
index d3bee7018..000000000
--- a/src/options/idl_options.toml
+++ /dev/null
@@ -1,11 +0,0 @@
-id     = "IDL"
-name   = "Idl"
-header = "options/idl_options.h"
-
-[[option]]
-  name       = "idlRewriteEq"
-  category   = "regular"
-  long       = "idl-rewrite-equalities"
-  type       = "bool"
-  default    = "false"
-  help       = "enable rewriting equalities into two inequalities in IDL solver (default is disabled)"
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.
@@ -381,19 +373,6 @@ public:
   ListenerCollection::Registration* registerRlimitPerListener(
       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.
    *
@@ -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();
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 3e6c4da3c..7fcc8f2ae 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -244,20 +244,6 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg)
   }
 }
 
-// theory/options_handlers.h
-std::string OptionsHandler::handleUseTheoryList(std::string option, std::string optarg) {
-  std::string currentList = options::useTheoryList();
-  if(currentList.empty()){
-    return optarg;
-  } else {
-    return currentList +','+ optarg;
-  }
-}
-
-void OptionsHandler::notifyUseTheoryList(std::string option) {
-  d_options->d_useTheoryListListeners.notify();
-}
-
 // printer/options_handlers.h
 const std::string OptionsHandler::s_instFormatHelp = "\
 Inst format modes currently supported by the --inst-format option:\n\
@@ -340,23 +326,6 @@ void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) {
   d_options->d_setDiagnosticChannelListeners.notify();
 }
 
-
-std::string OptionsHandler::checkReplayFilename(std::string option, std::string optarg) {
-#ifdef CVC4_REPLAY
-  if(optarg == "") {
-    throw OptionException (std::string("Bad file name for --replay"));
-  } else {
-    return optarg;
-  }
-#else /* CVC4_REPLAY */
-  throw OptionException("The replay feature was disabled in this build of CVC4.");
-#endif /* CVC4_REPLAY */
-}
-
-void OptionsHandler::notifySetReplayLogFilename(std::string option) {
-  d_options->d_setReplayFilenameListeners.notify();
-}
-
 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
 {
 #ifndef CVC4_STATISTICS_ON
@@ -453,7 +422,6 @@ void OptionsHandler::showConfiguration(std::string option) {
 
   print_config_cond("debug code", Configuration::isDebugBuild());
   print_config_cond("statistics", Configuration::isStatisticsBuild());
-  print_config_cond("replay", Configuration::isReplayBuild());
   print_config_cond("tracing", Configuration::isTracingBuild());
   print_config_cond("dumping", Configuration::isDumpingBuild());
   print_config_cond("muzzled", Configuration::isMuzzledBuild());
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index a395bb453..396b2c8ea 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -74,10 +74,6 @@ public:
 
   void setBitblastAig(std::string option, bool arg);
 
-  // theory/options_handlers.h
-  void notifyUseTheoryList(std::string option);
-  std::string handleUseTheoryList(std::string option, std::string optarg);
-
   // printer/options_handlers.h
   InstFormatMode stringToInstFormatMode(std::string option, std::string optarg);
 
@@ -96,8 +92,6 @@ public:
   void notifyDumpToFile(std::string option);
   void notifySetRegularOutputChannel(std::string option);
   void notifySetDiagnosticOutputChannel(std::string option);
-  std::string checkReplayFilename(std::string option, std::string optarg);
-  void notifySetReplayLogFilename(std::string option);
 
   void statsEnabledBuild(std::string option, bool value);
 
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index d1022c51c..bae60a374 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -187,10 +187,6 @@ std::string Options::getBinaryName() const{
   return (*this)[options::binary_name];
 }
 
-std::string Options::getReplayInputFilename() const{
-  return (*this)[options::replayInputFilename];
-}
-
 unsigned Options::getParseStep() const{
   return (*this)[options::parseStep];
 }
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index dad4f13a1..48b6a66dd 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -317,13 +317,6 @@ ListenerCollection::Registration* Options::registerRlimitPerListener(
   return registerAndNotify(d_rlimitPerListeners, listener, notify);
 }
 
-ListenerCollection::Registration* Options::registerUseTheoryListListener(
-   Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::useTheoryList);
-  return registerAndNotify(d_useTheoryListListeners, listener, notify);
-}
-
 ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
     Listener* listener, bool notifyIfSet)
 {
@@ -382,14 +375,6 @@ Options::registerSetDiagnosticOutputChannelListener(
   return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify);
 }
 
-ListenerCollection::Registration*
-Options::registerSetReplayLogFilename(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::replayLogFilename);
-  return registerAndNotify(d_setReplayFilenameListeners, listener, notify);
-}
-
 ${custom_handlers}$
 
 
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 67829ede8..c813e1900 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -626,27 +626,6 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "amount of resources spent for each sat conflict (bitvectors)"
 
-# --replay is currently broken; don't document it for 1.0
-[[option]]
-  name       = "replayInputFilename"
-  category   = "undocumented"
-  long       = "replay=FILE"
-  type       = "std::string"
-  handler    = "checkReplayFilename"
-  read_only  = true
-  help       = "replay decisions from file"
-
-# --replay is currently broken; don't document it for 1.0
-[[option]]
-  name       = "replayLogFilename"
-  category   = "undocumented"
-  long       = "replay-log=FILE"
-  type       = "std::string"
-  handler    = "checkReplayFilename"
-  notifies   = ["notifySetReplayLogFilename", "notifyBeforeSearch"]
-  read_only  = true
-  help       = "replay decisions from file"
-
 [[option]]
   name       = "forceNoLimitCpuWhileDump"
   category   = "regular"
diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml
index 13c3d5cfb..84c994c3f 100644
--- a/src/options/theory_options.toml
+++ b/src/options/theory_options.toml
@@ -18,17 +18,6 @@ header = "options/theory_options.h"
   name = "term"
   help = "Type variables as uninterpreted, type constants by theory, equalities by the parametric theory."
 
-[[option]]
-  name       = "useTheoryList"
-  smt_name   = "use-theory"
-  category   = "regular"
-  long       = "use-theory=NAME"
-  type       = "std::string"
-  handler    = "handleUseTheoryList"
-  notifies   = ["notifyUseTheoryList"]
-  read_only  = true
-  help       = "use alternate theory implementation NAME (--use-theory=help for a list). This option may be repeated or a comma separated list."
-
 [[option]]
   name       = "assignFunctionValues"
   category   = "regular"
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 7b3e1c4de..32604d03f 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1324,8 +1324,6 @@ restrictedTypePossiblyFunctionLHS[CVC4::api::Sort& t,
      * declared in the outer context.  What follows isn't quite right,
      * though, since type aliases and function definitions should be
      * retained in the set of current declarations. */
-    { /*symtab = PARSER_STATE->getSymbolTable();
-      PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ }
     formula[f] ( COMMA formula[f2] )? RPAREN
     {
       PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release");
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 72e175a58..cd4105cd0 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -26,7 +26,6 @@
 
 #include "api/cvc4cpp.h"
 #include "expr/expr.h"
-#include "expr/expr_stream.h"
 #include "expr/kind.h"
 #include "expr/symbol_table.h"
 #include "parser/input.h"
@@ -806,63 +805,9 @@ public:
     d_globalDeclarations = flag;
   }
 
-  /**
-   * Set the current symbol table used by this parser.
-   * From now on, this parser will perform its definitions and
-   * lookups in the declaration scope of the "parser" argument
-   * (but doesn't re-delegate if the other parser's declaration scope
-   * changes later).  A NULL argument restores this parser's
-   * "primordial" declaration scope assigned at its creation.  Calling
-   * p->useDeclarationsFrom(p) is a no-op.
-   *
-   * This feature is useful when e.g. reading out-of-band expression data:
-   * 1. Parsing --replay log files produced with --replay-log.
-   * 2. Perhaps a multi-query benchmark file is being single-stepped
-   *    with intervening queries on stdin that must reference the same
-   *    declaration scope(s).
-   *
-   * However, the feature must be used carefully.  Pushes and pops
-   * should be performed with the correct current declaration scope.
-   * Care must be taken to match up declaration scopes, of course;
-   * If variables in the deferred-to parser go out of scope, the
-   * secondary parser will give errors that they are undeclared.
-   * Also, an outer-scope variable shadowed by an inner-scope one of
-   * the same name may be temporarily inaccessible.
-   *
-   * In short, caveat emptor.
-   */
-  inline void useDeclarationsFrom(Parser* parser) {
-    if(parser == NULL) {
-      d_symtab = &d_symtabAllocated;
-    } else {
-      d_symtab = parser->d_symtab;
-    }
-  }
-
-  inline void useDeclarationsFrom(SymbolTable* symtab) {
-    d_symtab = symtab;
-  }
-
   inline SymbolTable* getSymbolTable() const {
     return d_symtab;
   }
-
-  /**
-   * An expression stream interface for a parser.  This stream simply
-   * pulls expressions from the given Parser object.
-   *
-   * Here, the ExprStream base class allows a Parser (from the parser
-   * library) and core components of CVC4 (in the core library) to
-   * communicate without polluting the public interface or having them
-   * reach into private (undocumented) interfaces.
-   */
-  class ExprStream : public CVC4::ExprStream {
-    Parser* d_parser;
-  public:
-    ExprStream(Parser* parser) : d_parser(parser) {}
-    ~ExprStream() { delete d_parser; }
-    Expr nextExpr() override { return d_parser->nextExpression().getExpr(); }
-  };/* class Parser::ExprStream */
   
   //------------------------ operator overloading
   /** is this function overloaded? */
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 80cce599f..f56f6a447 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -662,15 +662,6 @@ Lit Solver::pickBranchLit()
 {
     Lit nextLit;
 
-#ifdef CVC4_REPLAY
-
-    nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextReplayDecision());
-
-    if (nextLit != lit_Undef) {
-      return nextLit;
-    }
-#endif /* CVC4_REPLAY */
-
     // Theory requests
     nextLit =
         MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest());
@@ -1547,10 +1538,6 @@ lbool Solver::search(int nof_conflicts)
                     check_type = CHECK_FINAL;
                     continue;
                 }
-
-#ifdef CVC4_REPLAY
-                d_proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
-#endif /* CVC4_REPLAY */
             }
 
             // Increase decision level and enqueue 'next'
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2436aed04..89b919109 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -44,13 +44,6 @@
 using namespace std;
 using namespace CVC4::context;
 
-
-#ifdef CVC4_REPLAY
-#  define CVC4_USE_REPLAY true
-#else /* CVC4_REPLAY */
-#  define CVC4_USE_REPLAY false
-#endif /* CVC4_REPLAY */
-
 namespace CVC4 {
 namespace prop {
 
@@ -76,9 +69,7 @@ public:
 
 PropEngine::PropEngine(TheoryEngine* te,
                        Context* satContext,
-                       UserContext* userContext,
-                       std::ostream* replayLog,
-                       ExprStream* replayStream)
+                       UserContext* userContext)
     : d_inCheckSat(false),
       d_theoryEngine(te),
       d_context(satContext),
@@ -101,13 +92,8 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_cnfStream = new CVC4::prop::TseitinCnfStream(
       d_satSolver, d_registrar, userContext, true);
 
-  d_theoryProxy = new TheoryProxy(this,
-                                  d_theoryEngine,
-                                  d_decisionEngine.get(),
-                                  d_context,
-                                  d_cnfStream,
-                                  replayLog,
-                                  replayStream);
+  d_theoryProxy = new TheoryProxy(
+      this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
   d_satSolver->initialize(d_context, d_theoryProxy);
 
   d_decisionEngine->setSatSolver(d_satSolver);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 707244ff5..f1d73fc92 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -24,7 +24,6 @@
 #include <sys/time.h>
 
 #include "base/modal_exception.h"
-#include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "options/options.h"
 #include "preprocessing/assertion_pipeline.h"
@@ -62,9 +61,7 @@ class PropEngine
    */
   PropEngine(TheoryEngine*,
              context::Context* satContext,
-             context::UserContext* userContext,
-             std::ostream* replayLog,
-             ExprStream* replayStream);
+             context::UserContext* userContext);
 
   /**
    * Destructor.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 557dcc413..38c99f551 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -18,7 +18,6 @@
 
 #include "context/context.h"
 #include "decision/decision_engine.h"
-#include "expr/expr_stream.h"
 #include "options/decision_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
@@ -37,24 +36,17 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          TheoryEngine* theoryEngine,
                          DecisionEngine* decisionEngine,
                          context::Context* context,
-                         CnfStream* cnfStream,
-                         std::ostream* replayLog,
-                         ExprStream* replayStream)
+                         CnfStream* cnfStream)
     : d_propEngine(propEngine),
       d_cnfStream(cnfStream),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
-      d_replayLog(replayLog),
-      d_replayStream(replayStream),
-      d_queue(context),
-      d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0)
+      d_queue(context)
 {
-  smtStatisticsRegistry()->registerStat(&d_replayedDecisions);
 }
 
 TheoryProxy::~TheoryProxy() {
   /* nothing to do for now */
-  smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions);
 }
 
 void TheoryProxy::variableNotify(SatVariable var) {
@@ -150,29 +142,6 @@ void TheoryProxy::notifyRestart() {
   d_theoryEngine->notifyRestart();
 }
 
-SatLiteral TheoryProxy::getNextReplayDecision() {
-#ifdef CVC4_REPLAY
-  if(d_replayStream != NULL) {
-    Expr e = d_replayStream->nextExpr();
-    if(!e.isNull()) { // we get null node when out of decisions to replay
-      // convert & return
-      ++d_replayedDecisions;
-      return d_cnfStream->getLiteral(e);
-    }
-  }
-#endif /* CVC4_REPLAY */
-  return undefSatLiteral;
-}
-
-void TheoryProxy::logDecision(SatLiteral lit) {
-#ifdef CVC4_REPLAY
-  if(d_replayLog != NULL) {
-    Assert(lit != undefSatLiteral) << "logging an `undef' decision ?!";
-    (*d_replayLog) << d_cnfStream->getNode(lit) << std::endl;
-  }
-#endif /* CVC4_REPLAY */
-}
-
 void TheoryProxy::spendResource(ResourceManager::Resource r)
 {
   d_theoryEngine->spendResource(r);
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 0d76b473f..089d2082d 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -27,7 +27,6 @@
 #include <unordered_set>
 
 #include "context/cdqueue.h"
-#include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "prop/sat_solver.h"
 #include "theory/theory.h"
@@ -54,9 +53,7 @@ class TheoryProxy
               TheoryEngine* theoryEngine,
               DecisionEngine* decisionEngine,
               context::Context* context,
-              CnfStream* cnfStream,
-              std::ostream* replayLog,
-              ExprStream* replayStream);
+              CnfStream* cnfStream);
 
   ~TheoryProxy();
 
@@ -83,10 +80,6 @@ class TheoryProxy
 
   void notifyRestart();
 
-  SatLiteral getNextReplayDecision();
-
-  void logDecision(SatLiteral lit);
-
   void spendResource(ResourceManager::Resource r);
 
   bool isDecisionEngineDone();
@@ -111,12 +104,6 @@ class TheoryProxy
   /** The theory engine we are using. */
   TheoryEngine* d_theoryEngine;
 
-  /** Stream on which to log replay events. */
-  std::ostream* d_replayLog;
-
-  /** Stream for replaying decisions. */
-  ExprStream* d_replayStream;
-
   /** Queue of asserted facts */
   context::CDQueue<TNode> d_queue;
 
@@ -126,11 +113,6 @@ class TheoryProxy
    */
   std::unordered_set<Node, NodeHashFunction> d_shared;
 
-  /**
-   * Statistic: the number of replayed decisions (via --replay).
-   */
-  IntStat d_replayedDecisions;
-
 }; /* class SatSolver */
 
 }/* CVC4::prop namespace */
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"
@@ -799,13 +798,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.
    *
@@ -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.
    */
diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp
deleted file mode 100644
index 1e3905537..000000000
--- a/src/theory/idl/idl_assertion.cpp
+++ /dev/null
@@ -1,213 +0,0 @@
-/*********************                                                        */
-/*! \file idl_assertion.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/idl/idl_assertion.h"
-
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-IDLAssertion::IDLAssertion()
-: d_op(kind::LAST_KIND)
-{}
-
-IDLAssertion::IDLAssertion(TNode node) {
-  bool ok = parse(node, 1, false);
-  if (!ok) {
-    d_x = d_y = TNode::null();
-  } else {
-    if (d_op == kind::GT) {
-      // Turn GT into LT x - y > c is the same as y - x < -c
-      std::swap(d_x, d_y);
-      d_c = -d_c;
-      d_op = kind::LT;
-    }
-    if (d_op == kind::GEQ) {
-      // Turn GT into LT x - y >= c is the same as y - x <= -c
-      std::swap(d_x, d_y);
-      d_c = -d_c;
-      d_op = kind::LEQ;
-    }
-    if (d_op == kind::LT) {
-      // Turn strict into non-strict x - y < c is the same as x - y <= c-1
-      d_c = d_c - 1;
-      d_op = kind::LEQ;
-    }
-  }
-  d_original = node;
-}
-
-IDLAssertion::IDLAssertion(const IDLAssertion& other)
-: d_x(other.d_x)
-, d_y(other.d_y)
-, d_op(other.d_op)
-, d_c(other.d_c)
-, d_original(other.d_original)
-{}
-
-bool IDLAssertion::propagate(IDLModel& model) const {
-  Debug("theory::idl::model") << model << std::endl;
-  Assert(ok());
-  // Should be d_x - d_y <= d_c, or d_x - d_c <= d_y
-  Integer x_value = model.getValue(d_x);
-  Integer y_value = model.getValue(d_y);
-  if (x_value - y_value > d_c) {
-    model.setValue(d_y, x_value - d_c, IDLReason(d_x, d_original));
-    Debug("theory::idl::model") << model << std::endl;
-    return true;
-  } else {
-    return false;
-  }
-}
-
-void IDLAssertion::toStream(std::ostream& out) const {
-  out << "IDL[" << d_x << " - " << d_y << " " << d_op << " " << d_c << "]";
-}
-
-/** Negates the given arithmetic kind */
-static Kind negateOp(Kind op) {
-  switch (op) {
-  case kind::LT:
-    // not (a < b) = (a >= b)
-    return kind::GEQ;
-  case kind::LEQ:
-    // not (a <= b) = (a > b)
-    return kind::GT;
-  case kind::GT:
-    // not (a > b) = (a <= b)
-    return kind::LEQ;
-  case kind::GEQ:
-    // not (a >= b) = (a < b)
-    return kind::LT;
-  case kind::EQUAL:
-    // not (a = b) = (a != b)
-    return kind::DISTINCT;
-  case kind::DISTINCT:
-    // not (a != b) = (a = b)
-    return kind::EQUAL;
-  default:
-    Unreachable();
-    break;
-  }
-  return kind::LAST_KIND;
-}
-
-bool IDLAssertion::parse(TNode node, int c, bool negated) {
-
-  // Only unit coefficients allowed
-  if (c != 1 && c != -1) {
-    return false;
-  }
-
-  // Assume we're ok
-  bool ok = true;
-
-  // The kind of the node
-  switch(node.getKind()) {
-
-  case kind::NOT:
-    // We parse the negation
-    ok = parse(node[0], c, true);
-    // Setup the kind
-    if (ok) {
-      d_op = negateOp(d_op);
-    }
-    break;
-
-  case kind::EQUAL:
-  case kind::LT:
-  case kind::LEQ:
-  case kind::GT:
-  case kind::GEQ: {
-    // All relation operators are parsed on both sides
-    d_op = node.getKind();
-    ok = parse(node[0], c, negated);
-    if (ok) {
-      ok = parse(node[1],-c, negated);
-    }
-    break;
-  }
-
-  case kind::CONST_RATIONAL: {
-    // Constants
-    Rational m = node.getConst<Rational>();
-    if (m.isIntegral()) {
-      d_c +=  m.getNumerator() * (-c);
-    } else {
-      ok = false;
-    }
-    break;
-  }
-  case kind::MULT: {
-    // Only unit multiplication of variables
-    if (node.getNumChildren() == 2 && node[0].isConst()) {
-      Rational a = node[0].getConst<Rational>();
-      if (a == 1 || a == -1) {
-        ok = parse(node[1], c * a.sgn(), negated);
-      } else {
-        ok = false;
-      }
-    } else {
-      ok = false;
-    }
-    break;
-  }
-
-  case kind::PLUS: {
-    for(unsigned i = 0; i < node.getNumChildren(); ++i) {
-      ok = parse(node[i], c, negated);
-      if(!ok) {
-        break;
-      }
-    }
-    break;
-  }
-
-  case kind::MINUS: {
-    ok = parse(node[0], c, negated);
-    if (ok) {
-      ok = parse(node[1], -c, negated);
-    }
-    break;
-  }
-
-  case kind::UMINUS: {
-    ok = parse(node[0], -c, negated);
-    break;
-  }
-
-  default: {
-    if (c > 0) {
-      if (d_x.isNull()) {
-        d_x = node;
-      } else {
-        ok = false;
-      }
-    } else {
-      if (d_y.isNull()) {
-        d_y = node;
-      } else {
-        ok = false;
-      }
-    }
-    break;
-  }
-  } // End case
-
-  // Difference logic OK
-  return ok;
-}
diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h
deleted file mode 100644
index e24fbfc67..000000000
--- a/src/theory/idl/idl_assertion.h
+++ /dev/null
@@ -1,91 +0,0 @@
-/*********************                                                        */
-/*! \file idl_assertion.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#pragma once
-
-#include "theory/idl/idl_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-/**
- * An internal representation of the IDL assertions. Each IDL assertions is
- * of the form (x - y op c) where op is one of (<=, =, !=). IDL assertion
- * can be constructed from an expression.
- */
-class IDLAssertion {
-
-  /** The positive variable */
-  TNode d_x;
-  /** The negative variable */
-  TNode d_y;
-  /** The relation */
-  Kind d_op;
-  /** The RHS constant */
-  Integer d_c;
-
-  /** Original assertion we got this one from */
-  TNode d_original;
-
-  /** Parses the given node into an assertion, and return true if OK. */
-  bool parse(TNode node, int c = 1, bool negated = false);
-
-public:
-
-  /** Null assertion */
-  IDLAssertion();
-  /** Create the assertion from given node */
-  IDLAssertion(TNode node);
-  /** Copy constructor */
-  IDLAssertion(const IDLAssertion& other);
-
-  TNode getX() const { return d_x; }
-  TNode getY() const { return d_y; }
-  Kind getOp() const { return d_op;}
-  Integer getC() const { return d_c; }
-
-  /**
-   * Propagate the constraint using the model. For example, if the constraint
-   * is of the form x - y <= -1, and the value of x in the model is 0, then
-   *
-   *   (x - y <= -1) and (x = 0) implies y >= x + 1 = 1
-   *
-   * If the value of y is less then 1, is is set to 1 and true is returned. If
-   * the value of y is 1 or more, than false is return.
-   *
-   * @return true if value of y was updated
-   */
-  bool propagate(IDLModel& model) const;
-
-  /** Is this constraint proper */
-  bool ok() const {
-    return !d_x.isNull() || !d_y.isNull();
-  }
-
-  /** Output to the stream */
-  void toStream(std::ostream& out) const;
-};
-
-inline std::ostream& operator << (std::ostream& out, const IDLAssertion& assertion) {
-  assertion.toStream(out);
-  return out;
-}
-
-}
-}
-}
diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp
deleted file mode 100644
index 865d8b4f5..000000000
--- a/src/theory/idl/idl_assertion_db.cpp
+++ /dev/null
@@ -1,59 +0,0 @@
-/*********************                                                        */
-/*! \file idl_assertion_db.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/idl/idl_assertion_db.h"
-
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-IDLAssertionDB::IDLAssertionDB(context::Context* c)
-: d_assertions(c)
-, d_variableLists(c)
-{}
-
-void IDLAssertionDB::add(const IDLAssertion& assertion, TNode var) {
-  // Is there a list for the variable already?
-  unsigned previous = -1;
-  var_to_unsigned_map::iterator find = d_variableLists.find(var);
-  if (find != d_variableLists.end()) {
-    previous = (*find).second;
-  }
-  // Add to the DB
-  d_variableLists[var] = d_assertions.size();
-  d_assertions.push_back(IDLAssertionListElement(assertion, previous));
-}
-
-IDLAssertionDB::iterator::iterator(IDLAssertionDB& db, TNode var)
-: d_db(db)
-, d_current(-1)
-{
-  var_to_unsigned_map::const_iterator find = d_db.d_variableLists.find(var);
-  if (find != d_db.d_variableLists.end()) {
-    d_current = (*find).second;
-  }
-}
-
-void IDLAssertionDB::iterator::next() {
-  if (d_current != (unsigned)(-1)) {
-    d_current = d_db.d_assertions[d_current].d_previous;
-  }
-}
-
-IDLAssertion IDLAssertionDB::iterator::get() const {
-  return d_db.d_assertions[d_current].d_assertion;
-}
diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h
deleted file mode 100644
index ac87282d9..000000000
--- a/src/theory/idl/idl_assertion_db.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/*********************                                                        */
-/*! \file idl_assertion_db.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#pragma once
-
-#include "theory/idl/idl_assertion.h"
-#include "context/cdlist.h"
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-/**
- * Context-dependent database assertions, organized by variable. Each variable
- * can be associated a list of IDL assertions. The list of assertions can
- * be iterated over using the provided iterator class.
- */
-class IDLAssertionDB {
-
-  /** Elements of the assertion lists */
-  struct IDLAssertionListElement {
-    /** The assertion itself */
-    IDLAssertion d_assertion;
-    /** The index of the previous element (-1 for null) */
-    unsigned d_previous;
-
-    IDLAssertionListElement(const IDLAssertion& assertion, unsigned previous)
-    : d_assertion(assertion), d_previous(previous)
-    {}
-  };
-
-  /** All assertions in a context dependent stack */
-  context::CDList<IDLAssertionListElement> d_assertions;
-
-  typedef context::CDHashMap<TNode, unsigned, TNodeHashFunction> var_to_unsigned_map;
-
-  /** Map from variables to the first element of their list */
-  var_to_unsigned_map d_variableLists;
-
-public:
-
-  /** Create a new assertion database */
-  IDLAssertionDB(context::Context* c);
-
-  /** Add a new assertion, attach to the list of the given variable */
-  void add(const IDLAssertion& assertion, TNode var);
-
-  /** Iteration over the constraints of a variable */
-  class iterator {
-    /** The database */
-    const IDLAssertionDB& d_db;
-    /** Index of the current constraint */
-    unsigned d_current;
-  public:
-    /** Construct the iterator for the variable */
-    iterator(IDLAssertionDB& db, TNode var);
-    /** Is this iterator done */
-    bool done() const { return d_current == (unsigned)(-1); }
-    /** Next element */
-    void next();
-    /** Get the assertion */
-    IDLAssertion get() const;
-  };
-};
-
-}
-}
-}
-
-
-
-
diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp
deleted file mode 100644
index 4a3426222..000000000
--- a/src/theory/idl/idl_model.cpp
+++ /dev/null
@@ -1,74 +0,0 @@
-/*********************                                                        */
-/*! \file idl_model.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/idl/idl_model.h"
-
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-IDLModel::IDLModel(context::Context* context)
-    : d_model(context), d_reason(context)
-{
-}
-
-Integer IDLModel::getValue(TNode var) const
-{
-  model_value_map::const_iterator find = d_model.find(var);
-  if (find != d_model.end())
-  {
-    return (*find).second;
-  }
-  else
-  {
-    return 0;
-  }
-}
-
-void IDLModel::setValue(TNode var, Integer value, IDLReason reason)
-{
-  Assert(!reason.d_constraint.isNull());
-  d_model[var] = value;
-  d_reason[var] = reason;
-}
-
-void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons)
-{
-  TNode current = var;
-  do
-  {
-    Debug("theory::idl::model") << "processing: " << var << std::endl;
-    Assert(d_reason.find(current) != d_reason.end());
-    IDLReason reason = d_reason[current];
-    Debug("theory::idl::model")
-        << "adding reason: " << reason.d_constraint << std::endl;
-    reasons.push_back(reason.d_constraint);
-    current = reason.d_x;
-  } while (current != var);
-}
-
-void IDLModel::toStream(std::ostream& out) const
-{
-  model_value_map::const_iterator it = d_model.begin();
-  model_value_map::const_iterator it_end = d_model.end();
-  out << "Model[" << std::endl;
-  for (; it != it_end; ++it)
-  {
-    out << (*it).first << " -> " << (*it).second << std::endl;
-  }
-  out << "]";
-}
diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h
deleted file mode 100644
index 610b90695..000000000
--- a/src/theory/idl/idl_model.h
+++ /dev/null
@@ -1,84 +0,0 @@
-/*********************                                                        */
-/*! \file idl_model.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#pragma once
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-/**
- * A reason for a value of a variable in the model is a constraint that implies
- * this value by means of the value of another variable. For example, if the
- * value of x is 0, then the variable x and the constraint (y > 0) are a reason
- * for the y taking the value 1.
- */
-struct IDLReason
-{
-  /** The variable of the reason */
-  TNode d_x;
-  /** The constraint of the reason */
-  TNode d_constraint;
-
-  IDLReason(TNode x, TNode constraint) : d_x(x), d_constraint(constraint) {}
-  IDLReason() {}
-};
-
-/**
- * A model maps variables to integer values and backs them up with reasons.
- * Default values (if not set with setValue) for all variables are 0.
- */
-class IDLModel
-{
-  typedef context::CDHashMap<TNode, Integer, TNodeHashFunction> model_value_map;
-  typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction>
-      model_reason_map;
-
-  /** Values assigned to individual variables */
-  model_value_map d_model;
-
-  /** Reasons constraining the individual variables */
-  model_reason_map d_reason;
-
- public:
-  IDLModel(context::Context* context);
-
-  /** Get the model value of the variable */
-  Integer getValue(TNode var) const;
-
-  /** Set the value of the variable */
-  void setValue(TNode var, Integer value, IDLReason reason);
-
-  /** Get the cycle of reasons behind the variable var */
-  void getReasonCycle(TNode var, std::vector<TNode>& reasons);
-
-  /** Output to the given stream */
-  void toStream(std::ostream& out) const;
-};
-
-inline std::ostream& operator<<(std::ostream& out, const IDLModel& model)
-{
-  model.toStream(out);
-  return out;
-}
-
-}  // namespace idl
-}  // namespace theory
-}  // namespace CVC4
diff --git a/src/theory/idl/kinds b/src/theory/idl/kinds
deleted file mode 100644
index 6bf0218b0..000000000
--- a/src/theory/idl/kinds
+++ /dev/null
@@ -1,8 +0,0 @@
-# kinds                                                               -*- sh -*-
-#
-# For documentation on this file format, please refer to
-# src/theory/builtin/kinds.
-#
-
-alternate THEORY_ARITH "idl" ::CVC4::theory::idl::TheoryIdl "theory/idl/theory_idl.h"
-
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
deleted file mode 100644
index f92738bcb..000000000
--- a/src/theory/idl/theory_idl.cpp
+++ /dev/null
@@ -1,156 +0,0 @@
-/*********************                                                        */
-/*! \file theory_idl.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/idl/theory_idl.h"
-
-#include <set>
-#include <queue>
-
-#include "options/idl_options.h"
-#include "theory/rewriter.h"
-
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u,
-                     OutputChannel& out, Valuation valuation,
-                     const LogicInfo& logicInfo)
-    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
-    , d_model(c)
-    , d_assertionsDB(c)
-{}
-
-Node TheoryIdl::ppRewrite(TNode atom) {
-  if (atom.getKind() == kind::EQUAL  && options::idlRewriteEq()) {
-    // If the option is turned on, each equality into two inequalities. This in
-    // effect removes equalities, and theorefore dis-equalities too.
-    Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
-    Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
-    Node rewritten = Rewriter::rewrite(leq.andNode(geq));
-    return rewritten;
-  } else {
-    return atom;
-  }
-}
-
-void TheoryIdl::check(Effort level) {
-  if (done() && !fullEffort(level)) {
-    return;
-  }
-
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-
-  while(!done()) {
-
-    // Get the next assertion
-    Assertion assertion = get();
-    Debug("theory::idl") << "TheoryIdl::check(): processing "
-                         << assertion.d_assertion << std::endl;
-
-    // Convert the assertion into the internal representation
-    IDLAssertion idlAssertion(assertion.d_assertion);
-    Debug("theory::idl") << "TheoryIdl::check(): got " << idlAssertion << std::endl;
-
-    if (idlAssertion.ok()) {
-      if (idlAssertion.getOp() == kind::DISTINCT) {
-        // We don't handle dis-equalities
-        d_out->setIncomplete();
-      } else {
-        // Process the convex assertions immediately
-        bool ok = processAssertion(idlAssertion);
-        if (!ok) {
-          // In conflict, we're done
-          return;
-        }
-      }
-    } else {
-      // Not an IDL assertion, set incomplete
-      d_out->setIncomplete();
-    }
-  }
-
-}
-
-bool TheoryIdl::processAssertion(const IDLAssertion& assertion) {
-
-  Debug("theory::idl") << "TheoryIdl::processAssertion(" << assertion << ")" << std::endl;
-
-  // Add the constraint (x - y op c) to the list assertions of x
-  d_assertionsDB.add(assertion, assertion.getX());
-
-  // Update the model, if forced by the assertion
-  bool y_updated = assertion.propagate(d_model);
-
-  // If the value of y was updated, we might need to update further
-  if (y_updated) {
-
-    std::queue<TNode> queue; // Queue of variables to consider
-    std::set<TNode> inQueue; // Current elements of the queue
-
-    // Add the first updated variable to the queue
-    queue.push(assertion.getY());
-    inQueue.insert(assertion.getY());
-
-    while (!queue.empty()) {
-      // Pop a new variable x off the queue
-      TNode x = queue.front();
-      queue.pop();
-      inQueue.erase(x);
-
-      // Go through the constraint (x - y op c), and update values of y
-      IDLAssertionDB::iterator it(d_assertionsDB, x);
-      while (!it.done()) {
-        // Get the assertion and update y
-        IDLAssertion x_y_assertion = it.get();
-        y_updated = x_y_assertion.propagate(d_model);
-        // If updated add to the queue
-        if (y_updated) {
-          // If the variable that we updated is the same as the first
-          // variable that we updated, it's a cycle of updates => conflict
-          if (x_y_assertion.getY() == assertion.getX()) {
-            std::vector<TNode> reasons;
-            d_model.getReasonCycle(x_y_assertion.getY(), reasons);
-            // Construct the reason of the conflict
-            Node conflict = NodeManager::currentNM()->mkNode(kind::AND, reasons);
-            d_out->conflict(conflict);
-            return false;
-          } else {
-            // No cycle, just a model update, so we add to the queue
-            TNode y = x_y_assertion.getY();
-            if (inQueue.count(y) == 0) {
-              queue.push(y);
-              inQueue.insert(x_y_assertion.getY());
-            }
-          }
-        }
-        // Go to the next constraint
-        it.next();
-      }
-    }
-  }
-
-  // Everything fine, no conflict
-  return true;
-}
-
-} /* namepsace CVC4::theory::idl */
-} /* namepsace CVC4::theory */
-} /* namepsace CVC4 */
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
deleted file mode 100644
index 1d48d0785..000000000
--- a/src/theory/idl/theory_idl.h
+++ /dev/null
@@ -1,63 +0,0 @@
-/*********************                                                        */
-/*! \file theory_idl.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic, Mathias Preiner, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#pragma once
-
-#include "cvc4_private.h"
-
-#include "theory/theory.h"
-#include "theory/idl/idl_model.h"
-#include "theory/idl/idl_assertion_db.h"
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-/**
- * Handles integer difference logic (IDL) constraints.
- */
-class TheoryIdl : public Theory {
-
-  /** The current model */
-  IDLModel d_model;
-
-  /** The asserted constraints, organized by variable */
-  IDLAssertionDB d_assertionsDB;
-
-  /** Process a new assertion, returns false if in conflict */
-  bool processAssertion(const IDLAssertion& assertion);
-
-public:
-
-  /** Theory constructor. */
-  TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-            Valuation valuation, const LogicInfo& logicInfo);
-
-  /** Pre-processing of input atoms */
-  Node ppRewrite(TNode atom) override;
-
-  /** Check the assertions for satisfiability */
-  void check(Effort effort) override;
-
-  /** Identity string */
-  std::string identify() const override { return "THEORY_IDL"; }
-
-};/* class TheoryIdl */
-
-}/* CVC4::theory::idl namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 8a900e1e7..a87203015 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -121,12 +121,6 @@ function alternate {
   theory_header="$4"
   theory_includes="${theory_includes}#include \"$theory_header\"
 "
-
-  eval "alternate_for_$1=\"\${alternate_for_$1}
-      if(engine->useTheoryAlternative(\\\"$2\\\")) {
-        engine->addTheory< $3 >($1);
-        return;
-      }\""
 }
 
 function rewriter {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 32a80a418..e665f6115 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -350,7 +350,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_factsAsserted(context, false),
       d_preRegistrationVisitor(this, context),
       d_sharedTermsVisitor(d_sharedTerms),
-      d_theoryAlternatives(),
       d_attr_handle(),
       d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
 {
@@ -2374,18 +2373,6 @@ void TheoryEngine::spendResource(ResourceManager::Resource r)
   d_resourceManager->spendResource(r);
 }
 
-void TheoryEngine::enableTheoryAlternative(const std::string& name){
-  Debug("TheoryEngine::enableTheoryAlternative")
-      << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl;
-
-  d_theoryAlternatives.insert(name);
-}
-
-bool TheoryEngine::useTheoryAlternative(const std::string& name) {
-  return d_theoryAlternatives.find(name) != d_theoryAlternatives.end();
-}
-
-
 TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
     conflicts(getStatsPrefix(theory) + "::conflicts", 0),
     propagations(getStatsPrefix(theory) + "::propagations", 0),
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c1e1e4cac..840d42417 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -895,14 +895,7 @@ public:
   /** Prints the assertions to the debug stream */
   void printAssertions(const char* tag);
 
-  /** Theory alternative is in use. */
-  bool useTheoryAlternative(const std::string& name);
-
-  /** Enables using a theory alternative by name. */
-  void enableTheoryAlternative(const std::string& name);
-
 private:
-  std::set< std::string > d_theoryAlternatives;
 
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;