fixed type checking and computing for PRODUCT and JOIN

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 478dcbdb605f6fbff5e6471ca51b949db7950ab3..a709eff09123195ecde46c75a76662a465d56602 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -189,38 +189,38 @@ struct RelBinaryOperatorTypeRule {
     Assert(n.getKind() == kind::PRODUCT ||
            n.getKind() == kind::JOIN);
 
+
+
     TypeNode firstRelType = n[0].getType(check);
     TypeNode secondRelType = n[1].getType(check);
     TypeNode resultType = firstRelType;
 
-    if(check) {
-
-      if(!firstRelType.isSet() || !secondRelType.isSet()) {
-        throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets");
-      }
-      if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
-        throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)");
-      }
+    if(!firstRelType.isSet() || !secondRelType.isSet()) {
+      throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets");
+    }
+    if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
+      throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)");
+    }
 
-      std::vector<TypeNode> newTupleTypes;
-      std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes();
-      std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes();
+    std::vector<TypeNode> newTupleTypes;
+    std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes();
+    std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes();
 
-      // JOIN is not allowed to apply on two unary sets
-      if( n.getKind() == kind::JOIN ) {
-        if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) {
-          throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations");
-        } else if(firstTupleTypes.back() != secondTupleTypes.front()) {
-          throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
-        }
-        newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1);
-        newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end());
-      }else if( n.getKind() == kind::PRODUCT ) {
-        newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end());
-        newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end());
+    // JOIN is not allowed to apply on two unary sets
+    if( n.getKind() == kind::JOIN ) {
+      if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) {
+        throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations");
+      } else if(firstTupleTypes.back() != secondTupleTypes.front()) {
+        throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
       }
-      resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
+      newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1);
+      newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end());
+    }else if( n.getKind() == kind::PRODUCT ) {
+      newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end());
+      newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end());
     }
+    resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
+
     return resultType;
   }