diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-05-15 13:10:56 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-15 13:10:56 -0500 |
| commit | 7edea2f0ad49de9f33e8c3eb50540e191a4f3728 (patch) | |
| tree | 5522bdfe4495be9669a7b0fe2091a0ddc792aa3b /src | |
| parent | f6215a3d10c11976cffbeb4c88223e8434ffc4d3 (diff) | |
| parent | 370052d7bb7125376eeb7296091f5ce977421efa (diff) | |
Merge pull request #159 from 4tXJ7f/fix_set_types
Fix type checks for relation operators
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 6 |
1 files changed, 3 insertions, 3 deletions
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(); |