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.

12 files changed, 0 insertions, 860 deletions

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;