Patch for the subtype theoryof mode to make the equalities over disequal types get sent to the theory of the type.

Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.

1 files changed, 53 insertions, 47 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 2dd474a19..d9281e8ba 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -50,75 +50,81 @@ Theory::~Theory() {
 }
 
 TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
-
-  Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
-
+  TheoryId tid = THEORY_BUILTIN;
   switch(mode) {
   case THEORY_OF_TYPE_BASED:
     // Constants, variables, 0-ary constructors
     if (node.isVar() || node.isConst()) {
-      return theoryOf(node.getType());
-    }
-    // Equality is owned by the theory that owns the domain
-    if (node.getKind() == kind::EQUAL) {
-      return theoryOf(node[0].getType());
+      tid = Theory::theoryOf(node.getType());
+    } else if (node.getKind() == kind::EQUAL) {
+      // Equality is owned by the theory that owns the domain
+      tid = Theory::theoryOf(node[0].getType());
+    } else {
+      // Regular nodes are owned by the kind
+      tid = kindToTheoryId(node.getKind());
     }
-    // Regular nodes are owned by the kind
-    return kindToTheoryId(node.getKind());
     break;
   case THEORY_OF_TERM_BASED:
     // Variables
     if (node.isVar()) {
-      if (theoryOf(node.getType()) != theory::THEORY_BOOL) {
+      if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) {
         // We treat the variables as uninterpreted
-        return s_uninterpretedSortOwner;
+        tid = s_uninterpretedSortOwner;
       } else {
         // Except for the Boolean ones, which we just ignore anyhow
-        return theory::THEORY_BOOL;
+        tid = theory::THEORY_BOOL;
       }
-    }
-    // Constants
-    if (node.isConst()) {
+    } else if (node.isConst()) {
       // Constants go to the theory of the type
-      return theoryOf(node.getType());
-    }
-    // Equality
-    if (node.getKind() == kind::EQUAL) {
+      tid = Theory::theoryOf(node.getType());
+    } else if (node.getKind() == kind::EQUAL) { // Equality
       // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
       if (node[0].getKind() == kind::ITE) {
-        return theoryOf(node[0].getType());
-      }
-      if (node[1].getKind() == kind::ITE) {
-        return theoryOf(node[1].getType());
-      }
-      // If both sides belong to the same theory the choice is easy
-      TheoryId T1 = theoryOf(node[0]);
-      TheoryId T2 = theoryOf(node[1]);
-      if (T1 == T2) {
-        return T1;
-      }
-      TheoryId T3 = theoryOf(node[0].getType());
-      // This is a case of
-      // * x*y = f(z) -> UF
-      // * x = c      -> UF
-      // * f(x) = read(a, y) -> either UF or ARRAY
-      // at least one of the theories has to be parametric, i.e. theory of the type is different
-      // from the theory of the term
-      if (T1 == T3) {
-        return T2;
-      }
-      if (T2 == T3) {
-        return T1;
+        tid = Theory::theoryOf(node[0].getType());
+      } else if (node[1].getKind() == kind::ITE) {
+        tid = Theory::theoryOf(node[1].getType());
+      } else {
+        TNode l = node[0];
+        TNode r = node[1];
+        TypeNode ltype = l.getType();
+        TypeNode rtype = r.getType();
+        if( ltype != rtype ){
+          tid = Theory::theoryOf(l.getType());
+        }else {
+          // If both sides belong to the same theory the choice is easy
+          TheoryId T1 = Theory::theoryOf(l);
+          TheoryId T2 = Theory::theoryOf(r);
+          if (T1 == T2) {
+            tid = T1;
+          } else {
+            TheoryId T3 = Theory::theoryOf(ltype);
+            // This is a case of
+            // * x*y = f(z) -> UF
+            // * x = c      -> UF
+            // * f(x) = read(a, y) -> either UF or ARRAY
+            // at least one of the theories has to be parametric, i.e. theory of the type is different
+            // from the theory of the term
+            if (T1 == T3) {
+              tid = T2;
+            } else if (T2 == T3) {
+              tid = T1;
+            } else {
+              // If both are parametric, we take the smaller one (arbitrary)
+              tid = T1 < T2 ? T1 : T2;
+            }
+          }
+        }
       }
-      // If both are parametric, we take the smaller one (arbitraty)
-      return T1 < T2 ? T1 : T2;
+    } else {
+      // Regular nodes are owned by the kind
+      tid = kindToTheoryId(node.getKind());
     }
-    // Regular nodes are owned by the kind
-    return kindToTheoryId(node.getKind());
     break;
   default:
     Unreachable();
   }
+  Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
+  return tid;
 }
 
 void Theory::addSharedTermInternal(TNode n) {