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

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 */