diff options
Diffstat (limited to 'src/theory/bv/slicer.cpp')
-rw-r--r-- | src/theory/bv/slicer.cpp | 45 |
1 files changed, 22 insertions, 23 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index e633792d8..0ffd58d5a 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -58,7 +58,7 @@ Base::Base(uint32_t size) : d_size(size), d_repr(size/32 + (size % 32 == 0? 0 : 1), 0) { - Assert (d_size > 0); + Assert(d_size > 0); } void Base::sliceAt(Index index) @@ -73,7 +73,7 @@ void Base::sliceAt(Index index) } void Base::sliceWith(const Base& other) { - Assert (d_size == other.d_size); + 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]; } @@ -86,7 +86,7 @@ bool Base::isCutPoint (Index index) const return true; Index vector_index = index / 32; - Assert (vector_index < d_size); + Assert(vector_index < d_size); Index int_index = index % 32; uint32_t bit_mask = 1u << int_index; @@ -94,9 +94,9 @@ bool Base::isCutPoint (Index index) const } void Base::diffCutPoints(const Base& other, Base& res) const { - Assert (d_size == other.d_size && res.d_size == d_size); + 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); + Assert(res.d_repr[i] == 0); res.d_repr[i] = d_repr[i] ^ other.d_repr[i]; } } @@ -144,7 +144,7 @@ std::string ExtractTerm::debugPrint() const { */ std::pair<TermId, Index> NormalForm::getTerm(Index index, const UnionFind& uf) const { - Assert (index < base.getBitwidth()); + Assert(index < base.getBitwidth()); Index count = 0; for (unsigned i = 0; i < decomp.size(); ++i) { Index size = uf.getBitwidth(decomp[i]); @@ -207,17 +207,17 @@ TermId UnionFind::addTerm(Index bitwidth) { 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()); - + 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); - + 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]); } @@ -239,7 +239,7 @@ void UnionFind::merge(TermId t1, TermId t2) { if (t1 == t2) return; - Assert (! hasChildren(t1) && ! hasChildren(t2)); + Assert(!hasChildren(t1) && !hasChildren(t2)); setRepr(t1, t2); d_representatives.erase(t1); d_statistics.d_numRepresentatives += -1; @@ -271,7 +271,7 @@ void UnionFind::split(TermId id, Index i) { // nothing to do return; } - Assert (i < getBitwidth(id)); + Assert(i < getBitwidth(id)); if (!hasChildren(id)) { // first time we split this term TermId bottom_id = addTerm(i); @@ -303,13 +303,12 @@ void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) { void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) { // making sure the term is aligned - TermId id = find(term.id); + TermId id = find(term.id); - Assert (term.high < getBitwidth(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); + Assert(term.high == getBitwidth(id) - 1 && term.low == 0); decomp.push_back(id); return; } @@ -380,9 +379,9 @@ void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposit if (start2 - start1 < common_size) { Index overlap = start1 + common_size - start2; - Assert (overlap > 0); + Assert(overlap > 0); Index diff = common_size - overlap; - Assert (diff >= 0); + Assert(diff >= 0); Index granularity = gcd(diff, overlap); // split the common part for (unsigned i = 0; i < common_size; i+= granularity) { @@ -401,7 +400,7 @@ void UnionFind::alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2 getNormalForm(term1, nf1); getNormalForm(term2, nf2); - Assert (nf1.base.getBitwidth() == nf2.base.getBitwidth()); + Assert(nf1.base.getBitwidth() == nf2.base.getBitwidth()); // first check if the two have any common slices std::vector<TermId> intersection; @@ -480,8 +479,8 @@ ExtractTerm Slicer::registerTerm(TNode node) { void Slicer::processEquality(TNode eq) { Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl; - - Assert (eq.getKind() == kind::EQUAL); + + Assert(eq.getKind() == kind::EQUAL); TNode a = eq[0]; TNode b = eq[1]; ExtractTerm a_ex= registerTerm(a); @@ -508,7 +507,7 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) { low = utils::getExtractLow(node); top = node[0]; } - AlwaysAssert (d_nodeToId.find(top) != d_nodeToId.end()); + 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); |