diff options
Diffstat (limited to 'src/theory/booleans/proof_checker.cpp')
| -rw-r--r-- | src/theory/booleans/proof_checker.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index d6600f14d..6b9d3e44e 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -25,6 +25,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::SPLIT, this); pc->registerChecker(PfRule::RESOLUTION, this); pc->registerChecker(PfRule::CHAIN_RESOLUTION, this); + pc->registerTrustedChecker(PfRule::MACRO_RESOLUTION_TRUST, this, 3); pc->registerChecker(PfRule::MACRO_RESOLUTION, this); pc->registerChecker(PfRule::FACTORING, this); pc->registerChecker(PfRule::REORDERING, this); @@ -299,6 +300,12 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, : clauseNodes.size() == 1 ? clauseNodes[0] : nm->mkNode(kind::OR, clauseNodes); } + if (id == PfRule::MACRO_RESOLUTION_TRUST) + { + Assert(children.size() > 1); + Assert(args.size() == 2 * (children.size() - 1) + 1); + return args[0]; + } if (id == PfRule::MACRO_RESOLUTION) { Assert(children.size() > 1); |