diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 30 |
1 files changed, 27 insertions, 3 deletions
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; } /** |