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     TNode::iterator it = n.begin();
  39     TNode::iterator it_end = n.end();
  40         int size = 0;
  41     for (; it != it_end; ++ it) {
  42        TypeNode t = (*it).getType(check);
  43        if (!t.isString()) {
  44          throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
  45        }
  46            ++size;
  47     }
  48         if(size < 2) {
  49        throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
  50         }
  51     return nodeManager->stringType();
  52   }
  53 };
  54
  55 class StringLengthTypeRule {
  56 public:
  57   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  58       throw (TypeCheckingExceptionPrivate, AssertionException) {
  59     if( check ){
  60         TypeNode t = n[0].getType(check);
  61         if (!t.isString()) {
  62           throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
  63         }
  64     }
  65     return nodeManager->integerType();
  66   }
  67 };
  68
  69 class StringSubstrTypeRule {
  70 public:
  71   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  72       throw (TypeCheckingExceptionPrivate, AssertionException) {
  73     if( check ){
  74         TypeNode t = n[0].getType(check);
  75         if (!t.isString()) {
  76           throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
  77         }
  78                 t = n[1].getType(check);
  79         if (!t.isInteger()) {
  80           throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
  81         }
  82                 t = n[2].getType(check);
  83         if (!t.isInteger()) {
  84           throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
  85         }
  86     }
  87     return nodeManager->stringType();
  88   }
  89 };
  90
  91 class StringContainTypeRule {
  92 public:
  93   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  94       throw (TypeCheckingExceptionPrivate, AssertionException) {
  95     if( check ){
  96         TypeNode t = n[0].getType(check);
  97         if (!t.isString()) {
  98           throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
  99         }
 100                 t = n[1].getType(check);
 101         if (!t.isString()) {
 102           throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
 103         }
 104     }
 105     return nodeManager->booleanType();
 106   }
 107 };
 108
 109 class StringCharAtTypeRule {
 110 public:
 111   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 112       throw (TypeCheckingExceptionPrivate, AssertionException) {
 113     if( check ){
 114         TypeNode t = n[0].getType(check);
 115         if (!t.isString()) {
 116           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at");
 117         }
 118                 t = n[1].getType(check);
 119         if (!t.isInteger()) {
 120           throw TypeCheckingExceptionPrivate(n, "expecting an integer string term in string char at");
 121         }
 122     }
 123     return nodeManager->stringType();
 124   }
 125 };
 126
 127 class RegExpConstantTypeRule {
 128 public:
 129   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 130       throw (TypeCheckingExceptionPrivate, AssertionException) {
 131     return nodeManager->regexpType();
 132   }
 133 };
 134
 135 class RegExpConcatTypeRule {
 136 public:
 137   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 138       throw (TypeCheckingExceptionPrivate, AssertionException) {
 139     TNode::iterator it = n.begin();
 140     TNode::iterator it_end = n.end();
 141         int size = 0;
 142     for (; it != it_end; ++ it) {
 143        TypeNode t = (*it).getType(check);
 144        if (!t.isRegExp()) {
 145          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
 146        }
 147            ++size;
 148     }
 149         if(size < 2) {
 150        throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
 151         }
 152     return nodeManager->regexpType();
 153   }
 154 };
 155
 156 class RegExpOrTypeRule {
 157 public:
 158   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 159       throw (TypeCheckingExceptionPrivate, AssertionException) {
 160     TNode::iterator it = n.begin();
 161     TNode::iterator it_end = n.end();
 162     for (; it != it_end; ++ it) {
 163        TypeNode t = (*it).getType(check);
 164        if (!t.isRegExp()) {
 165          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 166        }
 167     }
 168     return nodeManager->regexpType();
 169   }
 170 };
 171
 172 class RegExpInterTypeRule {
 173 public:
 174   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 175       throw (TypeCheckingExceptionPrivate, AssertionException) {
 176     TNode::iterator it = n.begin();
 177     TNode::iterator it_end = n.end();
 178     for (; it != it_end; ++ it) {
 179        TypeNode t = (*it).getType(check);
 180        if (!t.isRegExp()) {
 181          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 182        }
 183     }
 184     return nodeManager->regexpType();
 185   }
 186 };
 187
 188 class RegExpStarTypeRule {
 189 public:
 190   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 191       throw (TypeCheckingExceptionPrivate, AssertionException) {
 192     TNode::iterator it = n.begin();
 193     TNode::iterator it_end = n.end();
 194     TypeNode t = (*it).getType(check);
 195     if (!t.isRegExp()) {
 196       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 197     }
 198     if(++it != it_end) {
 199       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 200     }
 201
 202     return nodeManager->regexpType();
 203   }
 204 };
 205
 206 class RegExpPlusTypeRule {
 207 public:
 208   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 209       throw (TypeCheckingExceptionPrivate, AssertionException) {
 210     TNode::iterator it = n.begin();
 211     TNode::iterator it_end = n.end();
 212     TypeNode t = (*it).getType(check);
 213     if (!t.isRegExp()) {
 214       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 215     }
 216     if(++it != it_end) {
 217       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 218     }
 219
 220     return nodeManager->regexpType();
 221   }
 222 };
 223
 224 class RegExpOptTypeRule {
 225 public:
 226   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 227       throw (TypeCheckingExceptionPrivate, AssertionException) {
 228     TNode::iterator it = n.begin();
 229     TNode::iterator it_end = n.end();
 230     TypeNode t = (*it).getType(check);
 231     if (!t.isRegExp()) {
 232       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 233     }
 234     if(++it != it_end) {
 235       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 236     }
 237
 238     return nodeManager->regexpType();
 239   }
 240 };
 241
 242 class RegExpRangeTypeRule {
 243 public:
 244   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 245       throw (TypeCheckingExceptionPrivate, AssertionException) {
 246     TNode::iterator it = n.begin();
 247     TNode::iterator it_end = n.end();
 248         char ch[2];
 249
 250         for(int i=0; i<2; ++i) {
 251                 TypeNode t = (*it).getType(check);
 252                 if (!t.isString()) {
 253                   throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
 254                 }
 255                 if( (*it).getKind() != kind::CONST_STRING ) {
 256                   throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
 257                 }
 258                 if( (*it).getConst<String>().size() != 1 ) {
 259                   throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
 260                 }
 261                 ch[i] = (*it).getConst<String>().getFirstChar();
 262                 ++it;
 263         }
 264         if(ch[0] > ch[1]) {
 265                 throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
 266         }
 267
 268     if( it != it_end ) {
 269       throw TypeCheckingExceptionPrivate(n, "too many terms in regexp range");
 270     }
 271
 272     return nodeManager->regexpType();
 273   }
 274 };
 275
 276 class StringToRegExpTypeRule {
 277 public:
 278   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 279       throw (TypeCheckingExceptionPrivate, AssertionException) {
 280     TNode::iterator it = n.begin();
 281     TNode::iterator it_end = n.end();
 282     TypeNode t = (*it).getType(check);
 283     if (!t.isString()) {
 284       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 285     }
 286     //if( (*it).getKind() != kind::CONST_STRING ) {
 287     //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
 288     //}
 289     if(++it != it_end) {
 290       throw TypeCheckingExceptionPrivate(n, "too many terms");
 291     }
 292
 293     return nodeManager->regexpType();
 294   }
 295 };
 296
 297 class StringInRegExpTypeRule {
 298 public:
 299   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 300       throw (TypeCheckingExceptionPrivate, AssertionException) {
 301     TNode::iterator it = n.begin();
 302     TNode::iterator it_end = n.end();
 303     TypeNode t = (*it).getType(check);
 304     if (!t.isString()) {
 305       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 306     }
 307     ++it;
 308     t = (*it).getType(check);
 309     if (!t.isRegExp()) {
 310       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 311     }
 312     if(++it != it_end) {
 313       throw TypeCheckingExceptionPrivate(n, "too many terms");
 314     }
 315
 316     return nodeManager->booleanType();
 317   }
 318 };
 319
 320
 321 }/* CVC4::theory::strings namespace */
 322 }/* CVC4::theory namespace */
 323 }/* CVC4 namespace */
 324
 325 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */