bv: Remove layered solver. (#7455)

This commit removes the old bit-vector solver code.

3 files changed, 0 insertions, 116 deletions

diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
deleted file mode 100644
index cea5bf37c..000000000
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ /dev/null
@@ -1,64 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Mathias Preiner, Andrew Reynolds, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * The BvAbstraction preprocessing pass.
- *
- * Abstract common structures over small domains to UF. This preprocessing
- * is particularly useful on QF_BV/mcm benchmarks and can be enabled via
- * option `--bv-abstraction`.
- * For more information see 3.4 Refactoring Isomorphic Circuits in [1].
- *
- * [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for
- *     Bit-vectors in Satisfiability Modulo Theories
- *     https://cs.nyu.edu/media/publications/hadarean_liana.pdf
- */
-
-#include "preprocessing/passes/bv_abstraction.h"
-
-#include <vector>
-
-#include "options/bv_options.h"
-#include "preprocessing/assertion_pipeline.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/rewriter.h"
-#include "theory/theory_engine.h"
-
-namespace cvc5 {
-namespace preprocessing {
-namespace passes {
-
-using namespace cvc5::theory;
-
-BvAbstraction::BvAbstraction(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "bv-abstraction"){};
-
-PreprocessingPassResult BvAbstraction::applyInternal(
-    AssertionPipeline* assertionsToPreprocess)
-{
-  std::vector<Node> new_assertions;
-  std::vector<Node> assertions(assertionsToPreprocess->begin(),
-                               assertionsToPreprocess->end());
-  TheoryEngine* te = d_preprocContext->getTheoryEngine();
-  bv::TheoryBV* bv_theory = static_cast<bv::TheoryBV*>(te->theoryOf(THEORY_BV));
-  bv_theory->applyAbstraction(assertions, new_assertions);
-  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
-  {
-    assertionsToPreprocess->replace(i, rewrite(new_assertions[i]));
-  }
-  return PreprocessingPassResult::NO_CONFLICT;
-}
-
-
-}  // namespace passes
-}  // namespace preprocessing
-}  // namespace cvc5
diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h
deleted file mode 100644
index 0f3db2f59..000000000
--- a/src/preprocessing/passes/bv_abstraction.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * The BvAbstraction preprocessing pass.
- *
- * Abstract common structures over small domains to UF. This preprocessing
- * is particularly useful on QF_BV/mcm benchmarks and can be enabled via
- * option `--bv-abstraction`.
- * For more information see 3.4 Refactoring Isomorphic Circuits in [1].
- *
- * [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for
- *     Bit-vectors in Satisfiability Modulo Theories
- *     https://cs.nyu.edu/media/publications/hadarean_liana.pdf
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H
-#define CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H
-
-#include "preprocessing/preprocessing_pass.h"
-
-namespace cvc5 {
-namespace preprocessing {
-namespace passes {
-
-class BvAbstraction : public PreprocessingPass
-{
- public:
-  BvAbstraction(PreprocessingPassContext* preprocContext);
-
- protected:
-  PreprocessingPassResult applyInternal(
-      AssertionPipeline* assertionsToPreprocess) override;
-};
-
-}  // namespace passes
-}  // namespace preprocessing
-}  // namespace cvc5
-
-#endif /* CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index f0bd5af86..b0f9992ca 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -27,7 +27,6 @@
 #include "preprocessing/passes/ackermann.h"
 #include "preprocessing/passes/apply_substs.h"
 #include "preprocessing/passes/bool_to_bv.h"
-#include "preprocessing/passes/bv_abstraction.h"
 #include "preprocessing/passes/bv_eager_atoms.h"
 #include "preprocessing/passes/bv_gauss.h"
 #include "preprocessing/passes/bv_intro_pow2.h"
@@ -137,7 +136,6 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("sort-inference", callCtor<SortInferencePass>);
   registerPassInfo("sep-skolem-emp", callCtor<SepSkolemEmp>);
   registerPassInfo("rewrite", callCtor<Rewrite>);
-  registerPassInfo("bv-abstraction", callCtor<BvAbstraction>);
   registerPassInfo("bv-eager-atoms", callCtor<BvEagerAtoms>);
   registerPassInfo("pseudo-boolean-processor",
                    callCtor<PseudoBooleanProcessor>);