diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-27 15:33:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-27 13:33:12 -0700 |
| commit | b90cfb462bde3e75c07bb14e2393ee8e4b4f4d42 (patch) | |
| tree | 4e7f89713008787557ae1293c6d0149e185c9b66 /src/theory/builtin | |
| parent | faa97a6f1ee19760dfb0a79ad18c53afdff6b09a (diff) | |
(proof-new) Proof production for term formula removal (#4687)
This adds proof support in the term formula removal pass.
It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.
Diffstat (limited to 'src/theory/builtin')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 59f405337..817d21fdf 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -15,6 +15,7 @@ #include "theory/builtin/proof_checker.h" #include "expr/skolem_manager.h" +#include "smt/term_formula_removal.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -61,6 +62,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); pc->registerChecker(PfRule::THEORY_REWRITE, this); pc->registerChecker(PfRule::PREPROCESS, this); + pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this); } Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite) @@ -321,6 +323,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } return args[0]; } + else if (id == PfRule::REMOVE_TERM_FORMULA_AXIOM) + { + Assert(children.empty()); + Assert(args.size() == 1); + return RemoveTermFormulas::getAxiomFor(args[0]); + } else if (id == PfRule::PREPROCESS) { Assert(children.empty()); |