[proof-new] Adding support for corner case of transitivity simulating MERGED_THROUGH_CONSTANTS (#4879)

2 files changed, 136 insertions, 16 deletions

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 15979bd44..513cf2f39 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -535,6 +535,88 @@ bool EqProof::expandTransitivityForDisequalities(
   return true;
 }
 
+// TEMPORARY NOTE: This may not be enough. Worst case scenario I need to
+// reproduce here a search for arbitrary chains between each of the variables in
+// the conclusion and a constant
+bool EqProof::expandTransitivityForTheoryDisequalities(
+    Node conclusion, std::vector<Node>& premises, CDProof* p) const
+{
+  // whether conclusion is a disequality (= (= t1 t2) false), modulo symmetry
+  unsigned termPos = -1;
+  for (unsigned i = 0; i < 2; ++i)
+  {
+    if (conclusion[i].getKind() == kind::CONST_BOOLEAN
+        && !conclusion[i].getConst<bool>()
+        && conclusion[1 - i].getKind() == kind::EQUAL)
+    {
+      termPos = i - 1;
+      break;
+    }
+  }
+  // no disequality
+  if (termPos == static_cast<unsigned>(-1))
+  {
+    return false;
+  }
+  Trace("eqproof-conv")
+      << "EqProof::expandTransitivityForTheoryDisequalities: check if need "
+         "to expand transitivity step to conclude disequality "
+      << conclusion << " from premises " << premises << "\n";
+
+  // Check if the premises are (= t1 c1) and (= t2 c2), modulo symmetry
+  std::vector<Node> subChildren, constChildren;
+  for (unsigned i = 0; i < 2; ++i)
+  {
+    Node term = conclusion[termPos][i];
+    for (const Node& premise : premises)
+    {
+      for (unsigned j = 0; j < 2; ++j)
+      {
+        if (premise[j] == term && premise[1 - j].isConst())
+        {
+          subChildren.push_back(premise[j].eqNode(premise[1 - j]));
+          constChildren.push_back(premise[1 - j]);
+          break;
+        }
+      }
+    }
+  }
+  if (subChildren.size() < 2)
+  {
+    return false;
+  }
+  // Now build
+  //   (= t1 c1)    (= t2 c2)
+  //  ------------------------- CONG   ------------------- MACRO_SR_PRED_INTRO
+  //   (= (= t1 t2) (= c1 c2))         (= (= c1 c2) false)
+  //  --------------------------------------------------------------------- TR
+  //                   (= (= t1 t2) false)
+  Node constApp = NodeManager::currentNM()->mkNode(kind::EQUAL, constChildren);
+  Node constEquality = constApp.eqNode(conclusion[1 - termPos]);
+  Trace("eqproof-conv")
+      << "EqProof::expandTransitivityForTheoryDisequalities: adding "
+      << PfRule::MACRO_SR_PRED_INTRO << " step for " << constApp << " = "
+      << conclusion[1 - termPos] << "\n";
+  p->addStep(constEquality, PfRule::MACRO_SR_PRED_INTRO, {}, {constEquality});
+  // build congruence conclusion (= (= t1 t2) (t c1 c2))
+  Node congConclusion = conclusion[termPos].eqNode(constApp);
+  Trace("eqproof-conv")
+      << "EqProof::expandTransitivityForTheoryDisequalities: adding  "
+      << PfRule::CONG << " step for " << congConclusion << " from "
+      << subChildren << "\n";
+  p->addStep(congConclusion,
+             PfRule::CONG,
+             {subChildren},
+             {ProofRuleChecker::mkKindNode(kind::EQUAL)},
+             true);
+  Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
+                           "congruence derived "
+                        << congConclusion << "\n";
+  std::vector<Node> transitivityChildren{congConclusion, constEquality};
+  p->addStep(conclusion, PfRule::TRANS, {transitivityChildren}, {});
+  return true;
+}
+
 bool EqProof::buildTransitivityChain(Node conclusion,
                                      std::vector<Node>& premises) const
 {
@@ -1059,22 +1141,30 @@ Node EqProof::addToProof(
             conclusion, children, p, assumptions))
     {
       Assert(!children.empty());
-      Trace("eqproof-conv")
-          << "EqProof::addToProof: build chain for transitivity premises"
-          << children << " to conclude " << conclusion << "\n";
-      // Build ordered transitivity chain from children to derive the conclusion
-      buildTransitivityChain(conclusion, children);
-      Assert(children.size() > 1
-             || (!children.empty()
-                 && (children[0] == conclusion
-                     || children[0][1].eqNode(children[0][0]) == conclusion)));
-      // Only add transitivity step if there is more than one premise in the
-      // chain. Otherwise the premise will be the conclusion itself and it'll
-      // already have had a step added to it when the premises were recursively
-      // processed.
-      if (children.size() > 1)
+      // similarly, if a disequality is concluded because of theory reasoning,
+      // the step is coarse-grained and needs to be expanded, in which case the
+      // proof is finalized in the call
+      if (!expandTransitivityForTheoryDisequalities(conclusion, children, p))
       {
-        p->addStep(conclusion, PfRule::TRANS, children, {}, true);
+        Trace("eqproof-conv")
+            << "EqProof::addToProof: build chain for transitivity premises"
+            << children << " to conclude " << conclusion << "\n";
+        // Build ordered transitivity chain from children to derive the
+        // conclusion
+        buildTransitivityChain(conclusion, children);
+        Assert(
+            children.size() > 1
+            || (!children.empty()
+                && (children[0] == conclusion
+                    || children[0][1].eqNode(children[0][0]) == conclusion)));
+        // Only add transitivity step if there is more than one premise in the
+        // chain. Otherwise the premise will be the conclusion itself and it'll
+        // already have had a step added to it when the premises were
+        // recursively processed.
+        if (children.size() > 1)
+        {
+          p->addStep(conclusion, PfRule::TRANS, children, {}, true);
+        }
       }
     }
     Assert(p->hasStep(conclusion));
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h
index ac440dc84..492252baa 100644
--- a/src/theory/uf/eq_proof.h
+++ b/src/theory/uf/eq_proof.h
@@ -182,7 +182,7 @@ class EqProof
    * themselves).
    * @return True if the EqProof transitivity step is in either of the above
    * cases, symbolizing that the ProofNode justifying the conclusion has already
