diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-21 12:09:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-21 12:09:33 -0500 |
commit | 44fd0bd8441d9dcce5aa9173757c9d8173924c17 (patch) | |
tree | db47d0c29fffeca7301d83ab6ef4320ccd37701b /src/theory/arrays | |
parent | 63e7c6bb6d9c99a5282241be8b32a04ea67dfb8d (diff) |
(proof-new) Add the arrays proof checker (#5047)
Includes adding the standard method for constructing the extensionality skolem using the skolem manager.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/proof_checker.cpp | 118 | ||||
-rw-r--r-- | src/theory/arrays/proof_checker.h | 49 | ||||
-rw-r--r-- | src/theory/arrays/skolem_cache.cpp | 87 | ||||
-rw-r--r-- | src/theory/arrays/skolem_cache.h | 57 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 4 |
6 files changed, 321 insertions, 0 deletions
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<Node>& children, + const std::vector<Node>& 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<Node>& children, + const std::vector<Node>& 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<ExtIndexVarAttributeId, Node> 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); |