Disable automatic symmetry in proofs of theory explanations (#7493)

This avoids cyclic proofs in a rare case where theory explanations involve an equality and its symmetric form.

This PR disables auto-symmetry on lazy proofs used for theory explanations, which is slightly less convenient but avoids potentials for cyclic proofs. Note this complication would not arise if the theory engine did not allow non-rewritten equalities to be propagated between theories.

Fixes cvc5/cvc5-projects#311.

5 files changed, 65 insertions, 28 deletions

diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp
index eab452d49..f6c9d8eb2 100644
--- a/src/proof/lazy_proof.cpp
+++ b/src/proof/lazy_proof.cpp
@@ -26,8 +26,11 @@ namespace cvc5 {
 LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
                          ProofGenerator* dpg,
                          context::Context* c,
-                         const std::string& name)
-    : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg)
+                         const std::string& name,
+                         bool autoSym)
+    : CDProof(pnm, c, name, autoSym),
+      d_gens(c ? c : &d_context),
+      d_defaultGen(dpg)
 {
 }
 
diff --git a/src/proof/lazy_proof.h b/src/proof/lazy_proof.h
index bf5bc229c..e14dc8a1c 100644
--- a/src/proof/lazy_proof.h
+++ b/src/proof/lazy_proof.h
@@ -41,11 +41,15 @@ class LazyCDProof : public CDProof
    * for facts that have no explicitly provided generator.
    * @param c The context that this class depends on. If none is provided,
    * this class is context-independent.
+   * @param name The name of this proof generator (for debugging)
+   * @param autoSym Whether symmetry steps are automatically added when adding
+   * steps to this proof
    */
   LazyCDProof(ProofNodeManager* pnm,
               ProofGenerator* dpg = nullptr,
               context::Context* c = nullptr,
-              const std::string& name = "LazyCDProof");
+              const std::string& name = "LazyCDProof",
+              bool autoSym = true);
   ~LazyCDProof();
   /**
    * Get lazy proof for fact, or nullptr if it does not exist. This may
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ee1528f4d..a186c05a0 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1535,8 +1535,26 @@ TrustNode TheoryEngine::getExplanation(
   {
     Trace("te-proof-exp") << "=== TheoryEngine::getExplanation " << conclusion
                           << std::endl;
-    lcp.reset(new LazyCDProof(
-        d_pnm, nullptr, nullptr, "TheoryEngine::LazyCDProof::getExplanation"));
+    // We do not use auto-symmetry in this proof, since in very rare cases, it
+    // is possible that the proof of explanations is cyclic when considering
+    // (dis)equalities modulo symmetry, where such a proof looks like:
+    // x = y
+    // -----
+    //   A    ...
+    // ----------
+    //   y = x
+    // Notice that this complication arises since propagations consider
+    // equalities that are not in rewritten form. This complication would not
+    // exist otherwise. It is the shared term database that introduces these
+    // unrewritten equalities; it must do so since theory combination requires
+    // communicating arrangements between shared terms, and the rewriter
+    // for arithmetic equalities does not preserve terms, e.g. x=y may become
+    // x+-1*y=0.
+    lcp.reset(new LazyCDProof(d_pnm,
+                              nullptr,
+                              nullptr,
+                              "TheoryEngine::LazyCDProof::getExplanation",
+                              false));
   }
   unsigned i = 0; // Index of the current literal we are processing
 
@@ -1643,7 +1661,7 @@ TrustNode TheoryEngine::getExplanation(
 
         if (lcp != nullptr)
         {
-          if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node))
+          if (toExplain.d_node != (*find).second.d_node)
           {
             Trace("te-proof-exp")
                 << "- t-explained cached: " << toExplain.d_node << " by "
@@ -1671,17 +1689,13 @@ TrustNode TheoryEngine::getExplanation(
       // should prove the propagation we asked for
       Assert(texplanation.getKind() == TrustNodeKind::PROP_EXP
              && texplanation.getProven()[1] == toExplain.d_node);
-      // if not a trivial explanation
-      if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node))
-      {
-        // We add it to the list of theory explanations, to be processed at
-        // the end of this method. We wait to explain here because it may
-        // be that a later explanation may preempt the need for proving this
-        // step. For instance, if the conclusion lit is later added as an
-        // assumption in the final explanation. This avoids cyclic proofs.
-        texplains.push_back(
-            std::pair<TheoryId, TrustNode>(toExplain.d_theory, texplanation));
-      }
+      // We add it to the list of theory explanations, to be processed at
+      // the end of this method. We wait to explain here because it may
+      // be that a later explanation may preempt the need for proving this
+      // step. For instance, if the conclusion lit is later added as an
+      // assumption in the final explanation. This avoids cyclic proofs.
+      texplains.push_back(
+          std::pair<TheoryId, TrustNode>(toExplain.d_theory, texplanation));
     }
     Node explanation = texplanation.getNode();
 
@@ -1759,16 +1773,6 @@ TrustNode TheoryEngine::getExplanation(
         Trace("te-proof-exp") << "...already added" << std::endl;
         continue;
       }
-      Node symTConc = CDProof::getSymmFact(tConc);
-      if (!symTConc.isNull())
-      {
-        if (exp.find(symTConc) != exp.end())
-        {
-          // symmetric direction
-          Trace("te-proof-exp") << "...already added (SYMM)" << std::endl;
-          continue;
-        }
-      }
       // remember that we've explained this formula, to avoid cycles in lcp
       exp.insert(tConc);
       TheoryId ttid = it->first;
@@ -1816,7 +1820,7 @@ TrustNode TheoryEngine::getExplanation(
       {
         Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl;
         // otherwise, trusted theory lemma
-        Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(it->first);
+        Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(ttid);
         lcp->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn});
       }
       std::vector<Node> pfChildren;
@@ -1824,6 +1828,24 @@ TrustNode TheoryEngine::getExplanation(
       pfChildren.push_back(proven);
       lcp->addStep(tConc, PfRule::MODUS_PONENS, pfChildren, {});
     }
+    // If we don't have a step and the conclusion is not part of the
+    // explanation (for unit T-conflicts), it must be by symmetry. We must do
+    // this manually since lcp does not have auto-symmetry enabled due to the
+    // complication mentioned above.
+    if (!lcp->hasStep(conclusion) && exp.find(conclusion) == exp.end())
+    {
+      Node sconc = CDProof::getSymmFact(conclusion);
+      if (!sconc.isNull())
+      {
+        lcp->addStep(conclusion, PfRule::SYMM, {sconc}, {});
+      }
+      else
+      {
+        Assert(false)
+            << "TheoryEngine::getExplanation: no step found for conclusion "
+            << conclusion;
+      }
+    }
     // store in the proof generator
     TrustNode trn = d_tepg->mkTrustExplain(conclusion, expNode, lcp);
     // return the trust node
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 34ef1a9f7..625d5faea 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1805,6 +1805,7 @@ set(regress_1_tests
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
   regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
   regress1/proofs/qgu-fuzz-1-strings-pp.smt2
+  regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
   regress1/proofs/quant-alpha-eq.smt2
   regress1/proofs/sat-trivial-cycle.smt2
   regress1/proofs/unsat-cores-proofs.smt2
diff --git a/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2 b/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
new file mode 100644
index 000000000..b55fb3d49
--- /dev/null
+++ b/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const x Int)
+(declare-fun b () (Array Int Int))
+(declare-fun y () Int)
+(assert (and (= b (store b x y)) (= b (store b y y)) (= y (ite (> y 0) 0 y)) (= (store b 0 0) (store (store b y 1) 1 1))))
+(check-sat)