diff options
author | lianah <lianahady@gmail.com> | 2013-03-21 19:25:33 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-21 19:25:33 -0400 |
commit | ff8572914d73449b26edba214ad134c596196e32 (patch) | |
tree | 8a3d70b2d1b4c703edc9757b2d4417ff6c49e393 /src/theory/bv/slicer.cpp | |
parent | 43ed2d4e9575232655db7df249ba9be1fc9eba61 (diff) |
fixed more equality stuff
Diffstat (limited to 'src/theory/bv/slicer.cpp')
-rw-r--r-- | src/theory/bv/slicer.cpp | 77 |
1 files changed, 43 insertions, 34 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 437be9bf4..5d376ea50 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -41,8 +41,11 @@ 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_size); + Assert (vector_index < d_repr.size()); Index int_index = index % 32; uint32_t bit_mask = utils::pow2(int_index); d_repr[vector_index] = d_repr[vector_index] | bit_mask; @@ -184,6 +187,15 @@ TermId UnionFind::addNode(Index bitwidth) { } TermId UnionFind::addExtract(TermId topLevel, Index high, Index low) { + if (isExtractTerm(topLevel)) { + ExtractTerm top = getExtractTerm(topLevel); + Index top_high = top.high; + Index top_low = top.low; + Assert (top_high - top_low + 1 > high); + high += top_low; + low += top_low; + topLevel = top.id; + } ExtractTerm extract(topLevel, high, low); if (d_extractToId.find(extract) != d_extractToId.end()) { return d_extractToId[extract]; @@ -292,13 +304,13 @@ void UnionFind::split(TermId id, Index i) { Assert (i < getBitwidth(id)); if (!hasChildren(id)) { // first time we split this term - TermId bottom_id = addExtract(getTopLevel(id), i - 1, 0); - TermId top_id = addExtract(getTopLevel(id), getBitwidth(id) - 1, i); + TermId bottom_id = addExtract(id, i - 1, 0); + TermId top_id = addExtract(id, getBitwidth(id) - 1, i); setChildren(id, top_id, bottom_id); recordOperation(UnionFind::SPLIT, id); if (d_slicer->termInEqualityEngine(id)) { - d_slicer->enqueueSplit(id, i); + d_slicer->enqueueSplit(id, i, top_id, bottom_id); } } else { Index cut = getCutPoint(id); @@ -310,13 +322,13 @@ void UnionFind::split(TermId id, Index i) { ++(d_statistics.d_numSplits); } -TermId UnionFind::getTopLevel(TermId id) const { - __gnu_cxx::hash_map<TermId, ExtractTerm, __gnu_cxx::hash<TermId> >::const_iterator it = d_idToExtract.find(id); - if (it != d_idToExtract.end()) { - return (*it).second.id; - } - return id; -} +// TermId UnionFind::getTopLevel(TermId id) const { +// __gnu_cxx::hash_map<TermId, ExtractTerm, __gnu_cxx::hash<TermId> >::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(); @@ -576,7 +588,7 @@ ExtractTerm Slicer::registerTerm(TNode node) { if (node.getKind() == kind::BITVECTOR_EXTRACT) { n = node[0]; high = utils::getExtractHigh(node); - low = utils::getExtractLow(node); + low = utils::getExtractLow(node); } if (d_nodeToId.find(n) == d_nodeToId.end()) { TermId id = d_unionFind.addNode(utils::getSize(n)); @@ -584,6 +596,7 @@ ExtractTerm Slicer::registerTerm(TNode node) { d_idToNode[id] = n; } TermId id = d_nodeToId[n]; + d_unionFind.addExtract(id, high, low); ExtractTerm res(id, high, low); Debug("bv-slicer") << "Slicer::registerTerm " << node << " => " << res.debugPrint() << endl; return res; @@ -631,7 +644,7 @@ void Slicer::registerEquality(TNode eq) { } } -void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<TNode>& explanation) { +void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<Node>& explanation) { Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl; Index high = utils::getSize(node) - 1; @@ -655,16 +668,8 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::ve explanation.push_back(exp); } - // construct actual extract nodes - Index size = utils::getSize(node); - Index current_low = size - 1; - Index current_high = size - 1; - for (int i = nf.decomp.size() - 1; i>=0 ; --i) { - Index current_size = d_unionFind.getBitwidth(nf.decomp[i]); - current_low = current_low - current_size; - Node current = Rewriter::rewrite(utils::mkExtract(node, current_high, current_low+1)); - current_high -= current_size; + Node current = getNode(nf.decomp[i]); decomp.push_back(current); } @@ -763,17 +768,16 @@ bool Slicer::hasNode(TermId id) const { } Node Slicer::getNode(TermId id) const { - // if it was an extract - if (d_unionFind.isExtractTerm(id)) { - ExtractTerm extract = d_unionFind.getExtractTerm(id); - Assert (hasNode(extract.id)); - TNode node = d_idToNode.find(extract.id)->second; - Node ex = utils::mkExtract(node, extract.high, extract.low); - return ex; + if (hasNode(id)) { + return d_idToNode.find(id)->second; } - // otherwise must be a top-level term - Assert (hasNode(id)); - return (d_idToNode.find(id))->second; + // otherwise must be an extract + Assert (d_unionFind.isExtractTerm(id)); + ExtractTerm extract = d_unionFind.getExtractTerm(id); + Assert (hasNode(extract.id)); + TNode node = d_idToNode.find(extract.id)->second; + Node ex = utils::mkExtract(node, extract.high, extract.low); + return ex; } bool Slicer::termInEqualityEngine(TermId id) { @@ -781,13 +785,18 @@ bool Slicer::termInEqualityEngine(TermId id) { return d_coreSolver->hasTerm(node); } -void Slicer::enqueueSplit(TermId id, Index i) { +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") << "Slicer::enqueueSplit " << eq << endl; + Debug("bv-slicer") << " " << id << "=" << top_id << " " << bottom_id << endl; } void Slicer::getNewSplits(std::vector<Node>& splits) { |