diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 16:34:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-12 18:34:47 -0300 |
commit | 85a8dfddd887a041f397d1ff2c3a6c34900c5775 (patch) | |
tree | 81344647d0ac9c61040dfa3954c8200c8efbf561 /src/expr/proof_rule.h | |
parent | bd184f9813a91d8f60eb0521893a5154b9f92357 (diff) |
(proof-new) Improve robustness of CONG rule (#4882)
This makes it so that the explicit Kind is wrapped in a Node as an argument to the CONG proof rule. This allows us to distinguish applications with the same parameterized operator but different kinds (e.g. APPLY_SELECTOR vs APPLY_SELECTOR_TOTAL).
Diffstat (limited to 'src/expr/proof_rule.h')
-rw-r--r-- | src/expr/proof_rule.h | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index beff92bd4..364598cf4 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -481,11 +481,14 @@ enum class PfRule : uint32_t // ----------------------- // Conclusion: (= t1 tn) TRANS, - // ======== Congruence (subsumed by Substitute?) + // ======== Congruence // Children: (P1:(= t1 s1), ..., Pn:(= tn sn)) - // Arguments: (f) + // Arguments: (<kind> f?) // --------------------------------------------- - // Conclusion: (= (f t1 ... tn) (f s1 ... sn)) + // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn)) + // Notice that f must be provided iff <kind> is a parameterized kind, e.g. + // APPLY_UF. The actual node for <kind> is constructible via + // ProofRuleChecker::mkKindNode. CONG, // ======== True intro // Children: (P:F) |