diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-08-28 14:42:51 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-28 16:42:51 -0500 |
commit | 48dfcfd271ff9fa04766e29fb82ba83290da1ad8 (patch) | |
tree | c187227cf376e9202c509a0fc05da500a427ac06 /src | |
parent | f51d3e353fe8e50e5e73c37c17229e603a56ecdd (diff) |
Incremental support for bv_to_int (#4967)
This PR adds support for incremental solving in bv_to_int.
This amounts to:
using context dependent data structures
adding a test
In addition, we check for parametrized operations in a more robust way (using kind::metakind::PARAMETERIZED) and rename some tests for convenience.
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 42 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_int.h | 15 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 9 |
3 files changed, 33 insertions, 33 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]); diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index 5015d1e8e..d8ee69879 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -62,6 +62,9 @@ #ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H #define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H +#include "context/cdhashmap.h" +#include "context/cdo.h" +#include "context/context.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -69,7 +72,7 @@ namespace CVC4 { namespace preprocessing { namespace passes { -using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>; +using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>; class BVToInt : public PreprocessingPass { @@ -245,10 +248,10 @@ class BVToInt : public PreprocessingPass /** * Caches for the different functions */ - NodeMap d_binarizeCache; - NodeMap d_eliminationCache; - NodeMap d_rebuildCache; - NodeMap d_bvToIntCache; + CDNodeMap d_binarizeCache; + CDNodeMap d_eliminationCache; + CDNodeMap d_rebuildCache; + CDNodeMap d_bvToIntCache; /** * Node manager that is used throughout the pass @@ -259,7 +262,7 @@ class BVToInt : public PreprocessingPass * A set of constraints of the form 0 <= x < 2^k * These are added for every new integer variable that we introduce. */ - unordered_set<Node, NodeHashFunction> d_rangeAssertions; + context::CDHashSet<Node, NodeHashFunction> d_rangeAssertions; /** * Useful constants diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 7d2427015..130f75894 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -151,14 +151,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { - // not compatible with incremental - if (options::incrementalSolving()) - { - throw OptionException( - "solving bitvectors as integers is currently not supported " - "when solving incrementally."); - } - else if (options::boolToBitvector() != options::BoolToBVMode::OFF) + if (options::boolToBitvector() != options::BoolToBVMode::OFF) { throw OptionException( "solving bitvectors as integers is incompatible with --bool-to-bv."); |