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

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