From 98f80e6ccc23df7d17f452a3259dd4c3d7aff4c6 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 22 Sep 2021 10:46:53 -0700 Subject: [PATCH] arrays: Use EnvObj::rewrite and EnvObj::options. (#7217) This does not yet clean up the usage of Rewriter::rewrite in the arrays type enumerator yet. Will be cleaned up in a follow-up PR. --- src/theory/arrays/theory_arrays.cpp | 102 +++++++++++-------- src/theory/arrays/theory_arrays_rewriter.cpp | 25 +++-- src/theory/arrays/theory_arrays_rewriter.h | 8 +- 3 files changed, 81 insertions(+), 54 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 774c5db3f..cf31f0cb6 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -29,7 +29,6 @@ #include "theory/arrays/skolem_cache.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/decision_manager.h" -#include "theory/rewriter.h" #include "theory/theory_model.h" #include "theory/trust_substitutions.h" #include "theory/valuation.h" @@ -80,7 +79,7 @@ TheoryArrays::TheoryArrays(Env& env, name + "number of setModelVal conflicts")), d_ppEqualityEngine(userContext(), name + "pp", true), d_ppFacts(userContext()), - d_rewriter(d_pnm), + d_rewriter(env.getRewriter(), d_pnm), d_state(env, valuation), d_im(env, *this, d_state, d_pnm), d_literalsToPropagate(context()), @@ -172,8 +171,8 @@ bool TheoryArrays::ppDisequal(TNode a, TNode b) { bool termsExist = d_ppEqualityEngine.hasTerm(a) && d_ppEqualityEngine.hasTerm(b); Assert(!termsExist || !a.isConst() || !b.isConst() || a == b || d_ppEqualityEngine.areDisequal(a, b, false)); - return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false)) || - Rewriter::rewrite(a.eqNode(b)) == d_false); + return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false)) + || rewrite(a.eqNode(b)) == d_false); } @@ -701,7 +700,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) // Record read in sharing data structure TNode index = d_equalityEngine->getRepresentative(node[1]); - if (!options::arraysWeakEquivalence() && index.isConst()) + if (!options().arrays.arraysWeakEquivalence && index.isConst()) { CTNodeList* temp; CNodeNListMap::iterator it = d_constReads.find(index); @@ -767,7 +766,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_infoMap.setModelRep(node, node); // Add-Store for Weak Equivalence - if (options::arraysWeakEquivalence()) + if (options().arrays.arraysWeakEquivalence) { Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a)); Assert(weakEquivGetRep(node) == node); @@ -1223,8 +1222,11 @@ Node TheoryArrays::getSkolem(TNode ref) void TheoryArrays::postCheck(Effort level) { - if ((options::arraysEagerLemmas() || fullEffort(level)) - && !d_state.isInConflict() && options::arraysWeakEquivalence()) + bool eagerLemmas = options().arrays.arraysEagerLemmas; + bool weakEquiv = options().arrays.arraysWeakEquivalence; + + if ((eagerLemmas || fullEffort(level)) && !d_state.isInConflict() + && weakEquiv) { // Replay all array merges to update weak equivalence data structures context::CDList::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end(); @@ -1287,9 +1289,9 @@ void TheoryArrays::postCheck(Effort level) if (weakEquivGetRepIndex(r[0], r[1]) == weakEquivGetRepIndex(r2[0], r[1])) { // add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2 vector conjunctions; - Assert(d_equalityEngine->areEqual(r, Rewriter::rewrite(r))); - Assert(d_equalityEngine->areEqual(r2, Rewriter::rewrite(r2))); - Node lemma = Rewriter::rewrite(r).eqNode(Rewriter::rewrite(r2)).negate(); + Assert(d_equalityEngine->areEqual(r, rewrite(r))); + Assert(d_equalityEngine->areEqual(r2, rewrite(r2))); + Node lemma = rewrite(r).eqNode(rewrite(r2)).negate(); d_permRef.push_back(lemma); conjunctions.push_back(lemma); if (r[1] != r2[1]) { @@ -1314,8 +1316,8 @@ void TheoryArrays::postCheck(Effort level) d_readTableContext->pop(); } - if (!options::arraysEagerLemmas() && fullEffort(level) - && !d_state.isInConflict() && !options::arraysWeakEquivalence()) + if (!eagerLemmas && fullEffort(level) && !d_state.isInConflict() + && !weakEquiv) { // generate the lemmas on the worklist Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n"; @@ -1378,7 +1380,7 @@ void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) Node eq = ak.eqNode(bk); Node lemma = fact[0].orNode(eq.notNode()); - if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak) + if (options().arrays.arraysPropagate > 0 && d_equalityEngine->hasTerm(ak) && d_equalityEngine->hasTerm(bk)) { // Propagate witness disequality - might produce a conflict @@ -1465,7 +1467,7 @@ Node TheoryArrays::mkAnd(std::vector& conjunctions, bool invert, unsigned void TheoryArrays::setNonLinear(TNode a) { - if (options::arraysWeakEquivalence()) return; + if (options().arrays.arraysWeakEquivalence) return; if (d_infoMap.isNonLinear(a)) return; Trace("arrays") << spaces(context()->getLevel()) << "Arrays::setNonLinear (" @@ -1519,6 +1521,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) } d_mergeInProgress = true; + bool optLinear = options().arrays.arraysOptimizeLinear; + bool weakEquiv = options().arrays.arraysWeakEquivalence; Node n; while (true) { @@ -1530,7 +1534,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) Trace("arrays-merge") << spaces(context()->getLevel()) << "Arrays::merge: (" << a << ", " << b << ")\n"; - if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) { + if (optLinear && !weakEquiv) + { bool aNL = d_infoMap.isNonLinear(a); bool bNL = d_infoMap.isNonLinear(b); if (aNL) { @@ -1606,7 +1611,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) // merge info adds the list of the 2nd argument to the first d_infoMap.mergeInfo(a, b); - if (options::arraysWeakEquivalence()) { + if (weakEquiv) + { d_arrayMerges.push_back(a.eqNode(b)); } @@ -1625,9 +1631,10 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) d_mergeInProgress = false; } +void TheoryArrays::checkStore(TNode a) +{ + if (options().arrays.arraysWeakEquivalence) return; -void TheoryArrays::checkStore(TNode a) { - if (options::arraysWeakEquivalence()) return; Trace("arrays-cri")<<"Arrays::checkStore "<getRepresentative(b); - if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(brep)) { + if (!options().arrays.arraysOptimizeLinear || d_infoMap.isNonLinear(brep)) + { const CTNodeList* js = d_infoMap.getIndices(brep); size_t it = 0; RowLemmaType lem; @@ -1656,10 +1664,10 @@ void TheoryArrays::checkStore(TNode a) { } } - void TheoryArrays::checkRowForIndex(TNode i, TNode a) { - if (options::arraysWeakEquivalence()) return; + if (options().arrays.arraysWeakEquivalence) return; + Trace("arrays-cri")<<"Arrays::checkRowForIndex "<size(); ++it) { TNode instore = (*instores)[it]; @@ -1724,7 +1733,8 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) // look for new ROW lemmas void TheoryArrays::checkRowLemmas(TNode a, TNode b) { - if (options::arraysWeakEquivalence()) return; + if (options().arrays.arraysWeakEquivalence) return; + Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<print(); @@ -1768,7 +1778,8 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) } } - if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(b)) { + if (!options().arrays.arraysOptimizeLinear || d_infoMap.isNonLinear(b)) + { for(it = 0 ; it < i_a->size(); ++it ) { TNode i = (*i_a)[it]; its = 0; @@ -1790,8 +1801,9 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) void TheoryArrays::propagateRowLemma(RowLemmaType lem) { - Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = " - << options::arraysPropagate() << std::endl; + Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. " + "options::arraysPropagate() = " + << options().arrays.arraysPropagate << std::endl; TNode a, b, i, j; std::tie(a, b, i, j) = lem; @@ -1812,7 +1824,7 @@ void TheoryArrays::propagateRowLemma(RowLemmaType lem) bool bothExist = ajExists && bjExists; // If propagating, check propagations - int prop = options::arraysPropagate(); + int64_t prop = options().arrays.arraysPropagate; if (prop > 0) { if (d_equalityEngine->areDisequal(i, j, true) && (bothExist || prop > 1)) { @@ -1877,13 +1889,14 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) bool bothExist = ajExists && bjExists; // If propagating, check propagations - int prop = options::arraysPropagate(); + int64_t prop = options().arrays.arraysPropagate; + if (prop > 0) { propagateRowLemma(lem); } // Prefer equality between indexes so as not to introduce new read terms - if (options::arraysEagerIndexSplitting() && !bothExist + if (options().arrays.arraysEagerIndexSplitting && !bothExist && !d_equalityEngine->areDisequal(i, j, false)) { Node i_eq_j; @@ -1897,10 +1910,10 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // TODO: maybe add triggers here - if (options::arraysEagerLemmas() || bothExist) + if (options().arrays.arraysEagerLemmas || bothExist) { // Make sure that any terms introduced by rewriting are appropriately stored in the equality database - Node aj2 = Rewriter::rewrite(aj); + Node aj2 = rewrite(aj); if (aj != aj2) { if (!ajExists) { preRegisterTermInternal(aj); @@ -1915,7 +1928,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) d_true, PfRule::MACRO_SR_PRED_INTRO); } - Node bj2 = Rewriter::rewrite(bj); + Node bj2 = rewrite(bj); if (bj != bj2) { if (!bjExists) { preRegisterTermInternal(bj); @@ -1936,7 +1949,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // construct lemma Node eq1 = aj2.eqNode(bj2); - Node eq1_r = Rewriter::rewrite(eq1); + Node eq1_r = rewrite(eq1); if (eq1_r == d_true) { if (!d_equalityEngine->hasTerm(aj2)) { @@ -1955,7 +1968,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } Node eq2 = i.eqNode(j); - Node eq2_r = Rewriter::rewrite(eq2); + Node eq2_r = rewrite(eq2); if (eq2_r == d_true) { d_im.assertInference(eq2, true, @@ -1992,9 +2005,11 @@ Node TheoryArrays::getNextDecisionRequest() bool TheoryArrays::dischargeLemmas() { + bool reduceSharing = options().arrays.arraysReduceSharing; bool lemmasAdded = false; - size_t sz = d_RowQueue.size(); - for (unsigned count = 0; count < sz; ++count) { + + for (size_t count = 0, sz = d_RowQueue.size(); count < sz; ++count) + { RowLemmaType l = d_RowQueue.front(); d_RowQueue.pop(); if (d_RowAlreadyAdded.contains(l)) { @@ -2021,7 +2036,7 @@ bool TheoryArrays::dischargeLemmas() continue; } - int prop = options::arraysPropagate(); + int64_t prop = options().arrays.arraysPropagate; if (prop > 0) { propagateRowLemma(l); if (d_state.isInConflict()) @@ -2031,7 +2046,7 @@ bool TheoryArrays::dischargeLemmas() } // Make sure that any terms introduced by rewriting are appropriately stored in the equality database - Node aj2 = Rewriter::rewrite(aj); + Node aj2 = rewrite(aj); if (aj != aj2) { if (!ajExists) { preRegisterTermInternal(aj); @@ -2046,7 +2061,7 @@ bool TheoryArrays::dischargeLemmas() d_true, PfRule::MACRO_SR_PRED_INTRO); } - Node bj2 = Rewriter::rewrite(bj); + Node bj2 = rewrite(bj); if (bj != bj2) { if (!bjExists) { preRegisterTermInternal(bj); @@ -2067,7 +2082,7 @@ bool TheoryArrays::dischargeLemmas() // construct lemma Node eq1 = aj2.eqNode(bj2); - Node eq1_r = Rewriter::rewrite(eq1); + Node eq1_r = rewrite(eq1); if (eq1_r == d_true) { if (!d_equalityEngine->hasTerm(aj2)) { @@ -2086,7 +2101,7 @@ bool TheoryArrays::dischargeLemmas() } Node eq2 = i.eqNode(j); - Node eq2_r = Rewriter::rewrite(eq2); + Node eq2_r = rewrite(eq2); if (eq2_r == d_true) { d_im.assertInference(eq2, true, @@ -2105,7 +2120,8 @@ bool TheoryArrays::dischargeLemmas() aj.eqNode(bj), InferenceId::ARRAYS_READ_OVER_WRITE, eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE); ++d_numRow; lemmasAdded = true; - if (options::arraysReduceSharing()) { + if (reduceSharing) + { return true; } } diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index dd7a56d33..4f11e323e 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -30,9 +30,13 @@ namespace theory { namespace arrays { namespace attr { - struct ArrayConstantMostFrequentValueTag { }; - struct ArrayConstantMostFrequentValueCountTag { }; - } // namespace attr +struct ArrayConstantMostFrequentValueTag +{ +}; +struct ArrayConstantMostFrequentValueCountTag +{ +}; +} // namespace attr typedef expr::Attribute ArrayConstantMostFrequentValueCountAttr; typedef expr::Attribute ArrayConstantMostFrequentValueAttr; @@ -51,8 +55,9 @@ void setMostFrequentValueCount(TNode store, uint64_t count) { return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count); } -TheoryArraysRewriter::TheoryArraysRewriter(ProofNodeManager* pnm) - : d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr) +TheoryArraysRewriter::TheoryArraysRewriter(Rewriter* rewriter, + ProofNodeManager* pnm) + : d_rewriter(rewriter), d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr) { } @@ -345,7 +350,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) } else { - n = Rewriter::rewrite(mkEqNode(store[1], index)); + n = d_rewriter->rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; @@ -417,7 +422,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) } else { - Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index)); + Node eqRewritten = d_rewriter->rewrite(mkEqNode(store[1], index)); if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { Trace("arrays-postrewrite") @@ -457,7 +462,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) } else { - n = Rewriter::rewrite(mkEqNode(store[1], index)); + n = d_rewriter->rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; @@ -557,7 +562,7 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node) } else { - n = Rewriter::rewrite(mkEqNode(store[1], index)); + n = d_rewriter->rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; @@ -620,7 +625,7 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node) } else { - Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index)); + Node eqRewritten = d_rewriter->rewrite(mkEqNode(store[1], index)); if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { break; diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 95a19004e..2c2da66a8 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -33,6 +33,9 @@ namespace cvc5 { class EagerProofGenerator; namespace theory { + +class Rewriter; + namespace arrays { Node getMostFrequentValue(TNode store); @@ -47,7 +50,7 @@ static inline Node mkEqNode(Node a, Node b) { class TheoryArraysRewriter : public TheoryRewriter { public: - TheoryArraysRewriter(ProofNodeManager* pnm); + TheoryArraysRewriter(Rewriter* rewriter, ProofNodeManager* pnm); /** Normalize a constant whose index type has cardinality indexCard */ static Node normalizeConstant(TNode node, Cardinality indexCard); @@ -74,6 +77,9 @@ class TheoryArraysRewriter : public TheoryRewriter */ static Node normalizeConstant(TNode node); + /** The associated rewriter. */ + Rewriter* d_rewriter; + std::unique_ptr d_epg; }; /* class TheoryArraysRewriter */ -- 2.30.2