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