diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 11:41:26 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-12 09:41:26 -0700 |
| commit | 9d1ce085de6df543d9d9a2fa9b8fa9001feb4b6b (patch) | |
| tree | 023474f131ee9f21e829fc623e31de808b9235d5 /src/expr/proof_rule.h | |
| parent | 3f77b4ac0d4ff8ab69e2f2932e9ced088bd339ed (diff) | |
(proof-new) Witness form proof generator (#4782)
This class is responsible for the connection between terms and their witness form in the final proof.
Diffstat (limited to 'src/expr/proof_rule.h')
| -rw-r--r-- | src/expr/proof_rule.h | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 62bc77cfb..3d468d08e 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -174,7 +174,7 @@ enum class PfRule : uint32_t THEORY_REWRITE, //================================================= Processing rules - // ======== Preprocess + // ======== Preprocess (trusted) // Children: none // Arguments: (F) // --------------------------------------------------------------- @@ -183,6 +183,14 @@ enum class PfRule : uint32_t // based on some preprocessing pass, or otherwise F was added as a new // assertion by some preprocessing pass. PREPROCESS, + // ======== Witness axiom (trusted) + // Children: none + // Arguments: (F) + // --------------------------------------------------------------- + // Conclusion: F + // where F is an existential (exists ((x T)) (P x)) used for introducing + // a witness term (witness ((x T)) (P x)). + WITNESS_AXIOM, // ======== Remove Term Formulas Axiom // Children: none // Arguments: (t) |