diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-12 16:24:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-12 16:24:13 -0600 |
| commit | f38cd31ddfd3d5caa2ffe3a0ffafbb2b0394391b (patch) | |
| tree | 33a0fba8f24e64348edf138dc691f8498746d1e0 | |
| parent | 982282eed2b02c1ca4aec2a335e460e622c4e963 (diff) | |
Ensure ext rewrites for associative ops dont throw assertions for kind arities (#3681)
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 10 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress1/bv/issue3654.smt2 | 24 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3649.sy (renamed from test/regress/regress1/sygus/issue3654.sy) | 0 |
4 files changed, 36 insertions, 1 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 05e789ce2..9e924f34d 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -155,6 +155,16 @@ Node ExtendedRewriter::extendedRewrite(Node n) // we may have subsumed children down to one ret = children[0]; } + else if (isAssoc && children.size() > kind::metakind::getUpperBoundForKind(k)) + { + Assert(kind::metakind::getUpperBoundForKind(k) >= 2); + // kind may require binary construction + ret = children[0]; + for (unsigned i = 1, nchild = children.size(); i < nchild; i++) + { + ret = nm->mkNode(k, ret, children[i]); + } + } else { ret = nm->mkNode(k, children); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index aaabd2301..150983187 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1191,6 +1191,7 @@ set(regress_1_tests regress1/bv/divtest.smt2 regress1/bv/fuzz34.smtv1.smt2 regress1/bv/fuzz38.smtv1.smt2 + regress1/bv/issue3654.smt2 regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 regress1/bvdiv2.smt2 @@ -1819,7 +1820,7 @@ set(regress_1_tests regress1/sygus/issue3635.smt2 regress1/sygus/issue3644.smt2 regress1/sygus/issue3648.smt2 - regress1/sygus/issue3654.sy + regress1/sygus/issue3649.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/bv/issue3654.smt2 b/test/regress/regress1/bv/issue3654.smt2 new file mode 100644 index 000000000..59c11456f --- /dev/null +++ b/test/regress/regress1/bv/issue3654.smt2 @@ -0,0 +1,24 @@ +; COMMAND_LINE: --ext-rew-prep +; EXPECT: sat +(set-logic QF_BV) +(declare-fun a () (_ BitVec 4)) +(assert (let ((a!1 ((_ sign_extend 3) + (ite (bvult ((_ sign_extend 15) #b0) #x2b7e) #b1 #b0))) + (a!2 ((_ zero_extend 15) + (ite (distinct #x2b7e ((_ sign_extend 12) a)) #b1 #b0))) + (a!4 (bvsgt (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)) + ((_ zero_extend 12) a))) + (a!5 (bvugt (ite (bvult ((_ sign_extend 15) #b0) #x2b7e) #b1 #b0) #b0)) + (a!6 (bvugt (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)) + #x2b7e))) +(let ((a!3 (bvslt a!2 + (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)))) + (a!7 (xor (ite a!4 a!5 a!4) + a!6 + (= (bvxnor #x2b7e ((_ zero_extend 12) a)) + (bvadd #x2b7e ((_ sign_extend 12) a)))))) + (ite (bvule a!1 a) a!3 a!7)))) +(check-sat) diff --git a/test/regress/regress1/sygus/issue3654.sy b/test/regress/regress1/sygus/issue3649.sy index 12949c55a..12949c55a 100644 --- a/test/regress/regress1/sygus/issue3654.sy +++ b/test/regress/regress1/sygus/issue3649.sy |