src/expr/type.cpp

   1 /*********************                                                        */
   2 /*! \file type.cpp
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: dejan, mdeters
   6  ** Minor contributors (to current version): 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 Implementation of expression types
  15  **
  16  ** Implementation of expression types.
  17  **/
  18
  19 #include <iostream>
  20 #include <string>
  21 #include <vector>
  22
  23 #include "expr/node_manager.h"
  24 #include "expr/type.h"
  25 #include "expr/type_node.h"
  26 #include "util/Assert.h"
  27
  28 using namespace std;
  29
  30 namespace CVC4 {
  31
  32 ostream& operator<<(ostream& out, const Type& t) {
  33   NodeManagerScope nms(t.d_nodeManager);
  34   return out << *Type::getTypeNode(t);
  35 }
  36
  37 Type Type::makeType(const TypeNode& typeNode) const {
  38   return Type(d_nodeManager, new TypeNode(typeNode));
  39 }
  40
  41 Type::Type(NodeManager* nm, TypeNode* node) :
  42   d_typeNode(node),
  43   d_nodeManager(nm) {
  44 }
  45
  46 Type::~Type() {
  47   NodeManagerScope nms(d_nodeManager);
  48   delete d_typeNode;
  49 }
  50
  51 Type::Type() :
  52   d_typeNode(new TypeNode),
  53   d_nodeManager(NULL) {
  54 }
  55
  56 Type::Type(const Type& t) :
  57   d_typeNode(new TypeNode(*t.d_typeNode)),
  58   d_nodeManager(t.d_nodeManager) {
  59 }
  60
  61 bool Type::isNull() const {
  62   return d_typeNode->isNull();
  63 }
  64
  65 Cardinality Type::getCardinality() const {
  66   NodeManagerScope nms(d_nodeManager);
  67   return d_typeNode->getCardinality();
  68 }
  69
  70 bool Type::isWellFounded() const {
  71   NodeManagerScope nms(d_nodeManager);
  72   return d_typeNode->isWellFounded();
  73 }
  74
  75 Expr Type::mkGroundTerm() const {
  76   NodeManagerScope nms(d_nodeManager);
  77   return d_typeNode->mkGroundTerm().toExpr();
  78 }
  79
  80 Type& Type::operator=(const Type& t) {
  81   Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
  82   Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");
  83
  84   if(this != &t) {
  85     if(d_nodeManager == t.d_nodeManager) {
  86       NodeManagerScope nms(d_nodeManager);
  87       *d_typeNode = *t.d_typeNode;
  88     } else {
  89       // This happens more than you think---every time you set to or
  90       // from the null Type.  It's tricky because each node manager
  91       // must be in play at the right time.
  92
  93       NodeManagerScope nms1(d_nodeManager);
  94       *d_typeNode = TypeNode::null();
  95
  96       NodeManagerScope nms2(t.d_nodeManager);
  97       *d_typeNode = *t.d_typeNode;
  98
  99       d_nodeManager = t.d_nodeManager;
 100     }
 101   }
 102   return *this;
 103 }
 104
 105 bool Type::operator==(const Type& t) const {
 106   return *d_typeNode == *t.d_typeNode;
 107 }
 108
 109 bool Type::operator!=(const Type& t) const {
 110   return *d_typeNode != *t.d_typeNode;
 111 }
 112
 113 bool Type::operator<(const Type& t) const {
 114   return *d_typeNode < *t.d_typeNode;
 115 }
 116
 117 bool Type::operator<=(const Type& t) const {
 118   return *d_typeNode <= *t.d_typeNode;
 119 }
 120
 121 bool Type::operator>(const Type& t) const {
 122   return *d_typeNode > *t.d_typeNode;
 123 }
 124
 125 bool Type::operator>=(const Type& t) const {
 126   return *d_typeNode >= *t.d_typeNode;
 127 }
 128
 129 Type Type::substitute(const Type& type, const Type& replacement) const {
 130   NodeManagerScope nms(d_nodeManager);
 131   return makeType(d_typeNode->substitute(*type.d_typeNode,
 132                                          *replacement.d_typeNode));
 133 }
 134
 135 Type Type::substitute(const std::vector<Type>& types,
 136                       const std::vector<Type>& replacements) const {
 137   NodeManagerScope nms(d_nodeManager);
 138
 139   vector<TypeNode> typesNodes, replacementsNodes;
 140
 141   for(vector<Type>::const_iterator i = types.begin(),
 142         iend = types.end();
 143       i != iend;
 144       ++i) {
 145     typesNodes.push_back(*(*i).d_typeNode);
 146   }
 147
 148   for(vector<Type>::const_iterator i = replacements.begin(),
 149         iend = replacements.end();
 150       i != iend;
 151       ++i) {
 152     replacementsNodes.push_back(*(*i).d_typeNode);
 153   }
 154
 155   return makeType(d_typeNode->substitute(typesNodes.begin(),
 156                                          typesNodes.end(),
 157                                          replacementsNodes.begin(),
 158                                          replacementsNodes.end()));
 159 }
 160
 161 ExprManager* Type::getExprManager() const {
 162   return d_nodeManager->toExprManager();
 163 }
 164
 165 void Type::toStream(std::ostream& out) const {
 166   NodeManagerScope nms(d_nodeManager);
 167   out << *d_typeNode;
 168   return;
 169 }
 170
 171 string Type::toString() const {
 172   NodeManagerScope nms(d_nodeManager);
 173   stringstream ss;
 174   ss << *d_typeNode;
 175   return ss.str();
 176 }
 177
 178 /** Is this the Boolean type? */
 179 bool Type::isBoolean() const {
 180   NodeManagerScope nms(d_nodeManager);
 181   return d_typeNode->isBoolean();
 182 }
 183
 184 /** Cast to a Boolean type */
 185 Type::operator BooleanType() const throw(AssertionException) {
 186   NodeManagerScope nms(d_nodeManager);
 187   Assert(isNull() || isBoolean());
 188   return BooleanType(*this);
 189 }
 190
 191 /** Is this the integer type? */
 192 bool Type::isInteger() const {
 193   NodeManagerScope nms(d_nodeManager);
 194   return d_typeNode->isInteger();
 195 }
 196
 197 /** Cast to a integer type */
 198 Type::operator IntegerType() const throw(AssertionException) {
 199   NodeManagerScope nms(d_nodeManager);
 200   Assert(isNull() || isInteger());
 201   return IntegerType(*this);
 202 }
 203
 204 /** Is this the real type? */
 205 bool Type::isReal() const {
 206   NodeManagerScope nms(d_nodeManager);
 207   return d_typeNode->isReal();
 208 }
 209
 210 /** Cast to a real type */
 211 Type::operator RealType() const throw(AssertionException) {
 212   NodeManagerScope nms(d_nodeManager);
 213   Assert(isNull() || isReal());
 214   return RealType(*this);
 215 }
 216
 217 /** Is this the pseudoboolean type? */
 218 bool Type::isPseudoboolean() const {
 219   NodeManagerScope nms(d_nodeManager);
 220   return d_typeNode->isPseudoboolean();
 221 }
 222
 223 /** Cast to a pseudoboolean type */
 224 Type::operator PseudobooleanType() const throw(AssertionException) {
 225   NodeManagerScope nms(d_nodeManager);
 226   Assert(isNull() || isPseudoboolean());
 227   return PseudobooleanType(*this);
 228 }
 229
 230 /** Is this the string type? */
 231 bool Type::isString() const {
 232   NodeManagerScope nms(d_nodeManager);
 233   return d_typeNode->isString();
 234 }
 235
 236 /** Cast to a string type */
 237 Type::operator StringType() const throw(AssertionException) {
 238   NodeManagerScope nms(d_nodeManager);
 239   Assert(isNull() || isString());
 240   return StringType(*this);
 241 }
 242
 243 /** Is this the bit-vector type? */
 244 bool Type::isBitVector() const {
 245   NodeManagerScope nms(d_nodeManager);
 246   return d_typeNode->isBitVector();
 247 }
 248
 249 /** Cast to a bit-vector type */
 250 Type::operator BitVectorType() const throw(AssertionException) {
 251   NodeManagerScope nms(d_nodeManager);
 252   Assert(isNull() || isBitVector());
 253   return BitVectorType(*this);
 254 }
 255
 256 /** Cast to a Constructor type */
 257 Type::operator DatatypeType() const throw(AssertionException) {
 258   NodeManagerScope nms(d_nodeManager);
 259   Assert(isNull() || isDatatype());
 260   return DatatypeType(*this);
 261 }
 262
 263 /** Is this a datatype type? */
 264 bool Type::isDatatype() const {
 265   NodeManagerScope nms(d_nodeManager);
 266   return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
 267 }
 268
 269 /** Cast to a Constructor type */
 270 Type::operator ConstructorType() const throw(AssertionException) {
 271   NodeManagerScope nms(d_nodeManager);
 272   Assert(isNull() || isConstructor());
 273   return ConstructorType(*this);
 274 }
 275
 276 /** Is this the Constructor type? */
 277 bool Type::isConstructor() const {
 278   NodeManagerScope nms(d_nodeManager);
 279   return d_typeNode->isConstructor();
 280 }
 281
 282 /** Cast to a Selector type */
 283 Type::operator SelectorType() const throw(AssertionException) {
 284   NodeManagerScope nms(d_nodeManager);
 285   Assert(isNull() || isSelector());
 286   return SelectorType(*this);
 287 }
 288
 289 /** Is this the Selector type? */
 290 bool Type::isSelector() const {
 291   NodeManagerScope nms(d_nodeManager);
 292   return d_typeNode->isSelector();
 293 }
 294
 295 /** Cast to a Tester type */
 296 Type::operator TesterType() const throw(AssertionException) {
 297   NodeManagerScope nms(d_nodeManager);
 298   Assert(isNull() || isTester());
 299   return TesterType(*this);
 300 }
 301
 302 /** Is this the Tester type? */
 303 bool Type::isTester() const {
 304   NodeManagerScope nms(d_nodeManager);
 305   return d_typeNode->isTester();
 306 }
 307
 308 /** Is this a function type? */
 309 bool Type::isFunction() const {
 310   NodeManagerScope nms(d_nodeManager);
 311   return d_typeNode->isFunction();
 312 }
 313
 314 /**
 315  * Is this a predicate type? NOTE: all predicate types are also
 316  * function types.
 317  */
 318 bool Type::isPredicate() const {
 319   NodeManagerScope nms(d_nodeManager);
 320   return d_typeNode->isPredicate();
 321 }
 322
 323 /** Cast to a function type */
 324 Type::operator FunctionType() const throw(AssertionException) {
 325   NodeManagerScope nms(d_nodeManager);
 326   Assert(isNull() || isFunction());
 327   return FunctionType(*this);
 328 }
 329
 330 /** Is this a tuple type? */
 331 bool Type::isTuple() const {
 332   NodeManagerScope nms(d_nodeManager);
 333   return d_typeNode->isTuple();
 334 }
 335
 336 /** Cast to a tuple type */
 337 Type::operator TupleType() const throw(AssertionException) {
 338   NodeManagerScope nms(d_nodeManager);
 339   Assert(isNull() || isTuple());
 340   return TupleType(*this);
 341 }
 342
 343 /** Is this an array type? */
 344 bool Type::isArray() const {
 345   NodeManagerScope nms(d_nodeManager);
 346   return d_typeNode->isArray();
 347 }
 348
 349 /** Cast to an array type */
 350 Type::operator ArrayType() const throw(AssertionException) {
 351   NodeManagerScope nms(d_nodeManager);
 352   return ArrayType(*this);
 353 }
 354
 355 /** Is this a sort kind */
 356 bool Type::isSort() const {
 357   NodeManagerScope nms(d_nodeManager);
 358   return d_typeNode->isSort();
 359 }
 360
 361 /** Cast to a sort type */
 362 Type::operator SortType() const throw(AssertionException) {
 363   NodeManagerScope nms(d_nodeManager);
 364   Assert(isNull() || isSort());
 365   return SortType(*this);
 366 }
 367
 368 /** Is this a sort constructor kind */
 369 bool Type::isSortConstructor() const {
 370   NodeManagerScope nms(d_nodeManager);
 371   return d_typeNode->isSortConstructor();
 372 }
 373
 374 /** Cast to a sort type */
 375 Type::operator SortConstructorType() const throw(AssertionException) {
 376   NodeManagerScope nms(d_nodeManager);
 377   Assert(isNull() || isSortConstructor());
 378   return SortConstructorType(*this);
 379 }
 380
 381 /** Is this a kind type (i.e., the type of a type)? */
 382 bool Type::isKind() const {
 383   NodeManagerScope nms(d_nodeManager);
 384   return d_typeNode->isKind();
 385 }
 386
 387 /** Cast to a kind type */
 388 Type::operator KindType() const throw(AssertionException) {
 389   NodeManagerScope nms(d_nodeManager);
 390   Assert(isNull() || isKind());
 391   return KindType(*this);
 392 }
 393
 394 vector<Type> FunctionType::getArgTypes() const {
 395   NodeManagerScope nms(d_nodeManager);
 396   vector<Type> args;
 397   vector<TypeNode> argNodes = d_typeNode->getArgTypes();
 398   vector<TypeNode>::iterator it = argNodes.begin();
 399   vector<TypeNode>::iterator it_end = argNodes.end();
 400   for(; it != it_end; ++ it) {
 401     args.push_back(makeType(*it));
 402   }
 403   return args;
 404 }
 405
 406 Type FunctionType::getRangeType() const {
 407   NodeManagerScope nms(d_nodeManager);
 408   Assert(isNull() || isFunction());
 409   return makeType(d_typeNode->getRangeType());
 410 }
 411
 412 vector<Type> TupleType::getTypes() const {
 413   NodeManagerScope nms(d_nodeManager);
 414   vector<Type> types;
 415   vector<TypeNode> typeNodes = d_typeNode->getTupleTypes();
 416   vector<TypeNode>::iterator it = typeNodes.begin();
 417   vector<TypeNode>::iterator it_end = typeNodes.end();
 418   for(; it != it_end; ++ it) {
 419     types.push_back(makeType(*it));
 420   }
 421   return types;
 422 }
 423
 424 string SortType::getName() const {
 425   NodeManagerScope nms(d_nodeManager);
 426   return d_typeNode->getAttribute(expr::VarNameAttr());
 427 }
 428
 429 bool SortType::isParameterized() const {
 430   return false;
 431 }
 432
 433 /** Get the parameter types */
 434 std::vector<Type> SortType::getParamTypes() const {
 435   vector<Type> params;
 436   return params;
 437 }
 438
 439 string SortConstructorType::getName() const {
 440   NodeManagerScope nms(d_nodeManager);
 441   return d_typeNode->getAttribute(expr::VarNameAttr());
 442 }
 443
 444 size_t SortConstructorType::getArity() const {
 445   NodeManagerScope nms(d_nodeManager);
 446   return d_typeNode->getAttribute(expr::SortArityAttr());
 447 }
 448
 449 SortType SortConstructorType::instantiate(const std::vector<Type>& params) const {
 450   NodeManagerScope nms(d_nodeManager);
 451   vector<TypeNode> paramsNodes;
 452   for(vector<Type>::const_iterator i = params.begin(),
 453         iend = params.end();
 454       i != iend;
 455       ++i) {
 456     paramsNodes.push_back(*getTypeNode(*i));
 457   }
 458   return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes)));
 459 }
 460
 461 BooleanType::BooleanType(const Type& t) throw(AssertionException) :
 462   Type(t) {
 463   Assert(isNull() || isBoolean());
 464 }
 465
 466 IntegerType::IntegerType(const Type& t) throw(AssertionException) :
 467   Type(t) {
 468   Assert(isNull() || isInteger());
 469 }
 470
 471 RealType::RealType(const Type& t) throw(AssertionException) :
 472   Type(t) {
 473   Assert(isNull() || isReal());
 474 }
 475
 476 PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) :
 477   Type(t) {
 478   Assert(isNull() || isPseudoboolean());
 479 }
 480
 481 StringType::StringType(const Type& t) throw(AssertionException) :
 482   Type(t) {
 483   Assert(isNull() || isString());
 484 }
 485
 486 BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
 487   Type(t) {
 488   Assert(isNull() || isBitVector());
 489 }
 490
 491 DatatypeType::DatatypeType(const Type& t) throw(AssertionException) :
 492   Type(t) {
 493   Assert(isNull() || isDatatype());
 494 }
 495
 496 ConstructorType::ConstructorType(const Type& t) throw(AssertionException) :
 497   Type(t) {
 498   Assert(isNull() || isConstructor());
 499 }
 500
 501 SelectorType::SelectorType(const Type& t) throw(AssertionException) :
 502   Type(t) {
 503   Assert(isNull() || isSelector());
 504 }
 505
 506 TesterType::TesterType(const Type& t) throw(AssertionException) :
 507   Type(t) {
 508   Assert(isNull() || isTester());
 509 }
 510
 511 FunctionType::FunctionType(const Type& t) throw(AssertionException) :
 512   Type(t) {
 513   Assert(isNull() || isFunction());
 514 }
 515
 516 TupleType::TupleType(const Type& t) throw(AssertionException) :
 517   Type(t) {
 518   Assert(isNull() || isTuple());
 519 }
 520
 521 ArrayType::ArrayType(const Type& t) throw(AssertionException) :
 522   Type(t) {
 523   Assert(isNull() || isArray());
 524 }
 525
 526 KindType::KindType(const Type& t) throw(AssertionException) :
 527   Type(t) {
 528   Assert(isNull() || isKind());
 529 }
 530
 531 SortType::SortType(const Type& t) throw(AssertionException) :
 532   Type(t) {
 533   Assert(isNull() || isSort());
 534 }
 535
 536 SortConstructorType::SortConstructorType(const Type& t)
 537   throw(AssertionException) :
 538   Type(t) {
 539   Assert(isNull() || isSortConstructor());
 540 }
 541
 542 unsigned BitVectorType::getSize() const {
 543   return d_typeNode->getBitVectorSize();
 544 }
 545
 546 Type ArrayType::getIndexType() const {
 547   return makeType(d_typeNode->getArrayIndexType());
 548 }
 549
 550 Type ArrayType::getConstituentType() const {
 551   return makeType(d_typeNode->getArrayConstituentType());
 552 }
 553
 554 DatatypeType ConstructorType::getRangeType() const {
 555   return DatatypeType(makeType(d_typeNode->getConstructorRangeType()));
 556 }
 557
 558 size_t ConstructorType::getArity() const {
 559   return d_typeNode->getNumChildren() - 1;
 560 }
 561
 562 std::vector<Type> ConstructorType::getArgTypes() const {
 563   NodeManagerScope nms(d_nodeManager);
 564   vector<Type> args;
 565   vector<TypeNode> argNodes = d_typeNode->getArgTypes();
 566   vector<TypeNode>::iterator it = argNodes.begin();
 567   vector<TypeNode>::iterator it_end = argNodes.end();
 568   for(; it != it_end; ++ it) {
 569     args.push_back(makeType(*it));
 570   }
 571   return args;
 572 }
 573
 574 const Datatype& DatatypeType::getDatatype() const {
 575   if( d_typeNode->isParametricDatatype() ) {
 576     Assert( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE );
 577     const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
 578     return dt;
 579   } else {
 580     return d_typeNode->getConst<Datatype>();
 581   }
 582 }
 583
 584 bool DatatypeType::isParametric() const {
 585   return d_typeNode->isParametricDatatype();
 586 }
 587
 588 Expr DatatypeType::getConstructor(std::string name) const {
 589   return getDatatype().getConstructor(name);
 590 }
 591
 592 bool DatatypeType::isInstantiated() const {
 593   return d_typeNode->isInstantiatedDatatype();
 594 }
 595
 596 bool DatatypeType::isParameterInstantiated(unsigned n) const {
 597   return d_typeNode->isParameterInstantiatedDatatype(n);
 598 }
 599
 600 size_t DatatypeType::getArity() const {
 601   NodeManagerScope nms(d_nodeManager);
 602   return d_typeNode->getNumChildren() - 1;
 603 }
 604
 605 std::vector<Type> DatatypeType::getParamTypes() const {
 606   NodeManagerScope nms(d_nodeManager);
 607   vector<Type> params;
 608   vector<TypeNode> paramNodes = d_typeNode->getParamTypes();
 609   vector<TypeNode>::iterator it = paramNodes.begin();
 610   vector<TypeNode>::iterator it_end = paramNodes.end();
 611   for(; it != it_end; ++it) {
 612     params.push_back(makeType(*it));
 613   }
 614   return params;
 615 }
 616
 617 DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
 618   NodeManagerScope nms(d_nodeManager);
 619   TypeNode cons = d_nodeManager->mkTypeConst( getDatatype() );
 620   vector<TypeNode> paramsNodes;
 621   paramsNodes.push_back( cons );
 622   for(vector<Type>::const_iterator i = params.begin(),
 623         iend = params.end();
 624       i != iend;
 625       ++i) {
 626     paramsNodes.push_back(*getTypeNode(*i));
 627   }
 628   return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE,paramsNodes)));
 629 }
 630
 631 DatatypeType SelectorType::getDomain() const {
 632   return DatatypeType(makeType((*d_typeNode)[0]));
 633 }
 634
 635 Type SelectorType::getRangeType() const {
 636   return makeType((*d_typeNode)[1]);
 637 }
 638
 639 DatatypeType TesterType::getDomain() const {
 640   return DatatypeType(makeType((*d_typeNode)[0]));
 641 }
 642
 643 BooleanType TesterType::getRangeType() const {
 644   return BooleanType(makeType(d_nodeManager->booleanType()));
 645 }
 646
 647 size_t TypeHashFunction::operator()(const Type& t) const {
 648   return TypeNodeHashFunction()(NodeManager::fromType(t));
 649 }
 650
 651 }/* CVC4 namespace */