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

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;
-}