diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-10 20:15:24 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-10 20:15:24 +0000 |
commit | 3544ad31b067fe6c54fcd34c058646852ef8d605 (patch) | |
tree | ec2be7e7cd277ebf3557cb2e3db535bea9bb6d13 /src/theory | |
parent | 8b5686a7dd0b559356e9e3bf76be93ad9c726085 (diff) |
Fixed missing \ in uflra/Makefile.ma
Fixed another model bug and added previously failing fuzz testcase
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 91 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 6 | ||||
-rw-r--r-- | src/theory/model.cpp | 3 |
3 files changed, 76 insertions, 24 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4931a18f0..b9f027afa 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -79,6 +79,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_sharedOther(c), d_sharedTerms(c, false), d_reads(c), + d_readsInternal(c), d_decisionRequests(c), d_permRef(c) { @@ -362,7 +363,7 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) { * Note: completeness depends on having pre-register called on all the input * terms before starting to instantiate lemmas. */ -void TheoryArrays::preRegisterTerm(TNode node) +void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert) { if (d_conflict) { return; @@ -398,7 +399,7 @@ void TheoryArrays::preRegisterTerm(TNode node) Assert(s.getKind()==kind::STORE); Node ni = nm->mkNode(kind::SELECT, s, s[1]); if (ni != node) { - preRegisterTerm(ni); + preRegisterTermInternal(ni); } d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); Assert(++it == stores->end()); @@ -421,6 +422,9 @@ void TheoryArrays::preRegisterTerm(TNode node) Assert(d_equalityEngine.getRepresentative(store) == store); d_infoMap.addIndex(store, node[1]); + if (internalAssert) { + d_readsInternal.push_back(node); + } d_reads.push_back(node); Assert((d_isPreRegistered.insert(node), true)); checkRowForIndex(node[1], store); @@ -441,7 +445,7 @@ void TheoryArrays::preRegisterTerm(TNode node) NodeManager* nm = NodeManager::currentNM(); Node ni = nm->mkNode(kind::SELECT, node, i); if (!d_equalityEngine.hasTerm(ni)) { - preRegisterTerm(ni); + preRegisterTermInternal(ni); } // Apply RIntro1 Rule @@ -471,6 +475,12 @@ void TheoryArrays::preRegisterTerm(TNode node) } +void TheoryArrays::preRegisterTerm(TNode node) +{ + preRegisterTermInternal(node, false); +} + + void TheoryArrays::propagate(Effort e) { // direct propagation now @@ -638,13 +648,49 @@ void TheoryArrays::computeCareGraph() // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// + +void TheoryArrays::collectReads(TNode n, set<Node>& readSet, set<Node>& cache) +{ + if (cache.find(n) != cache.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); + } + cache.insert(n); +} + + void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); std::map<Node, std::vector<Node> > selects; - std::vector<Node> arrays; - // Go through all equivalence classes + set<Node> readSet; + set<Node> cache; + // Collect all selects 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, cache); + } + + // Add selects 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, cache); + } + + // Add selects that were generated internally + unsigned size = d_readsInternal.size(); + for (unsigned i = 0; i < size; ++i) { + readSet.insert(d_readsInternal[i]); + } + + // Go through all equivalence classes and collect relevant arrays and reads + std::vector<Node> arrays; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); bool isArray, computeRep; while( !eqcs_i.isFinished() ){ @@ -659,8 +705,9 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ arrays.push_back(eqc); computeRep = true; } - // If this term is a select, record that the EC rep of its store parameter is being read from using this term - if (n.getKind()==kind::SELECT) { + // If this term is a select, and it appears in an assertion or was generated internally, + // 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()) { selects[d_equalityEngine.getRepresentative(n[0])].push_back(n); } ++eqc_i; @@ -966,7 +1013,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) NodeManager* nm = NodeManager::currentNM(); d_infoMap.setRIntro1Applied(s); Node ni = nm->mkNode(kind::SELECT, s, s[1]); - preRegisterTerm(ni); + preRegisterTermInternal(ni); d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); } } @@ -1202,10 +1249,10 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node reason = nm->mkNode(kind::OR, aj_eq_bj, i_eq_j); d_permRef.push_back(reason); if (!ajExists) { - preRegisterTerm(aj); + preRegisterTermInternal(aj); } if (!bjExists) { - preRegisterTerm(bj); + preRegisterTermInternal(bj); } d_equalityEngine.assertEquality(aj_eq_bj, true, reason); ++d_numProp; @@ -1244,20 +1291,20 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { if (!ajExists) { - preRegisterTerm(aj); + preRegisterTermInternal(aj); } if (!d_equalityEngine.hasTerm(aj2)) { - preRegisterTerm(aj2); + preRegisterTermInternal(aj2); } d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { if (!bjExists) { - preRegisterTerm(bj); + preRegisterTermInternal(bj); } if (!d_equalityEngine.hasTerm(bj2)) { - preRegisterTerm(bj2); + preRegisterTermInternal(bj2); } d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); } @@ -1270,10 +1317,10 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { if (!d_equalityEngine.hasTerm(aj2)) { - preRegisterTerm(aj2); + preRegisterTermInternal(aj2); } if (!d_equalityEngine.hasTerm(bj2)) { - preRegisterTerm(bj2); + preRegisterTermInternal(bj2); } d_equalityEngine.assertEquality(eq1, true, d_true); return; @@ -1344,20 +1391,20 @@ void TheoryArrays::dischargeLemmas() Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { if (!ajExists) { - preRegisterTerm(aj); + preRegisterTermInternal(aj); } if (!d_equalityEngine.hasTerm(aj2)) { - preRegisterTerm(aj2); + preRegisterTermInternal(aj2); } d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { if (!bjExists) { - preRegisterTerm(bj); + preRegisterTermInternal(bj); } if (!d_equalityEngine.hasTerm(bj2)) { - preRegisterTerm(bj2); + preRegisterTermInternal(bj2); } d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); } @@ -1370,10 +1417,10 @@ void TheoryArrays::dischargeLemmas() Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { if (!d_equalityEngine.hasTerm(aj2)) { - preRegisterTerm(aj2); + preRegisterTermInternal(aj2); } if (!d_equalityEngine.hasTerm(bj2)) { - preRegisterTerm(bj2); + preRegisterTermInternal(bj2); } d_equalityEngine.assertEquality(eq1, true, d_true); continue; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 92e04ed24..8358fe6c9 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -177,6 +177,9 @@ class TheoryArrays : public Theory { /** For debugging only- checks invariants about when things are preregistered*/ context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered; + /** Helper for preRegisterTerm, also used internally */ + void preRegisterTermInternal(TNode n, bool internalAssert = true); + public: void preRegisterTerm(TNode n); @@ -215,6 +218,8 @@ class TheoryArrays : public Theory { ///////////////////////////////////////////////////////////////////////////// private: + /** Helper function for collectModelInfo */ + void collectReads(TNode n, std::set<Node>& readSet, std::set<Node>& cache); public: void collectModelInfo( TheoryModel* m, bool fullModel ); @@ -331,6 +336,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; std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache; // The decision requests we have for the core diff --git a/src/theory/model.cpp b/src/theory/model.cpp index e79c2c479..6363cfb27 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -365,8 +365,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache) { - NodeSet::iterator it = cache.find(n); - if (it != cache.end()) { + if (cache.find(n) != cache.end()) { return; } if (isAssignable(n)) { |