From 5b5a421d79d12a31edde3902f2b8ddec6a3ca684 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Mon, 14 May 2012 20:57:12 +0000 Subject: [PATCH] fixes for shared term registration. previously the type was not considered when looking at theories of the term and for a term like read(a, f(x)) the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail. --- src/smt/smt_engine.cpp | 2 + src/theory/arith/theory_arith.cpp | 7 +- src/theory/term_registration_visitor.cpp | 108 ++++++++++++++++------- src/theory/theory.h | 14 +-- 4 files changed, 92 insertions(+), 39 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5d514744f..0acd81248 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1102,7 +1102,9 @@ void SmtEnginePrivate::processAssertions() { // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones +#ifdef CVC4_ASSERTIONS unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size(); +#endif Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1179de685..d660cb4cd 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1487,11 +1487,10 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { default: { if(isSetup(n)){ - ArithVar var = d_arithvarNodeMap.asArithVar(n); - return d_partialModel.getAssignment(var); + ArithVar var = d_arithvarNodeMap.asArithVar(n); + return d_partialModel.getAssignment(var); }else{ - Warning() << "you did not setup this up!: " << n << endl; - return DeltaRational(); + Unreachable(); } } } diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 0f8822e72..7d82dee8e 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -32,28 +32,41 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; - TNodeToTheorySetMap::iterator find = d_visited.find(current); - - // If node is not visited at all, just return false - if (find == d_visited.end()) { - Debug("register::internal") << "1:false" << std::endl; - return false; - } TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); + TheoryId parentTheoryId = Theory::theoryOf(parent); d_theories = Theory::setInsert(currentTheoryId, d_theories); d_theories = Theory::setInsert(parentTheoryId, d_theories); + // Should we use the theory of the type + bool useType = current != parent && currentTheoryId != parentTheoryId; + + // Get the theories that have already visited this node + TNodeToTheorySetMap::iterator find = d_visited.find(current); + if (find == d_visited.end()) { + if (useType) { + TheoryId typeTheoryId = Theory::theoryOf(current.getType()); + d_theories = Theory::setInsert(typeTheoryId, d_theories); + } + return false; + } + Theory::Set visitedTheories = (*find).second; if (Theory::setContains(currentTheoryId, visitedTheories)) { - // The current theory has already visited it, so now it depends on the parent - Debug("register::internal") << (Theory::setContains(parentTheoryId, visitedTheories) ? "2:true" : "2:false") << std::endl; - return Theory::setContains(parentTheoryId, visitedTheories); + // The current theory has already visited it, so now it depends on the parent and the type + if (Theory::setContains(parentTheoryId, visitedTheories)) { + if (useType) { + TheoryId typeTheoryId = Theory::theoryOf(current.getType()); + d_theories = Theory::setInsert(typeTheoryId, d_theories); + return Theory::setContains(typeTheoryId, visitedTheories); + } else { + return true; + } + } else { + return false; + } } else { - // If the current theory is not registered, it still needs to be visited - Debug("register::internal") << "3:false" << std::endl; return false; } } @@ -69,6 +82,9 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); + // Should we use the theory of the type + bool useType = current != parent && currentTheoryId != parentTheoryId; + Theory::Set visitedTheories = d_visited[current]; Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl; if (!Theory::setContains(currentTheoryId, visitedTheories)) { @@ -83,6 +99,15 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } + if (useType) { + TheoryId typeTheoryId = Theory::theoryOf(current.getType()); + if (!Theory::setContains(typeTheoryId, visitedTheories)) { + visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); + d_visited[current] = visitedTheories; + d_engine->theoryOf(typeTheoryId)->preRegisterTerm(current); + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; + } + } Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl; Assert(d_visited.find(current) != d_visited.end()); @@ -124,13 +149,21 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); + // Should we use the theory of the type + bool useType = current != parent && currentTheoryId != parentTheoryId; + if (Theory::setContains(currentTheoryId, theories)) { - // The current theory has already visited it, so now it depends on the parent - Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl; - return Theory::setContains(parentTheoryId, theories); + if (Theory::setContains(parentTheoryId, theories)) { + if (useType) { + TheoryId typeTheoryId = Theory::theoryOf(current.getType()); + return Theory::setContains(typeTheoryId, theories); + } else { + return true; + } + } else { + return false; + } } else { - // If the current theory is not registered, it still needs to be visited - Debug("register::internal") << "2:false" << std::endl; return false; } } @@ -144,24 +177,39 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); - Theory::Set theories = d_visited[current]; - unsigned theoriesCount = theories == 0 ? 0 : 1; - Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl; - if (!Theory::setContains(currentTheoryId, theories)) { - d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories); - theoriesCount ++; + bool useType = current != parent && currentTheoryId != parentTheoryId; + + unsigned newTheoriesCount = 0; + Theory::Set visitedTheories = d_visited[current]; + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl; + if (!Theory::setContains(currentTheoryId, visitedTheories)) { + visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories); + newTheoriesCount ++; Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } - if (!Theory::setContains(parentTheoryId, theories)) { - d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories); - theoriesCount ++; + if (!Theory::setContains(parentTheoryId, visitedTheories)) { + visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories); + newTheoriesCount ++; Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } - Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl; + if (useType) { + TheoryId typeTheoryId = Theory::theoryOf(current.getType()); + if (!Theory::setContains(typeTheoryId, visitedTheories)) { + visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); + newTheoriesCount ++; + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl; + } + } + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl; + + // Record the new theories that we visited + if (newTheoriesCount > 0) { + d_visited[current] = visitedTheories; + } // If there is more than two theories and a new one has been added notify the shared terms database - if (theoriesCount > 1) { - d_sharedTerms.addSharedTerm(d_atom, current, theories); + if (newTheoriesCount > 1) { + d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories); } Assert(d_visited.find(current) != d_visited.end()); diff --git a/src/theory/theory.h b/src/theory/theory.h index 40f72dafc..9ac07d849 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -619,7 +619,7 @@ public: /** Add the theory to the set. If no set specified, just returns a singleton set */ static inline Set setRemove(TheoryId theory, Set set = 0) { - return set ^ (1 << theory); + return setDifference(set, setInsert(theory)); } /** Check if the set contains the theory */ @@ -656,13 +656,15 @@ public: return ss.str(); } + typedef context::CDList::const_iterator assertions_iterator; + /** * Provides access to the facts queue, primarily intended for theory * debugging purposes. * * @return the iterator to the beginning of the fact queue */ - context::CDList::const_iterator facts_begin() const { + assertions_iterator facts_begin() const { return d_facts.begin(); } @@ -672,17 +674,19 @@ public: * * @return the iterator to the end of the fact queue */ - context::CDList::const_iterator facts_end() const { + assertions_iterator facts_end() const { return d_facts.end(); } + typedef context::CDList::const_iterator shared_terms_iterator; + /** * Provides access to the shared terms, primarily intended for theory * debugging purposes. * * @return the iterator to the beginning of the shared terms list */ - context::CDList::const_iterator shared_terms_begin() const { + shared_terms_iterator shared_terms_begin() const { return d_sharedTerms.begin(); } @@ -692,7 +696,7 @@ public: * * @return the iterator to the end of the shared terms list */ - context::CDList::const_iterator shared_terms_end() const { + shared_terms_iterator shared_terms_end() const { return d_sharedTerms.end(); } -- 2.30.2