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