1 /********************* */
2 /*! \file theory_strings_type_rules.h
4 ** Original author: Tianyi Liang
5 ** Major contributors: none
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 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 TypeNode t
= n
[0].getType(check
);
311 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
314 return nodeManager
->regexpType();
318 class RegExpPlusTypeRule
{
320 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
321 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
323 TypeNode t
= n
[0].getType(check
);
325 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
328 return nodeManager
->regexpType();
332 class RegExpOptTypeRule
{
334 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
335 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
337 TypeNode t
= n
[0].getType(check
);
339 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
342 return nodeManager
->regexpType();
346 class RegExpRangeTypeRule
{
348 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
349 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
351 TNode::iterator it
= n
.begin();
354 for(int i
=0; i
<2; ++i
) {
355 TypeNode t
= (*it
).getType(check
);
357 throw TypeCheckingExceptionPrivate(n
, "expecting a string term in regexp range");
359 if( (*it
).getKind() != kind::CONST_STRING
) {
360 throw TypeCheckingExceptionPrivate(n
, "expecting a constant string term in regexp range");
362 if( (*it
).getConst
<String
>().size() != 1 ) {
363 throw TypeCheckingExceptionPrivate(n
, "expecting a single constant string term in regexp range");
365 ch
[i
] = (*it
).getConst
<String
>().getFirstChar();
369 throw TypeCheckingExceptionPrivate(n
, "expecting the first constant is less or equal to the second one in regexp range");
372 return nodeManager
->regexpType();
376 class RegExpLoopTypeRule
{
378 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
379 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
381 TNode::iterator it
= n
.begin();
382 TNode::iterator it_end
= n
.end();
383 TypeNode t
= (*it
).getType(check
);
385 throw TypeCheckingExceptionPrivate(n
, "expecting a regexp term in regexp loop 1");
387 ++it
; t
= (*it
).getType(check
);
388 if (!t
.isInteger()) {
389 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term in regexp loop 2");
391 if(!(*it
).isConst()) {
392 throw TypeCheckingExceptionPrivate(n
, "expecting an const integer term in regexp loop 2");
396 t
= (*it
).getType(check
);
397 if (!t
.isInteger()) {
398 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term in regexp loop 3");
400 if(!(*it
).isConst()) {
401 throw TypeCheckingExceptionPrivate(n
, "expecting an const integer term in regexp loop 3");
403 //if(++it != it_end) {
404 // throw TypeCheckingExceptionPrivate(n, "too many regexp");
408 return nodeManager
->regexpType();
412 class StringToRegExpTypeRule
{
414 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
415 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
417 TypeNode t
= n
[0].getType(check
);
419 throw TypeCheckingExceptionPrivate(n
, "expecting string terms");
421 //if( (*it).getKind() != kind::CONST_STRING ) {
422 // throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
425 return nodeManager
->regexpType();
429 class StringInRegExpTypeRule
{
431 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
432 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
434 TNode::iterator it
= n
.begin();
435 TypeNode t
= (*it
).getType(check
);
437 throw TypeCheckingExceptionPrivate(n
, "expecting string terms");
440 t
= (*it
).getType(check
);
442 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
445 return nodeManager
->booleanType();
449 class EmptyRegExpTypeRule
{
451 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
452 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
454 Assert(n
.getKind() == kind::REGEXP_EMPTY
);
455 return nodeManager
->regexpType();
459 class SigmaRegExpTypeRule
{
461 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
462 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
464 Assert(n
.getKind() == kind::REGEXP_SIGMA
);
465 return nodeManager
->regexpType();
469 class RegExpRVTypeRule
{
471 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
472 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
474 TypeNode t
= n
[0].getType(check
);
475 if (!t
.isInteger()) {
476 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term in RV");
479 return nodeManager
->regexpType();
484 }/* CVC4::theory::strings namespace */
485 }/* CVC4::theory namespace */
486 }/* CVC4 namespace */
488 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */