From: Andrew Reynolds Date: Tue, 19 Apr 2022 17:15:33 +0000 (-0500) Subject: Generalize concat conflict for sequences in LFSC (#8625) X-Git-Tag: cvc5-1.0.1~248 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35c67d1d8aed4633c1c814f4196d2e328f015476;p=cvc5.git Generalize concat conflict for sequences in LFSC (#8625) This ensures LFSC proofs are correct when using CONCAT_CONFLICT for sequences. In detail, to justify why (seq.++ (seq.unit c1) t1) = (seq.++ (seq.unit c2) t2) is a conflict, where c1 and c2 are constants, we require an explicit step to evalute (seq.unit c1) = (seq.unit c2) to false, since c1 and c2 are theory-specific constants. Note this is different from (str.++ (char n1) t1) = (str.++ (char n2) t2) where a syntactic check of n1 and n2 suffices. This fixes proof checking for regress0/seq/seq-types.smt2. --- diff --git a/proofs/lfsc/signatures/strings_programs.plf b/proofs/lfsc/signatures/strings_programs.plf index eb7351e0c..e280bc77b 100644 --- a/proofs/lfsc/signatures/strings_programs.plf +++ b/proofs/lfsc/signatures/strings_programs.plf @@ -36,7 +36,7 @@ (program sc_skolem_first_ctn_post ((s term) (t term)) term (sc_skolem_suffix_rem s (a.+ (str.len (sc_skolem_first_ctn_pre s t)) (a.+ (str.len t) (int 0))))) -; Head and tail for string concatenation. +; Head and tail for string concatenation. Fails if not a concatentation term. (program sc_string_head ((t term)) term (nary_head f_str.++ t)) (program sc_string_tail ((t term)) term (nary_tail f_str.++ t)) @@ -242,7 +242,8 @@ ((apply t1 t2) (let t12 (getarg f_str.++ t1) (match t12 - ((char n) t12)))) + ((char n) t12) + ((apply t121 t122) (ifequal t121 f_seq.unit t12 (fail term)))))) (default (ifequal t (sc_mk_emptystr u) t (fail term))))) ; Flatten constants in str.++ application s. Notice that the rewritten form diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf index 5f945f465..46c6f67e8 100644 --- a/proofs/lfsc/signatures/strings_rules.plf +++ b/proofs/lfsc/signatures/strings_rules.plf @@ -111,6 +111,32 @@ (! r (^ (sc_concat_conflict s t rev u) ok) (holds false)))))))) +; For sequences, we use a variant of the PfRule::CONCAT_CONFLICT rule where the +; justification for the clashing characters is given in the form of a +; disequality. This is due to the fact that check whether a term is value is +; not a simple syntactic check for some types. +(program sc_concat_conflict_deq ((s term) (t term) (sc term) (tc term) (rev flag) (u sort)) Ok + (match (sc_strip_prefix + (sc_string_to_flat_form s rev u) + (sc_string_to_flat_form t rev u) u) + ((pair ss ts) + (ifequal (sc_string_first_char_or_empty s u) sc + (ifequal (sc_string_first_char_or_empty t u) tc + ok + (fail Ok)) + (fail Ok))))) + +(declare concat_conflict_deq (! s term + (! t term + (! sc term + (! tc term + (! rev flag + (! u sort + (! p (holds (= s t)) + (! pc (holds (not (= sc tc))) + (! r (^ (sc_concat_conflict_deq s t sc tc rev u) ok) + (holds false))))))))))) + (program sc_string_length_pos ((t term) (u sort)) term (or (and (= (str.len t) (int 0)) (and (= t (sc_mk_emptystr u)) true)) (or (a.> (str.len t) (int 0)) false)) ) diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp index df902e6d6..37f97b905 100644 --- a/src/proof/lfsc/lfsc_post_processor.cpp +++ b/src/proof/lfsc/lfsc_post_processor.cpp @@ -22,6 +22,7 @@ #include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" #include "proof/proof_node_updater.h" +#include "theory/strings/theory_strings_utils.h" using namespace cvc5::internal::kind; @@ -363,6 +364,38 @@ 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()) + { + // 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)) + 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); + } + break; default: return false; break; } AlwaysAssert(cdp->getProofFor(res)->getRule() != PfRule::ASSUME); diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index a2cabd7b6..59230870b 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -704,6 +704,11 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn, case LfscRule::PROCESS_SCOPE: pf << h << h << as[2] << cs[0]; break; case LfscRule::AND_INTRO2: pf << h << h << cs[0] << cs[1]; break; case LfscRule::ARITH_SUM_UB: pf << h << h << h << cs[0] << cs[1]; break; + case LfscRule::CONCAT_CONFLICT_DEQ: + pf << h << h << h << h << as[2].getConst() + << d_tproc.convertType(children[0]->getResult()[0].getType()) + << cs[0] << cs[1]; + break; default: return false; break; } } diff --git a/src/proof/lfsc/lfsc_util.cpp b/src/proof/lfsc/lfsc_util.cpp index c38470a52..de8fad306 100644 --- a/src/proof/lfsc/lfsc_util.cpp +++ b/src/proof/lfsc/lfsc_util.cpp @@ -35,6 +35,7 @@ const char* toString(LfscRule id) case LfscRule::NOT_AND_REV: return "not_and_rev"; case LfscRule::PROCESS_SCOPE: return "process_scope"; case LfscRule::ARITH_SUM_UB: return "arith_sum_ub"; + case LfscRule::CONCAT_CONFLICT_DEQ: return "concat_conflict_deq"; case LfscRule::INSTANTIATE: return "instantiate"; case LfscRule::SKOLEMIZE: return "skolemize"; case LfscRule::LAMBDA: return "\\"; diff --git a/src/proof/lfsc/lfsc_util.h b/src/proof/lfsc/lfsc_util.h index 761d9edb7..9a0d96fa0 100644 --- a/src/proof/lfsc/lfsc_util.h +++ b/src/proof/lfsc/lfsc_util.h @@ -53,6 +53,9 @@ enum class LfscRule : uint32_t PROCESS_SCOPE, // arithmetic ARITH_SUM_UB, + // sequences uses a different form of the concat conflict rule which takes + // an explicit disequality + CONCAT_CONFLICT_DEQ, // form of quantifier rules varies from internal calculus INSTANTIATE,