From: yoni206 Date: Wed, 14 Oct 2020 06:28:36 +0000 (-0700) Subject: bv2int: rewritings and unsat cores (#5263) X-Git-Tag: cvc5-1.0.0~2713 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1cecdb3b4d8be47d446be5d33cc4d3063061d2b3;p=cvc5.git bv2int: rewritings and unsat cores (#5263) This commit fixes several issues with bv-to-int preprocessing pass, mostly raised by @ajreynol: 1. make sure to rewrite the processed node before and after processing it 2. use the new `mkAnd` function 3. remove `--no-check-unsat-cores` from tests whenever possible 4. add new tests from #5230 . These tests now pass, and so this PR closes #5230 if merged. This also makes #5253 redundant. 5. remove an unused test --- diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 6f6ff3bae..8906ddeea 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -260,6 +260,8 @@ Node BVToInt::eliminationPass(Node n) */ Node BVToInt::bvToInt(Node n) { + // make sure the node is re-written before processing it. + n = Rewriter::rewrite(n); n = makeBinary(n); n = eliminationPass(n); // binarize again, in case the elimination pass introduced @@ -947,26 +949,17 @@ PreprocessingPassResult BVToInt::applyInternal( void BVToInt::addFinalizeRangeAssertions( AssertionPipeline* assertionsToPreprocess) { + // collect the range assertions from d_rangeAssertions + // (which is a context-dependent set) + // into a vector. vector vec_range; 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]); - Trace("bv-to-int-debug") - << "range constraints: " << vec_range[0].toString() << std::endl; - } - else if (vec_range.size() >= 2) - { - Node rangeAssertions = - Rewriter::rewrite(d_nm->mkNode(kind::AND, vec_range)); - assertionsToPreprocess->push_back(rangeAssertions); - Trace("bv-to-int-debug") - << "range constraints: " << rangeAssertions.toString() << std::endl; - } + // conjoin all range assertions and add the conjunction + // as a new assertion + Node rangeAssertions = Rewriter::rewrite(d_nm->mkAnd(vec_range)); + assertionsToPreprocess->push_back(rangeAssertions); + Trace("bv-to-int-debug") << "range constraints: " + << rangeAssertions.toString() << std::endl; } Node BVToInt::createShiftNode(vector children, @@ -1046,24 +1039,12 @@ Node BVToInt::translateQuantifiedFormula(Node quantifiedNode) newBoundVars.begin(), newBoundVars.end()); // A node to represent all the range constraints. - Node ranges; - if (rangeConstraints.size() > 0) - { - if (rangeConstraints.size() == 1) - { - ranges = rangeConstraints[0]; - } - else - { - ranges = d_nm->mkNode(kind::AND, rangeConstraints); - } - // Add the range constraints to the body of the quantifier. - // For "exists", this is added conjunctively - // For "forall", this is added to the left side of an implication. - matrix = d_nm->mkNode( - k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix); - } - + Node ranges = d_nm->mkAnd(rangeConstraints); + // Add the range constraints to the body of the quantifier. + // For "exists", this is added conjunctively + // For "forall", this is added to the left side of an implication. + matrix = d_nm->mkNode( + k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix); // create the new quantified formula and return it. Node newBoundVarsList = d_nm->mkNode(kind::BOUND_VAR_LIST, newBoundVars); Node result = d_nm->mkNode(kind::FORALL, newBoundVarsList, matrix); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f239492af..aedc27924 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -221,6 +221,9 @@ set(regress_0_tests regress0/bv/bv-to-bool1.smtv1.smt2 regress0/bv/bv-to-bool2.smt2 regress0/bv/bv_to_int1.smt2 + regress0/bv/bv_to_int_5230_shift_const.smt2 + regress0/bv/bv_to_int_5230_binary.smt2 + regress0/bv/bv_to_int_5230_missing_op.smt2 regress0/bv/bv_to_int_bvmul2.smt2 regress0/bv/bv_to_int_bvuf_to_intuf.smt2 regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index 9111ac25c..8410d04b9 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 new file mode 100644 index 000000000..32680d862 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 @@ -0,0 +1,9 @@ +; REQUIRES: proof +; EXPECT: sat +(set-logic QF_UFBV) +(set-option :produce-unsat-cores true) +(set-option :solve-bv-as-int sum) +(declare-const v8 Bool) +(declare-const bv_14-0 (_ BitVec 14)) +(declare-const v12 Bool) +(check-sat-assuming ((! (or (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7)))) (= bv_14-0 bv_14-0 bv_14-0) (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7)))) v12) :named IP_71) (! (or v12 v8 v8 (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))))) :named IP_75))) diff --git a/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 new file mode 100644 index 000000000..757b00e5f --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: proof +; EXPECT: sat +(set-logic ABV) +(set-option :check-unsat-cores true) +(set-option :solve-bv-as-int sum) +(assert (! (exists ((q4 (_ BitVec 6))) true) :named IP_2)) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 new file mode 100644 index 000000000..e94e0cae5 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 @@ -0,0 +1,12 @@ +; REQUIRES: proof +; EXPECT: sat +(set-logic QF_UFBV) +(set-option :check-unsat-cores true) +(set-option :solve-bv-as-int sum) +(declare-const v0 Bool) +(declare-const v5 Bool) +(declare-const v8 Bool) +(declare-const v9 Bool) +(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110))) +(assert (or v0 v8)) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2 index 42e06a940..8bf4a825d 100644 --- a/test/regress/regress0/bv/bv_to_int_zext.smt2 +++ b/test/regress/regress0/bv/bv_to_int_zext.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; EXPECT: unsat (set-logic QF_BV) (declare-fun T1_31078 () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2 index 5516f974b..b95dc6b7f 100644 --- a/test/regress/regress2/bv_to_int_ashr.smt2 +++ b/test/regress/regress2/bv_to_int_ashr.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2 index 37582d9d8..74e5ca95a 100644 --- a/test/regress/regress2/bv_to_int_mask_array_3.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; EXPECT: sat (set-logic ALL) (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4))) diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2 index 7971b2bfe..bcc31c38c 100644 --- a/test/regress/regress2/bv_to_int_shifts.smt2 +++ b/test/regress/regress2/bv_to_int_shifts.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress3/bv_to_int_signed_sub_or.smt2 b/test/regress/regress3/bv_to_int_signed_sub_or.smt2 deleted file mode 100644 index 50cce4511..000000000 --- a/test/regress/regress3/bv_to_int_signed_sub_or.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores -; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-unsat-cores -; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores -; COMMAND-LINE: --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-unsat-cores -; EXPECT: unsat -(set-logic QF_BV) -(declare-fun s () (_ BitVec 4)) -(declare-fun t () (_ BitVec 4)) -(assert (bvsgt s t)) -(assert (bvsge t (bvsub t (bvor (bvor s t) (bvneg s))))) -(check-sat) -(exit)