From 2d091366f7d437c3839307b1ad732a6999333fe0 Mon Sep 17 00:00:00 2001 From: lianah Date: Wed, 27 Mar 2013 17:48:39 -0400 Subject: reverted the core solver to do static slicing, added option --bv-core-solver --- src/theory/bv/slicer.cpp | 507 ++++++++--------------------------------------- 1 file changed, 80 insertions(+), 427 deletions(-) (limited to 'src/theory/bv/slicer.cpp') diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 121802b65..2837b075f 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -19,7 +19,7 @@ #include "theory/bv/slicer.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" -#include "theory/bv/bv_subtheory_core.h" +#include "theory/bv/options.h" using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; @@ -41,24 +41,15 @@ Base::Base(uint32_t size) void Base::sliceAt(Index index) { - if (index == d_size) - return; - Assert(index < d_size); Index vector_index = index / 32; - Assert (vector_index < d_repr.size()); + if (vector_index == d_repr.size()) + return; + Index int_index = index % 32; uint32_t bit_mask = utils::pow2(int_index); d_repr[vector_index] = d_repr[vector_index] | bit_mask; } -void Base::undoSliceAt(Index index) { - Index vector_index = index / 32; - Assert (vector_index < d_size); - Index int_index = index % 32; - uint32_t bit_mask = utils::pow2(int_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) { @@ -156,13 +147,13 @@ std::string NormalForm::debugPrint(const UnionFind& uf) const { return os.str(); } /** - * UnionFind::EqualityNode + * UnionFind::Node * */ -std::string UnionFind::EqualityNode::debugPrint() const { +std::string UnionFind::Node::debugPrint() const { ostringstream os; - os << "Repr " << d_edge.repr << " ["<< d_bitwidth << "] "; + os << "Repr " << d_repr << " ["<< d_bitwidth << "] "; os << "( " << d_ch1 <<", " << d_ch0 << ")" << endl; return os.str(); } @@ -172,94 +163,27 @@ std::string UnionFind::EqualityNode::debugPrint() const { * UnionFind * */ - -TermId UnionFind::registerTopLevelTerm(Index bitwidth) { - TermId id = mkEqualityNode(bitwidth); - d_topLevelIds.insert(id); - return id; -} - -TermId UnionFind::mkEqualityNode(Index bitwidth) { - Assert (bitwidth > 0); - EqualityNode node(bitwidth); - d_equalityNodes.push_back(node); - +TermId UnionFind::addTerm(Index bitwidth) { + Node node(bitwidth); + d_nodes.push_back(node); ++(d_statistics.d_numNodes); - TermId id = d_equalityNodes.size() - 1; - // d_representatives.insert(id); + 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; } -/** - * Create an extract term making sure there are no nested extracts. - * - * @param id - * @param high - * @param low - * - * @return - */ -ExtractTerm UnionFind::mkExtractTerm(TermId id, Index high, Index low) { - if (d_topLevelIds.find(id) != d_topLevelIds.end()) { - return ExtractTerm(id, high, low); - } - Assert (isExtractTerm(id)); - ExtractTerm top = getExtractTerm(id); - Assert (d_topLevelIds.find(top.id) != d_topLevelIds.end()); - - Index top_low = top.low; - Assert (top.high - top_low + 1 > high); - high += top_low; - low += top_low; - id = top.id; - return ExtractTerm(id, high, low); -} - -/** - * Associate the given extract term with the given id. - * - * @param id - * @param extract - */ -void UnionFind::storeExtractTerm(TermId id, const ExtractTerm& extract) { - if (d_extractToId.find(extract) != d_extractToId.end()) { - Assert (d_extractToId[extract] == id); - return; - } - Debug("bv-slicer") << "UnionFind::storeExtract " << extract.debugPrint() << " => id" << id << "\n"; - d_idToExtract[id] = extract; - d_extractToId[extract] = id; - } - -TermId UnionFind::addEqualityNode(unsigned bitwidth, TermId id, Index high, Index low) { - ExtractTerm extract(id, high, low); - if (d_extractToId.find(extract) != d_extractToId.end()) { - // if the extract already exists we don't need to make a new node - TermId extract_id = d_extractToId[extract]; - Assert (extract_id < d_equalityNodes.size()); - return extract_id; - } - // otherwise make an equality node for it and store the extract - TermId node_id = mkEqualityNode(bitwidth); - storeExtractTerm(node_id, extract); - return node_id; -} - /** * At this point we assume the slicings of the two terms are properly aligned. * * @param t1 * @param t2 */ -void UnionFind::unionTerms(TermId id1, TermId id2, TermId reason) { - const ExtractTerm& t1 = getExtractTerm(id1); - const ExtractTerm& t2 = getExtractTerm(id2); - +void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) { Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n" - << " " << t2.debugPrint() << "\n" - << " with reason " << reason << endl; + << " " << t2.debugPrint() << endl; Assert (t1.getBitwidth() == t2.getBitwidth()); NormalForm nf1(t1.getBitwidth()); @@ -272,11 +196,10 @@ void UnionFind::unionTerms(TermId id1, TermId id2, TermId reason) { Assert (nf1.base == nf2.base); for (unsigned i = 0; i < nf1.decomp.size(); ++i) { - merge (nf1.decomp[i], nf2.decomp[i], reason); + merge (nf1.decomp[i], nf2.decomp[i]); } } - /** * Merge the two terms in the union find. Both t1 and t2 * should be root terms. @@ -284,7 +207,7 @@ void UnionFind::unionTerms(TermId id1, TermId id2, TermId reason) { * @param t1 * @param t2 */ -void UnionFind::merge(TermId t1, TermId t2, TermId reason) { +void UnionFind::merge(TermId t1, TermId t2) { Debug("bv-slicer-uf") << "UnionFind::merge (" << t1 <<", " << t2 << ")" << endl; ++(d_statistics.d_numMerges); t1 = find(t1); @@ -294,9 +217,8 @@ void UnionFind::merge(TermId t1, TermId t2, TermId reason) { return; Assert (! hasChildren(t1) && ! hasChildren(t2)); - setRepr(t1, t2, reason); - recordOperation(UnionFind::MERGE, t1); - //d_representatives.erase(t1); + setRepr(t1, t2); + d_representatives.erase(t1); d_statistics.d_numRepresentatives += -1; } @@ -304,26 +226,11 @@ 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; } - -TermId UnionFind::findWithExplanation(TermId id, std::vector& explanation) { - TermId repr = getRepr(id); - - if (repr != UndefinedId) { - TermId reason = getReason(id); - Assert (reason != UndefinedId); - explanation.push_back(reason); - - TermId find_id = findWithExplanation(repr, explanation); - return find_id; - } - return id; -} - - /** * Splits the representative of the term between i-1 and i * @@ -335,30 +242,19 @@ TermId UnionFind::findWithExplanation(TermId id, std::vector& exp 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_equalityNodes[id].debugPrint() << endl; + Debug("bv-slicer-uf") << " node: " << d_nodes[id].debugPrint() << endl; if (i == 0 || i == getBitwidth(id)) { // nothing to do - return; + return; } - Assert (i < getBitwidth(id)); if (!hasChildren(id)) { - // first time we split this term - ExtractTerm bottom_extract = mkExtractTerm(id, i-1, 0); - ExtractTerm top_extract = mkExtractTerm(id, getBitwidth(id) - 1, i); - - TermId bottom_id = extractHasId(bottom_extract)? getExtractId(bottom_extract) : mkEqualityNode(i); - TermId top_id = extractHasId(top_extract)? getExtractId(top_extract) : mkEqualityNode(getBitwidth(id) - i); - storeExtractTerm(bottom_id, bottom_extract); - storeExtractTerm(top_id, top_extract); - + // first time we split this term + TermId bottom_id = addTerm(i); + TermId top_id = addTerm(getBitwidth(id) - i); setChildren(id, top_id, bottom_id); - recordOperation(UnionFind::SPLIT, id); - - if (d_slicer->termInEqualityEngine(id)) { - d_slicer->enqueueSplit(id, i, top_id, bottom_id); - } + } else { Index cut = getCutPoint(id); if (i < cut ) @@ -369,14 +265,6 @@ void UnionFind::split(TermId id, Index i) { ++(d_statistics.d_numSplits); } -// TermId UnionFind::getTopLevel(TermId id) const { -// __gnu_cxx::hash_map >::const_iterator it = d_idToExtract.find(id); -// if (it != d_idToExtract.end()) { -// return (*it).second.id; -// } -// return id; -// } - void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) { nf.clear(); getDecomposition(term, nf.decomp); @@ -423,56 +311,6 @@ void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) getDecomposition(high_child, decomp); } } - -void UnionFind::getNormalFormWithExplanation(const ExtractTerm& term, NormalForm& nf, - std::vector& explanation) { - nf.clear(); - getDecompositionWithExplanation(term, nf.decomp, explanation); - // 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::getDecompositionWithExplanation(const ExtractTerm& term, Decomposition& decomp, - std::vector& explanation) { - // making sure the term is aligned - TermId id = findWithExplanation(term.id, explanation); - - 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); - getDecompositionWithExplanation(child_ex, decomp, explanation); - } - 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); - getDecompositionWithExplanation(child_ex, decomp, explanation); - } - else { - // the extract is split over the two children - ExtractTerm low_child(getChild(id, 0), cut - 1, term.low); - getDecompositionWithExplanation(low_child, decomp, explanation); - ExtractTerm high_child(getChild(id, 1), term.high - cut, 0); - getDecompositionWithExplanation(high_child, decomp, explanation); - } -} - /** * May cause reslicings of the decompositions. Must not assume the decompositons * are the current normal form. @@ -518,10 +356,7 @@ void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposit } -void UnionFind::alignSlicings(TermId id1, TermId id2) { - const ExtractTerm& term1 = getExtractTerm(id1); - const ExtractTerm& term2 = getExtractTerm(id2); - +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()); @@ -569,169 +404,63 @@ void UnionFind::alignSlicings(TermId id1, TermId id2) { } } while (changed); } - - /** * Given an extract term a[i:j] makes sure a is sliced * at indices i and j. * * @param term */ -void UnionFind::ensureSlicing(TermId t) { - ExtractTerm term = getExtractTerm(t); +void UnionFind::ensureSlicing(const ExtractTerm& term) { //Debug("bv-slicer") << "Slicer::ensureSlicing " << term.debugPrint() << endl; - TermId id = term.id; + TermId id = find(term.id); split(id, term.high + 1); split(id, term.low); } -void UnionFind::backtrack() { - int size = d_undoStack.size(); - for (int i = size; i > (int)d_undoStackIndex.get(); --i) { - Assert (!d_undoStack.empty()); - Operation op = d_undoStack.back(); - d_undoStack.pop_back(); - if (op.op == UnionFind::MERGE) { - undoMerge(op.id); - } else { - Assert (op.op == UnionFind::SPLIT); - undoSplit(op.id); - } - } -} - -void UnionFind::undoMerge(TermId id) { - Assert (getRepr(id) != UndefinedId); - setRepr(id, UndefinedId, UndefinedId); -} - -void UnionFind::undoSplit(TermId id) { - Assert (hasChildren(id)); - setChildren(id, UndefinedId, UndefinedId); -} - -void UnionFind::recordOperation(OperationKind op, TermId term) { - d_undoStackIndex.set(d_undoStackIndex.get() + 1); - d_undoStack.push_back(Operation(op, term)); - Assert (d_undoStack.size() == d_undoStackIndex); -} - -void UnionFind::getBase(TermId id, Base& base, Index offset) { - id = find(id); - if (!hasChildren(id)) - return; - TermId id1 = find(getChild(id, 1)); - TermId id0 = find(getChild(id, 0)); - Index cut = getCutPoint(id); - base.sliceAt(cut + offset); - getBase(id1, base, cut + offset); - getBase(id0, base, offset); -} - -/// getter methods for the internal nodes -TermId UnionFind::getRepr(TermId id) const { - Assert (id < d_equalityNodes.size()); - return d_equalityNodes[id].getRepr(); -} -ExplanationId UnionFind::getReason(TermId id) const { - Assert (id < d_equalityNodes.size()); - return d_equalityNodes[id].getReason(); -} -TermId UnionFind::getChild(TermId id, Index i) const { - Assert (id < d_equalityNodes.size()); - return d_equalityNodes[id].getChild(i); -} -Index UnionFind::getCutPoint(TermId id) const { - return getBitwidth(getChild(id, 0)); -} -bool UnionFind::hasChildren(TermId id) const { - Assert (id < d_equalityNodes.size()); - return d_equalityNodes[id].hasChildren(); -} - -/// setter methods for the internal nodes -void UnionFind::setRepr(TermId id, TermId new_repr, ExplanationId reason) { - Assert (id < d_equalityNodes.size()); - d_equalityNodes[id].setRepr(new_repr, reason); -} -void UnionFind::setChildren(TermId id, TermId ch1, TermId ch0) { - Assert ((ch1 == UndefinedId && ch0 == UndefinedId) || - (id < d_equalityNodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0))); - d_equalityNodes[id].setChildren(ch1, ch0); -} - - /** * Slicer * */ -TermId Slicer::registerTerm(TNode node) { +ExtractTerm Slicer::registerTerm(TNode node) { + Index low = 0, high = utils::getSize(node) - 1; + TNode n = node; if (node.getKind() == kind::BITVECTOR_EXTRACT) { - TNode n = node[0]; - TermId top_id = registerTopLevelTerm(n); - Index high = utils::getExtractHigh(node); - Index low = utils::getExtractLow(node); - TermId id = d_unionFind.addEqualityNode(utils::getSize(node), top_id, high, low); - return id; + n = node[0]; + high = utils::getExtractHigh(node); + low = utils::getExtractLow(node); } - TermId id = registerTopLevelTerm(node); - return id; -} - -TermId Slicer::registerTopLevelTerm(TNode node) { - Assert (node.getKind() != kind::BITVECTOR_EXTRACT || - node.getKind() != kind::BITVECTOR_CONCAT); - - if (d_nodeToId.find(node) == d_nodeToId.end()) { - TermId id = d_unionFind.registerTopLevelTerm(utils::getSize(node)); - d_idToNode[id] = node; - d_nodeToId[node] = id; - Debug("bv-slicer") << "Slicer::registerTopLevelTerm " << node << " => id" << id << endl; - return id; + if (d_nodeToId.find(n) == d_nodeToId.end()) { + TermId id = d_unionFind.addTerm(utils::getSize(n)); + d_nodeToId[n] = id; + d_idToNode[id] = n; } - return d_nodeToId[node]; + 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; - - registerEquality(eq); + Assert (eq.getKind() == kind::EQUAL); TNode a = eq[0]; TNode b = eq[1]; - TermId a_id = registerTerm(a); - TermId b_id = registerTerm(b); + ExtractTerm a_ex= registerTerm(a); + ExtractTerm b_ex= registerTerm(b); - d_unionFind.ensureSlicing(a_id); - d_unionFind.ensureSlicing(b_id); + d_unionFind.ensureSlicing(a_ex); + d_unionFind.ensureSlicing(b_ex); - d_unionFind.alignSlicings(a_id, b_id); - - // 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; + 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::assertEquality(TNode eq) { - Assert (eq.getKind() == kind::EQUAL); - TermId a = registerTerm(eq[0]); - TermId b = registerTerm(eq[1]); - ExplanationId reason = getExplanationId(eq); - d_unionFind.unionTerms(a, b, reason); -} - - -void Slicer::registerEquality(TNode eq) { - if (d_explanationToId.find(eq) == d_explanationToId.end()) { - ExplanationId id = d_explanations.size(); - d_explanations.push_back(eq); - d_explanationToId[eq] = id; - Debug("bv-slicer-explanation") << "Slicer::registerEquality " << eq << " => id"<< id << "\n"; - } -} - -void Slicer::getBaseDecomposition(TNode node, std::vector& decomp, std::vector& explanation) { +void Slicer::getBaseDecomposition(TNode node, std::vector& decomp) { Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl; Index high = utils::getSize(node) - 1; @@ -742,47 +471,45 @@ void Slicer::getBaseDecomposition(TNode node, std::vector& decomp, std::ve low = utils::getExtractLow(node); top = node[0]; } - Assert (d_nodeToId.find(top) != d_nodeToId.end()); TermId id = d_nodeToId[top]; - NormalForm nf(high-low+1); - std::vector explanation_ids; - d_unionFind.getNormalFormWithExplanation(ExtractTerm(id, high, low), nf, explanation_ids); - - for (unsigned i = 0; i < explanation_ids.size(); ++i) { - Assert (hasExplanation(explanation_ids[i])); - TNode exp = getExplanation(explanation_ids[i]); - explanation.push_back(exp); - } + NormalForm nf(high-low+1); + d_unionFind.getNormalForm(ExtractTerm(id, high, low), nf); - for (int i = nf.decomp.size() - 1; i>=0 ; --i) { - Node current = getNode(nf.decomp[i]); + // 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); } - if (Debug.isOn("bv-slicer-explanation")) { - Debug("bv-slicer-explanation") << "Slicer::getBaseDecomposition for " << node << "\n" - << "as "; - for (unsigned i = 0; i < decomp.size(); ++i) { - Debug("bv-slicer-explanation") << decomp[i] <<" " ; - } - Debug("bv-slicer-explanation") << "\n Explanation : \n"; - for (unsigned i = 0; i < explanation.size(); ++i) { - Debug("bv-slicer-explanation") << " " << explanation[i] << "\n"; - } - + + 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(); - if (//kind != kind::BITVECTOR_EXTRACT && - //kind != kind::BITVECTOR_CONCAT && + Kind kind = node.getKind(); + bool not_core; + if (options::bitvectorCoreSolver()) { + 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 && - kind != kind::NOT && node.getMetaKind() != kind::metakind::VARIABLE && kind != kind::CONST_BITVECTOR) { d_coreTermCache[node] = false; @@ -845,81 +572,7 @@ void Slicer::splitEqualities(TNode node, std::vector& equalities) { equalities.push_back(node); } d_numAddedEqualities += equalities.size() - 1; -} - - -ExtractTerm UnionFind::getExtractTerm(TermId id) const { - if (d_topLevelIds.find(id) != d_topLevelIds.end()) { - // if it's a top level term so we don't have an extract stored for it - return ExtractTerm(id, getBitwidth(id) - 1, 0); - } - Assert (isExtractTerm(id)); - - return (d_idToExtract.find(id))->second; -} - -bool UnionFind::isExtractTerm(TermId id) const { - return d_idToExtract.find(id) != d_idToExtract.end(); -} - -bool Slicer::isTopLevelNode(TermId id) const { - return d_idToNode.find(id) != d_idToNode.end(); -} - -Node Slicer::getNode(TermId id) const { - if (isTopLevelNode(id)) { - return d_idToNode.find(id)->second; - } - Assert (d_unionFind.isExtractTerm(id)); - const ExtractTerm& extract = d_unionFind.getExtractTerm(id); - Assert (isTopLevelNode(extract.id)); - TNode node = d_idToNode.find(extract.id)->second; - if (extract.high == utils::getSize(node) -1 && extract.low == 0) { - return node; - } - Node ex = utils::mkExtract(node, extract.high, extract.low); - return ex; -} - -bool Slicer::termInEqualityEngine(TermId id) { - Node node = getNode(id); - return d_coreSolver->hasTerm(node); -} - -void Slicer::enqueueSplit(TermId id, Index i, TermId top_id, TermId bottom_id) { - Node node = getNode(id); - Node bottom = Rewriter::rewrite(utils::mkExtract(node, i -1 , 0)); - Node top = Rewriter::rewrite(utils::mkExtract(node, utils::getSize(node) - 1, i)); - // must add terms to equality engine so we get notified when they get split more - d_coreSolver->addTermToEqualityEngine(bottom); - d_coreSolver->addTermToEqualityEngine(top); - - Node eq = utils::mkNode(kind::EQUAL, node, utils::mkConcat(top, bottom)); - d_newSplits.push_back(eq); - Debug("bv-slicer") << "Slicer::enqueueSplit " << eq << endl; - Debug("bv-slicer") << " " << id << "=" << top_id << " " << bottom_id << endl; -} - -void Slicer::getNewSplits(std::vector& splits) { - for (unsigned i = d_newSplitsIndex; i < d_newSplits.size(); ++i) { - splits.push_back(d_newSplits[i]); - } - d_newSplitsIndex = d_newSplits.size(); -} - -bool Slicer::hasExplanation(ExplanationId id) const { - return id < d_explanations.size(); -} - -TNode Slicer::getExplanation(ExplanationId id) const { - Assert(hasExplanation(id)); - return d_explanations[id]; -} - -ExplanationId Slicer::getExplanationId(TNode reason) const { - Assert (d_explanationToId.find(reason) != d_explanationToId.end()); - return d_explanationToId.find(reason)->second; -} +} std::string UnionFind::debugPrint(TermId id) { ostringstream os; -- cgit v1.2.3