diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 14:01:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-02 16:01:39 -0300 |
| commit | c17f9b25cac7c0d2941ef136466cb750cf4c3e7b (patch) | |
| tree | 95abb34573b6fd33e2215a7b2cfafc2f27281054 /src/expr/proof_rule.h | |
| parent | a692d44ed5ba0107113df54d2654417bc9f9c345 (diff) | |
(proof-new) Add proof support in TheoryUF (#5002)
This makes TheoryUF use a standard theory inference manager, which thus makes it proof producing when proof-new is enabled.
This additionally cleans HoExtension so that it does not keep a backwards reference to TheoryUF and instead takes its inference manager. This additionally adds two rules for higher-order that are required to make its equality engine proofs correct.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
Diffstat (limited to 'src/expr/proof_rule.h')
| -rw-r--r-- | src/expr/proof_rule.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 59c406d28..b6b9f1ea8 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -520,6 +520,20 @@ enum class PfRule : uint32_t // ---------------------------------------- // Conclusion: (not F) FALSE_ELIM, + // ======== HO trust + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t)) + // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y) + HO_APP_ENCODE, + // ======== Congruence + // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn)) + // Arguments: () + // --------------------------------------------- + // Conclusion: (= (f t1 ... tn) (g s1 ... sn)) + // Notice that this rule is only used when the application kinds are APPLY_UF. + HO_CONG, //================================================= Quantifiers rules // ======== Witness intro |