Fix extended rewriter for binary associative operators. (#2751)

This was causing assertion failures when using Sets + Sygus.

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index b583a55dac56ed8573d7c684f32a4e064fdea447..ae053930c96f7427ccabbf13ddf843414842cc69 100644 (file)
--- 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 f8e8ed5ad0d6b100718b0347f088dbed06dd05a8..4c9cf2c8d3cff34a313f5f8e5e4cd7e4ee21a2b2 100644 (file)
--- 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 dd3e76ee23ddb41396c9a0579b5a299ab3fda66e..820821991140fb834d14960c6438446e8ef317ac 100644 (file)
--- 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 a3f1f989324950bdcc33c50b99eb4211f03d793f..2a20153198dd4611f38f382d83e1259273c8d8f0 100644 (file)
--- 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 9e942aae1f6685f60c83287bf728b8907aa2e4d3..95e4b887516b738fb330d5ebc8dfb09950237d3f 100644 (file)
--- 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 (file)
index 0000000..c497ff1
--- /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)
+