From: Andrew Reynolds Date: Thu, 7 Oct 2021 09:53:59 +0000 (-0500) Subject: Miscellaneous fixes from proof-new (#7313) X-Git-Tag: cvc5-1.0.0~1111 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=65431e88f8e0c48c90bc540b95c63b67d8387219;p=cvc5.git Miscellaneous fixes from proof-new (#7313) Includes a few fixes for strings and datatypes theory lemma proofs. --- diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index afbfd16c1..4aace5f1c 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -169,30 +169,37 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* Node concAtom = concPol ? conc : conc[0]; concEq = concAtom.eqNode(nm->mkConst(concPol)); } - Assert(concEq.getKind() == EQUAL - && concEq[0].getKind() == APPLY_SELECTOR_TOTAL); - Assert(exp[0].getType().isDatatype()); - Node sop = concEq[0].getOperator(); - Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]); - Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]); - // exp[0] = exp[1] - // --------------------- CONG ----------------- DT_COLLAPSE - // s(exp[0]) = s(exp[1]) s(exp[1]) = r - // --------------------------------------------------- TRANS - // s(exp[0]) = r - Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL); - Node seq = sl.eqNode(sr); - cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop}); - Node sceq = sr.eqNode(concEq[1]); - cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr}); - cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {}); - if (conc.getKind() != EQUAL) + if (concEq[0].getKind() != APPLY_SELECTOR_TOTAL) { - PfRule eid = - conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM; - cdp->addStep(conc, eid, {concEq}, {}); + // can happen for Boolean term variables, which are not currently + // supported. + success = false; + } + else + { + Assert(exp[0].getType().isDatatype()); + Node sop = concEq[0].getOperator(); + Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]); + Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]); + // exp[0] = exp[1] + // --------------------- CONG ----------------- DT_COLLAPSE + // s(exp[0]) = s(exp[1]) s(exp[1]) = r + // --------------------------------------------------- TRANS + // s(exp[0]) = r + Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL); + Node seq = sl.eqNode(sr); + cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop}); + Node sceq = sr.eqNode(concEq[1]); + cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr}); + cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {}); + if (conc.getKind() != EQUAL) + { + PfRule eid = + conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM; + cdp->addStep(conc, eid, {concEq}, {}); + } + success = true; } - success = true; } break; case InferenceId::DATATYPES_CLASH_CONFLICT: diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index e9a6da104..34597c8be 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -396,6 +396,25 @@ void InferProofCons::convert(InferenceId infer, Trace("strings-ipc-core") << "...success!" << std::endl; } } + else if (infer == InferenceId::STRINGS_F_NCTN + || infer == InferenceId::STRINGS_N_NCTN) + { + // May require extended equality rewrite, applied after the rewrite + // above. Notice we need both in sequence since ext equality rewriting + // is not recursive. + std::vector argsERew; + addMethodIds(argsERew, + MethodId::SB_DEFAULT, + MethodId::SBA_SEQUENTIAL, + MethodId::RW_REWRITE_EQ_EXT); + Node mainEqERew = + psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, {mainEqCeq}, argsERew); + if (mainEqERew == conc) + { + useBuffer = true; + Trace("strings-ipc-core") << "...success!" << std::endl; + } + } else { std::vector tvec; @@ -845,7 +864,11 @@ void InferProofCons::convert(InferenceId infer, Trace("strings-ipc-prefix") << "- Possible conflicting equality : " << curr << std::endl; std::vector emp; - Node concE = psb.applyPredElim(curr, emp); + Node concE = psb.applyPredElim(curr, + emp, + MethodId::SB_DEFAULT, + MethodId::SBA_SEQUENTIAL, + MethodId::RW_REWRITE_EQ_EXT); Trace("strings-ipc-prefix") << "- After pred elim: " << concE << std::endl; if (concE == conc) diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 9252babba..2fc86a5a5 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -104,7 +104,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc) lemma = nm->mkNode( AND, nm->mkNode( - OR, nm->mkConst(Rational(-1)).eqNode(t), nm->mkNode(GEQ, t, t[2])), + OR, t.eqNode(nm->mkConst(Rational(-1))), nm->mkNode(GEQ, t, t[2])), nm->mkNode(LEQ, t, l)); } else if (tk == STRING_STOI)