[proofs] Generalize handling of constants merged in equality engine (#8781)

Previously the reconstruction of EUF proofs was not considering a corner case from the equality engine where it infers that two constants are disequal from other equalities, but these other equalities all become of the form x = x at the time we are explaining this disquality. In this case the constant disequality is justified with MERGED_THROUGH_CONSTANTS rather than MERGED_THROUGH_TRANS as other disequalities.

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 6402dc99bdcc7bd2d91c9b6ccc12b120893a9393..a92e3430b7ccb03dd03fa8901388ebc793bf0bc5 100644 (file)
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -979,12 +979,27 @@ Node EqProof::addToProof(CDProof* p,
   // Equalities due to theory reasoning
   if (d_id == MERGED_THROUGH_CONSTANTS)
   {
-    Assert(!d_node.isNull() && d_node.getKind() == kind::EQUAL
-           && d_node[1].isConst())
+    Assert(!d_node.isNull()
+           && ((d_node.getKind() == kind::EQUAL && d_node[1].isConst())
+               || (d_node.getKind() == kind::NOT
+                   && d_node[0].getKind() == kind::EQUAL
+                   && d_node[0][0].isConst() && d_node[0][1].isConst())))
         << ". Conclusion " << d_node << " from " << d_id
-        << " was expected to be (= (f t1 ... tn) c)\n";
+        << " was expected to be (= (f t1 ... tn) c) or (not (= c1 c2))\n";
     Assert(!assumptions.count(d_node))
         << "Conclusion " << d_node << " from " << d_id << " is an assumption\n";
+    // The step has the form (not (= c1 c2)). We conclude it via
+    // MACRO_SR_PRED_INTRO and turn it into an equality with false, so that the
+    // rest of the reconstruction works
+    if (d_children.empty())
+    {
+      Node conclusion =
+          d_node[0].eqNode(NodeManager::currentNM()->mkConst<bool>(false));
+      p->addStep(d_node, PfRule::MACRO_SR_PRED_INTRO, {}, {d_node});
+      p->addStep(conclusion, PfRule::FALSE_INTRO, {}, {d_node});
+      visited[d_node] = conclusion;
+      return conclusion;
+    }
     // The step has the form
     //  [(= t1 c1)] ... [(= tn cn)]
     //  ------------------------

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 9cd7b42cc59a4564e17cec7b5f4ba59a5546ab26..05f55e11b59dc6c66f1115cf72c1e7b0ceeec625 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1103,13 +1103,16 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
   // The terms must be there already
   Assert(hasTerm(t1) && hasTerm(t2));
 
+  // Get the ids
+  EqualityNodeId t1Id = getNodeId(t1);
+  EqualityNodeId t2Id = getNodeId(t2);
+
+  Trace("pf::ee") << "Ids: " << t1Id << ", " << t2Id << "\n";
+
   if (TraceIsOn("equality::internal"))
   {
     debugPrintGraph();
   }
-  // Get the ids
-  EqualityNodeId t1Id = getNodeId(t1);
-  EqualityNodeId t2Id = getNodeId(t2);
 
   std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*> cache;
   if (polarity) {

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index f9264e14b4f7eb4be9601436f0d823bbaf9d8ebd..e11f6d78b5d119d68bdd2b2dd9592e43045e77ec 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2087,6 +2087,7 @@ set(regress_1_tests
   regress1/proj-issue406-diff-unsat-core.smt2
   regress1/proj-issue476-theoryOf-no-uf.smt2
   regress1/proof00.smt2
+  regress1/proofs/eq-engine-corner-case-constants-disequal.smt2
   regress1/proofs/issue6625-unsat-core-proofs.smt2
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
   regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2

diff --git a/test/regress/cli/regress1/proofs/eq-engine-corner-case-constants-disequal.smt2 b/test/regress/cli/regress1/proofs/eq-engine-corner-case-constants-disequal.smt2
new file mode 100644 (file)
index 0000000..c1b534b
--- /dev/null
+++ b/test/regress/cli/regress1/proofs/eq-engine-corner-case-constants-disequal.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --produce-proofs
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-const x Bool)
+(declare-fun s () String)
+(assert (ite (str.prefixof "-" (str.substr s 1 1)) true x))
+(assert (> (- (str.len s) 1 (+ 1 1) (+ 1 1)) 0))
+(assert (str.in_re s (re.+ (re.range "0" "9"))))
+(assert (= 1 (str.to_int (str.substr s (+ 1 1 1 1) (+ 1 1)))))
+(check-sat)