Core improvements to extended rewriter (#1820)

4 files changed, 70 insertions, 14 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index dd21822ed..c52d22cdb 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -42,6 +42,20 @@ void ExtendedRewriter::setCache(Node n, Node ret)
   n.setAttribute(era, ret);
 }
 
+bool ExtendedRewriter::addToChildren(Node nc,
+                                     std::vector<Node>& children,
+                                     bool dropDup)
+{
+  // If the operator is non-additive, do not consider duplicates
+  if (dropDup
+      && std::find(children.begin(), children.end(), nc) != children.end())
+  {
+    return false;
+  }
+  children.push_back(nc);
+  return true;
+}
+
 Node ExtendedRewriter::extendedRewrite(Node n)
 {
   n = Rewriter::rewrite(n);
@@ -97,19 +111,24 @@ Node ExtendedRewriter::extendedRewrite(Node n)
     Kind k = n.getKind();
     bool childChanged = false;
     bool isNonAdditive = TermUtil::isNonAdditive(k);
+    bool isAssoc = TermUtil::isAssoc(k);
     for (unsigned i = 0; i < n.getNumChildren(); i++)
     {
       Node nc = extendedRewrite(n[i]);
       childChanged = nc != n[i] || childChanged;
-      // If the operator is non-additive, do not consider duplicates
-      if (isNonAdditive
-          && std::find(children.begin(), children.end(), nc) != children.end())
+      if (isAssoc && nc.getKind() == n.getKind())
       {
-        childChanged = true;
+        for (const Node& ncc : nc)
+        {
+          if (!addToChildren(ncc, children, isNonAdditive))
+          {
+            childChanged = true;
+          }
+        }
       }
-      else
+      else if (!addToChildren(nc, children, isNonAdditive))
       {
-        children.push_back(nc);
+        childChanged = true;
       }
     }
     Assert(!children.empty());
@@ -923,16 +942,16 @@ Node ExtendedRewriter::extendedRewriteEqChain(
   }
 
   // sorted right associative chain
-  bool has_const = false;
-  unsigned const_index = 0;
+  bool has_nvar = false;
+  unsigned nvar_index = 0;
   for (std::pair<const Node, bool>& cp : cstatus)
   {
     if (cp.second)
     {
-      if (cp.first.isConst())
+      if (!cp.first.isVar())
       {
-        has_const = true;
-        const_index = children.size();
+        has_nvar = true;
+        nvar_index = children.size();
       }
       children.push_back(cp.first);
     }
@@ -943,7 +962,7 @@ Node ExtendedRewriter::extendedRewriteEqChain(
   if (!gpol)
   {
     // negate the constant child if it exists
-    unsigned nindex = has_const ? const_index : 0;
+    unsigned nindex = has_nvar ? nvar_index : 0;
     children[nindex] = TermUtil::mkNegate(notk, children[nindex]);
   }
   new_ret = children.back();
@@ -1051,12 +1070,32 @@ bool ExtendedRewriter::inferSubstitution(Node n,
     {
       n = slv_eq;
     }
+    NodeManager* nm = NodeManager::currentNM();
+
+    Node v[2];
     for (unsigned i = 0; i < 2; i++)
     {
-      TNode r1 = n[i];
-      TNode r2 = n[1 - i];
+      if (n[i].isVar() || n[i].isConst())
+      {
+        v[i] = n[i];
+      }
+      else if (TermUtil::isNegate(n[i].getKind()) && n[i][0].isVar())
+      {
+        v[i] = n[i][0];
+      }
+    }
+    for (unsigned i = 0; i < 2; i++)
+    {
+      TNode r1 = v[i];
+      Node r2 = v[1 - i];
       if (r1.isVar() && ((r2.isVar() && r1 < r2) || r2.isConst()))
       {
+        r2 = n[1 - i];
+        if (v[i] != n[i])
+        {
+          Assert( TermUtil::isNegate( n[i].getKind() ) );
+          r2 = TermUtil::mkNegate(n[i].getKind(), r2);
+        }
         // TODO (#1706) : union find
         if (std::find(vars.begin(), vars.end(), r1) == vars.end())
         {
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index bfae55730..937f522b2 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -66,6 +66,13 @@ class ExtendedRewriter
   bool d_aggr;
   /** cache that the extended rewritten form of n is ret */
   void setCache(Node n, Node ret);
+  /** add to children
+   *
+   * Adds nc to the vector of children, if dropDup is true, we do not add
+   * nc if it already occurs in children. This method returns false in this
+   * case, otherwise it returns true.
+   */
+  bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup);
 
   //--------------------------------------generic utilities
   /** Rewrite ITE, for example:
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index a80737fe2..9b04ce9b5 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -811,6 +811,11 @@ Node TermUtil::mkNegate(Kind notk, Node n)
   return NodeManager::currentNM()->mkNode(notk, n);
 }
 
+bool TermUtil::isNegate(Kind k)
+{
+  return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS;
+}
+
 bool TermUtil::isAssoc( Kind k ) {
   return k == PLUS || k == MULT || k == AND || k == OR || k == BITVECTOR_PLUS
          || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index df88c1b30..70f8bbcee 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -291,6 +291,11 @@ public:
   static int getTermDepth( Node n );
   /** simple negate */
   static Node simpleNegate( Node n );
+  /** is the kind k a negation kind?
+   *
+   * A kind k is a negation kind if <k>( <k>( n ) ) = n.
+   */
+  static bool isNegate(Kind k);
   /**
    * Make negated term, returns the negation of n wrt Kind notk, eliminating
    * double negation if applicable, e.g. mkNegate( ~, ~x ) ---> x.