From 075e3d97974c89dcbd4cf6c7a1c3b37cbb27403d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Dec 2018 20:17:50 -0600
Subject: [PATCH]  Fix extended rewriter for binary associative operators.
 (#2751)

This was causing assertion failures when using Sets + Sygus.
---
 src/theory/quantifiers/extended_rewrite.cpp |  3 ++-
 src/theory/quantifiers/term_util.cpp        | 20 ++++++++++++++++++--
 src/theory/quantifiers/term_util.h          | 16 ++++++++++++----
 src/theory/sets/theory_sets_rewriter.cpp    |  3 ++-
 test/regress/CMakeLists.txt                 |  1 +
 test/regress/regress0/sets/sets-extr.smt2   | 15 +++++++++++++++
 6 files changed, 50 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/regress0/sets/sets-extr.smt2

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index b583a55da..ae053930c 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -119,7 +119,8 @@ Node ExtendedRewriter::extendedRewrite(Node n)
     Kind k = n.getKind();
     bool childChanged = false;
     bool isNonAdditive = TermUtil::isNonAdditive(k);
-    bool isAssoc = TermUtil::isAssoc(k);
+    // We flatten associative operators below, which requires k to be n-ary.
+    bool isAssoc = TermUtil::isAssoc(k, true);
     for (unsigned i = 0; i < n.getNumChildren(); i++)
     {
       Node nc = extendedRewrite(n[i]);
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index f8e8ed5ad..4c9cf2c8d 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -654,7 +654,15 @@ bool TermUtil::isNegate(Kind k)
   return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS;
 }
 
-bool TermUtil::isAssoc( Kind k ) {
+bool TermUtil::isAssoc(Kind k, bool reqNAry)
+{
+  if (reqNAry)
+  {
+    if (k == UNION || k == INTERSECTION)
+    {
+      return false;
+    }
+  }
   return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR
          || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT
          || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
@@ -663,7 +671,15 @@ bool TermUtil::isAssoc( Kind k ) {
          || k == SEP_STAR;
 }
 
-bool TermUtil::isComm( Kind k ) {
+bool TermUtil::isComm(Kind k, bool reqNAry)
+{
+  if (reqNAry)
+  {
+    if (k == UNION || k == INTERSECTION)
+    {
+      return false;
+    }
+  }
   return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND
          || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT
          || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index dd3e76ee2..820821991 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -270,10 +270,18 @@ public:
    * double negation if applicable, e.g. mkNegate( ~, ~x ) ---> x.
    */
   static Node mkNegate(Kind notk, Node n);
-  /** is assoc */
-  static bool isAssoc( Kind k );
-  /** is k commutative? */
-  static bool isComm( Kind k );
+  /** is k associative?
+   *
+   * If flag reqNAry is true, then we additionally require that k is an
+   * n-ary operator.
+   */
+  static bool isAssoc(Kind k, bool reqNAry = false);
+  /** is k commutative?
+   *
+   * If flag reqNAry is true, then we additionally require that k is an
+   * n-ary operator.
+   */
+  static bool isComm(Kind k, bool reqNAry = false);
 
   /** is k non-additive?
    * Returns true if
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index a3f1f9893..2a2015319 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -47,7 +47,7 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
 RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   NodeManager* nm = NodeManager::currentNM();
   Kind kind = node.getKind();
-
+  Trace("sets-postrewrite") << "Process: " << node << std::endl;
 
   if(node.isConst()) {
     // Dare you touch the const and mangle it to something else.
@@ -204,6 +204,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       if( rew!=node ){
         Trace("sets-rewrite") << "Sets::rewrite " << node << " -> " << rew << std::endl;
       }
+      Trace("sets-rewrite") << "...no rewrite." << std::endl;
       return RewriteResponse(REWRITE_DONE, rew);
     }
     break;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9e942aae1..95e4b8875 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -776,6 +776,7 @@ set(regress_0_tests
   regress0/sets/pre-proc-univ.smt2
   regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
   regress0/sets/sets-equal.smt2
+  regress0/sets/sets-extr.smt2
   regress0/sets/sets-inter.smt2
   regress0/sets/sets-of-sets-subtypes.smt2
   regress0/sets/sets-poly-int-real.smt2
diff --git a/test/regress/regress0/sets/sets-extr.smt2 b/test/regress/regress0/sets/sets-extr.smt2
new file mode 100644
index 000000000..c497ff189
--- /dev/null
+++ b/test/regress/regress0/sets/sets-extr.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort Atom 0)
+
+(declare-fun a () Atom)
+(declare-fun b () Atom)
+(declare-fun c () Atom)
+(declare-fun S () (Set Atom))
+
+
+(assert (= S (union (singleton a) (union (singleton c) (singleton b)))))
+
+(check-sat)
+
-- 
2.30.2