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

5 files changed, 63 insertions, 14 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;
   }
 
   /**
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index e3b30827c..b7a60917b 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -8,9 +8,7 @@ TESTS =	\
 	arrays1.smt2 \
 	arrays2.smt2 \
 	arrays3.smt2 \
-	arrays4.smt2
-
-EXTRA_DIST = $(TESTS) \
+	arrays4.smt2 \
 	incorrect1.smt \
 	incorrect2.smt \
 	incorrect2.minimized.smt \
@@ -20,10 +18,13 @@ EXTRA_DIST = $(TESTS) \
 	incorrect6.smt \
 	incorrect7.smt \
 	incorrect8.smt \
+	incorrect8.minimized.smt \
 	incorrect9.smt \
 	incorrect10.smt \
 	incorrect11.smt
 
+EXTRA_DIST = $(TESTS)
+
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
 #TESTS += \
diff --git a/test/regress/regress0/arrays/incorrect2.minimized.smt b/test/regress/regress0/arrays/incorrect2.minimized.smt
index aa803d060..6bb3bbfd8 100644
--- a/test/regress/regress0/arrays/incorrect2.minimized.smt
+++ b/test/regress/regress0/arrays/incorrect2.minimized.smt
@@ -3,7 +3,7 @@
 :extrafuns ((v3 Index))
 :extrafuns ((v4 Index))
 :extrafuns ((v2 Index))
-:status unknown
+:status unsat
 :formula
 (flet ($n1 true)
 (flet ($n2 (= v4 v3))
diff --git a/test/regress/regress0/arrays/incorrect8.minimized.smt b/test/regress/regress0/arrays/incorrect8.minimized.smt
new file mode 100644
index 000000000..18067e654
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect8.minimized.smt
@@ -0,0 +1,20 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:extrafuns ((v4 Index))
+:extrafuns ((v3 Index))
+:extrafuns ((v5 Element))
+:extrafuns ((v1 Array))
+:status unknown
+:formula
+(let (?n1 (store v1 v4 v5))
+(let (?n2 (select ?n1 v3))
+(let (?n3 (select v1 v3))
+(flet ($n4 (distinct ?n2 ?n3))
+(let (?n5 (ite $n4 v4 v3))
+(let (?n6 (store ?n1 v4 v5))
+(let (?n7 (select ?n6 v3))
+(flet ($n8 (= ?n2 ?n7))
+(let (?n9 (ite $n8 v3 v4))
+(flet ($n10 (distinct ?n5 ?n9))
+$n10
+)))))))))))