src/theory/strings/theory_strings_type_rules.h

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