Includes adding the standard method for constructing the extensionality skolem using the skolem manager.
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
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";
// 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])
--- /dev/null
+/********************* */
+/*! \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
--- /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 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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
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;
}
#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"
/** 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);
projects / cvc5.git / commitdiff