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..

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;
   }
 
   /**