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                 TNode::iterator it_end = n.end();
 311                 TypeNode t = (*it).getType(check);
 312                 if (!t.isRegExp()) {
 313                   throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 314                 }
 315         }
 316     return nodeManager->regexpType();
 317   }
 318 };
 319
 320 class RegExpPlusTypeRule {
 321 public:
 322   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 323       throw (TypeCheckingExceptionPrivate, AssertionException) {
 324     if( check ) {
 325                 TNode::iterator it = n.begin();
 326                 TNode::iterator it_end = n.end();
 327                 TypeNode t = (*it).getType(check);
 328                 if (!t.isRegExp()) {
 329                   throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 330                 }
 331         }
 332     return nodeManager->regexpType();
 333   }
 334 };
 335
 336 class RegExpOptTypeRule {
 337 public:
 338   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 339       throw (TypeCheckingExceptionPrivate, AssertionException) {
 340     if( check ) {
 341                 TNode::iterator it = n.begin();
 342                 TNode::iterator it_end = n.end();
 343                 TypeNode t = (*it).getType(check);
 344                 if (!t.isRegExp()) {
 345                   throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 346                 }
 347         }
 348     return nodeManager->regexpType();
 349   }
 350 };
 351
 352 class RegExpRangeTypeRule {
 353 public:
 354   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 355       throw (TypeCheckingExceptionPrivate, AssertionException) {
 356     if( check ) {
 357                 TNode::iterator it = n.begin();
 358                 TNode::iterator it_end = n.end();
 359                 char ch[2];
 360
 361                 for(int i=0; i<2; ++i) {
 362                         TypeNode t = (*it).getType(check);
 363                         if (!t.isString()) {
 364                           throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
 365                         }
 366                         if( (*it).getKind() != kind::CONST_STRING ) {
 367                           throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
 368                         }
 369                         if( (*it).getConst<String>().size() != 1 ) {
 370                           throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
 371                         }
 372                         ch[i] = (*it).getConst<String>().getFirstChar();
 373                         ++it;
 374                 }
 375                 if(ch[0] > ch[1]) {
 376                         throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
 377                 }
 378         }
 379     return nodeManager->regexpType();
 380   }
 381 };
 382
 383 class RegExpLoopTypeRule {
 384 public:
 385   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 386       throw (TypeCheckingExceptionPrivate, AssertionException) {
 387     if( check ) {
 388                 TNode::iterator it = n.begin();
 389                 TNode::iterator it_end = n.end();
 390                 TypeNode t = (*it).getType(check);
 391                 if (!t.isRegExp()) {
 392                   throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1");
 393                 }
 394                 ++it; t = (*it).getType(check);
 395                 if (!t.isInteger()) {
 396                   throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
 397                 }
 398                 if(!(*it).isConst()) {
 399                   throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
 400                 }
 401                 ++it;
 402                 if(it != it_end) {
 403                         t = (*it).getType(check);
 404                         if (!t.isInteger()) {
 405                           throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
 406                         }
 407                         if(!(*it).isConst()) {
 408                           throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
 409                         }
 410                         //if(++it != it_end) {
 411                         //  throw TypeCheckingExceptionPrivate(n, "too many regexp");
 412                         //}
 413                 }
 414         }
 415     return nodeManager->regexpType();
 416   }
 417 };
 418
 419 class StringToRegExpTypeRule {
 420 public:
 421   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 422       throw (TypeCheckingExceptionPrivate, AssertionException) {
 423     if( check ) {
 424                 TNode::iterator it = n.begin();
 425                 TNode::iterator it_end = n.end();
 426                 TypeNode t = (*it).getType(check);
 427                 if (!t.isString()) {
 428                   throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 429                 }
 430                 //if( (*it).getKind() != kind::CONST_STRING ) {
 431                 //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
 432                 //}
 433         }
 434     return nodeManager->regexpType();
 435   }
 436 };
 437
 438 class StringInRegExpTypeRule {
 439 public:
 440   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 441       throw (TypeCheckingExceptionPrivate, AssertionException) {
 442     if( check ) {
 443                 TNode::iterator it = n.begin();
 444                 TNode::iterator it_end = n.end();
 445                 TypeNode t = (*it).getType(check);
 446                 if (!t.isString()) {
 447                   throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 448                 }
 449                 ++it;
 450                 t = (*it).getType(check);
 451                 if (!t.isRegExp()) {
 452                   throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 453                 }
 454         }
 455     return nodeManager->booleanType();
 456   }
 457 };
 458
 459 class EmptyRegExpTypeRule {
 460 public:
 461   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 462     throw (TypeCheckingExceptionPrivate, AssertionException) {
 463
 464     Assert(n.getKind() == kind::REGEXP_EMPTY);
 465     return nodeManager->regexpType();
 466   }
 467 };
 468
 469 class SigmaRegExpTypeRule {
 470 public:
 471   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 472     throw (TypeCheckingExceptionPrivate, AssertionException) {
 473
 474     Assert(n.getKind() == kind::REGEXP_SIGMA);
 475     return nodeManager->regexpType();
 476   }
 477 };
 478
 479 }/* CVC4::theory::strings namespace */
 480 }/* CVC4::theory namespace */
 481 }/* CVC4 namespace */
 482
 483 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */