Remove BV equality slicer (#4928)

This class is not used based on our coverage tests (although it appears to be possibly enabled based on non-standard runtime checking of assertions), and uses the equality engine in a highly nonstandard way that will be a burden to the new standardization of equality engine in theory solvers.

FYI @aniemetz @mpreiner

13 files changed, 7 insertions, 986 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index b5449470f..5cb2ab610 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -51,7 +51,7 @@ QF_UFBV)
   finishwith
   ;;
 QF_BV)
-  finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction
+  finishwith --bv-div-zero-const --no-bv-abstraction
   ;;
 QF_AUFLIA)
   finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index f7ec33f75..7c0aca100 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -109,24 +109,6 @@ header = "options/bv_options.h"
   help       = "use the equality engine for the bit-vector theory (only if --bitblast=lazy)"
 
 [[option]]
-  name       = "bitvectorEqualitySlicer"
-  category   = "regular"
-  long       = "bv-eq-slicer=MODE"
-  type       = "BvSlicerMode"
-  default    = "OFF"
-  help       = "turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)"
-  help_mode  = "Bit-vector equality slicer modes."
-[[option.mode.ON]]
-  name = "on"
-  help = "Turn slicer on."
-[[option.mode.OFF]]
-  name = "off"
-  help = "Turn slicer off."
-[[option.mode.AUTO]]
-  name = "auto"
-  help = "Turn slicer on if input has only equalities over core symbols."
-
-[[option]]
   name       = "bitvectorInequalitySolver"
   category   = "regular"
   long       = "bv-inequality-solver"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 1b18dd7f4..303937f77 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -172,17 +172,6 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
     {
       options::bitvectorEqualitySolver.set(true);
     }
-    if (!options::bitvectorEqualitySlicer.wasSetByUser())
-    {
-      if (options::incrementalSolving() || options::produceModels())
-      {
-        options::bitvectorEqualitySlicer.set(options::BvSlicerMode::OFF);
-      }
-      else
-      {
-        options::bitvectorEqualitySlicer.set(options::BvSlicerMode::AUTO);
-      }
-    }
 
     if (!options::bitvectorInequalitySolver.wasSetByUser())
     {
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 4da13f108..a69207512 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -503,11 +503,6 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
 
     Debug("smt") << " assertions     : " << assertions.size() << endl;
 
-    // before ppRewrite check if only core theory for BV theory
-    TheoryEngine* te = d_smt.getTheoryEngine();
-    Assert(te != nullptr);
-    te->staticInitializeBVOptions(assertions.ref());
-
     // Theory preprocessing
     bool doEarlyTheoryPp = !options::arithRewriteEq();
     if (doEarlyTheoryPp)
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index fa96d522c..5376d7418 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -82,11 +82,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Notice() << "SmtEngine: setting bitvectorAig" << std::endl;
     options::bitvectorAig.set(true);
   }
-  if (options::bitvectorEqualitySlicer.wasSetByUser())
-  {
-    Notice() << "SmtEngine: setting bitvectorEqualitySolver" << std::endl;
-    options::bitvectorEqualitySolver.set(true);
-  }
   if (options::bitvectorAlgebraicBudget.wasSetByUser())
   {
     Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 7e2b8a8b0..d8f376a74 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -19,7 +19,6 @@
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/bv/slicer.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ext_theory.h"
@@ -35,10 +34,8 @@ using namespace CVC4::theory::bv::utils;
 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt)
     : SubtheorySolver(c, bv),
       d_notify(*this),
-      d_slicer(new Slicer()),
       d_isComplete(c, true),
       d_lemmaThreshold(16),
-      d_useSlicer(false),
       d_preregisterCalled(false),
       d_checkCalled(false),
       d_bv(bv),
@@ -96,21 +93,10 @@ void CoreSolver::finishInit()
   d_equalityEngine->addFunctionKind(kind::INT_TO_BITVECTOR);
 }
 
-void CoreSolver::enableSlicer() {
-  AlwaysAssert(!d_preregisterCalled);
-  d_useSlicer = true;
-  d_statistics.d_slicerEnabled.setData(true);
-}
-
 void CoreSolver::preRegister(TNode node) {
   d_preregisterCalled = true;
   if (node.getKind() == kind::EQUAL) {
     d_equalityEngine->addTriggerPredicate(node);
-    if (d_useSlicer)
-    {
-      d_slicer->processEquality(node);
-      AlwaysAssert(!d_checkCalled);
-      }
   } else {
     d_equalityEngine->addTerm(node);
     // Register with the extended theory, for context-dependent simplification.
@@ -132,59 +118,6 @@ void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   }
 }
 
-Node CoreSolver::getBaseDecomposition(TNode a) {
-  std::vector<Node> a_decomp;
-  d_slicer->getBaseDecomposition(a, a_decomp);
-  Node new_a = utils::mkConcat(a_decomp);
-  Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n";
-  return new_a;
-}
-
-bool CoreSolver::decomposeFact(TNode fact) {
-  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
-  // FIXME: are this the right things to assert?
-  // assert decompositions since the equality engine does not know the semantics of
-  // concat:
-  //   a == a_1 concat ... concat a_k
-  //   b == b_1 concat ... concat b_k
-  TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;
-
-  TNode a = eq[0];
-  TNode b = eq[1];
-  Node new_a = getBaseDecomposition(a);
-  Node new_b = getBaseDecomposition(b);
-
-  Assert(utils::getSize(new_a) == utils::getSize(new_b)
-         && utils::getSize(new_a) == utils::getSize(a));
-
-  NodeManager* nm = NodeManager::currentNM();
-  Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
-  Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
-
-  bool ok = true;
-  ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
-  if (!ok) return false;
-  ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
-  if (!ok) return false;
-  ok = assertFactToEqualityEngine(fact, fact);
-  if (!ok) return false;
-
-  if (fact.getKind() == kind::EQUAL) {
-    // assert the individual equalities as well
-    //    a_i == b_i
-    if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
-        new_b.getKind() == kind::BITVECTOR_CONCAT) {
-      Assert(new_a.getNumChildren() == new_b.getNumChildren());
-      for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
-        Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
-        ok = assertFactToEqualityEngine(eq_i, fact);
-        if (!ok) return false;
-      }
-    }
-  }
-  return true;
-}
-
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
 
@@ -196,10 +129,6 @@ bool CoreSolver::check(Theory::Effort e) {
   bool ok = true;
   std::vector<Node> core_eqs;
   TNodeBoolMap seen;
-  // slicer does not deal with cardinality constraints yet
-  if (d_useSlicer) {
-    d_isComplete = false; 
-  }
   while (! done()) {
     TNode fact = get();
     if (d_isComplete && !isCompleteForTerm(fact, seen)) {
@@ -208,11 +137,7 @@ bool CoreSolver::check(Theory::Effort e) {
     
     // only reason about equalities
     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
-      if (d_useSlicer) {
-        ok = decomposeFact(fact);
-      } else {
-        ok = assertFactToEqualityEngine(fact, fact);
-      }
+      ok = assertFactToEqualityEngine(fact, fact);
     } else {
       ok = assertFactToEqualityEngine(fact, fact);
     }
@@ -416,17 +341,11 @@ void CoreSolver::conflict(TNode a, TNode b) {
 }
 
 bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
-  if (d_useSlicer)
-    return utils::isCoreTerm(term, seen);
-  
   return utils::isEqualityTerm(term, seen); 
 }
 
 bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
 {
-  if (d_useSlicer) {
-    Unreachable(); 
-  }
   if (Debug.isOn("bitvector-model")) {
     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
     for (; it!= d_assertionQueue.end(); ++it) {
@@ -505,12 +424,9 @@ void CoreSolver::addTermToEqualityEngine(TNode node)
 
 CoreSolver::Statistics::Statistics()
   : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
-  , d_slicerEnabled("theory::bv::CoreSolver::SlicerEnabled", false)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
-  smtStatisticsRegistry()->registerStat(&d_slicerEnabled);
 }
 CoreSolver::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
-  smtStatisticsRegistry()->unregisterStat(&d_slicerEnabled);
 }
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 19183c129..381804681 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -30,7 +30,6 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class Slicer;
 class Base;
 /**
  * Bitvector equality solver
@@ -43,7 +42,6 @@ class CoreSolver : public SubtheorySolver {
 
   struct Statistics {
     IntStat d_numCallstoCheck;
-    BackedStat<bool> d_slicerEnabled;
     Statistics();
     ~Statistics();
   };
@@ -75,12 +73,9 @@ class CoreSolver : public SubtheorySolver {
   /** Store a conflict from merging two constants */
   void conflict(TNode a, TNode b);
 
-  std::unique_ptr<Slicer> d_slicer;
   context::CDO<bool> d_isComplete;
   unsigned d_lemmaThreshold;
-  
-  /** Used to ensure that the core slicer is used properly*/
-  bool d_useSlicer;
+
   bool d_preregisterCalled;
   bool d_checkCalled;
 
@@ -116,7 +111,6 @@ class CoreSolver : public SubtheorySolver {
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   bool hasTerm(TNode node) const;
   void addTermToEqualityEngine(TNode node);
-  void enableSlicer();
 };
 
 
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 4524ddb8c..33472ec19 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -15,41 +15,15 @@
  **/
 #include "theory/bv/slicer.h"
 
-#include "options/bv_options.h"
-#include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
 using namespace std; 
 
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-const TermId UndefinedId = -1;
-
-namespace {
-
-void intersect(const std::vector<TermId>& v1,
-               const std::vector<TermId>& v2,
-               std::vector<TermId>& intersection)
-{
-  for (const TermId id1 : v1)
-  {
-    for (const TermId id2 : v2)
-    {
-      if (id2 == id1)
-      {
-        intersection.push_back(id1);
-        break;
-      }
-    }
-  }
-}
-
-}  // namespace
-
 /**
  * Base
  * 
@@ -72,13 +46,6 @@ void Base::sliceAt(Index index)
   d_repr[vector_index] = d_repr[vector_index] | bit_mask;
 }
 
-void Base::sliceWith(const Base& other) {
-  Assert(d_size == other.d_size);
-  for (unsigned i = 0; i < d_repr.size(); ++i) {
-    d_repr[i] = d_repr[i] | other.d_repr[i]; 
-  }
-}
-
 bool Base::isCutPoint (Index index) const
 {
   // there is an implicit cut point at the end and begining of the bv
@@ -93,22 +60,6 @@ bool Base::isCutPoint (Index index) const
   return (bit_mask & d_repr[vector_index]) != 0;
 }
 
-void Base::diffCutPoints(const Base& other, Base& res) const {
-  Assert(d_size == other.d_size && res.d_size == d_size);
-  for (unsigned i = 0; i < d_repr.size(); ++i) {
-    Assert(res.d_repr[i] == 0);
-    res.d_repr[i] = d_repr[i] ^ other.d_repr[i]; 
-  }
-}
-
-bool Base::isEmpty() const {
-  for (unsigned i = 0; i< d_repr.size(); ++i) {
-    if (d_repr[i] != 0)
-      return false;
-  }
-  return true;
-}
-
 std::string Base::debugPrint() const {
   std::ostringstream os;
   os << "[";
@@ -127,543 +78,6 @@ std::string Base::debugPrint() const {
   return os.str(); 
 }
 
-/**
- * ExtractTerm
- *
- */
-
-std::string ExtractTerm::debugPrint() const {
-  ostringstream os;
-  os << "id" << id << "[" << high << ":" << low <<"] ";  
-  return os.str(); 
-}
-
-/**
- * NormalForm
- *
- */
-
-std::pair<TermId, Index> NormalForm::getTerm(Index index, const UnionFind& uf) const {
-  Assert(index < base.getBitwidth());
-  Index count = 0;
-  for (unsigned i = 0; i < decomp.size(); ++i) {
-    Index size = uf.getBitwidth(decomp[i]); 
-    if ( count + size > index && index >= count) {
-      return pair<TermId, Index>(decomp[i], count); 
-    }
-    count += size; 
-  }
-  Unreachable(); 
-}
-
-
-
-std::string NormalForm::debugPrint(const UnionFind& uf) const {
-  ostringstream os;
-  os << "NF " << base.debugPrint() << endl;
-  os << "("; 
-  for (int i = decomp.size() - 1; i>= 0; --i) {
-    os << decomp[i] << "[" << uf.getBitwidth(decomp[i]) <<"]";
-    os << (i != 0? ", " : "");  
-  }
-  os << ") \n"; 
-  return os.str(); 
-}
-/**
- * UnionFind::Node
- * 
- */
-
-std::string UnionFind::Node::debugPrint() const {
-  ostringstream os;
-  os << "Repr " << d_repr << " ["<< d_bitwidth << "] ";
-  os << "( " << d_ch1 <<", " << d_ch0 << ")" << endl; 
-  return os.str(); 
-}
-
-
-/**
- * UnionFind
- * 
- */
-TermId UnionFind::addTerm(Index bitwidth) {
-  Node node(bitwidth);
-  d_nodes.push_back(node);
-  ++(d_statistics.d_numNodes);
-  
-  TermId id = d_nodes.size() - 1; 
-  d_representatives.insert(id);
-  ++(d_statistics.d_numRepresentatives); 
-
-  Debug("bv-slicer-uf") << "UnionFind::addTerm " << id << " size " << bitwidth << endl;
-  return id; 
-}
-/** 
- * At this point we assume the slicings of the two terms are properly aligned. 
- * 
- * @param t1 
- * @param t2 
- */
-void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) {
-  Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n"
-                     << "                      " << t2.debugPrint() << endl;
-  Assert(t1.getBitwidth() == t2.getBitwidth());
-
-  NormalForm nf1(t1.getBitwidth());
-  NormalForm nf2(t2.getBitwidth());
-  
-  getNormalForm(t1, nf1);
-  getNormalForm(t2, nf2);
-
-  Assert(nf1.decomp.size() == nf2.decomp.size());
-  Assert(nf1.base == nf2.base);
-
-  for (unsigned i = 0; i < nf1.decomp.size(); ++i) {
-    merge (nf1.decomp[i], nf2.decomp[i]); 
-  } 
-}
-
-/** 
- * Merge the two terms in the union find. Both t1 and t2
- * should be root terms. 
- * 
- * @param t1 
- * @param t2 
- */
-void UnionFind::merge(TermId t1, TermId t2) {
-  Debug("bv-slicer-uf") << "UnionFind::merge (" << t1 <<", " << t2 << ")" << endl;
-  ++(d_statistics.d_numMerges);
-  t1 = find(t1);
-  t2 = find(t2); 
-
-  if (t1 == t2)
-    return;
-
-  Assert(!hasChildren(t1) && !hasChildren(t2));
-  setRepr(t1, t2); 
-  d_representatives.erase(t1);
-  d_statistics.d_numRepresentatives += -1; 
-}
-
-TermId UnionFind::find(TermId id) {
-  TermId repr = getRepr(id); 
-  if (repr != UndefinedId) {
-    TermId find_id =  find(repr);
-    setRepr(id, find_id);
-    return find_id; 
-  }
-  return id; 
-}
-/** 
- * Splits the representative of the term between i-1 and i
- * 
- * @param id the id of the term
- * @param i the index we are splitting at
- * 
- * @return 
- */
-void UnionFind::split(TermId id, Index i) {
-  Debug("bv-slicer-uf") << "UnionFind::split " << id << " at " << i << endl;
-  id = find(id); 
-  Debug("bv-slicer-uf") << "   node: " << d_nodes[id].debugPrint() << endl;
-
-  if (i == 0 || i == getBitwidth(id)) {
-    // nothing to do 
-    return;
-  }
-  Assert(i < getBitwidth(id));
-  if (!hasChildren(id)) {
-    // first time we split this term 
-    TermId bottom_id = addTerm(i);
-    TermId top_id = addTerm(getBitwidth(id) - i);
-    setChildren(id, top_id, bottom_id);
-
-  } else {
-    Index cut = getCutPoint(id); 
-    if (i < cut )
-      split(getChild(id, 0), i);
-    else
-      split(getChild(id, 1), i - cut); 
-  }
-  ++(d_statistics.d_numSplits);
-}
-
-void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) {
-  nf.clear(); 
-  getDecomposition(term, nf.decomp);
-  // update nf base
-  Index count = 0; 
-  for (unsigned i = 0; i < nf.decomp.size(); ++i) {
-    count += getBitwidth(nf.decomp[i]);
-    nf.base.sliceAt(count); 
-  }
-  Debug("bv-slicer-uf") << "UnionFind::getNormalFrom term: " << term.debugPrint() << endl;
-  Debug("bv-slicer-uf") << "           nf: " << nf.debugPrint(*this) << endl; 
-}
-
-void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) {
-  // making sure the term is aligned
-  TermId id = find(term.id);
-
-  Assert(term.high < getBitwidth(id));
-  // because we split the node, this must be the whole extract
-  if (!hasChildren(id)) {
-    Assert(term.high == getBitwidth(id) - 1 && term.low == 0);
-    decomp.push_back(id);
-    return; 
-  }
-    
-  Index cut = getCutPoint(id);
-  
-  if (term.low < cut && term.high < cut) {
-    // the extract falls entirely on the low child
-    ExtractTerm child_ex(getChild(id, 0), term.high, term.low); 
-    getDecomposition(child_ex, decomp); 
-  }
-  else if (term.low >= cut && term.high >= cut){
-    // the extract falls entirely on the high child
-    ExtractTerm child_ex(getChild(id, 1), term.high - cut, term.low - cut);
-    getDecomposition(child_ex, decomp); 
-  }
-  else {
-    // the extract is split over the two children
-    ExtractTerm low_child(getChild(id, 0), cut - 1, term.low);
-    getDecomposition(low_child, decomp);
-    ExtractTerm high_child(getChild(id, 1), term.high - cut, 0);
-    getDecomposition(high_child, decomp); 
-  }
-}
-
-/* Compute the greatest common divisor of two indices.  */
-static Index gcd(Index a, Index b)
-{
-  while (b != 0)
-  {
-    Index t = b;
-    b = a % t;
-    a = t;
-  }
-  return a;
-}
-
-/** 
- * May cause reslicings of the decompositions. Must not assume the decompositons
- * are the current normal form. 
- * 
- * @param d1 
- * @param d2 
- * @param common 
- */
-void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposition& decomp2, TermId common) {
-  Debug("bv-slicer") << "UnionFind::handleCommonSlice common = " << common << endl; 
-  Index common_size = getBitwidth(common); 
-  // find starting points of common slice
-  Index start1 = 0;
-  for (unsigned j = 0; j < decomp1.size(); ++j) {
-    if (decomp1[j] == common)
-      break;
-    start1 += getBitwidth(decomp1[j]); 
-  }
-
-  Index start2 = 0; 
-  for (unsigned j = 0; j < decomp2.size(); ++j) {
-    if (decomp2[j] == common)
-      break;
-    start2 += getBitwidth(decomp2[j]); 
-  }
-  if (start1 > start2) {
-    Index temp = start1;
-    start1 = start2;
-    start2 = temp; 
-  }
-
-  if (start2 - start1 < common_size) {
-    Index overlap = start1 + common_size - start2;
-    Assert(overlap > 0);
-    Index diff = common_size - overlap;
-    Assert(diff >= 0);
-    Index granularity = gcd(diff, overlap);
-    // split the common part 
-    for (unsigned i = 0; i < common_size; i+= granularity) {
-      split(common, i); 
-    }
-  }
-
-}
-
-void UnionFind::alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2) {
-  Debug("bv-slicer") << "UnionFind::alignSlicings " << term1.debugPrint() << endl;
-  Debug("bv-slicer") << "                         " << term2.debugPrint() << endl;
-  NormalForm nf1(term1.getBitwidth());
-  NormalForm nf2(term2.getBitwidth());
-
-  getNormalForm(term1, nf1);
-  getNormalForm(term2, nf2);
-
-  Assert(nf1.base.getBitwidth() == nf2.base.getBitwidth());
-
-  // first check if the two have any common slices
-  std::vector<TermId> intersection;
-  intersect(nf1.decomp, nf2.decomp, intersection);
-  for (TermId id : intersection)
-  {
-    /* handleCommonSlice() may change the normal form */
-    handleCommonSlice(nf1.decomp, nf2.decomp, id);
-  }
-  // propagate cuts to a fixpoint 
-  bool changed;
-  Base cuts(term1.getBitwidth()); 
-  do {
-    changed = false; 
-    // we need to update the normal form which may have changed 
-    getNormalForm(term1, nf1);
-    getNormalForm(term2, nf2); 
-
-    // align the cuts points of the two slicings
-    // FIXME: this can be done more efficiently
-    cuts.sliceWith(nf1.base);
-    cuts.sliceWith(nf2.base); 
-
-    for (unsigned i = 0; i < cuts.getBitwidth(); ++i) {
-      if (cuts.isCutPoint(i)) {
-        if (!nf1.base.isCutPoint(i)) {
-          pair<TermId, Index> pair1 = nf1.getTerm(i, *this);
-          split(pair1.first, i - pair1.second);
-          changed = true; 
-        }
-        if (!nf2.base.isCutPoint(i)) {
-          pair<TermId, Index> pair2 = nf2.getTerm(i, *this);
-          split(pair2.first, i - pair2.second);
-          changed = true; 
-        }
-      }
-    }
-  } while (changed); 
-}
-/** 
- * Given an extract term a[i:j] makes sure a is sliced
- * at indices i and j. 
- * 
- * @param term 
- */
-void UnionFind::ensureSlicing(const ExtractTerm& term) {
-  //Debug("bv-slicer") << "Slicer::ensureSlicing " << term.debugPrint() << endl;
-  TermId id = find(term.id);
-  split(id, term.high + 1);
-  split(id, term.low);
-}
-
-/**
- * Slicer
- * 
- */
-
-ExtractTerm Slicer::registerTerm(TNode node) {
-  Index low = 0, high = utils::getSize(node) - 1; 
-  TNode n = node; 
-  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
-    n = node[0];
-    high = utils::getExtractHigh(node);
-    low = utils::getExtractLow(node); 
-  }
-  if (d_nodeToId.find(n) == d_nodeToId.end()) {
-    TermId id = d_unionFind.addTerm(utils::getSize(n)); 
-    d_nodeToId[n] = id;
-    d_idToNode[id] = n; 
-  }
-  TermId id = d_nodeToId[n];
-  ExtractTerm res(id, high, low); 
-  Debug("bv-slicer") << "Slicer::registerTerm " << node << " => " << res.debugPrint() << endl;
-  return res; 
-}
-
-void Slicer::processEquality(TNode eq) {
-  Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl;
-
-  Assert(eq.getKind() == kind::EQUAL);
-  TNode a = eq[0];
-  TNode b = eq[1];
-  ExtractTerm a_ex= registerTerm(a);
-  ExtractTerm b_ex= registerTerm(b);
-  
-  d_unionFind.ensureSlicing(a_ex);
-  d_unionFind.ensureSlicing(b_ex);
-  
-  d_unionFind.alignSlicings(a_ex, b_ex);
-  d_unionFind.unionTerms(a_ex, b_ex);
-  Debug("bv-slicer") << "Base of " << a_ex.id <<" " << d_unionFind.debugPrint(a_ex.id) << endl;
-  Debug("bv-slicer") << "Base of " << b_ex.id <<" " << d_unionFind.debugPrint(b_ex.id) << endl;
-  Debug("bv-slicer") << "Slicer::processEquality done. " << endl;
-}
-
-void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
-  Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl;
-  
-  Index high = utils::getSize(node) - 1;
-  Index low = 0;
-  TNode top = node; 
-  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
-    high = utils::getExtractHigh(node);
-    low = utils::getExtractLow(node);
-    top = node[0]; 
-  }
-  AlwaysAssert(d_nodeToId.find(top) != d_nodeToId.end());
-  TermId id = d_nodeToId[top];
-  NormalForm nf(high-low+1); 
-  d_unionFind.getNormalForm(ExtractTerm(id, high, low), nf);
-  
-  // construct actual extract nodes
-  unsigned size = utils::getSize(node); 
-  Index current_low = size;
-  Index current_high = size; 
-  for (int i = nf.decomp.size() - 1; i >= 0; --i) {
-    Index current_size = d_unionFind.getBitwidth(nf.decomp[i]); 
-    current_low -= current_size; 
-    Node current = Rewriter::rewrite(utils::mkExtract(node, current_high - 1, current_low));
-    current_high = current_low;
-    decomp.push_back(current); 
-  }
-
-  Debug("bv-slicer") << "as [";
-  for (unsigned i = 0; i < decomp.size(); ++i) {
-    Debug("bv-slicer") << decomp[i] <<" "; 
-  }
-  Debug("bv-slicer") << "]" << endl;
-
-}
-
-bool Slicer::isCoreTerm(TNode node) {
-  if (d_coreTermCache.find(node) == d_coreTermCache.end()) {
-    Kind kind = node.getKind();
-    bool not_core;
-    if (options::bitvectorEqualitySlicer() != options::BvSlicerMode::OFF)
-    {
-      not_core =
-          (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT);
-    }
-    else
-    {
-      not_core = true;
-    }
-    if (not_core &&
-        kind != kind::EQUAL &&
-        kind != kind::NOT &&
-        kind != kind::STORE &&
-        kind != kind::SELECT &&
-        node.getMetaKind() != kind::metakind::VARIABLE &&
-        kind != kind::CONST_BITVECTOR) {
-      d_coreTermCache[node] = false;
-      return false; 
-    } else {
-      // we need to recursively check whether the term is a root term or not
-      bool isCore = true;
-      for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-        isCore = isCore && isCoreTerm(node[i]); 
-      }
-      d_coreTermCache[node] = isCore;
-      return isCore; 
-    }
-  }
-  return d_coreTermCache[node]; 
-}
-unsigned Slicer::d_numAddedEqualities = 0;
-
-void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities)
-{
-  Assert(node.getKind() == kind::EQUAL);
-  NodeManager* nm = NodeManager::currentNM();
-  TNode t1 = node[0];
-  TNode t2 = node[1];
-
-  uint32_t width = utils::getSize(t1);
-
-  Base base1(width);
-  if (t1.getKind() == kind::BITVECTOR_CONCAT)
-  {
-    int size = 0;
-    // no need to count the last child since the end cut point is implicit
-    for (int i = t1.getNumChildren() - 1; i >= 1; --i)
-    {
-      size = size + utils::getSize(t1[i]);
-      base1.sliceAt(size);
-    }
-  }
-
-  Base base2(width);
-  if (t2.getKind() == kind::BITVECTOR_CONCAT)
-  {
-    unsigned size = 0;
-    for (int i = t2.getNumChildren() - 1; i >= 1; --i)
-    {
-      size = size + utils::getSize(t2[i]);
-      base2.sliceAt(size);
-    }
-  }
-
-  base1.sliceWith(base2);
-  if (!base1.isEmpty())
-  {
-    // we split the equalities according to the base
-    int last = 0;
-    for (unsigned i = 1; i <= utils::getSize(t1); ++i)
-    {
-      if (base1.isCutPoint(i))
-      {
-        Node extract1 = utils::mkExtract(t1, i - 1, last);
-        Node extract2 = utils::mkExtract(t2, i - 1, last);
-        last = i;
-        Assert(utils::getSize(extract1) == utils::getSize(extract2));
-        equalities.push_back(nm->mkNode(kind::EQUAL, extract1, extract2));
-      }
-    }
-  }
-  else
-  {
-    // just return same equality
-    equalities.push_back(node);
-  }
-  d_numAddedEqualities += equalities.size() - 1;
-}
-
-std::string UnionFind::debugPrint(TermId id) {
-  ostringstream os; 
-  if (hasChildren(id)) {
-    TermId id1 = find(getChild(id, 1));
-    TermId id0 = find(getChild(id, 0));
-    os << debugPrint(id1);
-    os << debugPrint(id0); 
-  } else {
-    if (getRepr(id) == UndefinedId) {
-      os <<"id"<< id <<"[" << getBitwidth(id) <<"] "; 
-    } else {
-      os << debugPrint(find(id));
-    }
-  }
-  return os.str(); 
-}
-
-UnionFind::Statistics::Statistics():
-  d_numNodes("theory::bv::slicer::NumNodes", 0),
-  d_numRepresentatives("theory::bv::slicer::NumRepresentatives", 0),
-  d_numSplits("theory::bv::slicer::NumSplits", 0),
-  d_numMerges("theory::bv::slicer::NumMerges", 0),
-  d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
-  d_numAddedEqualities("theory::bv::slicer::NumEqualitiesAdded", Slicer::d_numAddedEqualities)
-{
-  smtStatisticsRegistry()->registerStat(&d_numRepresentatives);
-  smtStatisticsRegistry()->registerStat(&d_numSplits);
-  smtStatisticsRegistry()->registerStat(&d_numMerges);
-  smtStatisticsRegistry()->registerStat(&d_avgFindDepth);
-  smtStatisticsRegistry()->registerStat(&d_numAddedEqualities);
-}
-
-UnionFind::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numRepresentatives);
-  smtStatisticsRegistry()->unregisterStat(&d_numSplits);
-  smtStatisticsRegistry()->unregisterStat(&d_numMerges);
-  smtStatisticsRegistry()->unregisterStat(&d_avgFindDepth);
-  smtStatisticsRegistry()->unregisterStat(&d_numAddedEqualities);
-}
 
 }  // namespace bv
 }  // namespace theory
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 794df633f..8946d59eb 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -16,33 +16,17 @@
 
 #include "cvc4_private.h"
 
-#include <math.h>
-
-#include <vector>
-#include <list>
-#include <unordered_map>
-
-#include "expr/node.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "util/bitvector.h"
-#include "util/index.h"
-#include "util/statistics_registry.h"
-
 #ifndef CVC4__THEORY__BV__SLICER_BV_H
 #define CVC4__THEORY__BV__SLICER_BV_H
 
+#include <string>
+#include <vector>
+#include "util/index.h"
 
 namespace CVC4 {
-
 namespace theory {
 namespace bv {
 
-
-
-typedef Index TermId;
-extern const TermId UndefinedId;
-
-
 /** 
  * Base
  * 
@@ -53,20 +37,10 @@ class Base {
 public:
   Base(Index size);
   void sliceAt(Index index); 
-  void sliceWith(const Base& other);
   bool isCutPoint(Index index) const;
-  void diffCutPoints(const Base& other, Base& res) const;
-  bool isEmpty() const;
   std::string debugPrint() const;
-  Index getBitwidth() const { return d_size; }
-  void clear() {
-    for (unsigned i = 0; i < d_repr.size(); ++i) {
-      d_repr[i] = 0; 
-    }
-  }
   bool operator==(const Base& other) const {
-    if (other.getBitwidth() != getBitwidth())
-      return false;
+    if (other.d_size != d_size) return false;
     for (unsigned i = 0; i < d_repr.size(); ++i) {
       if (d_repr[i] != other.d_repr[i])
         return false;
@@ -75,179 +49,6 @@ public:
   }
 }; 
 
-/**
- * UnionFind
- * 
- */
-typedef std::unordered_set<TermId> TermSet;
-typedef std::vector<TermId> Decomposition; 
-
-struct ExtractTerm {
-  TermId id;
-  Index high;
-  Index low;
-  ExtractTerm(TermId i, Index h, Index l)
-    : id (i),
-      high(h),
-      low(l)
-  {
-    Assert(h >= l && id != UndefinedId);
-  }
-  Index getBitwidth() const { return high - low + 1; }
-  std::string debugPrint() const; 
-};
-
-class UnionFind; 
-
-struct NormalForm {
-  Base base;
-  Decomposition decomp;
-
-  NormalForm(Index bitwidth)
-    : base(bitwidth),
-      decomp()
-  {}
-  /** 
-   * Returns the term in the decomposition on which the index i
-   * falls in
-   * @param i 
-   * 
-   * @return 
-   */
-  std::pair<TermId, Index> getTerm(Index i, const UnionFind& uf) const;
-  std::string debugPrint(const UnionFind& uf) const;
-  void clear() { base.clear(); decomp.clear(); }
-};
-
-
-class UnionFind {
-  class Node {
-    Index d_bitwidth;
-    TermId d_ch1, d_ch0;
-    TermId d_repr;
-  public:
-    Node(Index b)
-  : d_bitwidth(b),
-    d_ch1(UndefinedId),
-    d_ch0(UndefinedId), 
-    d_repr(UndefinedId)
-    {}
-    
-    TermId getRepr() const { return d_repr; }
-    Index getBitwidth() const { return d_bitwidth; }
-    bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; }
-
-    TermId getChild(Index i) const {
-      Assert(i < 2);
-      return i == 0? d_ch0 : d_ch1;
-    }
-    void setRepr(TermId id) {
-      Assert(!hasChildren());
-      d_repr = id;
-    }
-    void setChildren(TermId ch1, TermId ch0) {
-      Assert(d_repr == UndefinedId && !hasChildren());
-      d_ch1 = ch1;
-      d_ch0 = ch0; 
-    }
-    std::string debugPrint() const;
-  };
-  
-  /// map from TermId to the nodes that represent them 
-  std::vector<Node> d_nodes;
-  /// a term is in this set if it is its own representative
-  TermSet d_representatives;
-  
-  void getDecomposition(const ExtractTerm& term, Decomposition& decomp);
-  void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common);
-  /// getter methods for the internal nodes
-  TermId getRepr(TermId id)  const {
-    Assert(id < d_nodes.size());
-    return d_nodes[id].getRepr(); 
-  }
-  TermId getChild(TermId id, Index i) const {
-    Assert(id < d_nodes.size());
-    return d_nodes[id].getChild(i); 
-  }
-  Index getCutPoint(TermId id) const {
-    return getBitwidth(getChild(id, 0)); 
-  }
-  bool hasChildren(TermId id) const {
-    Assert(id < d_nodes.size());
-    return d_nodes[id].hasChildren(); 
-  }
-  /// setter methods for the internal nodes
-  void setRepr(TermId id, TermId new_repr) {
-    Assert(id < d_nodes.size());
-    d_nodes[id].setRepr(new_repr); 
-  }
-  void setChildren(TermId id, TermId ch1, TermId ch0) {
-    Assert(id < d_nodes.size()
-           && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0));
-    d_nodes[id].setChildren(ch1, ch0); 
-  }
-
-  class Statistics {
-  public:
-    IntStat d_numNodes; 
-    IntStat d_numRepresentatives;
-    IntStat d_numSplits;
-    IntStat d_numMerges;
-    AverageStat d_avgFindDepth;
-    ReferenceStat<unsigned> d_numAddedEqualities; 
-    //IntStat d_numAddedEqualities; 
-    Statistics();
-    ~Statistics();
-  };
-
-  Statistics d_statistics
-;
-  
-public:
-  UnionFind()
-    : d_nodes(),
-      d_representatives()
-  {}
-
-  TermId addTerm(Index bitwidth);
-  void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2); 
-  void merge(TermId t1, TermId t2);
-  TermId find(TermId t1); 
-  void split(TermId term, Index i);
-
-  void getNormalForm(const ExtractTerm& term, NormalForm& nf);
-  void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2);
-  void ensureSlicing(const ExtractTerm& term);
-  Index getBitwidth(TermId id) const {
-    Assert(id < d_nodes.size());
-    return d_nodes[id].getBitwidth(); 
-  }
-  std::string debugPrint(TermId id);
-  friend class Slicer; 
-};
-
-class Slicer {
-  std::unordered_map<TermId, TNode> d_idToNode;
-  std::unordered_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
-  std::unordered_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
-  UnionFind d_unionFind;
-  ExtractTerm registerTerm(TNode node); 
-public:
-  Slicer()
-    : d_idToNode(),
-      d_nodeToId(),
-      d_coreTermCache(),
-      d_unionFind()
-  {}
-  
-  void getBaseDecomposition(TNode node, std::vector<Node>& decomp);
-  void processEquality(TNode eq);
-  bool isCoreTerm (TNode node);
-  static void splitEqualities(TNode node, std::vector<Node>& equalities);
-  static unsigned d_numAddedEqualities; 
-}; 
-
-
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 2c095e198..d03d81a3d 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -27,7 +27,6 @@
 #include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/bv/bv_subtheory_core.h"
 #include "theory/bv/bv_subtheory_inequality.h"
-#include "theory/bv/slicer.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/bv/theory_bv_rewriter.h"
@@ -70,7 +69,6 @@ TheoryBV::TheoryBV(context::Context* c,
       d_propagatedBy(c),
       d_eagerSolver(),
       d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
-      d_isCoreTheory(false),
       d_calledPreregister(false),
       d_needsLastCallCheck(false),
       d_extf_range_infer(u),
@@ -725,10 +723,6 @@ TrustNode TheoryBV::ppRewrite(TNode t)
   if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) {
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
     res = Rewriter::rewrite(result);
-  } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) {
-    std::vector<Node> equalities;
-    Slicer::splitEqualities(t, equalities);
-    res = utils::mkAnd(equalities);
   } else if (RewriteRule<UltPlusOne>::applies(t)) {
     Node result = RewriteRule<UltPlusOne>::run<false>(t);
     res = Rewriter::rewrite(result);
@@ -912,17 +906,6 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
   return EQUALITY_UNKNOWN; ;
 }
 
-
-void TheoryBV::enableCoreTheorySlicer() {
-  Assert(!d_calledPreregister);
-  d_isCoreTheory = true;
-  if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
-    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-    core->enableSlicer();
-  }
-}
-
-
 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
   if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){
     return;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 11440cb81..65100f98f 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -114,8 +114,6 @@ class TheoryBV : public Theory {
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
-  void enableCoreTheorySlicer();
-
   TrustNode ppRewrite(TNode t) override;
 
   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
@@ -198,7 +196,6 @@ class TheoryBV : public Theory {
 
   std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
   std::unique_ptr<AbstractionModule> d_abstractionModule;
-  bool d_isCoreTheory;
   bool d_calledPreregister;
   
   //for extended functions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f8694e760..7431b26e4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1777,50 +1777,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     });
 }
 
-void TheoryEngine::staticInitializeBVOptions(
-    const std::vector<Node>& assertions)
-{
-  bool useSlicer = true;
-  if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::ON)
-  {
-    if (!d_logicInfo.isPure(theory::THEORY_BV) || d_logicInfo.isQuantified())
-      throw ModalException(
-          "Slicer currently only supports pure QF_BV formulas. Use "
-          "--bv-eq-slicer=off");
-    if (options::incrementalSolving())
-      throw ModalException(
-          "Slicer does not currently support incremental mode. Use "
-          "--bv-eq-slicer=off");
-    if (options::produceModels())
-      throw ModalException(
-          "Slicer does not currently support model generation. Use "
-          "--bv-eq-slicer=off");
-  }
-  else if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::OFF)
-  {
-    return;
-  }
-  else if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::AUTO)
-  {
-    if ((!d_logicInfo.isPure(theory::THEORY_BV) || d_logicInfo.isQuantified())
-        || options::incrementalSolving()
-        || options::produceModels())
-      return;
-
-    bv::utils::TNodeBoolMap cache;
-    for (unsigned i = 0; i < assertions.size(); ++i)
-    {
-      useSlicer = useSlicer && bv::utils::isCoreTerm(assertions[i], cache);
-    }
-  }
-
-  if (useSlicer)
-  {
-    bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
-    bv_theory->enableCoreTheorySlicer();
-  }
-}
-
 SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase()
 {
   return &d_sharedTerms;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bedd54130..91984daca 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -734,7 +734,6 @@ public:
 
   /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
 public:
-  void staticInitializeBVOptions(const std::vector<Node>& assertions);
 
   SharedTermsDatabase* getSharedTermsDatabase();