summaryrefslogtreecommitdiff
path: root/src/expr/proof_rule.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-08-12 16:34:47 -0500
committerGitHub <noreply@github.com>2020-08-12 18:34:47 -0300
commit85a8dfddd887a041f397d1ff2c3a6c34900c5775 (patch)
tree81344647d0ac9c61040dfa3954c8200c8efbf561 /src/expr/proof_rule.h
parentbd184f9813a91d8f60eb0521893a5154b9f92357 (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.h9
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback