src/theory/strings/theory_strings_type_rules.h

   1 /*********************                                                        */
   2 /*! \file theory_strings_type_rules.h
   3  ** \verbatim
   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
  11  **
  12  ** \brief Typing and cardinality rules for the theory of arrays
  13  **
  14  ** Typing and cardinality rules for the theory of arrays.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
  20 #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace strings {
  25
  26 class StringConstantTypeRule {
  27 public:
  28   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  29       throw (TypeCheckingExceptionPrivate, AssertionException) {
  30     return nodeManager->stringType();
  31   }
  32 };
  33
  34 class StringConcatTypeRule {
  35 public:
  36   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  37       throw (TypeCheckingExceptionPrivate, AssertionException) {
  38     if( check ){
  39                 TNode::iterator it = n.begin();
  40                 TNode::iterator it_end = n.end();
  41                 int size = 0;
  42                 for (; it != it_end; ++ it) {
  43                    TypeNode t = (*it).getType(check);
  44                    if (!t.isString()) {
  45                          throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
  46                    }
  47                    ++size;
  48                 }
  49                 if(size < 2) {
  50                    throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
  51                 }
  52         }
  53     return nodeManager->stringType();
  54   }
  55 };
  56
  57 class StringLengthTypeRule {
  58 public:
  59   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  60       throw (TypeCheckingExceptionPrivate, AssertionException) {
  61     if( check ) {
  62         TypeNode t = n[0].getType(check);
  63         if (!t.isString()) {
  64           throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
  65         }
  66     }
  67     return nodeManager->integerType();
  68   }
  69 };
  70
  71 class StringSubstrTypeRule {
  72 public:
  73   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  74       throw (TypeCheckingExceptionPrivate, AssertionException) {
  75     if( check ) {
  76         TypeNode t = n[0].getType(check);
  77         if (!t.isString()) {
  78           throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
  79         }
  80                 t = n[1].getType(check);
  81         if (!t.isInteger()) {
  82           throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
  83         }
  84                 t = n[2].getType(check);
  85         if (!t.isInteger()) {
  86           throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
  87         }
  88     }
  89     return nodeManager->stringType();
  90   }
  91 };
  92
  93 class StringContainTypeRule {
  94 public:
  95   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  96       throw (TypeCheckingExceptionPrivate, AssertionException) {
  97     if( check ) {
  98         TypeNode t = n[0].getType(check);
  99         if (!t.isString()) {
 100           throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
 101         }
 102                 t = n[1].getType(check);
 103         if (!t.isString()) {
 104           throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
 105         }
 106     }
 107     return nodeManager->booleanType();
 108   }
 109 };
 110
 111 class StringCharAtTypeRule {
 112 public:
 113   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 114       throw (TypeCheckingExceptionPrivate, AssertionException) {
 115     if( check ) {
 116         TypeNode t = n[0].getType(check);
 117         if (!t.isString()) {
 118           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0");
 119         }
 120                 t = n[1].getType(check);
 121         if (!t.isInteger()) {
 122           throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1");
 123         }
 124     }
 125     return nodeManager->stringType();
 126   }
 127 };
 128
 129 class StringIndexOfTypeRule {
 130 public:
 131   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 132       throw (TypeCheckingExceptionPrivate, AssertionException) {
 133     if( check ) {
 134         TypeNode t = n[0].getType(check);
 135         if (!t.isString()) {
 136           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0");
 137         }
 138                 t = n[1].getType(check);
 139         if (!t.isString()) {
 140           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1");
 141         }
 142                 t = n[2].getType(check);
 143         if (!t.isInteger()) {
 144           throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2");
 145         }
 146     }
 147     return nodeManager->integerType();
 148   }
 149 };
 150
 151 class StringReplaceTypeRule {
 152 public:
 153   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 154       throw (TypeCheckingExceptionPrivate, AssertionException) {
 155     if( check ) {
 156         TypeNode t = n[0].getType(check);
 157         if (!t.isString()) {
 158           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0");
 159         }
 160                 t = n[1].getType(check);
 161         if (!t.isString()) {
 162           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1");
 163         }
 164                 t = n[2].getType(check);
 165         if (!t.isString()) {
 166           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2");
 167         }
 168     }
 169     return nodeManager->stringType();
 170   }
 171 };
 172
 173 class StringPrefixOfTypeRule {
 174 public:
 175   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 176       throw (TypeCheckingExceptionPrivate, AssertionException) {
 177     if( check ) {
 178         TypeNode t = n[0].getType(check);
 179         if (!t.isString()) {
 180           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 0");
 181         }
 182                 t = n[1].getType(check);
 183         if (!t.isString()) {
 184           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
 185         }
 186     }
 187     return nodeManager->booleanType();
 188   }
 189 };
 190
 191 class StringSuffixOfTypeRule {
 192 public:
 193   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 194       throw (TypeCheckingExceptionPrivate, AssertionException) {
 195     if( check ) {
 196         TypeNode t = n[0].getType(check);
 197         if (!t.isString()) {
 198           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 0");
 199         }
 200                 t = n[1].getType(check);
 201         if (!t.isString()) {
 202           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
 203         }
 204     }
 205     return nodeManager->booleanType();
 206   }
 207 };
 208
 209 class StringIntToStrTypeRule {
 210 public:
 211   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 212       throw (TypeCheckingExceptionPrivate, AssertionException) {
 213     if( check ) {
 214         TypeNode t = n[0].getType(check);
 215         if (!t.isInteger()) {
 216           throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0");
 217         }
 218     }
 219     return nodeManager->stringType();
 220   }
 221 };
 222
 223 class StringStrToIntTypeRule {
 224 public:
 225   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 226       throw (TypeCheckingExceptionPrivate, AssertionException) {
 227     if( check ) {
 228         TypeNode t = n[0].getType(check);
 229         if (!t.isString()) {
 230           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string to int 0");
 231         }
 232     }
 233     return nodeManager->integerType();
 234   }
 235 };
 236
 237 class RegExpConstantTypeRule {
 238 public:
 239   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 240       throw (TypeCheckingExceptionPrivate, AssertionException) {
 241     return nodeManager->regexpType();
 242   }
 243 };
 244
 245 class RegExpConcatTypeRule {
 246 public:
 247   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 248       throw (TypeCheckingExceptionPrivate, AssertionException) {
 249     if( check ) {
 250                 TNode::iterator it = n.begin();
 251                 TNode::iterator it_end = n.end();
 252                 int size = 0;
 253                 for (; it != it_end; ++ it) {
 254                    TypeNode t = (*it).getType(check);
 255                    if (!t.isRegExp()) {
 256                          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
 257                    }
 258                    ++size;
 259                 }
 260                 if(size < 2) {
 261                    throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
 262                 }
 263         }
 264     return nodeManager->regexpType();
 265   }
 266 };
 267
 268 class RegExpUnionTypeRule {
 269 public:
 270   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 271       throw (TypeCheckingExceptionPrivate, AssertionException) {
 272     if( check ) {
 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);
 277                    if (!t.isRegExp()) {
 278                          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 279                    }
 280                 }
 281         }
 282     return nodeManager->regexpType();
 283   }
 284 };
 285
 286 class RegExpInterTypeRule {
 287 public:
 288   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 289       throw (TypeCheckingExceptionPrivate, AssertionException) {
 290     if( check ) {
 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);
 295                    if (!t.isRegExp()) {
 296                          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 297                    }
 298                 }
 299         }
 300     return nodeManager->regexpType();
 301   }
 302 };
 303
 304 class RegExpStarTypeRule {
 305 public:
 306   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 307       throw (TypeCheckingExceptionPrivate, AssertionException) {
 308     if( check ) {
 309                 TNode::iterator it = n.begin();
 310                 TypeNode t = (*it).getType(check);
 311                 if (!t.isRegExp()) {
 312                   throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 313                 }
 314         }
 315     return nodeManager->regexpType();
 316   }
 317 };
 318
 319 class RegExpPlusTypeRule {
 320 public:
 321   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 322       throw (TypeCheckingExceptionPrivate, AssertionException) {
 323     if( check ) {
 324                 TNode::iterator it = n.begin();
 325                 TypeNode t = (*it).getType(check);
 326                 if (!t.isRegExp()) {
 327                   throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 328                 }
 329         }
 330     return nodeManager->regexpType();
 331   }
 332 };
 333
 334 class RegExpOptTypeRule {
 335 public:
 336   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 337       throw (TypeCheckingExceptionPrivate, AssertionException) {
 338     if( check ) {
 339                 TNode::iterator it = n.begin();
 340                 TypeNode t = (*it).getType(check);
 341                 if (!t.isRegExp()) {
 342                   throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 343                 }
 344         }
 345     return nodeManager->regexpType();
 346   }
 347 };
 348
 349 class RegExpRangeTypeRule {
 350 public:
 351   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 352       throw (TypeCheckingExceptionPrivate, AssertionException) {
 353     if( check ) {
 354                 TNode::iterator it = n.begin();
 355                 char ch[2];
 356
 357                 for(int i=0; i<2; ++i) {
 358                         TypeNode t = (*it).getType(check);
 359                         if (!t.isString()) {
 360                           throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
 361                         }
 362                         if( (*it).getKind() != kind::CONST_STRING ) {
 363                           throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
 364                         }
 365                         if( (*it).getConst<String>().size() != 1 ) {
 366                           throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
 367                         }
 368                         ch[i] = (*it).getConst<String>().getFirstChar();
 369                         ++it;
 370                 }
 371                 if(ch[0] > ch[1]) {
 372                         throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
 373                 }
 374         }
 375     return nodeManager->regexpType();
 376   }
 377 };
 378
 379 class RegExpLoopTypeRule {
 380 public:
 381   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 382       throw (TypeCheckingExceptionPrivate, AssertionException) {
 383     if( check ) {
 384                 TNode::iterator it = n.begin();
 385                 TNode::iterator it_end = n.end();
 386                 TypeNode t = (*it).getType(check);
 387                 if (!t.isRegExp()) {
 388                   throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1");
 389                 }
 390                 ++it; t = (*it).getType(check);
 391                 if (!t.isInteger()) {
 392                   throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
 393                 }
 394                 if(!(*it).isConst()) {
 395                   throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
 396                 }
 397                 ++it;
 398                 if(it != it_end) {
 399                         t = (*it).getType(check);
 400                         if (!t.isInteger()) {
 401                           throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
 402                         }
 403                         if(!(*it).isConst()) {
 404                           throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
 405                         }
 406                         //if(++it != it_end) {
 407                         //  throw TypeCheckingExceptionPrivate(n, "too many regexp");
 408                         //}
 409                 }
 410         }
 411     return nodeManager->regexpType();
 412   }
 413 };
 414
 415 class StringToRegExpTypeRule {
 416 public:
 417   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 418       throw (TypeCheckingExceptionPrivate, AssertionException) {
 419     if( check ) {
 420                 TNode::iterator it = n.begin();
 421                 TypeNode t = (*it).getType(check);
 422                 if (!t.isString()) {
 423                   throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 424                 }
 425                 //if( (*it).getKind() != kind::CONST_STRING ) {
 426                 //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
 427                 //}
 428         }
 429     return nodeManager->regexpType();
 430   }
 431 };
 432
 433 class StringInRegExpTypeRule {
 434 public:
 435   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 436       throw (TypeCheckingExceptionPrivate, AssertionException) {
 437     if( check ) {
 438                 TNode::iterator it = n.begin();
 439                 TypeNode t = (*it).getType(check);
 440                 if (!t.isString()) {
 441                   throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 442                 }
 443                 ++it;
 444                 t = (*it).getType(check);
 445                 if (!t.isRegExp()) {
 446                   throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 447                 }
 448         }
 449     return nodeManager->booleanType();
 450   }
 451 };
 452
 453 class EmptyRegExpTypeRule {
 454 public:
 455   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 456     throw (TypeCheckingExceptionPrivate, AssertionException) {
 457
 458     Assert(n.getKind() == kind::REGEXP_EMPTY);
 459     return nodeManager->regexpType();
 460   }
 461 };
 462
 463 class SigmaRegExpTypeRule {
 464 public:
 465   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 466     throw (TypeCheckingExceptionPrivate, AssertionException) {
 467
 468     Assert(n.getKind() == kind::REGEXP_SIGMA);
 469     return nodeManager->regexpType();
 470   }
 471 };
 472
 473 }/* CVC4::theory::strings namespace */
 474 }/* CVC4::theory namespace */
 475 }/* CVC4 namespace */
 476
 477 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */