From: Andres Noetzli <noetzli@stanford.edu>
Date: Mon, 15 May 2017 17:09:45 +0000 (-0700)
Subject: Fix type checks for relation operators
X-Git-Tag: cvc5-1.0.0~5799^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=370052d7bb7125376eeb7296091f5ce977421efa;p=cvc5.git

Fix type checks for relation operators

This commit fixes an assertion error when applying transpose or transitive
closure to a set instead of a relation. Instead it now prints a parse error.
---

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index b8c0a8055..a5a78e691 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -277,8 +277,8 @@ struct RelTransposeTypeRule {
     throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::TRANSPOSE);
     TypeNode setType = n[0].getType(check);
-    if(check && !setType.isSet() && !setType.getSetElementType().isTuple()) {
-        throw TypeCheckingExceptionPrivate(n, "relation transpose operats on non-relation");
+    if(check && (!setType.isSet() || !setType.getSetElementType().isTuple())) {
+        throw TypeCheckingExceptionPrivate(n, "relation transpose operates on non-relation");
     }
     std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
     std::reverse(tupleTypes.begin(), tupleTypes.end());
@@ -296,7 +296,7 @@ struct RelTransClosureTypeRule {
     Assert(n.getKind() == kind::TCLOSURE);
     TypeNode setType = n[0].getType(check);
     if(check) {
-      if(!setType.isSet() && !setType.getSetElementType().isTuple()) {
+      if(!setType.isSet() || !setType.getSetElementType().isTuple()) {
         throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-relation");
       }
       std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();