From: yoni206 Date: Fri, 28 Aug 2020 21:42:51 +0000 (-0700) Subject: Incremental support for bv_to_int (#4967) X-Git-Tag: cvc5-1.0.0~2940 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=48dfcfd271ff9fa04766e29fb82ba83290da1ad8;p=cvc5.git 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. --- 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/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 new file mode 100644 index 000000000..c621aa112 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) +(declare-fun a () (_ BitVec 4)) +(declare-fun b () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4) ) +(assert (distinct (bvadd a b) (f a))) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 new file mode 100644 index 000000000..6196b2bb9 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 @@ -0,0 +1,81 @@ +;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores +;EXPECT: unsat + +(set-logic QF_UFBV) +(declare-fun z$n0s32 () (_ BitVec 32)) +(declare-fun dataOut () (_ BitVec 32)) +(declare-fun z$2 () (_ BitVec 1)) +(declare-fun stageOne () (_ BitVec 32)) +(declare-fun z$4 () (_ BitVec 1)) +(declare-fun stageTwo () (_ BitVec 32)) +(declare-fun z$6 () (_ BitVec 1)) +(declare-fun tmp_stageOne () (_ BitVec 32)) +(declare-fun z$8 () (_ BitVec 1)) +(declare-fun tmp_stageTwo () (_ BitVec 32)) +(declare-fun z$10 () (_ BitVec 1)) +(declare-fun reset_ () (_ BitVec 1)) +(declare-fun z$14 () (_ BitVec 1)) +(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32)) +(declare-fun z$15 () (_ BitVec 32)) +(declare-fun z$17 () (_ BitVec 32)) +(declare-fun dataOut$next () (_ BitVec 32)) +(declare-fun z$19 () (_ BitVec 1)) +(declare-fun c1 () (_ BitVec 32)) +(declare-fun dataIn () (_ BitVec 32)) +(declare-fun z$23 () (_ BitVec 32)) +(declare-fun stageOne$next () (_ BitVec 32)) +(declare-fun z$25 () (_ BitVec 1)) +(declare-fun c2 () (_ BitVec 32)) +(declare-fun z$28 () (_ BitVec 32)) +(declare-fun stageTwo$next () (_ BitVec 32)) +(declare-fun z$30 () (_ BitVec 1)) +(declare-fun tmp_stageOne$next () (_ BitVec 32)) +(declare-fun z$32 () (_ BitVec 1)) +(declare-fun tmp_stageTwo$next () (_ BitVec 32)) +(declare-fun z$34 () (_ BitVec 1)) +(declare-fun z$35 () (_ BitVec 1)) +(declare-fun z$55 () (_ BitVec 32)) +(declare-fun z$57 () (_ BitVec 1)) +(declare-fun z$58 () (_ BitVec 1)) +(declare-fun z$59 () (_ BitVec 1)) +(declare-fun prop$next () (_ BitVec 1)) +(declare-fun z$61 () (_ BitVec 1)) +(declare-fun z$54 () (_ BitVec 1)) +(declare-fun z$63 () (_ BitVec 1)) +(assert + (= z$15 (Add_32_32_32 stageTwo stageOne))) +(assert + (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32))) +(assert + (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1)))) + + +(assert + (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1)))) +(assert + (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1))))) + (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1))))) +(assert + (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next))) +(assert + (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1)))) +(assert + (let (($x52 (= z$2 (_ bv1 1)))) + (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1))))) + (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1)))))) +(assert + (= z$63 (_ bv1 1))) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 new file mode 100644 index 000000000..8fbe96eab --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) +(declare-sort S 0) +(declare-fun s () S) +(declare-fun a () (_ BitVec 4)) +(declare-fun b () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4) ) +(declare-fun g (S) (_ BitVec 4)) +(declare-fun h ((_ BitVec 4)) S) +(assert (distinct (bvadd a b) (f a))) +(assert (distinct (f a) (g s))) +(assert (distinct (h a) s)) +(check-sat) diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bvuf_to_intuf.smt2 deleted file mode 100644 index c621aa112..000000000 --- a/test/regress/regress0/bv/bvuf_to_intuf.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; EXPECT: sat -(set-logic QF_UFBV) -(declare-fun a () (_ BitVec 4)) -(declare-fun b () (_ BitVec 4)) -(declare-fun f ((_ BitVec 4)) (_ BitVec 4) ) -(assert (distinct (bvadd a b) (f a))) -(check-sat) diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 deleted file mode 100644 index 6196b2bb9..000000000 --- a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 +++ /dev/null @@ -1,81 +0,0 @@ -;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores -;EXPECT: unsat - -(set-logic QF_UFBV) -(declare-fun z$n0s32 () (_ BitVec 32)) -(declare-fun dataOut () (_ BitVec 32)) -(declare-fun z$2 () (_ BitVec 1)) -(declare-fun stageOne () (_ BitVec 32)) -(declare-fun z$4 () (_ BitVec 1)) -(declare-fun stageTwo () (_ BitVec 32)) -(declare-fun z$6 () (_ BitVec 1)) -(declare-fun tmp_stageOne () (_ BitVec 32)) -(declare-fun z$8 () (_ BitVec 1)) -(declare-fun tmp_stageTwo () (_ BitVec 32)) -(declare-fun z$10 () (_ BitVec 1)) -(declare-fun reset_ () (_ BitVec 1)) -(declare-fun z$14 () (_ BitVec 1)) -(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32)) -(declare-fun z$15 () (_ BitVec 32)) -(declare-fun z$17 () (_ BitVec 32)) -(declare-fun dataOut$next () (_ BitVec 32)) -(declare-fun z$19 () (_ BitVec 1)) -(declare-fun c1 () (_ BitVec 32)) -(declare-fun dataIn () (_ BitVec 32)) -(declare-fun z$23 () (_ BitVec 32)) -(declare-fun stageOne$next () (_ BitVec 32)) -(declare-fun z$25 () (_ BitVec 1)) -(declare-fun c2 () (_ BitVec 32)) -(declare-fun z$28 () (_ BitVec 32)) -(declare-fun stageTwo$next () (_ BitVec 32)) -(declare-fun z$30 () (_ BitVec 1)) -(declare-fun tmp_stageOne$next () (_ BitVec 32)) -(declare-fun z$32 () (_ BitVec 1)) -(declare-fun tmp_stageTwo$next () (_ BitVec 32)) -(declare-fun z$34 () (_ BitVec 1)) -(declare-fun z$35 () (_ BitVec 1)) -(declare-fun z$55 () (_ BitVec 32)) -(declare-fun z$57 () (_ BitVec 1)) -(declare-fun z$58 () (_ BitVec 1)) -(declare-fun z$59 () (_ BitVec 1)) -(declare-fun prop$next () (_ BitVec 1)) -(declare-fun z$61 () (_ BitVec 1)) -(declare-fun z$54 () (_ BitVec 1)) -(declare-fun z$63 () (_ BitVec 1)) -(assert - (= z$15 (Add_32_32_32 stageTwo stageOne))) -(assert - (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32))) -(assert - (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1)))) -(assert - (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1)))) - - -(assert - (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1)))) -(assert - (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1)))) -(assert - (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1))))) - (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1))))) -(assert - (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next))) -(assert - (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1)))) -(assert - (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1)))) -(assert - (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1)))) -(assert - (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1)))) -(assert - (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1)))) -(assert - (let (($x52 (= z$2 (_ bv1 1)))) - (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1))))) - (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1)))))) -(assert - (= z$63 (_ bv1 1))) -(check-sat) -(exit) diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 deleted file mode 100644 index 8fbe96eab..000000000 --- a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 +++ /dev/null @@ -1,14 +0,0 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; EXPECT: sat -(set-logic QF_UFBV) -(declare-sort S 0) -(declare-fun s () S) -(declare-fun a () (_ BitVec 4)) -(declare-fun b () (_ BitVec 4)) -(declare-fun f ((_ BitVec 4)) (_ BitVec 4) ) -(declare-fun g (S) (_ BitVec 4)) -(declare-fun h ((_ BitVec 4)) S) -(assert (distinct (bvadd a b) (f a))) -(assert (distinct (f a) (g s))) -(assert (distinct (h a) s)) -(check-sat) 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)