diff options
Diffstat (limited to 'src/preprocessing/passes/bv_to_int.cpp')
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 42 |
1 files changed, 23 insertions, 19 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index bb0bde2f9..041312113 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -108,7 +108,7 @@ Node BVToInt::makeBinary(Node n) d_binarizeCache[current] = Node(); toVisit.insert(toVisit.end(), current.begin(), current.end()); } - else if (d_binarizeCache[current].isNull()) + else if (d_binarizeCache[current].get().isNull()) { /* * We already visited the sub-dag rooted at the current node, @@ -137,14 +137,13 @@ Node BVToInt::makeBinary(Node n) { // current has children, but we do not binarize it NodeBuilder<> builder(k); - if (current.getKind() == kind::BITVECTOR_EXTRACT - || current.getKind() == kind::APPLY_UF) + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); } for (Node child : current) { - builder << d_binarizeCache[child]; + builder << d_binarizeCache[child].get(); } d_binarizeCache[current] = builder.constructNode(); } @@ -186,6 +185,7 @@ Node BVToInt::eliminationPass(Node n) (d_rebuildCache.find(current) != d_rebuildCache.end()); if (!inEliminationCache) { + // current is not the elimination of any previously-visited node // current hasn't been eliminated yet. // eliminate operators from it Node currentEliminated = @@ -221,7 +221,7 @@ Node BVToInt::eliminationPass(Node n) if (inRebuildCache) { // current was already added to the rebuild cache. - if (d_rebuildCache[current].isNull()) + if (d_rebuildCache[current].get().isNull()) { // current wasn't rebuilt yet. uint64_t numChildren = current.getNumChildren(); @@ -235,8 +235,7 @@ Node BVToInt::eliminationPass(Node n) // The main operator is replaced, and the children // are replaced with their eliminated counterparts. NodeBuilder<> builder(current.getKind()); - if (current.getKind() == kind::BITVECTOR_EXTRACT - || current.getKind() == kind::APPLY_UF) + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); } @@ -245,8 +244,8 @@ Node BVToInt::eliminationPass(Node n) Assert(d_eliminationCache.find(child) != d_eliminationCache.end()); Node eliminatedChild = d_eliminationCache[child]; Assert(d_rebuildCache.find(eliminatedChild) != d_eliminationCache.end()); - Assert(!d_rebuildCache[eliminatedChild].isNull()); - builder << d_rebuildCache[eliminatedChild]; + Assert(!d_rebuildCache[eliminatedChild].get().isNull()); + builder << d_rebuildCache[eliminatedChild].get(); } d_rebuildCache[current] = builder.constructNode(); } @@ -256,7 +255,7 @@ Node BVToInt::eliminationPass(Node n) Assert(d_eliminationCache.find(n) != d_eliminationCache.end()); Node eliminated = d_eliminationCache[n]; Assert(d_rebuildCache.find(eliminated) != d_rebuildCache.end()); - Assert(!d_rebuildCache[eliminated].isNull()); + Assert(!d_rebuildCache[eliminated].get().isNull()); return d_rebuildCache[eliminated]; } @@ -270,6 +269,7 @@ Node BVToInt::bvToInt(Node n) vector<Node> toVisit; toVisit.push_back(n); uint64_t granularity = options::BVAndIntegerGranularity(); + Assert(0 <= granularity && granularity <= 8); while (!toVisit.empty()) { @@ -284,7 +284,7 @@ Node BVToInt::bvToInt(Node n) else { // We already visited this node - if (!d_bvToIntCache[current].isNull()) + if (!d_bvToIntCache[current].get().isNull()) { // We are done computing the translation for current toVisit.pop_back(); @@ -643,7 +643,7 @@ Node BVToInt::bvToInt(Node n) Assert(d_bvToIntCache.find(a) != d_bvToIntCache.end()); Assert(i >= j); Node div = d_nm->mkNode( - kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a], pow2(j)); + kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a].get(), pow2(j)); d_bvToIntCache[current] = modpow2(div, i - j + 1); break; } @@ -814,7 +814,7 @@ bool BVToInt::childrenTypesChanged(Node n) { bool result = false; for (Node child : n) { TypeNode originalType = child.getType(); - TypeNode newType = d_bvToIntCache[child].getType(); + TypeNode newType = d_bvToIntCache[child].get().getType(); if (! newType.isSubtypeOf(originalType)) { result = true; break; @@ -825,10 +825,11 @@ bool BVToInt::childrenTypesChanged(Node n) { BVToInt::BVToInt(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-to-int"), - d_binarizeCache(), - d_eliminationCache(), - d_bvToIntCache(), - d_rangeAssertions() + d_binarizeCache(preprocContext->getUserContext()), + d_eliminationCache(preprocContext->getUserContext()), + d_rebuildCache(preprocContext->getUserContext()), + d_bvToIntCache(preprocContext->getUserContext()), + d_rangeAssertions(preprocContext->getUserContext()) { d_nm = NodeManager::currentNM(); d_zero = d_nm->mkConst<Rational>(0); @@ -838,7 +839,6 @@ BVToInt::BVToInt(PreprocessingPassContext* preprocContext) PreprocessingPassResult BVToInt::applyInternal( AssertionPipeline* assertionsToPreprocess) { - AlwaysAssert(!options::incrementalSolving()); for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i) { Node bvNode = (*assertionsToPreprocess)[i]; @@ -857,7 +857,11 @@ void BVToInt::addFinalizeRangeAssertions( AssertionPipeline* assertionsToPreprocess) { vector<Node> vec_range; - vec_range.assign(d_rangeAssertions.begin(), d_rangeAssertions.end()); + vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end()); + if (vec_range.size() == 0) + { + return; + } if (vec_range.size() == 1) { assertionsToPreprocess->push_back(vec_range[0]); |