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.

diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp
index eab452d49398159bd6c4daf85b7a274deb83f28a..f6c9d8eb2f0b57e9b2265d5d9e7c4827cb417cc1 100644 (file)
--- 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 bf5bc229cc629aed7e8aad1ca9b4ef2db87eb144..e14dc8a1c0d52ea8e186b91d28d3b2ee59558efa 100644 (file)
--- 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 ee1528f4d67718288d45eae2f266a50f78561804..a186c05a0dffa2ca1c7680a9b56d2046f8099bb1 100644 (file)
--- 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 34ef1a9f7653c432b6d928ef1537dfa95bcdb19d..625d5faea52082335537d763b2fb66189195502c 100644 (file)
--- 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 (file)
index 0000000..b55fb3d
--- /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)