From b76c2b5f1df7b523d90a086eb77f5d811049bddc Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 19 Dec 2024 13:54:23 -0600 Subject: [PATCH 1/7] Disable lfsc tester on t3_rw903 (#11464) This fixes a timeout in the nightlies. --- test/regress/cli/regress0/proofs/t3_rw903.smt2 | 1 + 1 file changed, 1 insertion(+) diff --git a/test/regress/cli/regress0/proofs/t3_rw903.smt2 b/test/regress/cli/regress0/proofs/t3_rw903.smt2 index 93cc7ebfb7d..890ac068460 100644 --- a/test/regress/cli/regress0/proofs/t3_rw903.smt2 +++ b/test/regress/cli/regress0/proofs/t3_rw903.smt2 @@ -1,5 +1,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: lfsc (set-logic UFNIA) (declare-fun pow2 (Int) Int) (declare-fun intor (Int Int Int) Int) From cbbeb5158edb89608f1c4aa066b3333ce16a512c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Dec 2024 08:32:02 -0600 Subject: [PATCH 2/7] Only try to use basic rewriter to automatically reconstruct trust steps (#11388) This part of the code attempts to cast trust steps as rewrites, with the hope of making DSL rewrite rule elaboration easier. This PR changes the code so that we only try the basic rewriter, not the extended one. Since the extended rewriter does not have fine-grained proof support, reconstructing trust steps in it does not provide much benefit. Furthermore, it is less overhead to compute basic rewrites. --- src/smt/proof_post_processor.cpp | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 168abd5ceaa..6e6ee0d5e50 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -218,20 +218,11 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id, { TrustId tid; getTrustId(args[0], tid); - // we don't do this for steps that are already extended theory rewrite - // steps, or we would get an infinite loop in reconstruction. - if (tid == TrustId::EXT_THEORY_REWRITE) - { - return Node::null(); - } - // maybe we can show it rewrites to true based on (extended) rewriting + // maybe we can show it rewrites to true based on rewriting // modulo original forms (MACRO_SR_PRED_INTRO). TheoryProofStepBuffer psb(d_pc); - if (psb.applyPredIntro(res, - {}, - MethodId::SB_DEFAULT, - MethodId::SBA_SEQUENTIAL, - MethodId::RW_EXT_REWRITE)) + if (psb.applyPredIntro( + res, {}, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL)) { cdp->addSteps(psb); return res; From b0382ba12a4f5d2b436956d179db89e0d67da055 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Dec 2024 10:12:13 -0600 Subject: [PATCH 3/7] Add proof support for quantifiers term indexing conflicts (#11454) A term indexing conflict can be explained by congruence. A simple regression is added. This should cover all remaining theory lemmas from quantifiers when safe mode is enabled. --- src/theory/quantifiers/ho_term_database.cpp | 3 +- src/theory/quantifiers/term_database.cpp | 84 +++++++++++++++++-- src/theory/quantifiers/term_database.h | 7 +- test/regress/cli/CMakeLists.txt | 1 + .../regress1/quantifiers/pivc-deq-cong.smt2 | 10 +++ 5 files changed, 94 insertions(+), 11 deletions(-) create mode 100644 test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2 diff --git a/src/theory/quantifiers/ho_term_database.cpp b/src/theory/quantifiers/ho_term_database.cpp index dfd81376a5c..7a057c77931 100644 --- a/src/theory/quantifiers/ho_term_database.cpp +++ b/src/theory/quantifiers/ho_term_database.cpp @@ -155,7 +155,6 @@ bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) { return false; } - exp.push_back(a.eqNode(b)); // operators might be disequal Node af = getMatchOperator(a); Node bf = getMatchOperator(b); @@ -163,7 +162,7 @@ bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) { if (a.getKind() == Kind::APPLY_UF && b.getKind() == Kind::APPLY_UF) { - exp.push_back(af.eqNode(bf).negate()); + exp.push_back(af.eqNode(bf)); Assert(d_qstate.areEqual(af, bf)) << af << " and " << bf << " are not equal"; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 915d46b031c..4402c9017f8 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -23,6 +23,10 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "proof/proof.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" #include "theory/quantifiers/ematching/trigger_term_info.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" @@ -39,6 +43,68 @@ namespace cvc5::internal { namespace theory { namespace quantifiers { +/** + * A proof generator for proving simple congruence lemmas discovered by TermDb. + */ +class DeqCongProofGenerator : protected EnvObj, public ProofGenerator +{ + public: + DeqCongProofGenerator(Env& env) : EnvObj(env) {} + virtual ~DeqCongProofGenerator() {} + /** + * The lemma is of the form: + * (=> (and (= ti si) .. (= tj sj)) (= (f t1 ... tn) (f s1 ... sn))) + * which can be proven by a congruence step. + */ + std::shared_ptr getProofFor(Node fact) override + { + Assert(fact.getKind() == Kind::IMPLIES); + Assert(fact[1].getKind() == Kind::EQUAL); + Node a = fact[1][0]; + Node b = fact[1][1]; + std::vector assumps; + if (fact[0].getKind() == Kind::AND) + { + assumps.insert(assumps.end(), fact[0].begin(), fact[0].end()); + } + else + { + assumps.push_back(fact[0]); + } + CDProof cdp(d_env); + if (a.getOperator() != b.getOperator()) + { + // TODO: wishue #158, likely corresponds to a higher-order term + // indexing conflict. + cdp.addTrustedStep(fact, TrustId::QUANTIFIERS_PREPROCESS, {}, {}); + return cdp.getProofFor(fact); + } + Assert(a.getNumChildren() == b.getNumChildren()); + std::vector cargs; + ProofRule cr = expr::getCongRule(a, cargs); + size_t nchild = a.getNumChildren(); + std::vector premises; + for (size_t i = 0; i < nchild; i++) + { + Node eq = a[i].eqNode(b[i]); + premises.push_back(eq); + if (a[i] == b[i]) + { + cdp.addStep(eq, ProofRule::REFL, {}, {a[i]}); + } + else + { + Assert(std::find(assumps.begin(), assumps.end(), eq) != assumps.end()); + } + } + cdp.addStep(fact[1], cr, premises, cargs); + std::shared_ptr pfn = cdp.getProofFor(fact[1]); + return d_env.getProofNodeManager()->mkScope(pfn, assumps); + } + /** identify */ + std::string identify() const override { return "DeqCongProofGenerator"; } +}; + TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) : QuantifiersUtil(env), d_qstate(qs), @@ -48,7 +114,9 @@ TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) d_typeMap(context()), d_ops(context()), d_opMap(context()), - d_inactive_map(context()) + d_inactive_map(context()), + d_dcproof(options().smt.produceProofs ? new DeqCongProofGenerator(d_env) + : nullptr) { d_true = nodeManager()->mkConst(true); d_false = nodeManager()->mkConst(false); @@ -390,19 +458,19 @@ void TermDb::computeUfTerms( TNode f ) { congruentCount++; continue; } - std::vector lits; - if (checkCongruentDisequal(at, n, lits)) + std::vector antec; + if (checkCongruentDisequal(at, n, antec)) { Assert(at.getNumChildren() == n.getNumChildren()); for (size_t k = 0, size = at.getNumChildren(); k < size; k++) { if (at[k] != n[k]) { - lits.push_back(nm->mkNode(Kind::EQUAL, at[k], n[k]).negate()); + antec.push_back(nm->mkNode(Kind::EQUAL, at[k], n[k])); Assert(d_qstate.areEqual(at[k], n[k])); } } - Node lem = nm->mkOr(lits); + Node lem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(antec), at.eqNode(n)); if (TraceIsOn("term-db-lemma")) { Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " @@ -415,7 +483,10 @@ void TermDb::computeUfTerms( TNode f ) { } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } - d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_TDB_DEQ_CONG); + d_qim->addPendingLemma(lem, + InferenceId::QUANTIFIERS_TDB_DEQ_CONG, + LemmaProperty::NONE, + d_dcproof.get()); d_qstate.notifyInConflict(); return; } @@ -442,7 +513,6 @@ bool TermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) { if (d_qstate.areDisequal(a, b)) { - exp.push_back(a.eqNode(b)); return true; } return false; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index baa52fa2082..957fb56cf73 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -36,6 +36,7 @@ namespace quantifiers { class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; +class DeqCongProofGenerator; /** Context-dependent list of nodes */ class DbList @@ -263,6 +264,8 @@ class TermDb : public QuantifiersUtil { * of equality engine (for higher-order). */ std::map d_ho_type_match_pred; + /** A proof generator for disequal congruent terms */ + std::shared_ptr d_dcproof; //----------------------------- implementation-specific /** * Finish reset internal, called at the end of reset(e). Returning false will @@ -279,8 +282,8 @@ class TermDb : public QuantifiersUtil { * This method is called when terms a and b are indexed by the same operator, * and have equivalent arguments. This method checks if we are in conflict, * which is the case if a and b are disequal in the equality engine. - * If so, it adds the set of literals that are implied but do not hold, e.g. - * the equality (= a b). + * If so, it adds any additional arguments that explain why a = b, e.g. the + * equivalence of their operators if their operators are different. */ virtual bool checkCongruentDisequal(TNode a, TNode b, std::vector& exp); //----------------------------- end implementation-specific diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 71ae0c13d55..138f90df7bb 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2878,6 +2878,7 @@ set(regress_1_tests regress1/quantifiers/nra-interleave-inst.smt2 regress1/quantifiers/opisavailable-12.smt2 regress1/quantifiers/parametric-lists.smt2 + regress1/quantifiers/pivc-deq-cong.smt2 regress1/quantifiers/pool-decidable-arrays-1.smt2 regress1/quantifiers/pool-example.smt2 regress1/quantifiers/pool-tuple.smt2 diff --git a/test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2 b/test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2 new file mode 100644 index 00000000000..8597415dae3 --- /dev/null +++ b/test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --enum-inst +; EXPECT: unsat +(set-logic ALL) +(declare-fun V () Int) +(declare-fun e () Int) +(declare-fun a2 () (Array Int Int)) +(declare-fun a () (Array Int Int)) +(declare-fun i () Int) +(assert (and (< i V) (<= 0 i) (forall ((? Int)) (= 1 (select a2 i))) (forall ((? Int)) (= (select a ?) (select a2 ?))) (forall ((? Int)) (forall ((? Int)) (= 1 (select a2 ?)))) (forall ((? Int)) (or (distinct e (select a ?)) (> ? (- i 1)))) (or (and (= 1 V) (exists ((? Int)) (> 1 (select a 0)))) (exists ((? Int)) (and (<= ? i) (= e (select a ?))))))) +(check-sat) From b47cbd4079971a6a9f1c9172b52f625e4604dab3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Dec 2024 11:04:26 -0600 Subject: [PATCH 4/7] Fix issues with shared selectors in proofs (#11415) We do not generally support shared selectors in proofs. This disables them when full strict proofs are enabled, and makes the internal proof checker not support them. It also adds proper printing support for them in the Eunoia signature in case they are enabled. --- proofs/eo/cpc/theories/Datatypes.eo | 4 +-- src/proof/alf/alf_node_converter.cpp | 33 ++++++++++++------- src/smt/set_defaults.cpp | 4 ++- src/theory/datatypes/datatypes_rewriter.cpp | 11 +++++-- src/theory/datatypes/proof_checker.cpp | 5 ++- src/theory/datatypes/proof_checker.h | 4 +-- src/theory/datatypes/theory_datatypes.cpp | 2 +- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/datatypes/pf-v2l60078.smt2 | 6 ++++ 9 files changed, 46 insertions(+), 24 deletions(-) create mode 100644 test/regress/cli/regress0/datatypes/pf-v2l60078.smt2 diff --git a/proofs/eo/cpc/theories/Datatypes.eo b/proofs/eo/cpc/theories/Datatypes.eo index 47545f10e53..8b396d30c31 100644 --- a/proofs/eo/cpc/theories/Datatypes.eo +++ b/proofs/eo/cpc/theories/Datatypes.eo @@ -59,5 +59,5 @@ ; disclaimer: This function is not in the SMT-LIB standard. (declare-const nullable.lift (-> (! Type :var F :implicit) F ($get_type_nullable_lift F))) -; skolems -;SHARED_SELECTOR +; shared selector +(declare-const @shared_selector (-> (! Type :var D) (! Type :var T) Int D T)) diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp index 17852b3776c..17df4681d44 100644 --- a/src/proof/alf/alf_node_converter.cpp +++ b/src/proof/alf/alf_node_converter.cpp @@ -25,6 +25,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/sequence.h" +#include "expr/sort_to_term.h" #include "printer/smt2/smt2_printer.h" #include "theory/builtin/generic_op.h" #include "theory/bv/theory_bv_utils.h" @@ -545,22 +546,30 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast) else if (k == Kind::APPLY_SELECTOR) { // maybe a shared selector - ret = maybeMkSkolemFun(op); - if (!ret.isNull()) + if (op.getSkolemId() == SkolemId::SHARED_SELECTOR) { - return ret; - } - unsigned index = DType::indexOf(op); - const DType& dt = DType::datatypeOf(op); - if (dt.isTuple()) - { - indices.push_back(d_nm->mkConstInt(index)); - opName << "tuple.select"; + std::vector kindices = op.getSkolemIndices(); + opName << "@shared_selector"; + indices.push_back( + typeAsNode(kindices[0].getConst().getType())); + indices.push_back( + typeAsNode(kindices[1].getConst().getType())); + indices.push_back(kindices[2]); } else { - unsigned cindex = DType::cindexOf(op); - opName << dt[cindex][index].getSelector(); + unsigned index = DType::indexOf(op); + const DType& dt = DType::datatypeOf(op); + if (dt.isTuple()) + { + indices.push_back(d_nm->mkConstInt(index)); + opName << "tuple.select"; + } + else + { + unsigned cindex = DType::cindexOf(op); + opName << dt[cindex][index].getSelector(); + } } } else diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 7441fd8e03f..66a888d2e9d 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1139,11 +1139,13 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, if (opts.smt.proofMode == options::ProofMode::FULL_STRICT) { // symmetry breaking does not have proof support - SET_AND_NOTIFY_VAL_SYM(uf, ufSymmetryBreaker, false, "full strict proofs"); + SET_AND_NOTIFY(uf, ufSymmetryBreaker, false, "full strict proofs"); // CEGQI with deltas and infinities is not supported SET_AND_NOTIFY(quantifiers, cegqiMidpoint, true, "full strict proofs"); SET_AND_NOTIFY(quantifiers, cegqiUseInfInt, false, "full strict proofs"); SET_AND_NOTIFY(quantifiers, cegqiUseInfReal, false, "full strict proofs"); + // shared selectors are not supported + SET_AND_NOTIFY(datatypes, dtSharedSelectors, false, "full strict proofs"); } return false; } diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index b57b00912e0..aa3cba4b47c 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -78,8 +78,10 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) Assert(tn.isDatatype()); const DType& dt = tn.getDType(); size_t i = utils::indexOf(n.getOperator()); - bool sharedSel = d_opts.datatypes.dtSharedSelectors; - Node ticons = utils::getInstCons(t, dt, i, sharedSel); + // Note that we set shared selectors to false. This proof rule will + // be (unintentionally) unsuccessful when reconstructing proofs of the + // rewriter when using shared selectors. + Node ticons = utils::getInstCons(t, dt, i, false); return t.eqNode(ticons); } case ProofRewriteRule::DT_COLLAPSE_SELECTOR: @@ -90,6 +92,11 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) return Node::null(); } Node selector = n.getOperator(); + // shared selectors are not supported + if (selector.getSkolemId() == SkolemId::SHARED_SELECTOR) + { + return Node::null(); + } size_t constructorIndex = utils::indexOf(n[0].getOperator()); const DType& dt = utils::datatypeOf(selector); const DTypeConstructor& c = dt[constructorIndex]; diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp index 623f5e0d28c..3260fce7e5c 100644 --- a/src/theory/datatypes/proof_checker.cpp +++ b/src/theory/datatypes/proof_checker.cpp @@ -23,9 +23,8 @@ namespace cvc5::internal { namespace theory { namespace datatypes { -DatatypesProofRuleChecker::DatatypesProofRuleChecker(NodeManager* nm, - bool sharedSel) - : ProofRuleChecker(nm), d_sharedSel(sharedSel) +DatatypesProofRuleChecker::DatatypesProofRuleChecker(NodeManager* nm) + : ProofRuleChecker(nm) { } diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h index 42bab401b50..c31a51ac5a2 100644 --- a/src/theory/datatypes/proof_checker.h +++ b/src/theory/datatypes/proof_checker.h @@ -30,7 +30,7 @@ namespace datatypes { class DatatypesProofRuleChecker : public ProofRuleChecker { public: - DatatypesProofRuleChecker(NodeManager* nm, bool sharedSel); + DatatypesProofRuleChecker(NodeManager* nm); /** Register all rules owned by this rule checker into pc. */ void registerTo(ProofChecker* pc) override; @@ -40,8 +40,6 @@ class DatatypesProofRuleChecker : public ProofRuleChecker Node checkInternal(ProofRule id, const std::vector& children, const std::vector& args) override; - /** Whether we are using shared selectors */ - bool d_sharedSel; }; } // namespace datatypes diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index edbab9eefba..055e6b79239 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -64,7 +64,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env, d_state(env, valuation), d_im(env, *this, d_state), d_notify(d_im, *this), - d_checker(nodeManager(), options().datatypes.dtSharedSelectors), + d_checker(nodeManager()), d_cpacb(*this) { d_true = nodeManager()->mkConst(true); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 138f90df7bb..f02fec093aa 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -724,6 +724,7 @@ set(regress_0_tests regress0/datatypes/pair-real-bool.smt2 regress0/datatypes/par-updater-type-rule.smt2 regress0/datatypes/parametric-alt-list.cvc.smt2 + regress0/datatypes/pf-v2l60078.smt2 regress0/datatypes/proj-issue172.smt2 regress0/datatypes/proj-issue474-app-cons-value.smt2 regress0/datatypes/proj-issue578-clash-pf.smt2 diff --git a/test/regress/cli/regress0/datatypes/pf-v2l60078.smt2 b/test/regress/cli/regress0/datatypes/pf-v2l60078.smt2 new file mode 100644 index 00000000000..f58dabb38a8 --- /dev/null +++ b/test/regress/cli/regress0/datatypes/pf-v2l60078.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +(set-logic QF_DT) +(declare-datatypes ((n 0) (l 0) (t 0)) (((z)) ((ln) (n (r l))) ((f)))) +(declare-fun x () l) +(assert (and (not (= ln (r x))) (not ((_ is n) (r x))))) +(check-sat) From dede2eaf5f282736e27444aac4f272796e8c9f21 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Dec 2024 11:36:32 -0600 Subject: [PATCH 5/7] Minor fixes for printers (#11430) Minor for AST printer and smt2 printer when using --expr-depth. --- src/printer/ast/ast_printer.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 21d3f7d5bb8..678c2a2d886 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -83,6 +83,7 @@ void AstPrinter::toStream(std::ostream& out, { for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) { + out << ' '; // body is re-letified if (i == 1) { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0bee9b74bad..a32b812166e 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1116,6 +1116,10 @@ void Smt2Printer::toStream(std::ostream& out, { visit.pop_back(); out << "(...)"; + if (cur.getNumChildren() > 0) + { + out << ')'; + } continue; } } From 5ee60a5f289aaa876ba25a8a33400129f2878777 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Dec 2024 11:37:41 -0600 Subject: [PATCH 6/7] Do not print BITVECTOR_EAGER_ATOM in cpc proofs (#11377) BV_EAGER_ATOM can now be `refl`. Note that I've opened a wishue if we want a deeper refactoring to never print this kind at all, which will require changes to the smt2 printer. --- proofs/eo/cpc/theories/BitVectors.eo | 2 -- src/proof/alf/alf_node_converter.cpp | 7 +++++++ src/proof/alf/alf_printer.cpp | 4 +++- 3 files changed, 10 insertions(+), 3 deletions(-) diff --git a/proofs/eo/cpc/theories/BitVectors.eo b/proofs/eo/cpc/theories/BitVectors.eo index 258365b1310..833d4eb1ff0 100644 --- a/proofs/eo/cpc/theories/BitVectors.eo +++ b/proofs/eo/cpc/theories/BitVectors.eo @@ -343,8 +343,6 @@ (BitVec m) Int) ) -(declare-const BITVECTOR_EAGER_ATOM (-> Bool Bool)) - ; internal operators (declare-const @bit diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp index 17df4681d44..c0ae25145fd 100644 --- a/src/proof/alf/alf_node_converter.cpp +++ b/src/proof/alf/alf_node_converter.cpp @@ -295,6 +295,13 @@ Node AlfNodeConverter::postConvert(Node n) return mkInternalApp("to_fp_bv", children, tn); } } + else if (k == Kind::BITVECTOR_EAGER_ATOM) + { + // For now, we explicity remove the application. + // https://github.com/cvc5/cvc5-wishues/issues/156: if the smt2 printer + // is refactored to silently ignore this kind, this case can be deleted. + return n[0]; + } else if (GenericOp::isIndexedOperatorKind(k)) { TypeNode tn = n.getType(); diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 151873738c4..30db9ff22bf 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -180,6 +180,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn) case ProofRule::QUANT_VAR_REORDERING: case ProofRule::ENCODE_EQ_INTRO: case ProofRule::HO_APP_ENCODE: + case ProofRule::BV_EAGER_ATOM: case ProofRule::ACI_NORM: case ProofRule::ARITH_POLY_NORM: case ProofRule::ARITH_POLY_NORM_REL: @@ -496,7 +497,8 @@ std::string AlfPrinter::getRuleName(const ProofNode* pfn) const ss << id; return ss.str(); } - else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE) + else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE + || r == ProofRule::BV_EAGER_ATOM) { // ENCODE_EQ_INTRO proves (= t (convert t)) from argument t, // where (convert t) is indistinguishable from t according to the proof. From 96a35d7cc97ee375e263ab43a2ed9ba03cc32858 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Dec 2024 13:34:40 -0600 Subject: [PATCH 7/7] Do not rewrite datatype inferences prior to proof reconstruction (#11465) It is not clear why this was done, it makes proof reconstruction fail in rare cases, added a regression for this. --- src/theory/datatypes/inference_manager.cpp | 5 ----- test/regress/cli/CMakeLists.txt | 1 + .../regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 | 15 +++++++++++++++ 3 files changed, 16 insertions(+), 5 deletions(-) create mode 100644 test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 6b3e3e48b5f..38b1532a7b8 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -150,11 +150,6 @@ Node InferenceManager::prepareDtInference(Node conc, { Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp << " by " << id << std::endl; - if (conc.getKind() == Kind::EQUAL && conc[0].getType().isBoolean()) - { - // must turn (= conc false) into (not conc) - conc = rewrite(conc); - } if (isProofEnabled()) { Assert(ipc != nullptr); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index f02fec093aa..175c419f4c6 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1461,6 +1461,7 @@ set(regress_0_tests regress0/quantifiers/cond-var-elim-binary.smt2 regress0/quantifiers/dd_german169_semi_eval.smt2 regress0/quantifiers/dd_spark2014-pat.smt2 + regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 regress0/quantifiers/dd.german169-ieval.smt2 regress0/quantifiers/dd.german169-lemma-inp.smt2 regress0/quantifiers/dd.ho-matching-enum.smt2 diff --git a/test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 b/test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 new file mode 100644 index 00000000000..19723e2c7eb --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +; DISABLE-TESTER: cpc +; Disabled cpc due to congruence on overloaded user functions. +(set-logic ALL) +(declare-sort i 0) +(declare-sort s 0) +(declare-datatypes ((u 0)) (((us (r Bool) (e Int) (c s))))) +(declare-datatypes ((us_ 0)) (((us (c i) (e u))))) +(declare-datatypes ((_r 0)) (((s_ (_s us_))))) +(declare-fun s_ (s) _r) +(declare-fun us (_r) s) +(assert (forall ((x _r)) (= x (s_ (us x))))) +(declare-const n u) +(assert (exists ((x_ us_)) (not (=> (r n) (= (s_ x_) (s_ (c (us false 0 (us (s_ (us (c (_s (s_ (c n)))) n))))))) (forall ((o u)) (or (forall ((x us_)) (or (forall ((o u)) (or (forall ((x us_)) (or (forall ((o u)) (or (forall ((x us_)) (or (exists ((t u)) (= (r o) (= (r o) (r (e (_s (s_ (c t)))))))) (= (s_ x_) (s_ (c (us false 0 (us (s_ (us (c (_s (s_ (c o)))) (us (r (e (_s (s_ (c (us false 0 (us (s_ x_)))))))) (e (e (_s (s_ (c o))))) (us (s_ x_)))))))))))))))))))))))))) +(check-sat)