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, 32 deletions

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