diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 18:48:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 18:48:16 +0000 |
commit | 4c428c8f74ae913f05287c0595c8887c31089520 (patch) | |
tree | ab3041c59d6d8700e96c623675a1570208c6374f /src | |
parent | b16e3a3187ce721e32042f241cc718529cdd0573 (diff) |
if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as well as pre-registration of free constants of uninterpreted sort, etc..
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_engine.cpp | 18 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 30 |
2 files changed, 38 insertions, 10 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4237e0992..3571171f8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -182,7 +182,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { preregister_stack_element& stackHead = toVisit.back(); // The current node we are processing TNode current = stackHead.node; - // If we already added all the children its time to register or just pop from the stack + // If we already added all the children its time to register or just + // pop from the stack if (stackHead.children_added || current.getAttribute(PreRegistered())) { if (!current.getAttribute(PreRegistered())) { // Mark it as registered @@ -194,18 +195,21 @@ void TheoryEngine::preRegister(TNode preprocessed) { } else { Theory* theory = theoryOf(current); TheoryId theoryLHS = theory->getId(); - Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; + Debug("register") << "preregistering " << current + << " with " << theoryLHS << std::endl; markActive(theoryLHS); theory->preRegisterTerm(current); } } else { - TheoryId theory = Theory::theoryOf(current); - Debug("register") << "preregistering " << current << " with " << theory << std::endl; + TheoryId theory = theoryIdOf(current); + Debug("register") << "preregistering " << current + << " with " << theory << std::endl; markActive(theory); d_theoryTable[theory]->preRegisterTerm(current); - TheoryId typeTheory = Theory::theoryOf(current.getType()); + TheoryId typeTheory = theoryIdOf(current.getType()); if (theory != typeTheory) { - Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; + Debug("register") << "preregistering " << current + << " with " << typeTheory << std::endl; markActive(typeTheory); d_theoryTable[typeTheory]->preRegisterTerm(current); } @@ -408,7 +412,7 @@ Node TheoryEngine::preprocess(TNode assertion) { } // If this is an atom, we preprocess it with the theory - if (Theory::theoryOf(current) != THEORY_BOOL) { + if (theoryIdOf(current) != THEORY_BOOL) { d_atomPreprocessingCache[current] = theoryOf(current)->preprocess(current); continue; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5b724a7c7..94ba8cabb 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -290,20 +290,44 @@ public: */ inline theory::Theory* theoryOf(TNode node) { if (node.getKind() == kind::EQUAL) { - return d_theoryTable[theory::Theory::theoryOf(node[0])]; + return d_theoryTable[theoryIdOf(node[0])]; } else { - return d_theoryTable[theory::Theory::theoryOf(node)]; + return d_theoryTable[theoryIdOf(node)]; } } /** + * Wrapper for theory::Theory::theoryOf() that implements the + * array/EUF hack. + */ + inline theory::TheoryId theoryIdOf(TNode node) { + theory::TheoryId id = theory::Theory::theoryOf(node); + if(d_logic == "QF_AX" && id == theory::THEORY_UF) { + id = theory::THEORY_ARRAY; + } + return id; + } + + /** * Get the theory associated to a given Node. * * @returns the theory, or NULL if the TNode is * of built-in type. */ inline theory::Theory* theoryOf(const TypeNode& typeNode) { - return d_theoryTable[theory::Theory::theoryOf(typeNode)]; + return d_theoryTable[theoryIdOf(typeNode)]; + } + + /** + * Wrapper for theory::Theory::theoryOf() that implements the + * array/EUF hack. + */ + inline theory::TheoryId theoryIdOf(const TypeNode& typeNode) { + theory::TheoryId id = theory::Theory::theoryOf(typeNode); + if(d_logic == "QF_AX" && id == theory::THEORY_UF) { + id = theory::THEORY_ARRAY; + } + return id; } /** |