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 RegExpConstantTypeRule {
  65 public:
  66   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  67       throw (TypeCheckingExceptionPrivate, AssertionException) {
  68     return nodeManager->regexpType();
  69   }
  70 };
  71
  72 class RegExpConcatTypeRule {
  73 public:
  74   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  75       throw (TypeCheckingExceptionPrivate, AssertionException) {
  76     TNode::iterator it = n.begin();
  77     TNode::iterator it_end = n.end();
  78     for (; it != it_end; ++ it) {
  79        TypeNode t = (*it).getType(check);
  80        if (!t.isRegExp()) {
  81          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
  82        }
  83     }
  84     return nodeManager->regexpType();
  85   }
  86 };
  87
  88 class RegExpOrTypeRule {
  89 public:
  90   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  91       throw (TypeCheckingExceptionPrivate, AssertionException) {
  92     TNode::iterator it = n.begin();
  93     TNode::iterator it_end = n.end();
  94     for (; it != it_end; ++ it) {
  95        TypeNode t = (*it).getType(check);
  96        if (!t.isRegExp()) {
  97          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
  98        }
  99     }
 100     return nodeManager->regexpType();
 101   }
 102 };
 103
 104 class RegExpInterTypeRule {
 105 public:
 106   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 107       throw (TypeCheckingExceptionPrivate, AssertionException) {
 108     TNode::iterator it = n.begin();
 109     TNode::iterator it_end = n.end();
 110     for (; it != it_end; ++ it) {
 111        TypeNode t = (*it).getType(check);
 112        if (!t.isRegExp()) {
 113          throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 114        }
 115     }
 116     return nodeManager->regexpType();
 117   }
 118 };
 119
 120 class RegExpStarTypeRule {
 121 public:
 122   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 123       throw (TypeCheckingExceptionPrivate, AssertionException) {
 124     TNode::iterator it = n.begin();
 125     TNode::iterator it_end = n.end();
 126     TypeNode t = (*it).getType(check);
 127     if (!t.isRegExp()) {
 128       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 129     }
 130     if(++it != it_end) {
 131       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 132     }
 133
 134     return nodeManager->regexpType();
 135   }
 136 };
 137
 138 class RegExpPlusTypeRule {
 139 public:
 140   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 141       throw (TypeCheckingExceptionPrivate, AssertionException) {
 142     TNode::iterator it = n.begin();
 143     TNode::iterator it_end = n.end();
 144     TypeNode t = (*it).getType(check);
 145     if (!t.isRegExp()) {
 146       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 147     }
 148     if(++it != it_end) {
 149       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 150     }
 151
 152     return nodeManager->regexpType();
 153   }
 154 };
 155
 156 class RegExpOptTypeRule {
 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     TypeNode t = (*it).getType(check);
 163     if (!t.isRegExp()) {
 164       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 165     }
 166     if(++it != it_end) {
 167       throw TypeCheckingExceptionPrivate(n, "too many regexp");
 168     }
 169
 170     return nodeManager->regexpType();
 171   }
 172 };
 173
 174 class StringToRegExpTypeRule {
 175 public:
 176   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 177       throw (TypeCheckingExceptionPrivate, AssertionException) {
 178     TNode::iterator it = n.begin();
 179     TNode::iterator it_end = n.end();
 180     TypeNode t = (*it).getType(check);
 181     if (!t.isString()) {
 182       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 183     }
 184         if( (*it).getKind() != kind::CONST_STRING ) {
 185       throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
 186         }
 187     if(++it != it_end) {
 188       throw TypeCheckingExceptionPrivate(n, "too many terms");
 189     }
 190
 191     return nodeManager->regexpType();
 192   }
 193 };
 194
 195 class StringInRegExpTypeRule {
 196 public:
 197   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 198       throw (TypeCheckingExceptionPrivate, AssertionException) {
 199     TNode::iterator it = n.begin();
 200     TNode::iterator it_end = n.end();
 201     TypeNode t = (*it).getType(check);
 202     if (!t.isString()) {
 203       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
 204     }
 205     ++it;
 206     t = (*it).getType(check);
 207     if (!t.isRegExp()) {
 208       throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
 209     }
 210     if(++it != it_end) {
 211       throw TypeCheckingExceptionPrivate(n, "too many terms");
 212     }
 213
 214     return nodeManager->booleanType();
 215   }
 216 };
 217
 218
 219 }/* CVC4::theory::strings namespace */
 220 }/* CVC4::theory namespace */
 221 }/* CVC4 namespace */
 222
 223 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */