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.

4 files changed, 145 insertions, 103 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 5aa904aed..1d9abc38b 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -355,6 +355,9 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
   Polynomial pleft = Polynomial::parsePolynomial(left);
   Polynomial pright = Polynomial::parsePolynomial(right);
 
+  Debug("arith::rewriter") << "pleft " << pleft.getNode() << std::endl;
+  Debug("arith::rewriter") << "pright " << pright.getNode() << std::endl;
+
   Comparison cmp = Comparison::mkComparison(atom.getKind(), pleft, pright);
   Assert(cmp.isNormalForm());
   return RewriteResponse(REWRITE_DONE, cmp.getNode());
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 9ccf057b1..afaaedbf9 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -118,10 +118,32 @@ bool VarList::isMember(Node n) {
     return false;
   }
 }
+
 int VarList::cmp(const VarList& vl) const {
   int dif = this->size() - vl.size();
   if (dif == 0) {
-    return this->getNode().getId() - vl.getNode().getId();
+    if(this->getNode() == vl.getNode()) {
+      return 0;
+    }
+
+    Assert(!empty());
+    Assert(!vl.empty());
+    if(this->size() == 1){
+      return Variable::VariableNodeCmp::cmp(this->getNode(), vl.getNode());
+    }
+
+
+    internal_iterator ii=this->internalBegin(), ie=this->internalEnd();
+    internal_iterator ci=vl.internalBegin(), ce=vl.internalEnd();
+    for(; ii != ie; ++ii, ++ci){
+      Node vi = *ii;
+      Node vc = *ci;
+      int tmp = Variable::VariableNodeCmp::cmp(vi, vc);
+      if(tmp != 0){
+        return tmp;
+      }
+    }
+    Unreachable();
   } else if(dif < 0) {
     return -1;
   } else {
@@ -559,6 +581,36 @@ bool Polynomial::variableMonomialAreStrictlyGreater(const Monomial& m) const{
   }
 }
 
+bool Polynomial::isMember(TNode n) {
+  if(Monomial::isMember(n)){
+    return true;
+  }else if(n.getKind() == kind::PLUS){
+    Assert(n.getNumChildren() >= 2);
+    Node::iterator currIter = n.begin(), end = n.end();
+    Node prev = *currIter;
+    if(!Monomial::isMember(prev)){
+      return false;
+    }
+
+    Monomial mprev = Monomial::parseMonomial(prev);
+    ++currIter;
+    for(; currIter != end; ++currIter){
+      Node curr = *currIter;
+      if(!Monomial::isMember(curr)){
+        return false;
+      }
+      Monomial mcurr = Monomial::parseMonomial(curr);
+      if(!(mprev < mcurr)){
+        return false;
+      }
+      mprev = mcurr;
+    }
+    return true;
+  } else {
+    return false;
+  }
+}
+
 Node SumPair::computeQR(const SumPair& sp, const Integer& div){
   Assert(sp.isIntegral());
 
@@ -1156,6 +1208,7 @@ Comparison Comparison::mkComparison(Kind k, const Polynomial& l, const Polynomia
     VarList vRight = r.asVarList();
 
     if(vLeft == vRight){
+      // return true for equalities and false for disequalities
       return Comparison(k == kind::EQUAL);
     }else{
       Node eqNode = vLeft < vRight ? toNode( kind::EQUAL, l, r) : toNode( kind::EQUAL, r, l);
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 7e8ff556d..3267834b5 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -270,40 +270,48 @@ public:
   bool operator<(const Variable& v) const {
     VariableNodeCmp cmp;
     return cmp(this->getNode(), v.getNode());
-
-    // bool thisIsVariable = isMetaKindVariable();
-    // bool vIsVariable = v.isMetaKindVariable();
-
-    // if(thisIsVariable == vIsVariable){
-    //   bool thisIsInteger = isIntegral();
-    //   bool vIsInteger = v.isIntegral();
-    //   if(thisIsInteger == vIsInteger){
-    //     return getNode() < v.getNode();
-    //   }else{
-    //     return thisIsInteger && !vIsInteger;
-    //   }
-    // }else{
-    //   return thisIsVariable && !vIsVariable;
-    // }
   }
 
   struct VariableNodeCmp {
-    bool operator()(Node n, Node m) const {
-      bool nIsVariable = n.isVar();
-      bool mIsVariable = m.isVar();
-
-      if(nIsVariable == mIsVariable){
-        bool nIsInteger = n.getType().isInteger();
-        bool mIsInteger = m.getType().isInteger();
-        if(nIsInteger == mIsInteger){
-          return n < m;
+    static inline int cmp(Node n, Node m) {
+      if ( n == m ) { return 0; }
+
+      // this is now slightly off of the old variable order.
+
+      bool nIsInteger = n.getType().isInteger();
+      bool mIsInteger = m.getType().isInteger();
+
+      if(nIsInteger == mIsInteger){
+        bool nIsVariable = n.isVar();
+        bool mIsVariable = m.isVar();
+
+        if(nIsVariable == mIsVariable){
+          if(n < m){
+            return -1;
+          }else{
+            Assert( n != m );
+            return 1;
+          }
         }else{
-          return nIsInteger && !mIsInteger;
+          if(nIsVariable){
+            return -1; // nIsVariable => !mIsVariable
+          }else{
+            return 1; // !nIsVariable => mIsVariable
+          }
         }
       }else{
-        return nIsVariable && !mIsVariable;
+        Assert(nIsInteger != mIsInteger);
+        if(nIsInteger){
+          return 1; // nIsInteger => !mIsInteger
+        }else{
+          return -1; // !nIsInteger => mIsInteger
+        }
       }
     }
+
+    bool operator()(Node n, Node m) const {
+      return VariableNodeCmp::cmp(n,m) < 0;
+    }
   };
 
   bool operator==(const Variable& v) const { return getNode() == v.getNode();}
@@ -821,35 +829,7 @@ private:
   bool singleton() const { return d_singleton; }
 
 public:
-  static bool isMember(TNode n) {
-    if(Monomial::isMember(n)){
-      return true;
-    }else if(n.getKind() == kind::PLUS){
-      Assert(n.getNumChildren() >= 2);
-      Node::iterator currIter = n.begin(), end = n.end();
-      Node prev = *currIter;
-      if(!Monomial::isMember(prev)){
-        return false;
-      }
-
-      Monomial mprev = Monomial::parseMonomial(prev);
-      ++currIter;
-      for(; currIter != end; ++currIter){
-        Node curr = *currIter;
-        if(!Monomial::isMember(curr)){
-          return false;
-        }
-        Monomial mcurr = Monomial::parseMonomial(curr);
-        if(!(mprev < mcurr)){
-          return false;
-        }
-        mprev = mcurr;
-      }
-      return true;
-    } else {
-      return false;
-    }
-  }
+  static bool isMember(TNode n);
 
   class iterator {
   private:
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) {