// ---------------------
// Conclusion: F
ARRAYS_TRUST,
+
+ //================================================= Datatype rules
+ // ======== Unification
+ // Children: (P:(= (C t1 ... tn) (C s1 ... sn)))
+ // Arguments: (i)
+ // ----------------------------------------
+ // Conclusion: (= ti si)
+ // where C is a constructor.
+ DT_UNIF,
+ // ======== Instantiate
+ // Children: none
+ // Arguments: (t, n)
+ // ----------------------------------------
+ // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t))))
+ // where C is the n^th constructor of the type of T, and (_ is C) is the
+ // discriminator (tester) for C.
+ DT_INST,
+ // ======== Collapse
+ // Children: none
+ // Arguments: ((sel_i (C_j t_1 ... t_n)))
+ // ----------------------------------------
+ // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r)
+ // where C_j is a constructor, r is t_i if sel_i is a correctly applied
+ // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice
+ // that the use of mkGroundTerm differs from the rewriter which uses
+ // mkGroundValue in this case.
+ DT_COLLAPSE,
+ // ======== Split
+ // Children: none
+ // Arguments: (t)
+ // ----------------------------------------
+ // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t))
+ DT_SPLIT,
+ // ======== Clash
+ // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t))
+ // Arguments: none
+ // ----------------------------------------
+ // Conclusion: false
+ // for i != j.
+ DT_CLASH,
+ // ======== Datatype Trust
+ // Children: (P1 ... Pn)
+ // Arguments: (F)
+ // ---------------------
+ // Conclusion: F
+ DT_TRUST,
//================================================= Quantifiers rules
// ======== Witness intro
--- /dev/null
+/********************* */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 datatypes proof checker
+ **/
+
+#include "theory/datatypes/proof_checker.h"
+
+#include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+void DatatypesProofRuleChecker::registerTo(ProofChecker* pc)
+{
+ pc->registerChecker(PfRule::DT_UNIF, this);
+ pc->registerChecker(PfRule::DT_INST, this);
+ pc->registerChecker(PfRule::DT_COLLAPSE, this);
+ pc->registerChecker(PfRule::DT_SPLIT, this);
+ pc->registerChecker(PfRule::DT_CLASH, this);
+ // trusted rules
+ pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2);
+}
+
+Node DatatypesProofRuleChecker::checkInternal(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ if (id == PfRule::DT_UNIF)
+ {
+ Assert(children.size() == 1);
+ Assert(args.size() == 1);
+ uint32_t i;
+ if (children[0].getKind() != kind::EQUAL
+ || children[0][0].getKind() != kind::APPLY_CONSTRUCTOR
+ || children[0][1].getKind() != kind::APPLY_CONSTRUCTOR
+ || children[0][0].getOperator() != children[0][1].getOperator()
+ || !getUInt32(args[0], i))
+ {
+ return Node::null();
+ }
+ if (i >= children[0][0].getNumChildren())
+ {
+ return Node::null();
+ }
+ Assert(children[0][0].getNumChildren() == children[0][1].getNumChildren());
+ return children[0][0][i].eqNode(children[0][1][i]);
+ }
+ else if (id == PfRule::DT_INST)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 2);
+ Node t = args[0];
+ TypeNode tn = t.getType();
+ uint32_t i;
+ if (!tn.isDatatype() || !getUInt32(args[1], i))
+ {
+ return Node::null();
+ }
+ const DType& dt = tn.getDType();
+ if (i >= dt.getNumConstructors())
+ {
+ return Node::null();
+ }
+ Node tester = utils::mkTester(t, i, dt);
+ Node ticons = Rewriter::rewrite(utils::getInstCons(t, dt, i));
+ return tester.eqNode(t.eqNode(ticons));
+ }
+ else if (id == PfRule::DT_COLLAPSE)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ Node t = args[0];
+ if (t.getKind() != kind::APPLY_SELECTOR_TOTAL
+ || t[0].getKind() != kind::APPLY_CONSTRUCTOR)
+ {
+ return Node::null();
+ }
+ Node selector = t.getOperator();
+ size_t constructorIndex = utils::indexOf(t[0].getOperator());
+ const DType& dt = utils::datatypeOf(selector);
+ const DTypeConstructor& dtc = dt[constructorIndex];
+ int selectorIndex = dtc.getSelectorIndexInternal(selector);
+ Node r =
+ selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex];
+ return t.eqNode(r);
+ }
+ else if (id == PfRule::DT_SPLIT)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ TypeNode tn = args[0].getType();
+ if (!tn.isDatatype())
+ {
+ return Node::null();
+ }
+ const DType& dt = tn.getDType();
+ return utils::mkSplit(args[0], dt);
+ }
+ else if (id == PfRule::DT_CLASH)
+ {
+ Assert(children.size() == 2);
+ Assert(args.empty());
+ if (children[0].getKind() != kind::APPLY_TESTER
+ || children[1].getKind() != kind::APPLY_TESTER
+ || children[0][0] != children[1][0] || children[0] == children[1])
+ {
+ return Node::null();
+ }
+ return nm->mkConst(false);
+ }
+ else if (id == PfRule::DT_TRUST)
+ {
+ Assert(!args.empty());
+ Assert(args[0].getType().isBoolean());
+ return args[0];
+ }
+ // no rule
+ return Node::null();
+}
+
+} // namespace datatypes
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file proof_checker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Datatypes proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__DATATYPES__PROOF_CHECKER_H
+#define CVC4__THEORY__DATATYPES__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+/** A checker for array reasoning in proofs */
+class DatatypesProofRuleChecker : public ProofRuleChecker
+{
+ public:
+ DatatypesProofRuleChecker() {}
+ ~DatatypesProofRuleChecker() {}
+
+ /** 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 datatypes
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__DATATYPES__PROOF_CHECKER_H */
projects / cvc5.git / commitdiff