From 4c87b04c95b60c34d2e8313e82579fbb0415eaf7 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 27 Jul 2021 12:39:53 -0700 Subject: [PATCH] proof: Add eqrange expansion rule. (#6936) Adds proof support for the eqrange operator. Co-authored-by: Andrew Reynolds --- src/proof/proof_rule.cpp | 1 + src/proof/proof_rule.h | 9 ++ src/theory/arrays/proof_checker.cpp | 8 ++ src/theory/arrays/skolem_cache.cpp | 15 +++ src/theory/arrays/skolem_cache.h | 7 ++ src/theory/arrays/theory_arrays.cpp | 1 + src/theory/arrays/theory_arrays_rewriter.cpp | 103 +++++++++++-------- src/theory/arrays/theory_arrays_rewriter.h | 25 +++-- 8 files changed, 119 insertions(+), 50 deletions(-) diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 3991305ca..7e1cdf8d3 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -120,6 +120,7 @@ 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"; + case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND"; //================================================= Bit-Vector rules case PfRule::BV_BITBLAST: return "BV_BITBLAST"; case PfRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 173e4df9a..78e773bdc 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -713,6 +713,15 @@ enum class PfRule : uint32_t // Conclusion: (not (= (select a k) (select b k))) // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))). ARRAYS_EXT, + // ======== EQ_RANGE expansion + // Children: none + // Arguments: ((eqrange a b i j)) + // ---------------------------------------- + // Conclusion: (= + // (eqrange a b i j) + // (forall ((x T)) + // (=> (and (<= i x) (<= x j)) (= (select a x) (select b x))))) + ARRAYS_EQ_RANGE_EXPAND, // ======== Array Trust // Children: (P1 ... Pn) // Arguments: (F) diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp index f8c5b2669..6d546d746 100644 --- a/src/theory/arrays/proof_checker.cpp +++ b/src/theory/arrays/proof_checker.cpp @@ -14,8 +14,10 @@ */ #include "theory/arrays/proof_checker.h" + #include "expr/skolem_manager.h" #include "theory/arrays/skolem_cache.h" +#include "theory/arrays/theory_arrays_rewriter.h" #include "theory/rewriter.h" namespace cvc5 { @@ -28,6 +30,7 @@ void ArraysProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this); pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this); pc->registerChecker(PfRule::ARRAYS_EXT, this); + pc->registerChecker(PfRule::ARRAYS_EQ_RANGE_EXPAND, this); // trusted rules pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2); } @@ -103,6 +106,11 @@ Node ArraysProofRuleChecker::checkInternal(PfRule id, Node bs = nm->mkNode(kind::SELECT, b, k); return as.eqNode(bs).notNode(); } + if (id == PfRule::ARRAYS_EQ_RANGE_EXPAND) + { + Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]); + return args[0].eqNode(expandedEqRange); + } if (id == PfRule::ARRAYS_TRUST) { // "trusted" rules diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp index 19ab1aaae..7cf192b7f 100644 --- a/src/theory/arrays/skolem_cache.cpp +++ b/src/theory/arrays/skolem_cache.cpp @@ -35,6 +35,14 @@ struct ExtIndexVarAttributeId }; typedef expr::Attribute ExtIndexVarAttribute; +/** + * A bound variable corresponding to the index used in the eqrange expansion. + */ +struct EqRangeVarAttributeId +{ +}; +typedef expr::Attribute EqRangeVarAttribute; + SkolemCache::SkolemCache() {} Node SkolemCache::getExtIndexSkolem(Node deq) @@ -66,6 +74,13 @@ Node SkolemCache::getExtIndexSkolem(Node deq) "an extensional lemma index variable from the theory of arrays"); } +Node SkolemCache::getEqRangeVar(TNode eqr) +{ + Assert(eqr.getKind() == kind::EQ_RANGE); + BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager(); + return bvm->mkBoundVar(eqr, eqr[2].getType()); +} + Node SkolemCache::getExtIndexVar(Node deq) { Node a = deq[0][0]; diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h index 12578c01f..17a5c6975 100644 --- a/src/theory/arrays/skolem_cache.h +++ b/src/theory/arrays/skolem_cache.h @@ -43,6 +43,13 @@ class SkolemCache */ static Node getExtIndexSkolem(Node deq); + /** + * Get the bound variable for given EQ_RANGE operator. This bound variable + * is unique for `eqr`. Calling this method will always return the same bound + * variable over the lifetime of `eqr`. + */ + static Node getEqRangeVar(TNode eqr); + private: /** * Get the bound variable x of the witness term above for disequality deq diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index be8e1a08e..8fa7e0fd3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -85,6 +85,7 @@ TheoryArrays::TheoryArrays(context::Context* c, name + "number of setModelVal conflicts")), d_ppEqualityEngine(u, name + "pp", true), d_ppFacts(u), + d_rewriter(pnm), d_state(c, u, valuation), d_im(*this, d_state, pnm), d_literalsToPropagate(c), diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 1072ffaf4..dd7a56d33 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -20,6 +20,9 @@ #include "expr/array_store_all.h" #include "expr/attribute.h" +#include "proof/conv_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "theory/arrays/skolem_cache.h" #include "util/cardinality.h" namespace cvc5 { @@ -48,6 +51,11 @@ void setMostFrequentValueCount(TNode store, uint64_t count) { return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count); } +TheoryArraysRewriter::TheoryArraysRewriter(ProofNodeManager* pnm) + : d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr) +{ +} + Node TheoryArraysRewriter::normalizeConstant(TNode node) { return normalizeConstant(node, node[1].getType().getCardinality()); @@ -271,6 +279,48 @@ Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard) return n; } +Node TheoryArraysRewriter::expandEqRange(TNode node) +{ + Assert(node.getKind() == kind::EQ_RANGE); + + NodeManager* nm = NodeManager::currentNM(); + TNode a = node[0]; + TNode b = node[1]; + TNode i = node[2]; + TNode j = node[3]; + Node k = SkolemCache::getEqRangeVar(node); + Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k); + TypeNode type = k.getType(); + + Kind kle; + Node range; + if (type.isBitVector()) + { + kle = kind::BITVECTOR_ULE; + } + else if (type.isFloatingPoint()) + { + kle = kind::FLOATINGPOINT_LEQ; + } + else if (type.isInteger() || type.isReal()) + { + kle = kind::LEQ; + } + else + { + Unimplemented() << "Type " << type << " is not supported for predicate " + << node.getKind(); + } + + range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j)); + + Node eq = nm->mkNode(kind::EQUAL, + nm->mkNode(kind::SELECT, a, k), + nm->mkNode(kind::SELECT, b, k)); + Node implies = nm->mkNode(kind::IMPLIES, range, eq); + return nm->mkNode(kind::FORALL, bvl, implies); +} + RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) { Trace("arrays-postrewrite") @@ -610,57 +660,22 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node) TrustNode TheoryArraysRewriter::expandDefinition(Node node) { - NodeManager* nm = NodeManager::currentNM(); Kind kind = node.getKind(); - /* Expand - * - * (eqrange a b i j) - * - * to - * - * forall k . i <= k <= j => a[k] = b[k] - * - */ if (kind == kind::EQ_RANGE) { - TNode a = node[0]; - TNode b = node[1]; - TNode i = node[2]; - TNode j = node[3]; - Node k = nm->mkBoundVar(i.getType()); - Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k); - TypeNode type = k.getType(); - - Kind kle; - Node range; - if (type.isBitVector()) - { - kle = kind::BITVECTOR_ULE; - } - else if (type.isFloatingPoint()) + Node expandedEqRange = expandEqRange(node); + if (d_epg) { - kle = kind::FLOATINGPOINT_LEQ; + TrustNode tn = d_epg->mkTrustNode(node.eqNode(expandedEqRange), + PfRule::ARRAYS_EQ_RANGE_EXPAND, + {}, + {node}); + return TrustNode::mkTrustRewrite(node, expandedEqRange, d_epg.get()); } - else if (type.isInteger() || type.isReal()) - { - kle = kind::LEQ; - } - else - { - Unimplemented() << "Type " << type << " is not supported for predicate " - << kind; - } - - range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j)); - - Node eq = nm->mkNode(kind::EQUAL, - nm->mkNode(kind::SELECT, a, k), - nm->mkNode(kind::SELECT, b, k)); - Node implies = nm->mkNode(kind::IMPLIES, range, eq); - Node ret = nm->mkNode(kind::FORALL, bvl, implies); - return TrustNode::mkTrustRewrite(node, ret, nullptr); + return TrustNode::mkTrustRewrite(node, expandedEqRange, nullptr); } + return TrustNode::null(); } diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 498266ce3..95a19004e 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -29,6 +29,9 @@ #include "theory/type_enumerator.h" namespace cvc5 { + +class EagerProofGenerator; + namespace theory { namespace arrays { @@ -43,16 +46,18 @@ static inline Node mkEqNode(Node a, Node b) { class TheoryArraysRewriter : public TheoryRewriter { - /** - * Puts array constant node into normal form. This is so that array constants - * that are distinct nodes are semantically disequal. - */ - static Node normalizeConstant(TNode node); - public: + TheoryArraysRewriter(ProofNodeManager* pnm); + /** Normalize a constant whose index type has cardinality indexCard */ static Node normalizeConstant(TNode node, Cardinality indexCard); + /* Expands the eqrange predicate (eqrange a b i j) to the quantified formula + * (forall ((x T)) + * (=> (and (<= i x) (<= x j)) (= (select a x) (select b x)))). + */ + static Node expandEqRange(TNode node); + RewriteResponse postRewrite(TNode node) override; RewriteResponse preRewrite(TNode node) override; @@ -62,6 +67,14 @@ class TheoryArraysRewriter : public TheoryRewriter static inline void init() {} static inline void shutdown() {} + private: + /** + * Puts array constant node into normal form. This is so that array constants + * that are distinct nodes are semantically disequal. + */ + static Node normalizeConstant(TNode node); + + std::unique_ptr d_epg; }; /* class TheoryArraysRewriter */ } // namespace arrays -- 2.30.2