From 971a6ac1ccdeb52572565b6b47afedb9eccb7833 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 Aug 2020 08:39:25 -0500 Subject: [PATCH] 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 --- .../run-script-smtcomp-current-unsat-cores | 2 +- src/options/bv_options.toml | 18 - src/options/options_handler.cpp | 11 - src/smt/process_assertions.cpp | 5 - src/smt/set_defaults.cpp | 5 - src/theory/bv/bv_subtheory_core.cpp | 86 +-- src/theory/bv/bv_subtheory_core.h | 8 +- src/theory/bv/slicer.cpp | 586 ------------------ src/theory/bv/slicer.h | 207 +------ src/theory/bv/theory_bv.cpp | 17 - src/theory/bv/theory_bv.h | 3 - src/theory/theory_engine.cpp | 44 -- src/theory/theory_engine.h | 1 - 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 @@ -108,24 +108,6 @@ header = "options/bv_options.h" default = "true" 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" 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& assumptions) { } } -Node CoreSolver::getBaseDecomposition(TNode a) { - std::vector 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 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::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 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 d_slicer; context::CDO 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& v1, - const std::vector& v2, - std::vector& 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 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(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 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 pair1 = nf1.getTerm(i, *this); - split(pair1.first, i - pair1.second); - changed = true; - } - if (!nf2.base.isCutPoint(i)) { - pair 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& 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& 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 - -#include -#include -#include - -#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 +#include +#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 TermSet; -typedef std::vector 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 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 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 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 d_idToNode; - std::unordered_map d_nodeToId; - std::unordered_map 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& decomp); - void processEquality(TNode eq); - bool isCoreTerm (TNode node); - static void splitEqualities(TNode node, std::vector& 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::applies(t)) { Node result = RewriteRule::run(t); res = Rewriter::rewrite(result); - } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) { - std::vector equalities; - Slicer::splitEqualities(t, equalities); - res = utils::mkAnd(equalities); } else if (RewriteRule::applies(t)) { Node result = RewriteRule::run(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 d_eagerSolver; std::unique_ptr 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& 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& assertions); SharedTermsDatabase* getSharedTermsDatabase(); -- 2.30.2