diff options
author | Paul Meng <baolmeng@gmail.com> | 2016-09-13 16:11:16 -0500 |
---|---|---|
committer | Paul Meng <baolmeng@gmail.com> | 2016-09-13 16:11:16 -0500 |
commit | 56670c697402a74b1769215bcde87b56f17e79b9 (patch) | |
tree | 322f17846afc6ac473ac686a6310eb5e188b20c3 /src/theory/sets | |
parent | 680e0d843eced443e9d484c441b895abb403d4e0 (diff) |
fixed type checking and computing for PRODUCT and JOIN
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 48 |
1 files changed, 24 insertions, 24 deletions
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; } |