From 66d8d5a6755170e91bb272b2a7dbf78e53b2eb9e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Jan 2022 14:39:59 -0600 Subject: [PATCH] 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. --- src/theory/datatypes/infer_proof_cons.cpp | 13 ++++++++----- src/theory/datatypes/theory_datatypes.cpp | 5 ++++- test/regress/CMakeLists.txt | 1 + .../datatypes/proj-issue433-tester-merge-pf.smt2 | 8 ++++++++ 4 files changed, 21 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress1/datatypes/proj-issue433-tester-merge-pf.smt2 diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index d2e4947bb..e49d58f91 100644 --- 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 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 f413015c4..a689be7c5 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -902,7 +902,10 @@ void TheoryDatatypes::addTester( std::vector 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 1358f7dc7..53df6519e 100644 --- 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 index 000000000..9e2a428db --- /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) -- 2.30.2