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 prototype.
   8  ** Copyright (c) 2013-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     for (; it != it_end; ++ it) {
  41        TypeNode t = (*it).getType(check);
  42        if (!t.isString()) {
  43          throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
  44        }
  45     }
  46     return nodeManager->stringType();
  47   }
  48 };
  49
  50 class StringLengthTypeRule {
  51 public:
  52   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  53       throw (TypeCheckingExceptionPrivate, AssertionException) {
  54     if( check ){
  55         TypeNode t = n[0].getType(check);
  56         if (!t.isString()) {
  57           throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
  58         }
  59     }
  60     return nodeManager->integerType();
  61   }
  62 };
  63
  64 class StringSubstrTypeRule {
  65 public:
  66   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  67       throw (TypeCheckingExceptionPrivate, AssertionException) {
  68     if( check ){
  69         TypeNode t = n[0].getType(check);
  70         if (!t.isString()) {
  71           throw TypeCheckingExceptionPrivate(n, "expecting string terms in substr");
  72         }
  73                 t = n[1].getType(check);
  74         if (!t.isInteger()) {
  75           throw TypeCheckingExceptionPrivate(n, "expecting start int terms in substr");
  76         }
  77                 t = n[2].getType(check);
  78         if (!t.isInteger()) {
  79           throw TypeCheckingExceptionPrivate(n, "expecting length int terms in substr");
  80         }
  81     }
  82     return nodeManager->stringType();
  83   }
  84 };
  85
  86 class RegExpConstantTypeRule {
  87 public:
  88   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  89       throw (TypeCheckingExceptionPrivate, AssertionException) {
  90     return nodeManager->regexpType();
  91   }
  92 };
  93
  94 class RegExpConcatTypeRule {
  95 public:
  96   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  97       throw (TypeCheckingExceptionPrivate, AssertionException) {
  98     TNode::iterator it = n.begin();
  99     TNode::iterator it_end = n.end();
 100     for (; it != it_end; ++ it) {
 101        TypeNode t = (*it).getType(check);
 102        if (!t.isRegExp()) {
 103          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 104        }
 105     }
 106     return nodeManager->regexpType();
 107   }
 108 };
 109
 110 class RegExpOrTypeRule {
 111 public:
 112   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 113       throw (TypeCheckingExceptionPrivate, AssertionException) {
 114     TNode::iterator it = n.begin();
 115     TNode::iterator it_end = n.end();
 116     for (; it != it_end; ++ it) {
 117        TypeNode t = (*it).getType(check);
 118        if (!t.isRegExp()) {
 119          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 120        }
 121     }
 122     return nodeManager->regexpType();
 123   }
 124 };
 125
 126 class RegExpInterTypeRule {
 127 public:
 128   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 129       throw (TypeCheckingExceptionPrivate, AssertionException) {
 130     TNode::iterator it = n.begin();
 131     TNode::iterator it_end = n.end();
 132     for (; it != it_end; ++ it) {
 133        TypeNode t = (*it).getType(check);
 134        if (!t.isRegExp()) {
 135          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 136        }
 137     }
 138     return nodeManager->regexpType();
 139   }
 140 };
 141
 142 class RegExpStarTypeRule {
 143 public:
 144   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 145       throw (TypeCheckingExceptionPrivate, AssertionException) {
 146     TNode::iterator it = n.begin();
 147     TNode::iterator it_end = n.end();
 148     TypeNode t = (*it).getType(check);
 149     if (!t.isRegExp()) {
 150       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 151     }
 152     if(++it != it_end) {
 153       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 154     }
 155
 156     return nodeManager->regexpType();
 157   }
 158 };
 159
 160 class RegExpPlusTypeRule {
 161 public:
 162   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 163       throw (TypeCheckingExceptionPrivate, AssertionException) {
 164     TNode::iterator it = n.begin();
 165     TNode::iterator it_end = n.end();
 166     TypeNode t = (*it).getType(check);
 167     if (!t.isRegExp()) {
 168       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 169     }
 170     if(++it != it_end) {
 171       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 172     }
 173
 174     return nodeManager->regexpType();
 175   }
 176 };
 177
 178 class RegExpOptTypeRule {
 179 public:
 180   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 181       throw (TypeCheckingExceptionPrivate, AssertionException) {
 182     TNode::iterator it = n.begin();
 183     TNode::iterator it_end = n.end();
 184     TypeNode t = (*it).getType(check);
 185     if (!t.isRegExp()) {
 186       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 187     }
 188     if(++it != it_end) {
 189       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 190     }
 191
 192     return nodeManager->regexpType();
 193   }
 194 };
 195
 196 class StringToRegExpTypeRule {
 197 public:
 198   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 199       throw (TypeCheckingExceptionPrivate, AssertionException) {
 200     TNode::iterator it = n.begin();
 201     TNode::iterator it_end = n.end();
 202     TypeNode t = (*it).getType(check);
 203     if (!t.isString()) {
 204       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 205     }
 206     if( (*it).getKind() != kind::CONST_STRING ) {
 207       throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
 208     }
 209     if(++it != it_end) {
 210       throw TypeCheckingExceptionPrivate(n, "too many terms");
 211     }
 212
 213     return nodeManager->regexpType();
 214   }
 215 };
 216
 217 class StringInRegExpTypeRule {
 218 public:
 219   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 220       throw (TypeCheckingExceptionPrivate, AssertionException) {
 221     TNode::iterator it = n.begin();
 222     TNode::iterator it_end = n.end();
 223     TypeNode t = (*it).getType(check);
 224     if (!t.isString()) {
 225       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 226     }
 227     ++it;
 228     t = (*it).getType(check);
 229     if (!t.isRegExp()) {
 230       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 231     }
 232     if(++it != it_end) {
 233       throw TypeCheckingExceptionPrivate(n, "too many terms");
 234     }
 235
 236     return nodeManager->booleanType();
 237   }
 238 };
 239
 240
 241 }/* CVC4::theory::strings namespace */
 242 }/* CVC4::theory namespace */
 243 }/* CVC4 namespace */
 244
 245 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */