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/booleans | |
| 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/booleans')
| -rw-r--r-- | src/theory/booleans/proof_checker.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 6e7cabccd..6a8244ce0 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -21,6 +21,7 @@ namespace booleans { void BoolProofRuleChecker::registerTo(ProofChecker* pc) { pc->registerChecker(PfRule::SPLIT, this); + pc->registerChecker(PfRule::EQ_RESOLVE, this); pc->registerChecker(PfRule::AND_ELIM, this); pc->registerChecker(PfRule::AND_INTRO, this); pc->registerChecker(PfRule::NOT_OR_ELIM, this); @@ -74,6 +75,16 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, return NodeManager::currentNM()->mkNode( kind::OR, args[0], args[0].notNode()); } + if (id == PfRule::EQ_RESOLVE) + { + Assert(children.size() == 2); + Assert(args.empty()); + if (children[1].getKind() != kind::EQUAL || children[0] != children[1][0]) + { + return Node::null(); + } + return children[1][1]; + } // natural deduction rules if (id == PfRule::AND_ELIM) { |