From: Paul Meng <baolmeng@gmail.com>
Date: Tue, 13 Sep 2016 21:11:16 +0000 (-0500)
Subject: fixed type checking and computing for PRODUCT and JOIN
X-Git-Tag: cvc5-1.0.0~6031
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=56670c697402a74b1769215bcde87b56f17e79b9;p=cvc5.git

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 478dcbdb6..a709eff09 100644
--- 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;
   }