diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/term_registration_visitor.cpp | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 39 |
1 files changed, 33 insertions, 6 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 22b87c32f..b0b712356 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -2,10 +2,10 @@ /*! \file term_registration_visitor.h ** \verbatim ** Original author: dejan - ** Major contributors: - ** Minor contributors (to current version): + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -32,6 +32,14 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; + if( ( parent.getKind() == kind::FORALL || + parent.getKind() == kind::EXISTS || + parent.getKind() == kind::REWRITE_RULE ) && + current != parent ) { + Debug("register::internal") << "quantifier:true" << std::endl; + return true; + } + TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); @@ -89,13 +97,21 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { if (!Theory::setContains(currentTheoryId, visitedTheories)) { visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories); d_visited[current] = visitedTheories; - d_engine->theoryOf(currentTheoryId)->preRegisterTerm(current); + Theory* th = d_engine->theoryOf(currentTheoryId); + th->preRegisterTerm(current); + if(th->getInstantiator() != NULL) { + th->getInstantiator()->preRegisterTerm(current); + } Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } if (!Theory::setContains(parentTheoryId, visitedTheories)) { visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories); d_visited[current] = visitedTheories; - d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current); + Theory* th = d_engine->theoryOf(parentTheoryId); + th->preRegisterTerm(current); + if(th->getInstantiator() != NULL) { + th->getInstantiator()->preRegisterTerm(current); + } Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { @@ -103,7 +119,11 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { if (!Theory::setContains(typeTheoryId, visitedTheories)) { visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); d_visited[current] = visitedTheories; - d_engine->theoryOf(typeTheoryId)->preRegisterTerm(current); + Theory* th = d_engine->theoryOf(typeTheoryId); + th->preRegisterTerm(current); + if(th->getInstantiator() != NULL) { + th->getInstantiator()->preRegisterTerm(current); + } Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } } @@ -135,6 +155,13 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; + if( ( parent.getKind() == kind::FORALL || + parent.getKind() == kind::EXISTS || + parent.getKind() == kind::REWRITE_RULE) && + current != parent ) { + Debug("register::internal") << "quantifier:true" << std::endl; + return true; + } TNodeVisitedMap::const_iterator find = d_visited.find(current); // If node is not visited at all, just return false |