if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as...

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4237e0992194e608d96f46ea3f755dbf88c27b89..3571171f88c4e4714680ca6cfdaf24c78fbb9c06 100644 (file)
--- 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 5b724a7c73ca6ce50a1eca841ecf4765985c74d0..94ba8cabbb1a950f9aa27a4255114585f1894b4f 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -290,12 +290,24 @@ 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.
    *
@@ -303,7 +315,19 @@ public:
    * 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 e3b30827ce215819f0f54d290bb79da33de521d0..b7a60917bef3050c727b6ac9de62266698e7e297 100644 (file)
--- 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 aa803d060c53df7694c71a1ec281c4d22f4ad091..6bb3bbfd80495b9c00524eb2e322551c65189fc2 100644 (file)
--- 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 (file)
index 0000000..18067e6
--- /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
+)))))))))))