From: Haniel Barbosa Date: Wed, 3 Jun 2020 23:52:49 +0000 (-0300) Subject: (proof-new) Adding rules and proof checker for EUF (#4559) X-Git-Tag: cvc5-1.0.0~3262 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=418b0281e62a6b657da32f6504965269ad90c18b;p=cvc5.git (proof-new) Adding rules and proof checker for EUF (#4559) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 97c352d5d..44b5dfeaf 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -754,6 +754,8 @@ libcvc4_add_sources( theory/uf/equality_engine.cpp theory/uf/equality_engine.h theory/uf/equality_engine_types.h + theory/uf/proof_checker.cpp + theory/uf/proof_checker.h theory/uf/ho_extension.cpp theory/uf/ho_extension.h theory/uf/symmetry_breaker.cpp diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7bc98f65d..427afd5af 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -865,4 +865,26 @@ void NodeManager::debugHook(int debugFlag){ // For debugging purposes only, DO NOT CHECK IN ANY CODE! } +Kind NodeManager::getKindForFunction(TNode fun) +{ + TypeNode tn = fun.getType(); + if (tn.isFunction()) + { + return kind::APPLY_UF; + } + else if (tn.isConstructor()) + { + return kind::APPLY_CONSTRUCTOR; + } + else if (tn.isSelector()) + { + return kind::APPLY_SELECTOR; + } + else if (tn.isTester()) + { + return kind::APPLY_TESTER; + } + return kind::UNDEFINED_KIND; +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 45d3d5b7d..1fab328e9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -444,6 +444,20 @@ public: /** Get a Kind from an operator expression */ static inline Kind operatorToKind(TNode n); + /** Get corresponding application kind for function + * + * Different functional nodes are applied differently, according to their + * type. For example, uninterpreted functions (of FUNCTION_TYPE) are applied + * via APPLY_UF, while constructors (of CONSTRUCTOR_TYPE) via + * APPLY_CONSTRUCTOR. This method provides the correct application according + * to which functional type fun has. + * + * @param fun The functional node + * @return the correct application kind for fun. If fun's type is not function + * like (see TypeNode::isFunctionLike), then UNDEFINED_KIND is returned. + */ + static Kind getKindForFunction(TNode fun); + // general expression-builders /** Create a node with one child. */ diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 0e73d8c10..595e1d5f7 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -31,7 +31,15 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; - + //================================================= Equality rules + case PfRule::REFL: return "REFL"; + case PfRule::SYMM: return "SYMM"; + case PfRule::TRANS: return "TRANS"; + case PfRule::CONG: return "CONG"; + case PfRule::TRUE_INTRO: return "TRUE_INTRO"; + case PfRule::TRUE_ELIM: return "TRUE_ELIM"; + case PfRule::FALSE_INTRO: return "FALSE_INTRO"; + case PfRule::FALSE_ELIM: return "FALSE_ELIM"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; case PfRule::AND_ELIM: return "AND_ELIM"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 9dc1d017f..6acccfffd 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -71,6 +71,56 @@ enum class PfRule : uint32_t // has the conclusion (=> F F) and has no free assumptions. More generally, a // proof with no free assumptions always concludes a valid formula. SCOPE, + //================================================= Equality rules + // ======== Reflexive + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= t t) + REFL, + // ======== Symmetric + // Children: (P:(= t1 t2)) or (P:(not (= t1 t2))) + // Arguments: none + // ----------------------- + // Conclusion: (= t2 t1) or (not (= t2 t1)) + SYMM, + // ======== Transitivity + // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn)) + // Arguments: none + // ----------------------- + // Conclusion: (= t1 tn) + TRANS, + // ======== Congruence (subsumed by Substitute?) + // Children: (P1:(= t1 s1), ..., Pn:(= tn sn)) + // Arguments: (f) + // --------------------------------------------- + // Conclusion: (= (f t1 ... tn) (f s1 ... sn)) + CONG, + // ======== True intro + // Children: (P:F) + // Arguments: none + // ---------------------------------------- + // Conclusion: (= F true) + TRUE_INTRO, + // ======== True elim + // Children: (P:(= F true) + // Arguments: none + // ---------------------------------------- + // Conclusion: F + TRUE_ELIM, + // ======== False intro + // Children: (P:(not F)) + // Arguments: none + // ---------------------------------------- + // Conclusion: (= F false) + FALSE_INTRO, + // ======== False elim + // Children: (P:(= F false) + // Arguments: none + // ---------------------------------------- + // Conclusion: (not F) + FALSE_ELIM, + //================================================= Boolean rules // ======== Split // Children: none diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp new file mode 100644 index 000000000..28ae34b7b --- /dev/null +++ b/src/theory/uf/proof_checker.cpp @@ -0,0 +1,172 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of equality proof checker + **/ + +#include "theory/uf/proof_checker.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace uf { + +void UfProofRuleChecker::registerTo(ProofChecker* pc) +{ + // add checkers + pc->registerChecker(PfRule::REFL, this); + pc->registerChecker(PfRule::SYMM, this); + pc->registerChecker(PfRule::TRANS, this); + pc->registerChecker(PfRule::CONG, this); + pc->registerChecker(PfRule::TRUE_INTRO, this); + pc->registerChecker(PfRule::TRUE_ELIM, this); + pc->registerChecker(PfRule::FALSE_INTRO, this); + pc->registerChecker(PfRule::FALSE_ELIM, this); +} + +Node UfProofRuleChecker::checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) +{ + // compute what was proven + if (id == PfRule::REFL) + { + Assert(children.empty()); + Assert(args.size() == 1); + return args[0].eqNode(args[0]); + } + else if (id == PfRule::SYMM) + { + Assert(children.size() == 1); + Assert(args.empty()); + bool polarity = children[0].getKind() != NOT; + Node eqp = polarity ? children[0] : children[0][0]; + if (eqp.getKind() != EQUAL) + { + // not a (dis)equality + return Node::null(); + } + Node conc = eqp[1].eqNode(eqp[0]); + return polarity ? conc : conc.notNode(); + } + else if (id == PfRule::TRANS) + { + Assert(children.size() > 0); + Assert(args.empty()); + Node first; + Node curr; + for (size_t i = 0, nchild = children.size(); i < nchild; i++) + { + Node eqp = children[i]; + if (eqp.getKind() != EQUAL) + { + return Node::null(); + } + if (first.isNull()) + { + first = eqp[0]; + } + else if (eqp[0] != curr) + { + return Node::null(); + } + curr = eqp[1]; + } + return first.eqNode(curr); + } + else if (id == PfRule::CONG) + { + Assert(children.size() > 0); + Assert(args.size() == 1); + // We do congruence over builtin kinds using operatorToKind + std::vector lchildren; + std::vector rchildren; + // get the expected kind for args[0] + Kind k = NodeManager::getKindForFunction(args[0]); + if (k == kind::UNDEFINED_KIND) + { + k = NodeManager::operatorToKind(args[0]); + } + if (k == kind::UNDEFINED_KIND) + { + return Node::null(); + } + Trace("uf-pfcheck") << "congruence for " << args[0] << " uses kind " << k + << ", metakind=" << kind::metaKindOf(k) << std::endl; + if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED) + { + // parameterized kinds require the operator + lchildren.push_back(args[0]); + rchildren.push_back(args[0]); + } + 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(k, lchildren); + Node r = nm->mkNode(k, rchildren); + return l.eqNode(r); + } + else if (id == PfRule::TRUE_INTRO) + { + Assert(children.size() == 1); + Assert(args.empty()); + Node trueNode = NodeManager::currentNM()->mkConst(true); + return children[0].eqNode(trueNode); + } + else if (id == PfRule::TRUE_ELIM) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != EQUAL || !children[0][1].isConst() + || !children[0][1].getConst()) + { + return Node::null(); + } + return children[0][0]; + } + else if (id == PfRule::FALSE_INTRO) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT) + { + return Node::null(); + } + Node falseNode = NodeManager::currentNM()->mkConst(false); + return children[0][0].eqNode(falseNode); + } + else if (id == PfRule::FALSE_ELIM) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != EQUAL || !children[0][1].isConst() + || children[0][1].getConst()) + { + return Node::null(); + } + return children[0][0].notNode(); + } + // no rule + return Node::null(); +} + +} // namespace uf +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h new file mode 100644 index 000000000..022574eab --- /dev/null +++ b/src/theory/uf/proof_checker.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file proof_checker.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Equality proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__UF__PROOF_CHECKER_H +#define CVC4__THEORY__UF__PROOF_CHECKER_H + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +/** A checker for builtin proofs */ +class UfProofRuleChecker : public ProofRuleChecker +{ + public: + UfProofRuleChecker() {} + ~UfProofRuleChecker() {} + + /** Register all rules owned by this rule checker into pc. */ + void registerTo(ProofChecker* pc) override; + + protected: + /** Return the conclusion of the given proof step, or null if it is invalid */ + Node checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) override; +}; + +} // namespace uf +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__UF__PROOF_CHECKER_H */