From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 12 Feb 2020 22:24:13 +0000 (-0600)
Subject: Ensure ext rewrites for associative ops dont throw assertions for kind arities (... 
X-Git-Tag: cvc5-1.0.0~3653
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f38cd31ddfd3d5caa2ffe3a0ffafbb2b0394391b;p=cvc5.git

Ensure ext rewrites for associative ops dont throw assertions for kind arities (#3681)
---

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/issue3649.sy b/test/regress/regress1/sygus/issue3649.sy
new file mode 100644
index 000000000..12949c55a
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3649.sy
@@ -0,0 +1,24 @@
+; EXPECT: unknown
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool)
+
+(define-fun init-fn ((i Int) (x (Array Int Int)) (c Int)) Bool 
+	(and (= i 0)
+	(= (select x 10) c)))
+
+(define-fun post-fn ((i Int) (x (Array Int Int))(c Int)) Bool 
+	(exists ((index Int)) (and (= (select x index) c)
+	(forall ((index2 Int)) (=> (< index2 index) (not (= (select x index) c))))
+	)))
+
+(declare-var x (Array Int Int))
+(declare-var x! (Array Int Int))
+(declare-var i Int)
+(declare-var i! Int)
+(declare-var c Int)
+
+	
+(constraint (=> (init-fn i x c) (inv-fn i x c)))
+(constraint (=> (inv-fn i x c) (post-fn i x c)))
+(check-synth)
diff --git a/test/regress/regress1/sygus/issue3654.sy b/test/regress/regress1/sygus/issue3654.sy
deleted file mode 100644
index 12949c55a..000000000
--- a/test/regress/regress1/sygus/issue3654.sy
+++ /dev/null
@@ -1,24 +0,0 @@
-; EXPECT: unknown
-; COMMAND-LINE: --sygus-out=status
-(set-logic ALL)
-(synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool)
-
-(define-fun init-fn ((i Int) (x (Array Int Int)) (c Int)) Bool 
-	(and (= i 0)
-	(= (select x 10) c)))
-
-(define-fun post-fn ((i Int) (x (Array Int Int))(c Int)) Bool 
-	(exists ((index Int)) (and (= (select x index) c)
-	(forall ((index2 Int)) (=> (< index2 index) (not (= (select x index) c))))
-	)))
-
-(declare-var x (Array Int Int))
-(declare-var x! (Array Int Int))
-(declare-var i Int)
-(declare-var i! Int)
-(declare-var c Int)
-
-	
-(constraint (=> (init-fn i x c) (inv-fn i x c)))
-(constraint (=> (inv-fn i x c) (post-fn i x c)))
-(check-synth)