src/expr/type_node.cpp

   1 /*********************                                                        */
   2 /*! \file type_node.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): taking, ajreynol
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Reference-counted encapsulation of a pointer to node information.
  15  **
  16  ** Reference-counted encapsulation of a pointer to node information.
  17  **/
  18
  19 #include <vector>
  20
  21 #include "expr/type_node.h"
  22 #include "expr/type_properties.h"
  23
  24 using namespace std;
  25
  26 namespace CVC4 {
  27
  28 TypeNode TypeNode::s_null( &expr::NodeValue::s_null );
  29
  30 TypeNode TypeNode::substitute(const TypeNode& type,
  31                               const TypeNode& replacement,
  32                               std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
  33   // in cache?
  34   std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
  35   if(i != cache.end()) {
  36     return (*i).second;
  37   }
  38
  39   // otherwise compute
  40   NodeBuilder<> nb(getKind());
  41   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
  42     // push the operator
  43     nb << TypeNode(d_nv->d_children[0]);
  44   }
  45   for(TypeNode::const_iterator i = begin(),
  46         iend = end();
  47       i != iend;
  48       ++i) {
  49     if(*i == type) {
  50       nb << replacement;
  51     } else {
  52       (*i).substitute(type, replacement);
  53     }
  54   }
  55
  56   // put in cache
  57   TypeNode tn = nb.constructTypeNode();
  58   cache[*this] = tn;
  59   return tn;
  60 }
  61
  62 Cardinality TypeNode::getCardinality() const {
  63   return kind::getCardinality(*this);
  64 }
  65
  66 bool TypeNode::isWellFounded() const {
  67   return kind::isWellFounded(*this);
  68 }
  69
  70 Node TypeNode::mkGroundTerm() const {
  71   return kind::mkGroundTerm(*this);
  72 }
  73
  74 bool TypeNode::isBoolean() const {
  75   return getKind() == kind::TYPE_CONSTANT &&
  76     ( getConst<TypeConstant>() == BOOLEAN_TYPE ||
  77       getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
  78 }
  79
  80 bool TypeNode::isInteger() const {
  81   return getKind() == kind::TYPE_CONSTANT &&
  82     ( getConst<TypeConstant>() == INTEGER_TYPE ||
  83       getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
  84 }
  85
  86 bool TypeNode::isReal() const {
  87   return getKind() == kind::TYPE_CONSTANT &&
  88     ( getConst<TypeConstant>() == REAL_TYPE ||
  89       getConst<TypeConstant>() == INTEGER_TYPE ||
  90       getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
  91 }
  92
  93 bool TypeNode::isPseudoboolean() const {
  94   return getKind() == kind::TYPE_CONSTANT &&
  95     getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE;
  96 }
  97
  98 bool TypeNode::isString() const {
  99   return getKind() == kind::TYPE_CONSTANT &&
 100     getConst<TypeConstant>() == STRING_TYPE;
 101 }
 102
 103 bool TypeNode::isArray() const {
 104   return getKind() == kind::ARRAY_TYPE;
 105 }
 106
 107 TypeNode TypeNode::getArrayIndexType() const {
 108   Assert(isArray());
 109   return (*this)[0];
 110 }
 111
 112 TypeNode TypeNode::getArrayConstituentType() const {
 113   Assert(isArray());
 114   return (*this)[1];
 115 }
 116
 117 TypeNode TypeNode::getConstructorRangeType() const {
 118   Assert(isConstructor());
 119   return (*this)[getNumChildren()-1];
 120 }
 121
 122 bool TypeNode::isFunction() const {
 123   return getKind() == kind::FUNCTION_TYPE;
 124 }
 125
 126 bool TypeNode::isFunctionLike() const {
 127   return
 128     getKind() == kind::FUNCTION_TYPE ||
 129     getKind() == kind::CONSTRUCTOR_TYPE ||
 130     getKind() == kind::SELECTOR_TYPE ||
 131     getKind() == kind::TESTER_TYPE;
 132 }
 133
 134 bool TypeNode::isPredicate() const {
 135   return isFunction() && getRangeType().isBoolean();
 136 }
 137
 138 std::vector<TypeNode> TypeNode::getArgTypes() const {
 139   vector<TypeNode> args;
 140   if(isTester()) {
 141     Assert(getNumChildren() == 1);
 142     args.push_back((*this)[0]);
 143   } else {
 144     Assert(isFunction() || isConstructor() || isSelector());
 145     for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
 146       args.push_back((*this)[i]);
 147     }
 148   }
 149   return args;
 150 }
 151
 152 std::vector<TypeNode> TypeNode::getParamTypes() const {
 153   vector<TypeNode> params;
 154   Assert(isParametricDatatype());
 155   for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
 156     params.push_back((*this)[i]);
 157   }
 158   return params;
 159 }
 160
 161 TypeNode TypeNode::getRangeType() const {
 162   if(isTester()) {
 163     return NodeManager::currentNM()->booleanType();
 164   }
 165   Assert(isFunction() || isConstructor() || isSelector());
 166   return (*this)[getNumChildren()-1];
 167 }
 168
 169 /** Is this a tuple type? */
 170 bool TypeNode::isTuple() const {
 171   return getKind() == kind::TUPLE_TYPE;
 172 }
 173
 174 /** Is this a tuple type? */
 175 vector<TypeNode> TypeNode::getTupleTypes() const {
 176   Assert(isTuple());
 177   vector<TypeNode> types;
 178   for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
 179     types.push_back((*this)[i]);
 180   }
 181   return types;
 182 }
 183
 184 /** Is this a sort kind */
 185 bool TypeNode::isSort() const {
 186   return getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr());
 187 }
 188
 189 /** Is this a sort constructor kind */
 190 bool TypeNode::isSortConstructor() const {
 191   return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
 192 }
 193
 194 /** Is this a kind type (i.e., the type of a type)? */
 195 bool TypeNode::isKind() const {
 196   return getKind() == kind::TYPE_CONSTANT &&
 197     getConst<TypeConstant>() == KIND_TYPE;
 198 }
 199
 200 /** Is this a bit-vector type */
 201 bool TypeNode::isBitVector() const {
 202   return getKind() == kind::BITVECTOR_TYPE;
 203 }
 204
 205 /** Is this a datatype type */
 206 bool TypeNode::isDatatype() const {
 207   return getKind() == kind::DATATYPE_TYPE;
 208 }
 209
 210 /** Is this a parametric datatype type */
 211 bool TypeNode::isParametricDatatype() const {
 212   return getKind() == kind::PARAMETRIC_DATATYPE;
 213 }
 214
 215 /** Is this an instantiated datatype type */
 216 bool TypeNode::isInstantiatedDatatype() const {
 217   if(getKind() == kind::DATATYPE_TYPE) {
 218     return true;
 219   }
 220   if(getKind() != kind::PARAMETRIC_DATATYPE) {
 221     return false;
 222   }
 223   const Datatype& dt = (*this)[0].getConst<Datatype>();
 224   unsigned n = dt.getNumParameters();
 225   Assert(n < getNumChildren());
 226   for(unsigned i = 0; i < n; ++i) {
 227     if(TypeNode::fromType(dt.getParameter(i)) == (*this)[i + 1]) {
 228       return false;
 229     }
 230   }
 231   return true;
 232 }
 233
 234 /** Is this an instantiated datatype parameter */
 235 bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
 236   AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
 237   const Datatype& dt = (*this)[0].getConst<Datatype>();
 238   AssertArgument(n < dt.getNumParameters(), *this);
 239   return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
 240 }
 241
 242 /** Is this a constructor type */
 243 bool TypeNode::isConstructor() const {
 244   return getKind() == kind::CONSTRUCTOR_TYPE;
 245 }
 246
 247 /** Is this a selector type */
 248 bool TypeNode::isSelector() const {
 249   return getKind() == kind::SELECTOR_TYPE;
 250 }
 251
 252 /** Is this a tester type */
 253 bool TypeNode::isTester() const {
 254   return getKind() == kind::TESTER_TYPE;
 255 }
 256
 257 /** Is this a bit-vector type of size <code>size</code> */
 258 bool TypeNode::isBitVector(unsigned size) const {
 259   return getKind() == kind::BITVECTOR_TYPE &&
 260     getConst<BitVectorSize>() == size;
 261 }
 262
 263 /** Get the size of this bit-vector type */
 264 unsigned TypeNode::getBitVectorSize() const {
 265   Assert(isBitVector());
 266   return getConst<BitVectorSize>();
 267 }
 268
 269 }/* CVC4 namespace */