From 55392bd73a7af71411a3157520b758623f2f4723 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 May 2022 14:16:56 -0500 Subject: [PATCH] Fix LFSC proof construction for concat clash of sequences (#8739) Changes the internal proof calculus to require an explicit disequality between character constants for clashing sequences. Makes it so that the disequality is expanded prior to proof post-processing, so that character clashing is properly expanded as it may require rewriting. --- src/proof/lfsc/lfsc_post_processor.cpp | 29 ++++---------------- src/proof/proof_rule.h | 15 +++++++++- src/theory/strings/infer_proof_cons.cpp | 27 ++++++++++++------ src/theory/strings/proof_checker.cpp | 16 ++++++++++- test/regress/cli/regress0/seq/seq-types.smt2 | 1 - 5 files changed, 54 insertions(+), 34 deletions(-) diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp index f849047ff..9fe578230 100644 --- a/src/proof/lfsc/lfsc_post_processor.cpp +++ b/src/proof/lfsc/lfsc_post_processor.cpp @@ -366,34 +366,17 @@ bool LfscProofPostprocessCallback::update(Node res, break; case PfRule::CONCAT_CONFLICT: { - Assert(children.size() == 1); - Assert(children[0].getKind() == EQUAL); - if (children[0][0].getType().isString()) + if (children.size() == 1) { // no need to change return false; } - bool isRev = args[0].getConst(); - std::vector tvec; - std::vector svec; - theory::strings::utils::getConcat(children[0][0], tvec); - theory::strings::utils::getConcat(children[0][1], svec); - Node t0 = tvec[isRev ? tvec.size() - 1 : 0]; - Node s0 = svec[isRev ? svec.size() - 1 : 0]; - Assert(t0.isConst() && s0.isConst()); - // We introduce an explicit disequality for the constants: - // ------------------- EVALUATE - // (= (= c1 c2) false) - // ------------------- FALSE_ELIM - // (not (= c1 c2)) + Assert(children.size() == 2); + Assert(children[0].getKind() == EQUAL); + Assert(children[0][0].getType().isSequence()); + // must use the sequences version of the rule Node falsen = nm->mkConst(false); - Node eq = t0.eqNode(s0); - Node eqEqFalse = eq.eqNode(falsen); - cdp->addStep(eqEqFalse, PfRule::EVALUATE, {}, {eq}); - Node deq = eq.notNode(); - cdp->addStep(deq, PfRule::FALSE_ELIM, {eqEqFalse}, {}); - addLfscRule( - cdp, falsen, {children[0], deq}, LfscRule::CONCAT_CONFLICT_DEQ, args); + addLfscRule(cdp, falsen, children, LfscRule::CONCAT_CONFLICT_DEQ, args); } break; default: return false; break; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index be1d7b040..c6f2b9a16 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -1436,7 +1436,20 @@ enum class PfRule : uint32_t * where :math:`b` indicates if the direction is reversed, :math:`c_1,\,c_2` * are constants such that :math:`\texttt{Word::splitConstant}(c_1,c_2, * \mathit{index},b)` is null, in other words, neither is a prefix of the - * other. + * other. Note it may be the case that one side of the equality denotes the + * empty string. + * + * Alternatively, if the equality is between sequences, this rule has the + * form: + * + * .. math:: + * + * \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq s_1 \mid b}{\bot} + * + * where t_1 and s_1 are constants of length one, or otherwise one side + * of the equality is the empty sequence and t_1 or s_1 corresponding to + * that side is the empty sequence. + * * \endverbatim */ CONCAT_CONFLICT, diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 8d57068e6..212bc56d3 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -392,6 +392,13 @@ void InferProofCons::convert(InferenceId infer, // fail break; } + // get the heads of the equality + std::vector tvec; + std::vector svec; + theory::strings::utils::getConcat(mainEqCeq[0], tvec); + theory::strings::utils::getConcat(mainEqCeq[1], svec); + Node t0 = tvec[isRev ? tvec.size() - 1 : 0]; + Node s0 = svec[isRev ? svec.size() - 1 : 0]; // Now, mainEqCeq is an equality t ++ ... == s ++ ... where the // inference involved t and s. if (infer == InferenceId::STRINGS_N_ENDPOINT_EQ @@ -427,10 +434,20 @@ void InferProofCons::convert(InferenceId infer, // should be a constant conflict std::vector childrenC; childrenC.push_back(mainEqCeq); + // if it is between sequences, we require the explicit disequality + if (mainEqCeq[0].getType().isSequence()) + { + Assert(t0.isConst() && s0.isConst()); + // We introduce an explicit disequality for the constants + Node deq = t0.eqNode(s0).notNode(); + psb.addStep(PfRule::MACRO_SR_PRED_INTRO, {}, {deq}, deq); + Assert(!deq.isNull()); + childrenC.push_back(deq); + } std::vector argsC; argsC.push_back(nodeIsRev); - Node mainEqC = psb.tryStep(PfRule::CONCAT_CONFLICT, childrenC, argsC); - if (mainEqC == conc) + Node conflict = psb.tryStep(PfRule::CONCAT_CONFLICT, childrenC, argsC); + if (conflict == conc) { useBuffer = true; Trace("strings-ipc-core") << "...success!" << std::endl; @@ -457,12 +474,6 @@ void InferProofCons::convert(InferenceId infer, } else { - std::vector tvec; - std::vector svec; - utils::getConcat(mainEqCeq[0], tvec); - utils::getConcat(mainEqCeq[1], svec); - Node t0 = tvec[isRev ? tvec.size() - 1 : 0]; - Node s0 = svec[isRev ? svec.size() - 1 : 0]; bool applySym = false; // may need to apply symmetry if ((infer == InferenceId::STRINGS_SSPLIT_CST diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index a938a120f..0b7f84fc3 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -181,7 +181,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id, } else if (id == PfRule::CONCAT_CONFLICT) { - Assert(children.size() == 1); + Assert(children.size() >= 1 && children.size() <= 2); if (!t0.isConst() || !s0.isConst()) { // not constants @@ -195,6 +195,20 @@ Node StringProofRuleChecker::checkInternal(PfRule id, // versa. return Node::null(); } + // if a disequality was provided, ensure that it is correct + if (children.size() == 2) + { + if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL + || children[1][0][0] != t0 || children[1][0][1] != s0) + { + return Node::null(); + } + } + else if (t0.getType().isSequence()) + { + // we require the disequality for sequences + return Node::null(); + } return nm->mkConst(false); } else if (id == PfRule::CONCAT_SPLIT) diff --git a/test/regress/cli/regress0/seq/seq-types.smt2 b/test/regress/cli/regress0/seq/seq-types.smt2 index f8d8aa8b3..3facf688a 100644 --- a/test/regress/cli/regress0/seq/seq-types.smt2 +++ b/test/regress/cli/regress0/seq/seq-types.smt2 @@ -1,4 +1,3 @@ -; DISABLE-TESTER: lfsc ; COMMAND-LINE: --strings-exp ;EXPECT: unsat (set-logic ALL) -- 2.30.2