diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-21 08:39:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-21 08:39:25 -0500 |
| commit | 971a6ac1ccdeb52572565b6b47afedb9eccb7833 (patch) | |
| tree | 119b7a9cb0e174daf4d730165c6476330972d534 /src/theory/bv/theory_bv.cpp | |
| parent | 01a9d18f2b2ce20cf7a0672a865cf0c2873d6f6a (diff) | |
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
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 17 |
1 files changed, 0 insertions, 17 deletions
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; |