diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-07 12:44:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-07 17:44:20 +0000 |
| commit | 7e9e71c7bd2bcbdcb2cef0d8f99bf34082bf4081 (patch) | |
| tree | 201fe80043ddb91a72f56f34c2906ef990ad6faf /src/proof | |
| parent | 4cb2b23322794fc684db4f4a9f9e14e0157c83b0 (diff) | |
(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.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/proof_rule.cpp | 1 | ||||
| -rw-r--r-- | src/proof/proof_rule.h | 11 |
2 files changed, 10 insertions, 2 deletions
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 |