-   * beenproduced.
+   * been produced.
    */
   bool expandTransitivityForDisequalities(
       Node conclusion,
@@ -190,6 +190,36 @@ class EqProof
       CDProof* p,
       std::unordered_set<Node, NodeHashFunction>& assumptions) const;
 
+  /** Expand coarse-grained transitivity steps for theory disequalities
+   *
+   * Currently the equality engine can represent disequality reasoning of theory
+   * symbols in a rather coarse-grained manner with EqProof. This is the case
+   * when EqProof is
+   *            (= t1 c1) (= t2 c2)
+   *  ------------------------------------- EQP::TR
+   *             (= (t1 t2) false)
+   *
+   * which is converted into
+   *
+   *   (= t1 c1)        (= t2 c2)
+   *  -------------------------- CONG  --------------------- MACRO_SR_PRED_INTRO
+   *   (= (= t1 t2) (= c1 t2))           (= (= c1 c2) false)
+   *  --------------------------------------------------------- TR
+   *           (= (= t1 t2) false)
+   *
+   * @param conclusion the conclusion of the (possibly) coarse-grained
+   * transitivity step
+   * @param premises the premises of the (possibly) coarse-grained
+   * transitivity step
+   * @param p a pointer to a CDProof to store the conversion of this EqProof
+   * @return True if the EqProof transitivity step is the above case,
+   * indicating that the ProofNode justifying the conclusion has already been
+   * produced.
+   */
+  bool expandTransitivityForTheoryDisequalities(Node conclusion,
+                                                std::vector<Node>& premises,
+                                                CDProof* p) const;
+
   /** Builds a transitivity chain from equalities to derive a conclusion
    *
    * Given an equality (= t1 tn), and a list of equalities premises, attempts to