Fix proofs for trivial cases of datatypes tester merge (#7969)

Fixes cvc5/cvc5-projects#433.

Also ensures we don't add (= t t) as part of a reported conflict.

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index d2e4947bba15602a65c856dfbdc64246520ec5a2..e49d58f9162e67fb96d8dc1a3f90e991db80e53a 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -218,14 +218,17 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
     break;
     case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
     {
-      Assert(expv.size() == 3);
+      Assert(2 <= expv.size() && expv.size() <= 3);
       Node tester1 = expv[0];
       Node tester1c =
           nm->mkNode(APPLY_TESTER, expv[1].getOperator(), expv[0][0]);
-      cdp->addStep(tester1c,
-                   PfRule::MACRO_SR_PRED_TRANSFORM,
-                   {expv[1], expv[2]},
-                   {tester1c});
+      std::vector<Node> targs{expv[1]};
+      if (expv.size() == 3)
+      {
+        targs.push_back(expv[2]);
+      }
+      cdp->addStep(
+          tester1c, PfRule::MACRO_SR_PRED_TRANSFORM, targs, {tester1c});
       Node fn = nm->mkConst(false);
       cdp->addStep(fn, PfRule::DT_CLASH, {tester1, tester1c}, {});
       success = true;

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f413015c4c8b1379ffb99ab2876983635d176335..a689be7c5c50b7cb0b4cea34734892732be71a74 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -902,7 +902,10 @@ void TheoryDatatypes::addTester(
     std::vector<Node> conf;
     conf.push_back(j);
     conf.push_back(t);
-    conf.push_back(jt[0].eqNode(t_arg));
+    if (jt[0] != t_arg)
+    {
+      conf.push_back(jt[0].eqNode(t_arg));
+    }
     Trace("dt-conflict") << "CONFLICT: Tester conflict : " << conf << std::endl;
     d_im.sendDtConflict(conf, InferenceId::DATATYPES_TESTER_MERGE_CONFLICT);
   }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1358f7dc774e5df4f4baafdd1afcc6c7e0f4f5a4..53df6519e8229a71b0d7c3585acb20db535ecff1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1708,6 +1708,7 @@ set(regress_1_tests
   regress1/datatypes/non-simple-rec.smt2
   regress1/datatypes/non-simple-rec-mut-unsat.smt2
   regress1/datatypes/non-simple-rec-param.smt2
+  regress1/datatypes/proj-issue433-tester-merge-pf.smt2
   regress1/datatypes/tuple_projection.smt2
   regress1/decision/bug374a.smtv1.smt2
   regress1/decision/error3.smtv1.smt2

diff --git a/test/regress/regress1/datatypes/proj-issue433-tester-merge-pf.smt2 b/test/regress/regress1/datatypes/proj-issue433-tester-merge-pf.smt2
new file mode 100644 (file)
index 0000000..9e2a428
--- /dev/null
+++ b/test/regress/regress1/datatypes/proj-issue433-tester-merge-pf.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((L 0)) (((i))))
+(declare-datatypes ((O 0)) (((N) (S (i (_ BitVec 3))))))
+(declare-fun m (L) O)
+(declare-fun g ((_ BitVec 3) L) L)
+(assert (exists ((B L) (n (_ BitVec 3))) (not (ite ((_ is S) (m (g n B))) (not ((_ is N) (m (g n B)))) true))))
+(check-sat)