1 /********************* */ 2 /*! \file theory_sets_type_rules.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Kshitij Bansal, Andrew Reynolds, Paul Meng 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Sets theory type rules. 13 ** 14 ** Sets theory type rules. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H 20 #define __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H 21 22 #include "theory/sets/normal_form.h" 23 24 namespace CVC4 { 25 namespace theory { 26 namespace sets { 27 28 class SetsTypeRule { 29 public: 30 31 /** 32 * Compute the type for (and optionally typecheck) a term belonging 33 * to the theory of sets. 34 * 35 * @param check if true, the node's type should be checked as well 36 * as computed. 37 */ computeType(NodeManager * nodeManager,TNode n,bool check)38 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 39 bool check) 40 { 41 // TODO: implement me! 42 Unimplemented(); 43 44 } 45 46 };/* class SetsTypeRule */ 47 48 struct SetsBinaryOperatorTypeRule { computeTypeSetsBinaryOperatorTypeRule49 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 50 { 51 Assert(n.getKind() == kind::UNION || 52 n.getKind() == kind::INTERSECTION || 53 n.getKind() == kind::SETMINUS); 54 TypeNode setType = n[0].getType(check); 55 if( check ) { 56 if(!setType.isSet()) { 57 throw TypeCheckingExceptionPrivate(n, "operator expects a set, first argument is not"); 58 } 59 TypeNode secondSetType = n[1].getType(check); 60 if(secondSetType != setType) { 61 if( n.getKind() == kind::INTERSECTION ){ 62 setType = TypeNode::mostCommonTypeNode( secondSetType, setType ); 63 }else{ 64 setType = TypeNode::leastCommonTypeNode( secondSetType, setType ); 65 } 66 if( setType.isNull() ){ 67 throw TypeCheckingExceptionPrivate(n, "operator expects two sets of comparable types"); 68 } 69 70 } 71 } 72 return setType; 73 } 74 computeIsConstSetsBinaryOperatorTypeRule75 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 76 Assert(n.getKind() == kind::UNION || 77 n.getKind() == kind::INTERSECTION || 78 n.getKind() == kind::SETMINUS); 79 if(n.getKind() == kind::UNION) { 80 return NormalForm::checkNormalConstant(n); 81 } else { 82 return false; 83 } 84 } 85 };/* struct SetUnionTypeRule */ 86 87 struct SubsetTypeRule { computeTypeSubsetTypeRule88 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 89 { 90 Assert(n.getKind() == kind::SUBSET); 91 TypeNode setType = n[0].getType(check); 92 if( check ) { 93 if(!setType.isSet()) { 94 throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set"); 95 } 96 TypeNode secondSetType = n[1].getType(check); 97 if(secondSetType != setType) { 98 if( !setType.isComparableTo( secondSetType ) ){ 99 throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types"); 100 } 101 } 102 } 103 return nodeManager->booleanType(); 104 } 105 };/* struct SetSubsetTypeRule */ 106 107 struct MemberTypeRule { computeTypeMemberTypeRule108 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 109 { 110 Assert(n.getKind() == kind::MEMBER); 111 TypeNode setType = n[1].getType(check); 112 if( check ) { 113 if(!setType.isSet()) { 114 throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set"); 115 } 116 TypeNode elementType = n[0].getType(check); 117 // TODO : still need to be flexible here due to situations like: 118 // 119 // T : (Set Int) 120 // S : (Set Real) 121 // (= (as T (Set Real)) S) 122 // (member 0.5 S) 123 // ...where (member 0.5 T) is inferred 124 // 125 // or 126 // 127 // S : (Set Real) 128 // (not (member 0.5 s)) 129 // (member 0.0 s) 130 // ...find model M where M( s ) = { 0 }, check model will generate (not (member 0.5 (singleton 0))) 131 // 132 if(!elementType.isComparableTo(setType.getSetElementType())) { 133 //if(!elementType.isSubtypeOf(setType.getSetElementType())) { //FIXME:typing 134 std::stringstream ss; 135 ss << "member operating on sets of different types:\n" 136 << "child type: " << elementType << "\n" 137 << "not subtype: " << setType.getSetElementType() << "\n" 138 << "in term : " << n; 139 throw TypeCheckingExceptionPrivate(n, ss.str()); 140 } 141 } 142 return nodeManager->booleanType(); 143 } 144 };/* struct MemberTypeRule */ 145 146 struct SingletonTypeRule { computeTypeSingletonTypeRule147 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 148 { 149 Assert(n.getKind() == kind::SINGLETON); 150 return nodeManager->mkSetType(n[0].getType(check)); 151 } 152 computeIsConstSingletonTypeRule153 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 154 Assert(n.getKind() == kind::SINGLETON); 155 return n[0].isConst(); 156 } 157 };/* struct SingletonTypeRule */ 158 159 struct EmptySetTypeRule { computeTypeEmptySetTypeRule160 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 161 { 162 Assert(n.getKind() == kind::EMPTYSET); 163 EmptySet emptySet = n.getConst<EmptySet>(); 164 Type setType = emptySet.getType(); 165 return TypeNode::fromType(setType); 166 } 167 };/* struct EmptySetTypeRule */ 168 169 struct CardTypeRule { computeTypeCardTypeRule170 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 171 { 172 Assert(n.getKind() == kind::CARD); 173 TypeNode setType = n[0].getType(check); 174 if( check ) { 175 if(!setType.isSet()) { 176 throw TypeCheckingExceptionPrivate(n, "cardinality operates on a set, non-set object found"); 177 } 178 } 179 return nodeManager->integerType(); 180 } 181 computeIsConstCardTypeRule182 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 183 Assert(n.getKind() == kind::CARD); 184 return false; 185 } 186 };/* struct CardTypeRule */ 187 188 struct ComplementTypeRule { computeTypeComplementTypeRule189 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 190 { 191 Assert(n.getKind() == kind::COMPLEMENT); 192 TypeNode setType = n[0].getType(check); 193 if( check ) { 194 if(!setType.isSet()) { 195 throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found"); 196 } 197 } 198 return setType; 199 } 200 computeIsConstComplementTypeRule201 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 202 Assert(n.getKind() == kind::COMPLEMENT); 203 return false; 204 } 205 };/* struct ComplementTypeRule */ 206 207 struct UniverseSetTypeRule { computeTypeUniverseSetTypeRule208 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 209 { 210 Assert(n.getKind() == kind::UNIVERSE_SET); 211 // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation 212 Assert(check); 213 TypeNode setType = n.getType(); 214 if(!setType.isSet()) { 215 throw TypeCheckingExceptionPrivate(n, "Non-set type found for universe set"); 216 } 217 return setType; 218 } 219 };/* struct ComplementTypeRule */ 220 221 struct InsertTypeRule { computeTypeInsertTypeRule222 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 223 { 224 Assert(n.getKind() == kind::INSERT); 225 size_t numChildren = n.getNumChildren(); 226 Assert( numChildren >= 2 ); 227 TypeNode setType = n[numChildren-1].getType(check); 228 if( check ) { 229 if(!setType.isSet()) { 230 throw TypeCheckingExceptionPrivate(n, "inserting into a non-set"); 231 } 232 for(size_t i = 0; i < numChildren-1; ++i) { 233 TypeNode elementType = n[i].getType(check); 234 if(elementType != setType.getSetElementType()) { 235 throw TypeCheckingExceptionPrivate 236 (n, "type of element should be same as element type of set being inserted into"); 237 } 238 } 239 } 240 return setType; 241 } 242 computeIsConstInsertTypeRule243 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 244 Assert(n.getKind() == kind::INSERT); 245 return false; 246 } 247 };/* struct InsertTypeRule */ 248 249 struct RelBinaryOperatorTypeRule { computeTypeRelBinaryOperatorTypeRule250 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 251 { 252 Assert(n.getKind() == kind::PRODUCT || 253 n.getKind() == kind::JOIN); 254 255 TypeNode firstRelType = n[0].getType(check); 256 TypeNode secondRelType = n[1].getType(check); 257 TypeNode resultType = firstRelType; 258 259 if(!firstRelType.isSet() || !secondRelType.isSet()) { 260 throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-sets"); 261 } 262 if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) { 263 throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-relations (sets of tuples)"); 264 } 265 266 std::vector<TypeNode> newTupleTypes; 267 std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes(); 268 std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes(); 269 270 // JOIN is not allowed to apply on two unary sets 271 if( n.getKind() == kind::JOIN ) { 272 if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) { 273 throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations"); 274 } else if(firstTupleTypes.back() != secondTupleTypes.front()) { 275 throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations"); 276 } 277 newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1); 278 newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end()); 279 }else if( n.getKind() == kind::PRODUCT ) { 280 newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()); 281 newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end()); 282 } 283 resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); 284 285 return resultType; 286 } 287 computeIsConstRelBinaryOperatorTypeRule288 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 289 Assert(n.getKind() == kind::JOIN || 290 n.getKind() == kind::PRODUCT); 291 return false; 292 } 293 };/* struct RelBinaryOperatorTypeRule */ 294 295 struct RelTransposeTypeRule { computeTypeRelTransposeTypeRule296 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 297 { 298 Assert(n.getKind() == kind::TRANSPOSE); 299 TypeNode setType = n[0].getType(check); 300 if(check && (!setType.isSet() || !setType.getSetElementType().isTuple())) { 301 throw TypeCheckingExceptionPrivate(n, "relation transpose operates on non-relation"); 302 } 303 std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes(); 304 std::reverse(tupleTypes.begin(), tupleTypes.end()); 305 return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); 306 } 307 computeIsConstRelTransposeTypeRule308 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 309 return false; 310 } 311 };/* struct RelTransposeTypeRule */ 312 313 struct RelTransClosureTypeRule { computeTypeRelTransClosureTypeRule314 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 315 { 316 Assert(n.getKind() == kind::TCLOSURE); 317 TypeNode setType = n[0].getType(check); 318 if(check) { 319 if(!setType.isSet() || !setType.getSetElementType().isTuple()) { 320 throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-relation"); 321 } 322 std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes(); 323 if(tupleTypes.size() != 2) { 324 throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-binary relations"); 325 } 326 if(tupleTypes[0] != tupleTypes[1]) { 327 throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-homogeneous binary relations"); 328 } 329 } 330 return setType; 331 } 332 computeIsConstRelTransClosureTypeRule333 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 334 Assert(n.getKind() == kind::TCLOSURE); 335 return false; 336 } 337 };/* struct RelTransClosureTypeRule */ 338 339 struct JoinImageTypeRule { computeTypeJoinImageTypeRule340 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 341 { 342 Assert(n.getKind() == kind::JOIN_IMAGE); 343 344 TypeNode firstRelType = n[0].getType(check); 345 346 if(!firstRelType.isSet()) { 347 throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations"); 348 } 349 if(!firstRelType[0].isTuple()) { 350 throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations (sets of tuples)"); 351 } 352 353 std::vector<TypeNode> tupleTypes = firstRelType[0].getTupleTypes(); 354 if(tupleTypes.size() != 2) { 355 throw TypeCheckingExceptionPrivate(n, " JoinImage operates on a non-binary relation"); 356 } 357 TypeNode valType = n[1].getType(check); 358 if (valType != nodeManager->integerType()) { 359 throw TypeCheckingExceptionPrivate( 360 n, " JoinImage cardinality constraint must be integer"); 361 } 362 if (n[1].getKind() != kind::CONST_RATIONAL) { 363 throw TypeCheckingExceptionPrivate( 364 n, " JoinImage cardinality constraint must be a constant"); 365 } 366 CVC4::Rational r(INT_MAX); 367 if (n[1].getConst<Rational>() > r) { 368 throw TypeCheckingExceptionPrivate( 369 n, " JoinImage Exceeded INT_MAX in cardinality constraint"); 370 } 371 if (n[1].getConst<Rational>().getNumerator().getSignedInt() < 0) { 372 throw TypeCheckingExceptionPrivate( 373 n, " JoinImage cardinality constraint must be non-negative"); 374 } 375 std::vector<TypeNode> newTupleTypes; 376 newTupleTypes.push_back(tupleTypes[0]); 377 return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); 378 } 379 computeIsConstJoinImageTypeRule380 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 381 Assert(n.getKind() == kind::JOIN_IMAGE); 382 return false; 383 } 384 };/* struct JoinImageTypeRule */ 385 386 struct RelIdenTypeRule { computeTypeRelIdenTypeRule387 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 388 { 389 Assert(n.getKind() == kind::IDEN); 390 TypeNode setType = n[0].getType(check); 391 if(check) { 392 if(!setType.isSet() && !setType.getSetElementType().isTuple()) { 393 throw TypeCheckingExceptionPrivate(n, " Identity operates on non-relation"); 394 } 395 if(setType[0].getTupleTypes().size() != 1) { 396 throw TypeCheckingExceptionPrivate(n, " Identity operates on non-unary relations"); 397 } 398 } 399 std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes(); 400 tupleTypes.push_back(tupleTypes[0]); 401 return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); 402 } 403 computeIsConstRelIdenTypeRule404 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 405 return false; 406 } 407 };/* struct RelIdenTypeRule */ 408 409 struct SetsProperties { computeCardinalitySetsProperties410 inline static Cardinality computeCardinality(TypeNode type) { 411 Assert(type.getKind() == kind::SET_TYPE); 412 Cardinality elementCard = 2; 413 elementCard ^= type[0].getCardinality(); 414 return elementCard; 415 } 416 isWellFoundedSetsProperties417 inline static bool isWellFounded(TypeNode type) { 418 return type[0].isWellFounded(); 419 } 420 mkGroundTermSetsProperties421 inline static Node mkGroundTerm(TypeNode type) { 422 Assert(type.isSet()); 423 return NodeManager::currentNM()->mkConst(EmptySet(type.toType())); 424 } 425 };/* struct SetsProperties */ 426 427 }/* CVC4::theory::sets namespace */ 428 }/* CVC4::theory namespace */ 429 }/* CVC4 namespace */ 430 431 #endif /* __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */ 432