From 8cc4bc292c6ac60edfa356355ad235e51ad15310 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 25 Apr 2018 16:00:11 -0500
Subject: [PATCH] Equality resolution in the extended rewriter (#1811)

---
 src/theory/quantifiers/extended_rewrite.cpp | 87 +++++++++++++++++++++
 src/theory/quantifiers/extended_rewrite.h   | 20 +++++
 2 files changed, 107 insertions(+)

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 756413b54..dd21822ed 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -152,6 +152,13 @@ Node ExtendedRewriter::extendedRewrite(Node n)
     std::map<Kind, bool> bcp_kinds;
     new_ret = extendedRewriteBcp(AND, OR, NOT, bcp_kinds, ret);
     debugExtendedRewrite(ret, new_ret, "Bool bcp");
+    if (new_ret.isNull())
+    {
+      // equality resolution
+      new_ret =
+          extendedRewriteEqRes(AND, OR, EQUAL, NOT, bcp_kinds, ret, false);
+      debugExtendedRewrite(ret, new_ret, "Bool eq res");
+    }
   }
   else if (ret.getKind() == EQUAL)
   {
@@ -718,6 +725,86 @@ Node ExtendedRewriter::extendedRewriteBcp(
   return Node::null();
 }
 
+Node ExtendedRewriter::extendedRewriteEqRes(Kind andk,
+                                            Kind ork,
+                                            Kind eqk,
+                                            Kind notk,
+                                            std::map<Kind, bool>& bcp_kinds,
+                                            Node n,
+                                            bool isXor)
+{
+  Assert(n.getKind() == andk || n.getKind() == ork);
+  Trace("ext-rew-eqres") << "Eq res: **** INPUT: " << n << std::endl;
+
+  NodeManager* nm = NodeManager::currentNM();
+  Kind nk = n.getKind();
+  bool gpol = (nk == andk);
+  for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+  {
+    Node lit = n[i];
+    if (lit.getKind() == eqk)
+    {
+      // eq is the equality we are basing a substitution on
+      Node eq;
+      if (gpol == isXor)
+      {
+        // can only turn disequality into equality if types are the same
+        if (lit[1].getType() == lit.getType())
+        {
+          // t != s ---> ~t = s
+          Assert(lit[1].getKind() != notk);
+          eq = nm->mkNode(EQUAL, TermUtil::mkNegate(notk, lit[0]), lit[1]);
+        }
+      }
+      else
+      {
+        eq = eqk == EQUAL ? lit : nm->mkNode(EQUAL, lit[0], lit[1]);
+      }
+      if (!eq.isNull())
+      {
+        // see if it corresponds to a substitution
+        std::vector<Node> vars;
+        std::vector<Node> subs;
+        if (inferSubstitution(eq, vars, subs))
+        {
+          Assert(vars.size() == 1);
+          std::vector<Node> children;
+          bool childrenChanged = false;
+          // apply to all other children
+          for (unsigned j = 0; j < nchild; j++)
+          {
+            Node ccs = n[j];
+            if (i != j)
+            {
+              if (bcp_kinds.empty())
+              {
+                ccs = ccs.substitute(
+                    vars.begin(), vars.end(), subs.begin(), subs.end());
+              }
+              else
+              {
+                std::map<Node, Node> assign;
+                // vars.size()==subs.size()==1
+                assign[vars[0]] = subs[0];
+                // substitution is only applicable to compatible kinds
+                ccs = partialSubstitute(ccs, assign, bcp_kinds);
+              }
+              childrenChanged = childrenChanged || n[j] != ccs;
+            }
+            children.push_back(ccs);
+          }
+          if (childrenChanged)
+          {
+            return nm->mkNode(nk, children);
+          }
+        }
+      }
+    }
+  }
+
+  return Node::null();
+}
+
 Node ExtendedRewriter::extendedRewriteEqChain(
     Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor)
 {
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 2daa42b18..bfae55730 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -120,6 +120,26 @@ class ExtendedRewriter
    */
   Node extendedRewriteBcp(
       Kind andk, Kind ork, Kind notk, std::map<Kind, bool>& bcp_kinds, Node n);
+  /** (type-independent) equality resolution, for example:
+   *
+   *   ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B )
+   *   ( A V ~B ) & ( A = B ) ----> ( A = B )
+   *   ( A V B ) & ( A xor B ) ----> ( A xor B )
+   *   ( A & B ) V ( A xor B ) ----> B V ( A xor B )
+   *
+   * This function takes as arguments the kinds that specify AND, OR, EQUAL,
+   * and NOT. The equal kind eqk is interpreted as XOR if isXor is true.
+   * It additionally takes as argument a map bcp_kinds, which
+   * serves the same purpose as the above function.
+   * If this function returns a non-null node ret, then n ---> ret.
+   */
+  Node extendedRewriteEqRes(Kind andk,
+                            Kind ork,
+                            Kind eqk,
+                            Kind notk,
+                            std::map<Kind, bool>& bcp_kinds,
+                            Node n,
+                            bool isXor = false);
   /** (type-independent) Equality chain rewriting, for example:
    *
    *   A = ( A = B ) ---> B
-- 
2.30.2