diff options
Diffstat (limited to 'src/theory/uf/proof_checker.cpp')
-rw-r--r-- | src/theory/uf/proof_checker.cpp | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp index b010b6d17..ea95c1f24 100644 --- a/src/theory/uf/proof_checker.cpp +++ b/src/theory/uf/proof_checker.cpp @@ -14,6 +14,8 @@ #include "theory/uf/proof_checker.h" +#include "theory/uf/theory_uf_rewriter.h" + using namespace CVC4::kind; namespace CVC4 { @@ -31,6 +33,8 @@ void UfProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::TRUE_ELIM, this); pc->registerChecker(PfRule::FALSE_INTRO, this); pc->registerChecker(PfRule::FALSE_ELIM, this); + pc->registerChecker(PfRule::HO_CONG, this); + pc->registerChecker(PfRule::HO_APP_ENCODE, this); } Node UfProofRuleChecker::checkInternal(PfRule id, @@ -171,6 +175,32 @@ Node UfProofRuleChecker::checkInternal(PfRule id, } return children[0][0].notNode(); } + if (id == PfRule::HO_CONG) + { + Assert(children.size() > 0); + std::vector<Node> lchildren; + std::vector<Node> rchildren; + for (size_t i = 0, nchild = children.size(); i < nchild; ++i) + { + Node eqp = children[i]; + if (eqp.getKind() != EQUAL) + { + return Node::null(); + } + lchildren.push_back(eqp[0]); + rchildren.push_back(eqp[1]); + } + NodeManager* nm = NodeManager::currentNM(); + Node l = nm->mkNode(kind::APPLY_UF, lchildren); + Node r = nm->mkNode(kind::APPLY_UF, rchildren); + return l.eqNode(r); + } + else if (id == PfRule::HO_APP_ENCODE) + { + Assert(args.size() == 1); + Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]); + return args[0].eqNode(ret); + } // no rule return Node::null(); } |