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
// 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 */
/** 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. */
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";
// 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
--- /dev/null
+/********************* */
+/*! \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<Node>& children,
+ const std::vector<Node>& 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<Node> lchildren;
+ std::vector<Node> 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<bool>())
+ {
+ 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<bool>())
+ {
+ return Node::null();
+ }
+ return children[0][0].notNode();
+ }
+ // no rule
+ return Node::null();
+}
+
+} // namespace uf
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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<Node>& children,
+ const std::vector<Node>& args) override;
+};
+
+} // namespace uf
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__UF__PROOF_CHECKER_H */
projects / cvc5.git / commitdiff