1 /********************* */
2 /*! \file theory_strings_type_rules.h
4 ** Original author: Tianyi Liang
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Typing and cardinality rules for the theory of arrays
14 ** Typing and cardinality rules for the theory of arrays.
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
20 #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
26 class StringConstantTypeRule
{
28 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
29 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
30 return nodeManager
->stringType();
34 class StringConcatTypeRule
{
36 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
37 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
39 TNode::iterator it
= n
.begin();
40 TNode::iterator it_end
= n
.end();
42 for (; it
!= it_end
; ++ it
) {
43 TypeNode t
= (*it
).getType(check
);
45 throw TypeCheckingExceptionPrivate(n
, "expecting string terms in string concat");
50 throw TypeCheckingExceptionPrivate(n
, "expecting at least 2 terms in string concat");
53 return nodeManager
->stringType();
57 class StringLengthTypeRule
{
59 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
60 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
62 TypeNode t
= n
[0].getType(check
);
64 throw TypeCheckingExceptionPrivate(n
, "expecting string terms in string length");
67 return nodeManager
->integerType();
71 class StringSubstrTypeRule
{
73 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
74 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
76 TypeNode t
= n
[0].getType(check
);
78 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in substr");
80 t
= n
[1].getType(check
);
82 throw TypeCheckingExceptionPrivate(n
, "expecting a start int term in substr");
84 t
= n
[2].getType(check
);
86 throw TypeCheckingExceptionPrivate(n
, "expecting a length int term in substr");
89 return nodeManager
->stringType();
93 class StringContainTypeRule
{
95 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
96 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
98 TypeNode t
= n
[0].getType(check
);
100 throw TypeCheckingExceptionPrivate(n
, "expecting an orginal string term in string contain");
102 t
= n
[1].getType(check
);
104 throw TypeCheckingExceptionPrivate(n
, "expecting a target string term in string contain");
107 return nodeManager
->booleanType();
111 class StringCharAtTypeRule
{
113 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
114 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
116 TypeNode t
= n
[0].getType(check
);
118 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string char at 0");
120 t
= n
[1].getType(check
);
121 if (!t
.isInteger()) {
122 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term in string char at 1");
125 return nodeManager
->stringType();
129 class StringIndexOfTypeRule
{
131 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
132 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
134 TypeNode t
= n
[0].getType(check
);
136 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string indexof 0");
138 t
= n
[1].getType(check
);
140 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string indexof 1");
142 t
= n
[2].getType(check
);
143 if (!t
.isInteger()) {
144 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term in string indexof 2");
147 return nodeManager
->integerType();
151 class StringReplaceTypeRule
{
153 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
154 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
156 TypeNode t
= n
[0].getType(check
);
158 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string replace 0");
160 t
= n
[1].getType(check
);
162 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string replace 1");
164 t
= n
[2].getType(check
);
166 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string replace 2");
169 return nodeManager
->stringType();
173 class StringPrefixOfTypeRule
{
175 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
176 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
178 TypeNode t
= n
[0].getType(check
);
180 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string prefixof 0");
182 t
= n
[1].getType(check
);
184 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string prefixof 1");
187 return nodeManager
->booleanType();
191 class StringSuffixOfTypeRule
{
193 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
194 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
196 TypeNode t
= n
[0].getType(check
);
198 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string suffixof 0");
200 t
= n
[1].getType(check
);
202 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string suffixof 1");
205 return nodeManager
->booleanType();
209 class StringIntToStrTypeRule
{
211 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
212 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
214 TypeNode t
= n
[0].getType(check
);
215 if (!t
.isInteger()) {
216 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term in int to string 0");
219 return nodeManager
->stringType();
223 class StringStrToIntTypeRule
{
225 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
226 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
228 TypeNode t
= n
[0].getType(check
);
230 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in string to int 0");
233 return nodeManager
->integerType();
237 class RegExpConstantTypeRule
{
239 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
240 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
241 return nodeManager
->regexpType();
245 class RegExpConcatTypeRule
{
247 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
248 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
250 TNode::iterator it
= n
.begin();
251 TNode::iterator it_end
= n
.end();
253 for (; it
!= it_end
; ++ it
) {
254 TypeNode t
= (*it
).getType(check
);
256 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms in regexp concat");
261 throw TypeCheckingExceptionPrivate(n
, "expecting at least 2 terms in regexp concat");
264 return nodeManager
->regexpType();
268 class RegExpUnionTypeRule
{
270 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
271 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
273 TNode::iterator it
= n
.begin();
274 TNode::iterator it_end
= n
.end();
275 for (; it
!= it_end
; ++ it
) {
276 TypeNode t
= (*it
).getType(check
);
278 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
282 return nodeManager
->regexpType();
286 class RegExpInterTypeRule
{
288 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
289 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
291 TNode::iterator it
= n
.begin();
292 TNode::iterator it_end
= n
.end();
293 for (; it
!= it_end
; ++ it
) {
294 TypeNode t
= (*it
).getType(check
);
296 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
300 return nodeManager
->regexpType();
304 class RegExpStarTypeRule
{
306 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
307 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
309 TNode::iterator it
= n
.begin();
310 TNode::iterator it_end
= n
.end();
311 TypeNode t
= (*it
).getType(check
);
313 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
316 return nodeManager
->regexpType();
320 class RegExpPlusTypeRule
{
322 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
323 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
325 TNode::iterator it
= n
.begin();
326 TNode::iterator it_end
= n
.end();
327 TypeNode t
= (*it
).getType(check
);
329 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
332 return nodeManager
->regexpType();
336 class RegExpOptTypeRule
{
338 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
339 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
341 TNode::iterator it
= n
.begin();
342 TNode::iterator it_end
= n
.end();
343 TypeNode t
= (*it
).getType(check
);
345 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
348 return nodeManager
->regexpType();
352 class RegExpRangeTypeRule
{
354 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
355 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
357 TNode::iterator it
= n
.begin();
358 TNode::iterator it_end
= n
.end();
361 for(int i
=0; i
<2; ++i
) {
362 TypeNode t
= (*it
).getType(check
);
364 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in regexp range");
366 if( (*it
).getKind() != kind::CONST_STRING
) {
367 throw TypeCheckingExceptionPrivate(n
, "expecting a constant string term in regexp range");
369 if( (*it
).getConst
<String
>().size() != 1 ) {
370 throw TypeCheckingExceptionPrivate(n
, "expecting a single constant string term in regexp range");
372 ch
[i
] = (*it
).getConst
<String
>().getFirstChar();
376 throw TypeCheckingExceptionPrivate(n
, "expecting the first constant is less or equal to the second one in regexp range");
379 return nodeManager
->regexpType();
383 class RegExpLoopTypeRule
{
385 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
386 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
388 TNode::iterator it
= n
.begin();
389 TNode::iterator it_end
= n
.end();
390 TypeNode t
= (*it
).getType(check
);
392 throw TypeCheckingExceptionPrivate(n
, "expecting a regexp term in regexp loop 1");
394 ++it
; t
= (*it
).getType(check
);
395 if (!t
.isInteger()) {
396 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term in regexp loop 2");
398 if(!(*it
).isConst()) {
399 throw TypeCheckingExceptionPrivate(n
, "expecting an const integer term in regexp loop 2");
403 t
= (*it
).getType(check
);
404 if (!t
.isInteger()) {
405 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term in regexp loop 3");
407 if(!(*it
).isConst()) {
408 throw TypeCheckingExceptionPrivate(n
, "expecting an const integer term in regexp loop 3");
410 //if(++it != it_end) {
411 // throw TypeCheckingExceptionPrivate(n, "too many regexp");
415 return nodeManager
->regexpType();
419 class StringToRegExpTypeRule
{
421 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
422 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
424 TNode::iterator it
= n
.begin();
425 TNode::iterator it_end
= n
.end();
426 TypeNode t
= (*it
).getType(check
);
428 throw TypeCheckingExceptionPrivate(n
, "expecting string terms");
430 //if( (*it).getKind() != kind::CONST_STRING ) {
431 // throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
434 return nodeManager
->regexpType();
438 class StringInRegExpTypeRule
{
440 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
441 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
443 TNode::iterator it
= n
.begin();
444 TNode::iterator it_end
= n
.end();
445 TypeNode t
= (*it
).getType(check
);
447 throw TypeCheckingExceptionPrivate(n
, "expecting string terms");
450 t
= (*it
).getType(check
);
452 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
455 return nodeManager
->booleanType();
459 class EmptyRegExpTypeRule
{
461 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
462 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
464 Assert(n
.getKind() == kind::REGEXP_EMPTY
);
465 return nodeManager
->regexpType();
469 class SigmaRegExpTypeRule
{
471 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
472 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
474 Assert(n
.getKind() == kind::REGEXP_SIGMA
);
475 return nodeManager
->regexpType();
479 }/* CVC4::theory::strings namespace */
480 }/* CVC4::theory namespace */
481 }/* CVC4 namespace */
483 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */