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/theory/builtin/proof_checker.cpp | |
| 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/theory/builtin/proof_checker.cpp')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index f6b41104a..a8249ae7c 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -59,6 +59,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this); pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this); pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); + pc->registerChecker(PfRule::PREPROCESS, this); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -309,6 +310,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } return args[0]; } + else if (id == PfRule::PREPROCESS) + { + Assert(children.empty()); + Assert(args.size() == 1); + return args[0]; + } // no rule return Node::null(); } |