From 44fd0bd8441d9dcce5aa9173757c9d8173924c17 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Sep 2020 12:09:33 -0500 Subject: [PATCH] (proof-new) Add the arrays proof checker (#5047) Includes adding the standard method for constructing the extensionality skolem using the skolem manager. --- src/CMakeLists.txt | 4 + src/expr/proof_rule.cpp | 7 ++ src/expr/proof_rule.h | 33 ++++++++ src/theory/arrays/proof_checker.cpp | 118 ++++++++++++++++++++++++++++ src/theory/arrays/proof_checker.h | 49 ++++++++++++ src/theory/arrays/skolem_cache.cpp | 87 ++++++++++++++++++++ src/theory/arrays/skolem_cache.h | 57 ++++++++++++++ src/theory/arrays/theory_arrays.cpp | 6 ++ src/theory/arrays/theory_arrays.h | 4 + 9 files changed, 365 insertions(+) create mode 100644 src/theory/arrays/proof_checker.cpp create mode 100644 src/theory/arrays/proof_checker.h create mode 100644 src/theory/arrays/skolem_cache.cpp create mode 100644 src/theory/arrays/skolem_cache.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5695e271e..a72a5f6bb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -366,6 +366,10 @@ libcvc4_add_sources( theory/arith/type_enumerator.h theory/arrays/array_info.cpp theory/arrays/array_info.h + theory/arrays/proof_checker.cpp + theory/arrays/proof_checker.h + theory/arrays/skolem_cache.cpp + theory/arrays/skolem_cache.h theory/arrays/theory_arrays.cpp theory/arrays/theory_arrays.h theory/arrays/theory_arrays_rewriter.cpp diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 57dd3e0bd..400567b5d 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -102,6 +102,13 @@ const char* toString(PfRule id) case PfRule::FALSE_ELIM: return "FALSE_ELIM"; case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE"; case PfRule::HO_CONG: return "HO_CONG"; + //================================================= Array rules + case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; + case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA: + return "ARRAYS_READ_OVER_WRITE_CONTRA"; + 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"; //================================================= 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 c02292dab..a51cb92f0 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -595,6 +595,39 @@ enum class PfRule : uint32_t // Notice that this rule is only used when the application kinds are APPLY_UF. HO_CONG, + //================================================= Array rules + // ======== Read over write + // Children: (P:(not (= i1 i2))) + // Arguments: ((select (store a i2 e) i1)) + // ---------------------------------------- + // Conclusion: (= (select (store a i2 e) i1) (select a i1)) + ARRAYS_READ_OVER_WRITE, + // ======== Read over write, contrapositive + // Children: (P:(not (= (select (store a i2 e) i1) (select a i1))) + // Arguments: none + // ---------------------------------------- + // Conclusion: (= i1 i2) + ARRAYS_READ_OVER_WRITE_CONTRA, + // ======== Read over write 1 + // Children: none + // Arguments: ((select (store a i e) i)) + // ---------------------------------------- + // Conclusion: (= (select (store a i e) i) e) + ARRAYS_READ_OVER_WRITE_1, + // ======== Extensionality + // Children: (P:(not (= a b))) + // Arguments: none + // ---------------------------------------- + // Conclusion: (not (= (select a k) (select b k))) + // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))). + ARRAYS_EXT, + // ======== Array Trust + // Children: (P1 ... Pn) + // Arguments: (F) + // --------------------- + // Conclusion: F + ARRAYS_TRUST, + //================================================= Quantifiers rules // ======== Witness intro // Children: (P:F[t]) diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp new file mode 100644 index 000000000..a3cd82678 --- /dev/null +++ b/src/theory/arrays/proof_checker.cpp @@ -0,0 +1,118 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** 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 arrays proof checker + **/ + +#include "theory/arrays/proof_checker.h" +#include "expr/skolem_manager.h" +#include "theory/arrays/skolem_cache.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +void ArraysProofRuleChecker::registerTo(ProofChecker* pc) +{ + pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE, this); + pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this); + pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this); + pc->registerChecker(PfRule::ARRAYS_EXT, this); + // trusted rules + pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2); +} + +Node ArraysProofRuleChecker::checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) +{ + NodeManager* nm = NodeManager::currentNM(); + if (id == PfRule::ARRAYS_READ_OVER_WRITE) + { + Assert(children.size() == 1); + Assert(args.size() == 1); + Node ideq = children[0]; + if (ideq.getKind() != kind::NOT || ideq[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + Node lhs = args[0]; + if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE + || lhs[0][1] != ideq[0][0]) + { + return Node::null(); + } + Node rhs = nm->mkNode(kind::SELECT, lhs[0][0], ideq[0][1]); + return lhs.eqNode(rhs); + } + else if (id == PfRule::ARRAYS_READ_OVER_WRITE_CONTRA) + { + Assert(children.size() == 1); + Assert(args.empty()); + Node adeq = children[0]; + if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + Node lhs = adeq[0][0]; + Node rhs = adeq[0][1]; + if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE + || rhs.getKind() != kind::SELECT || lhs[1] != rhs[1]) + { + return Node::null(); + } + return lhs[1].eqNode(lhs[0][1]); + } + if (id == PfRule::ARRAYS_READ_OVER_WRITE_1) + { + Assert(children.empty()); + Assert(args.size() == 1); + Node lhs = args[0]; + if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE + || lhs[0][1] != lhs[1]) + { + return Node::null(); + } + Node rhs = lhs[0][2]; + return lhs.eqNode(rhs); + } + if (id == PfRule::ARRAYS_EXT) + { + Assert(children.size() == 1); + Assert(args.empty()); + Node adeq = children[0]; + if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL + || !adeq[0][0].getType().isArray()) + { + return Node::null(); + } + Node k = SkolemCache::getExtIndexSkolem(adeq); + Node a = adeq[0][0]; + Node b = adeq[0][1]; + Node as = nm->mkNode(kind::SELECT, a, k); + Node bs = nm->mkNode(kind::SELECT, b, k); + return as.eqNode(bs).notNode(); + } + if (id == PfRule::ARRAYS_TRUST) + { + // "trusted" rules + Assert(!args.empty()); + Assert(args[0].getType().isBoolean()); + return args[0]; + } + // no rule + return Node::null(); +} + +} // namespace arrays +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h new file mode 100644 index 000000000..3bf7afecb --- /dev/null +++ b/src/theory/arrays/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 Array proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARRAYS__PROOF_CHECKER_H +#define CVC4__THEORY__ARRAYS__PROOF_CHECKER_H + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +/** A checker for array reasoning in proofs */ +class ArraysProofRuleChecker : public ProofRuleChecker +{ + public: + ArraysProofRuleChecker() {} + ~ArraysProofRuleChecker() {} + + /** 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 arrays +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARRAYS__PROOF_CHECKER_H */ diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp new file mode 100644 index 000000000..70217a4d7 --- /dev/null +++ b/src/theory/arrays/skolem_cache.cpp @@ -0,0 +1,87 @@ +/********************* */ +/*! \file skolem_cache.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 Arrays skolem cache + **/ + +#include "theory/arrays/skolem_cache.h" + +#include "expr/attribute.h" +#include "expr/skolem_manager.h" +#include "expr/type_node.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arrays { + +/** + * A bound variable corresponding to an index for witnessing the satisfiability + * of array disequalities. + */ +struct ExtIndexVarAttributeId +{ +}; +typedef expr::Attribute ExtIndexVarAttribute; + +SkolemCache::SkolemCache() {} + +Node SkolemCache::getExtIndexSkolem(Node deq) +{ + Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL); + Node a = deq[0][0]; + Node b = deq[0][1]; + Assert(a.getType().isArray()); + Assert(b.getType() == a.getType()); + + NodeManager* nm = NodeManager::currentNM(); + + // get the reference index, which notice is deterministic for a, b in the + // lifetime of the node manager + Node x = getExtIndexVar(deq); + + // make the axiom for x + Node as = nm->mkNode(SELECT, a, x); + Node bs = nm->mkNode(SELECT, b, x); + Node deqIndex = as.eqNode(bs).notNode(); + Node axiom = nm->mkNode(IMPLIES, deq, deqIndex); + + // make the skolem that witnesses the above axiom + SkolemManager* sm = nm->getSkolemManager(); + return sm->mkSkolem( + x, + axiom, + "array_ext_index", + "an extensional lemma index variable from the theory of arrays"); +} + +Node SkolemCache::getExtIndexVar(Node deq) +{ + ExtIndexVarAttribute eiva; + if (deq.hasAttribute(eiva)) + { + return deq.getAttribute(eiva); + } + Node a = deq[0][0]; + Node b = deq[0][1]; + TypeNode atn = a.getType(); + Assert(atn.isArray()); + Assert(atn == b.getType()); + TypeNode atnIndex = atn.getArrayIndexType(); + Node v = NodeManager::currentNM()->mkBoundVar(atnIndex); + deq.setAttribute(eiva, v); + return v; +} + +} // namespace arrays +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h new file mode 100644 index 000000000..b07e87dc6 --- /dev/null +++ b/src/theory/arrays/skolem_cache.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file skolem_cache.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 Arrays skolem cache + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARRAYS__SKOLEM_CACHE_H +#define CVC4__THEORY__ARRAYS__SKOLEM_CACHE_H + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +/** + * The arrays skolem cache, which provides static methods for constructing + * skolems with witness forms. + */ +class SkolemCache +{ + public: + SkolemCache(); + ~SkolemCache() {} + + /** + * Get the skolem correspoding to the index that witnesses the disequality + * deq between arrays a and b. The witness form of this skolem is: + * (witness ((x T)) (=> (not (= a b)) (not (= (select a x) (select b x))))) + * This skolem is unique for deq, calling this method will always return the + * same skolem over the lifetime of deq. + */ + static Node getExtIndexSkolem(Node deq); + + private: + /** + * Get the bound variable x of the witness term above for disequality deq + * between arrays. + */ + static Node getExtIndexVar(Node deq); +}; + +} // namespace arrays +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 28953ab05..cfa956f8b 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -126,6 +126,12 @@ TheoryArrays::TheoryArrays(context::Context* c, d_ppEqualityEngine.addFunctionKind(kind::SELECT); d_ppEqualityEngine.addFunctionKind(kind::STORE); + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + d_pchecker.registerTo(pc); + } + // indicate we are using the default theory state object d_theoryState = &d_state; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index dea3d4136..a35074f15 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -26,6 +26,7 @@ #include "context/cdhashset.h" #include "context/cdqueue.h" #include "theory/arrays/array_info.h" +#include "theory/arrays/proof_checker.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -341,6 +342,9 @@ class TheoryArrays : public Theory { /** The notify class for d_equalityEngine */ NotifyClass d_notify; + /** The proof checker */ + ArraysProofRuleChecker d_pchecker; + /** Conflict when merging constants */ void conflict(TNode a, TNode b); -- 2.30.2