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 prototype.
8 ** Copyright (c) 2013-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
) {
38 TNode::iterator it
= n
.begin();
39 TNode::iterator it_end
= n
.end();
40 for (; it
!= it_end
; ++ it
) {
41 TypeNode t
= (*it
).getType(check
);
43 throw TypeCheckingExceptionPrivate(n
, "expecting string terms in string concat");
46 return nodeManager
->stringType();
50 class StringLengthTypeRule
{
52 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
53 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
55 TypeNode t
= n
[0].getType(check
);
57 throw TypeCheckingExceptionPrivate(n
, "expecting string terms in string length");
60 return nodeManager
->integerType();
64 class StringSubstrTypeRule
{
66 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
67 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
69 TypeNode t
= n
[0].getType(check
);
71 throw TypeCheckingExceptionPrivate(n
, "expecting string terms in substr");
73 t
= n
[1].getType(check
);
75 throw TypeCheckingExceptionPrivate(n
, "expecting start int terms in substr");
77 t
= n
[2].getType(check
);
79 throw TypeCheckingExceptionPrivate(n
, "expecting length int terms in substr");
82 return nodeManager
->stringType();
86 class RegExpConstantTypeRule
{
88 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
89 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
90 return nodeManager
->regexpType();
94 class RegExpConcatTypeRule
{
96 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
97 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
98 TNode::iterator it
= n
.begin();
99 TNode::iterator it_end
= n
.end();
100 for (; it
!= it_end
; ++ it
) {
101 TypeNode t
= (*it
).getType(check
);
103 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
106 return nodeManager
->regexpType();
110 class RegExpOrTypeRule
{
112 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
113 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
114 TNode::iterator it
= n
.begin();
115 TNode::iterator it_end
= n
.end();
116 for (; it
!= it_end
; ++ it
) {
117 TypeNode t
= (*it
).getType(check
);
119 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
122 return nodeManager
->regexpType();
126 class RegExpInterTypeRule
{
128 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
129 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
130 TNode::iterator it
= n
.begin();
131 TNode::iterator it_end
= n
.end();
132 for (; it
!= it_end
; ++ it
) {
133 TypeNode t
= (*it
).getType(check
);
135 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
138 return nodeManager
->regexpType();
142 class RegExpStarTypeRule
{
144 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
145 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
146 TNode::iterator it
= n
.begin();
147 TNode::iterator it_end
= n
.end();
148 TypeNode t
= (*it
).getType(check
);
150 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
153 throw TypeCheckingExceptionPrivate(n
, "too many regexp");
156 return nodeManager
->regexpType();
160 class RegExpPlusTypeRule
{
162 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
163 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
164 TNode::iterator it
= n
.begin();
165 TNode::iterator it_end
= n
.end();
166 TypeNode t
= (*it
).getType(check
);
168 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
171 throw TypeCheckingExceptionPrivate(n
, "too many regexp");
174 return nodeManager
->regexpType();
178 class RegExpOptTypeRule
{
180 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
181 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
182 TNode::iterator it
= n
.begin();
183 TNode::iterator it_end
= n
.end();
184 TypeNode t
= (*it
).getType(check
);
186 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
189 throw TypeCheckingExceptionPrivate(n
, "too many regexp");
192 return nodeManager
->regexpType();
196 class StringToRegExpTypeRule
{
198 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
199 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
200 TNode::iterator it
= n
.begin();
201 TNode::iterator it_end
= n
.end();
202 TypeNode t
= (*it
).getType(check
);
204 throw TypeCheckingExceptionPrivate(n
, "expecting string terms");
206 if( (*it
).getKind() != kind::CONST_STRING
) {
207 throw TypeCheckingExceptionPrivate(n
, "expecting constant string terms");
210 throw TypeCheckingExceptionPrivate(n
, "too many terms");
213 return nodeManager
->regexpType();
217 class StringInRegExpTypeRule
{
219 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
220 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
221 TNode::iterator it
= n
.begin();
222 TNode::iterator it_end
= n
.end();
223 TypeNode t
= (*it
).getType(check
);
225 throw TypeCheckingExceptionPrivate(n
, "expecting string terms");
228 t
= (*it
).getType(check
);
230 throw TypeCheckingExceptionPrivate(n
, "expecting regexp terms");
233 throw TypeCheckingExceptionPrivate(n
, "too many terms");
236 return nodeManager
->booleanType();
241 }/* CVC4::theory::strings namespace */
242 }/* CVC4::theory namespace */
243 }/* CVC4 namespace */
245 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */