From 04640a15faeee34b064dc4f1d2045300c2a6f329 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Oct 2020 12:33:01 -0500 Subject: [PATCH] (proof-new) Add datatypes proof checker (#5340) This adds the proof rules and proof checker for datatypes. --- src/expr/proof_rule.cpp | 7 ++ src/expr/proof_rule.h | 46 +++++++++ src/theory/datatypes/proof_checker.cpp | 135 +++++++++++++++++++++++++ src/theory/datatypes/proof_checker.h | 49 +++++++++ 4 files changed, 237 insertions(+) create mode 100644 src/theory/datatypes/proof_checker.cpp create mode 100644 src/theory/datatypes/proof_checker.h diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 9448e1939..4ba483101 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -114,6 +114,13 @@ const char* toString(PfRule id) case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; + //================================================= Datatype rules + case PfRule::DT_UNIF: return "DT_UNIF"; + case PfRule::DT_INST: return "DT_INST"; + case PfRule::DT_COLLAPSE: return "DT_COLLAPSE"; + case PfRule::DT_SPLIT: return "DT_SPLIT"; + case PfRule::DT_CLASH: return "DT_CLASH"; + case PfRule::DT_TRUST: return "DT_TRUST"; //================================================= Quantifiers rules case PfRule::WITNESS_INTRO: return "WITNESS_INTRO"; case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 2b5565318..19efe6285 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -674,6 +674,52 @@ enum class PfRule : uint32_t // --------------------- // 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 diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp new file mode 100644 index 000000000..98060480b --- /dev/null +++ b/src/theory/datatypes/proof_checker.cpp @@ -0,0 +1,135 @@ +/********************* */ +/*! \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& children, + const std::vector& 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 diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h new file mode 100644 index 000000000..e5bd7cad5 --- /dev/null +++ b/src/theory/datatypes/proof_checker.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \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& children, + const std::vector& args) override; +}; + +} // namespace datatypes +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__DATATYPES__PROOF_CHECKER_H */ -- 2.30.2