From 48dfcfd271ff9fa04766e29fb82ba83290da1ad8 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 28 Aug 2020 14:42:51 -0700 Subject: [PATCH] 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. --- src/preprocessing/passes/bv_to_int.cpp | 42 ++++++++++--------- src/preprocessing/passes/bv_to_int.h | 15 ++++--- src/smt/set_defaults.cpp | 9 +--- test/regress/CMakeLists.txt | 7 ++-- ...ntuf.smt2 => bv_to_int_bvuf_to_intuf.smt2} | 0 ...t2 => bv_to_int_bvuf_to_intuf_smtlib.smt2} | 0 ...mt2 => bv_to_int_bvuf_to_intuf_sorts.smt2} | 0 test/regress/regress2/bv_to_int_inc1.smt2 | 30 +++++++++++++ 8 files changed, 67 insertions(+), 36 deletions(-) rename test/regress/regress0/bv/{bvuf_to_intuf.smt2 => bv_to_int_bvuf_to_intuf.smt2} (100%) rename test/regress/regress0/bv/{bvuf_to_intuf_smtlib.smt2 => bv_to_int_bvuf_to_intuf_smtlib.smt2} (100%) rename test/regress/regress0/bv/{bvuf_to_intuf_sorts.smt2 => bv_to_int_bvuf_to_intuf_sorts.smt2} (100%) create mode 100644 test/regress/regress2/bv_to_int_inc1.smt2 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 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(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 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; +using CDNodeMap = context::CDHashMap; 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 d_rangeAssertions; + context::CDHashSet 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."); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7a1366b3a..0caeafb36 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -213,11 +213,11 @@ set(regress_0_tests regress0/bv/bv_to_int_bvmul1.smt2 regress0/bv/bv_to_int_bvmul2.smt2 regress0/bv/bv_to_int_bitwise.smt2 + regress0/bv/bv_to_int_bvuf_to_intuf.smt2 + regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 + regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 regress0/bv/bv_to_int_elim_err.smt2 regress0/bv/bv_to_int_zext.smt2 - regress0/bv/bvuf_to_intuf.smt2 - regress0/bv/bvuf_to_intuf_smtlib.smt2 - regress0/bv/bvuf_to_intuf_sorts.smt2 regress0/bv/bv2nat-ground-c.smt2 regress0/bv/bv2nat-simp-range.smt2 regress0/bv/bvmul-pow2-only.smt2 @@ -2075,6 +2075,7 @@ set(regress_2_tests regress2/bug812.smt2 regress2/bv/opStructure_MBA_6.scrambled.min.smt2 regress2/bv_to_int_ashr.smt2 + regress2/bv_to_int_inc1.smt2 regress2/bv_to_int_mask_array_1.smt2 regress2/bv_to_int_mask_array_2.smt2 regress2/bv_to_int_shifts.smt2 diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 similarity index 100% rename from test/regress/regress0/bv/bvuf_to_intuf.smt2 rename to test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 similarity index 100% rename from test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 rename to test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 similarity index 100% rename from test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 rename to test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2 new file mode 100644 index 000000000..0d09a7252 --- /dev/null +++ b/test/regress/regress2/bv_to_int_inc1.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --incremental --solve-bv-as-int=sum +; EXPECT sat +; EXPECT sat +; EXPECT unsat +; EXPECT sat +(set-logic QF_BV) +(set-option :incremental true) +(declare-fun a () (_ BitVec 3)) +(declare-fun b () (_ BitVec 3)) +(declare-fun c () (_ BitVec 3)) + +(assert (bvult a (bvand b c))) +(check-sat) +; EXPECT: sat + +(push 1) +(assert (bvult c b)) +(check-sat) +; EXPECT: sat + + +(push 1) +(assert (bvugt c b)) +(check-sat) +; EXPECT: unsat +(pop 2) + +(check-sat) +; EXPECT: sat +(exit) -- 2.30.2