diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-13 17:42:57 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-13 17:42:57 -0500 |
commit | 1cb249c9dd06a049953f001cd6d82c0e6f1246f2 (patch) | |
tree | 000398841f1869d9911e1e496623520ffb6de21a /src/expr/proof_rule.h | |
parent | a34f29798b3f4d1f83e1ced57fe53db53b9956f0 (diff) |
(proof-new) SMT Preprocess proof generator (#4708)
This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.
It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.
Diffstat (limited to 'src/expr/proof_rule.h')
-rw-r--r-- | src/expr/proof_rule.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index a15d8a2d2..87e8565ca 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -164,6 +164,16 @@ enum class PfRule : uint32_t // MACRO_SR_PRED_INTRO. MACRO_SR_PRED_TRANSFORM, + //================================================= Processing rules + // ======== Preprocess + // Children: none + // Arguments: (F) + // --------------------------------------------------------------- + // Conclusion: F + // 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. + PREPROCESS, //================================================= Boolean rules // ======== Split // Children: none @@ -171,6 +181,13 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (or F (not F)) SPLIT, + // ======== Equality resolution + // Children: (P1:F1, P2:(= F1 F2)) + // Arguments: none + // --------------------- + // Conclusion: (F2) + // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION. + EQ_RESOLVE, // ======== And elimination // Children: (P:(and F1 ... Fn)) // Arguments: (i) |