From: Andrew Reynolds Date: Mon, 7 Jun 2021 17:44:20 +0000 (-0500) Subject: (proof-new) Fix missing connection in trust substitution proofs (#6685) X-Git-Tag: cvc5-1.0.0~1634 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e9e71c7bd2bcbdcb2cef0d8f99bf34082bf4081;p=cvc5.git (proof-new) Fix missing connection in trust substitution proofs (#6685) This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs. Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity. --- diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 0cefe1209..676fa6a63 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -46,6 +46,7 @@ const char* toString(PfRule id) case PfRule::TRUST_REWRITE: return "TRUST_REWRITE"; case PfRule::TRUST_SUBS: return "TRUST_SUBS"; case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP"; + case PfRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ"; //================================================= Boolean rules case PfRule::RESOLUTION: return "RESOLUTION"; case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 107285cc3..a42b30773 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -219,11 +219,13 @@ enum class PfRule : uint32_t THEORY_REWRITE, // The remaining rules in this section have the signature of a "trusted rule": // - // Children: none + // Children: ? // Arguments: (F) // --------------------------------------------------------------- // Conclusion: F // + // Unless stated below, the expected children vector of the rule is empty. + // // where F is an equality of the form t = t' where t was replaced by t' // based on some preprocessing pass, or otherwise F was added as a new // assertion by some preprocessing pass. @@ -248,8 +250,13 @@ enum class PfRule : uint32_t // could not be replayed during proof postprocessing. TRUST_SUBS, // where F is an equality (= t t') that holds by a form of substitution that - // could not be determined by the TrustSubstitutionMap. + // could not be determined by the TrustSubstitutionMap. This inference may + // contain possibly multiple children corresponding to the formulas used to + // derive the substitution. TRUST_SUBS_MAP, + // where F is a solved equality of the form (= x t) derived as the solved + // form of F', where F' is given as a child. + TRUST_SUBS_EQ, // ========= SAT Refutation for assumption-based unsat cores // Children: (P1, ..., Pn) // Arguments: none diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 7ec0525c9..dae3922e6 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -52,6 +52,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); + pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -399,7 +400,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS - || id == PfRule::TRUST_SUBS_MAP) + || id == PfRule::TRUST_SUBS_MAP || id == PfRule::TRUST_SUBS_EQ) { // "trusted" rules Assert(!args.empty()); diff --git a/src/theory/theory.h b/src/theory/theory.h index d71348ce3..378305c75 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -675,8 +675,8 @@ class Theory { * add the solved substitutions to the map, if any. The method should return * true if the literal can be safely removed from the input problem. * - * Note that tin has trude node kind LEMMA. Its proof generator should be - * take into account when adding a substitution to outSubstitutions when + * Note that tin has trust node kind LEMMA. Its proof generator should be + * taken into account when adding a substitution to outSubstitutions when * proofs are enabled. */ virtual PPAssertStatus ppAssert(TrustNode tin, diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index 7a2fb19bd..7934231b9 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -115,11 +115,10 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x, // Try to transform tn.getProven() to (= x t) here, if necessary if (!d_tspb->applyPredTransform(proven, eq, {})) { - // failed to rewrite, it is critical for unsat cores that proven is a - // premise here, since the conclusion depends on it - addSubstitution(x, t, PfRule::TRUST_SUBS_MAP, {proven}, {eq}); - Trace("trust-subs") << "...failed to rewrite" << std::endl; - return nullptr; + // failed to rewrite, we add a trust step which assumes eq is provable + // from proven, and proceed as normal. + Trace("trust-subs") << "...failed to rewrite " << proven << std::endl; + d_tspb->addStep(PfRule::TRUST_SUBS_EQ, {proven}, {eq}, eq); } Trace("trust-subs") << "...successful rewrite" << std::endl; solvePg->addSteps(*d_tspb.get()); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 237ca77dd..207840516 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -806,6 +806,7 @@ set(regress_0_tests regress0/printer/tuples_and_records.cvc regress0/proofs/issue277-circuit-propagator.smt2 regress0/proofs/scope.smt2 + regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 regress0/push-pop/boolean/fuzz_14.smt2 diff --git a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 index 78dd44d66..63273b899 100644 --- a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 +++ b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: ; EXPECT: unsat (set-option :incremental false) (set-info :source "Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. diff --git a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 index b149c0570..79af1ce94 100644 --- a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 +++ b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: ; EXPECT: unsat (set-option :incremental false) (set-info :source "Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2 index f9d2e022d..e433e58e2 100644 --- a/test/regress/regress0/bv/core/constant_core.smt2 +++ b/test/regress/regress0/bv/core/constant_core.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: ; EXPECT: unsat (set-logic QF_BV) (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/cores/issue3455.smt2 b/test/regress/regress0/cores/issue3455.smt2 index ec72daa32..7050e8c7d 100644 --- a/test/regress/regress0/cores/issue3455.smt2 +++ b/test/regress/regress0/cores/issue3455.smt2 @@ -13,4 +13,4 @@ (assert (<= x0 (- 13))) (check-sat) (check-sat) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/proofs/trust-subs-eq-open.smt2 b/test/regress/regress0/proofs/trust-subs-eq-open.smt2 new file mode 100644 index 000000000..5f6bd9ef9 --- /dev/null +++ b/test/regress/regress0/proofs/trust-subs-eq-open.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun c () (_ BitVec 3)) +(check-sat-assuming ( +(and +(= (_ bv0 1) ((_ extract 1 1) c)) +(= (_ bv1 1) ((_ extract 0 0) c)) +(not (= (_ bv1 2) ((_ extract 1 0) c))))))