diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
commit | 56013a80a76b0d46f6f8497d7570e51877dbf99d (patch) | |
tree | 9d4ed01590a15b13b91485333fd497e26889e0c0 /src/theory/arrays | |
parent | b273e586629c5759dc88cd962e52a89f65b674a7 (diff) |
bug fixes to models, array rewriter with previously failing testcases
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 107 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 10 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 10 |
3 files changed, 75 insertions, 52 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 342e67654..3a109b51a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -423,7 +423,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert) Assert(d_equalityEngine.getRepresentative(store) == store); d_infoMap.addIndex(store, node[1]); if (internalAssert) { - d_readsInternal.push_back(node); + d_readsInternal.insert(node); } d_reads.push_back(node); Assert((d_isPreRegistered.insert(node), true)); @@ -445,7 +445,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert) NodeManager* nm = NodeManager::currentNM(); Node ni = nm->mkNode(kind::SELECT, node, i); if (!d_equalityEngine.hasTerm(ni)) { - preRegisterTermInternal(ni); + preRegisterTermInternal(ni, false); } // Apply RIntro1 Rule @@ -649,81 +649,80 @@ void TheoryArrays::computeCareGraph() ///////////////////////////////////////////////////////////////////////////// -void TheoryArrays::collectReads(TNode n, set<Node>& readSet, set<Node>& cache) +void TheoryArrays::collectTerms(TNode n, set<Node>& termSet) { - if (cache.find(n) != cache.end()) { + if (termSet.find(n) != termSet.end()) { return; } - if (n.getKind() == kind::SELECT) { - readSet.insert(n); - } - for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { - collectReads(*child_it, readSet, cache); + termSet.insert(n); + if (n.getType().isBoolean() || !isLeaf(n)) { + for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { + collectTerms(*child_it, termSet); + } } - cache.insert(n); } -void TheoryArrays::collectArrays(TNode n, set<Node>& arraySet, set<Node>& cache) +void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) { - if (cache.find(n) != cache.end()) { - return; - } - if (n.getType().isArray()) { - arraySet.insert(n); - } - for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { - collectArrays(*child_it, arraySet, cache); - } - cache.insert(n); -} + set<Node> termSet; + set<Node> cache; - -void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ - m->assertEqualityEngine( &d_equalityEngine ); - - std::map<Node, std::vector<Node> > selects; - - set<Node> readSet, arraySet; - set<Node> readCache, arrayCache; - // Collect all arrays and selects appearing in assertions + // Collect all terms appearing in assertions context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); for (; assert_it != assert_it_end; ++assert_it) { - collectReads(*assert_it, readSet, readCache); - collectArrays(*assert_it, arraySet, arrayCache); + collectTerms(*assert_it, termSet); } - // Add arrays and selects that are shared terms + // Add terms that are shared terms context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(); - for (; shared_it != shared_it_end; ++ shared_it) { - collectReads(*shared_it, readSet, readCache); - collectArrays(*shared_it, arraySet, arrayCache); + for (; shared_it != shared_it_end; ++shared_it) { + collectTerms(*shared_it, termSet); } // Add selects that were generated internally - unsigned size = d_readsInternal.size(); - for (unsigned i = 0; i < size; ++i) { - readSet.insert(d_readsInternal[i]); + context::CDHashSet<TNode, TNodeHashFunction>::iterator internal_it = d_readsInternal.begin(), internal_it_end = d_readsInternal.end(); + for (; internal_it != internal_it_end; ++internal_it) { + termSet.insert(*internal_it); } // Go through all equivalence classes and collect relevant arrays and reads std::vector<Node> arrays; + std::map<Node, std::vector<Node> > selects; + bool computeRep, isArray; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - bool computeRep; while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); + isArray = eqc.getType().isArray(); computeRep = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ Node n = *eqc_i; // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly - if (!computeRep && n.getKind() != kind::STORE && arraySet.find(n) != arraySet.end()) { - arrays.push_back(eqc); - computeRep = true; + if (isArray && termSet.find(n) != termSet.end()) { + if (n.getKind() == kind::STORE) { + // Make sure RIntro1 reads are included + termSet.insert(NodeManager::currentNM()->mkNode(kind::SELECT, n, n[1])); + } + else if (!computeRep) { + arrays.push_back(eqc); + computeRep = true; + } } - // If this term is a select, and it appears in an assertion or was generated internally, + ++eqc_i; + } + ++eqcs_i; + } + + eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + // If this term is a select, and it appears in an assertion or was derived from one, // record that the EC rep of its store parameter is being read from using this term - if (n.getKind() == kind::SELECT && readSet.find(n) != readSet.end()) { + if (n.getKind() == kind::SELECT && termSet.find(n) != termSet.end()) { selects[d_equalityEngine.getRepresentative(n[0])].push_back(n); } ++eqc_i; @@ -731,6 +730,8 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ ++eqcs_i; } + m->assertEqualityEngine(&d_equalityEngine, &termSet); + NodeManager* nm = NodeManager::currentNM(); Node rep; map<Node, Node> defValues; @@ -1259,6 +1260,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node i_eq_j = i.eqNode(j); Node reason = nm->mkNode(kind::OR, aj_eq_bj, i_eq_j); d_permRef.push_back(reason); + d_readsInternal.insert(aj); + d_readsInternal.insert(bj); if (!ajExists) { preRegisterTermInternal(aj); } @@ -1301,6 +1304,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // Make sure that any terms introduced by rewriting are appropriately stored in the equality database Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { + d_readsInternal.insert(aj); + d_readsInternal.insert(aj2); if (!ajExists) { preRegisterTermInternal(aj); } @@ -1311,6 +1316,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { + d_readsInternal.insert(bj); + d_readsInternal.insert(bj2); if (!bjExists) { preRegisterTermInternal(bj); } @@ -1327,6 +1334,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node eq1 = aj2.eqNode(bj2); Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { + d_readsInternal.insert(aj2); + d_readsInternal.insert(bj2); if (!d_equalityEngine.hasTerm(aj2)) { preRegisterTermInternal(aj2); } @@ -1401,6 +1410,8 @@ void TheoryArrays::dischargeLemmas() // Make sure that any terms introduced by rewriting are appropriately stored in the equality database Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { + d_readsInternal.insert(aj); + d_readsInternal.insert(aj2); if (!ajExists) { preRegisterTermInternal(aj); } @@ -1411,6 +1422,8 @@ void TheoryArrays::dischargeLemmas() } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { + d_readsInternal.insert(bj); + d_readsInternal.insert(bj2); if (!bjExists) { preRegisterTermInternal(bj); } @@ -1427,6 +1440,8 @@ void TheoryArrays::dischargeLemmas() Node eq1 = aj2.eqNode(bj2); Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { + d_readsInternal.insert(aj2); + d_readsInternal.insert(bj2); if (!d_equalityEngine.hasTerm(aj2)) { preRegisterTermInternal(aj2); } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index a47c8440e..9bf1201f3 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -218,12 +218,12 @@ class TheoryArrays : public Theory { ///////////////////////////////////////////////////////////////////////////// private: - /** Helper functions for collectModelInfo */ - void collectReads(TNode n, std::set<Node>& readSet, std::set<Node>& cache); - void collectArrays(TNode n, std::set<Node>& arraySet, std::set<Node>& cache); + /** Helper function for collectModelInfo */ + void collectTerms(TNode n, std::set<Node>& termSet); + public: - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo(TheoryModel* m, bool fullModel); ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS @@ -337,7 +337,7 @@ class TheoryArrays : public Theory { context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther; context::CDO<bool> d_sharedTerms; context::CDList<TNode> d_reads; - context::CDList<TNode> d_readsInternal; + context::CDHashSet<TNode, TNodeHashFunction> d_readsInternal; std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache; // The decision requests we have for the core diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 62782f90e..da479616d 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -306,7 +306,15 @@ public: NodeManager* nm = NodeManager::currentNM(); if (val) { // store(store(a,i,v),i,w) = store(a,i,w) - Node result = nm->mkNode(kind::STORE, store[0], index, value); + Node result; + if (value.getKind() == kind::SELECT && + value[0] == store[0] && + value[1] == index) { + result = store[0]; + } + else { + result = nm->mkNode(kind::STORE, store[0], index, value); + } Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl; return RewriteResponse(REWRITE_DONE, result); } |