src/expr/datatype.cpp

   1 /*********************                                                        */
   2 /*! \file datatype.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A class representing a Datatype definition
  13  **
  14  ** A class representing a Datatype definition for the theory of
  15  ** inductive datatypes.
  16  **/
  17 #include "expr/datatype.h"
  18
  19 #include <string>
  20 #include <sstream>
  21
  22 #include "base/cvc4_assert.h"
  23 #include "expr/attribute.h"
  24 #include "expr/expr_manager.h"
  25 #include "expr/expr_manager_scope.h"
  26 #include "expr/matcher.h"
  27 #include "expr/node.h"
  28 #include "expr/node_manager.h"
  29 #include "expr/type.h"
  30 #include "options/set_language.h"
  31
  32 using namespace std;
  33
  34 namespace CVC4 {
  35
  36 namespace expr {
  37   namespace attr {
  38     struct DatatypeIndexTag {};
  39     struct DatatypeConsIndexTag {};
  40     struct DatatypeFiniteTag {};
  41     struct DatatypeFiniteComputedTag {};
  42     struct DatatypeUFiniteTag {};
  43     struct DatatypeUFiniteComputedTag {};
  44   }/* CVC4::expr::attr namespace */
  45 }/* CVC4::expr namespace */
  46
  47 typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
  48 typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
  49 typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
  50 typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
  51 typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
  52 typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
  53
  54 Datatype::~Datatype(){
  55   Trace("ajr-temp") << "delete datatype " << getName() << " " << this << std::endl;
  56   delete d_record;
  57 }
  58
  59 const Datatype& Datatype::datatypeOf(Expr item) {
  60   ExprManagerScope ems(item);
  61   TypeNode t = Node::fromExpr(item).getType();
  62   switch(t.getKind()) {
  63   case kind::CONSTRUCTOR_TYPE:
  64     return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype();
  65   case kind::SELECTOR_TYPE:
  66   case kind::TESTER_TYPE:
  67     return DatatypeType(t[0].toType()).getDatatype();
  68   default:
  69     Unhandled("arg must be a datatype constructor, selector, or tester");
  70   }
  71 }
  72
  73 size_t Datatype::indexOf(Expr item) {
  74   ExprManagerScope ems(item);
  75   PrettyCheckArgument(item.getType().isConstructor() ||
  76                 item.getType().isTester() ||
  77                 item.getType().isSelector(),
  78                 item,
  79                 "arg must be a datatype constructor, selector, or tester");
  80   TNode n = Node::fromExpr(item);
  81   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
  82     return indexOf( item[0] );
  83   }else{
  84     Assert(n.hasAttribute(DatatypeIndexAttr()));
  85     return n.getAttribute(DatatypeIndexAttr());
  86   }
  87 }
  88
  89 size_t Datatype::cindexOf(Expr item) {
  90   ExprManagerScope ems(item);
  91   PrettyCheckArgument(item.getType().isSelector(),
  92                 item,
  93                 "arg must be a datatype selector");
  94   TNode n = Node::fromExpr(item);
  95   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
  96     return cindexOf( item[0] );
  97   }else{
  98     Assert(n.hasAttribute(DatatypeConsIndexAttr()));
  99     return n.getAttribute(DatatypeConsIndexAttr());
 100   }
 101 }
 102
 103 void Datatype::resolve(ExprManager* em,
 104                        const std::map<std::string, DatatypeType>& resolutions,
 105                        const std::vector<Type>& placeholders,
 106                        const std::vector<Type>& replacements,
 107                        const std::vector< SortConstructorType >& paramTypes,
 108                        const std::vector< DatatypeType >& paramReplacements)
 109   throw(IllegalArgumentException, DatatypeResolutionException) {
 110
 111   PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
 112   PrettyCheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
 113   PrettyCheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
 114                 "Datatype::resolve(): resolutions doesn't contain me!");
 115   PrettyCheckArgument(placeholders.size() == replacements.size(), placeholders,
 116                 "placeholders and replacements must be the same size");
 117   PrettyCheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
 118                 "paramTypes and paramReplacements must be the same size");
 119   PrettyCheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
 120   DatatypeType self = (*resolutions.find(d_name)).second;
 121   PrettyCheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
 122   d_resolved = true;
 123   size_t index = 0;
 124   for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
 125     (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index);
 126     Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
 127     Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
 128   }
 129   d_self = self;
 130
 131   d_involvesExt =  false;
 132   d_involvesUt =  false;
 133   for(const_iterator i = begin(); i != end(); ++i) {
 134     if( (*i).involvesExternalType() ){
 135       d_involvesExt =  true;
 136     }
 137     if( (*i).involvesUninterpretedType() ){
 138       d_involvesUt =  true;
 139     }
 140   }
 141
 142   if( d_isRecord ){
 143     std::vector< std::pair<std::string, Type> > fields;
 144     for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){
 145       fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) );
 146     }
 147     d_record = new Record(fields);
 148   }
 149 }
 150
 151 void Datatype::addConstructor(const DatatypeConstructor& c) {
 152   PrettyCheckArgument(!d_resolved, this,
 153                 "cannot add a constructor to a finalized Datatype");
 154   d_constructors.push_back(c);
 155 }
 156
 157
 158 void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
 159   PrettyCheckArgument(!d_resolved, this,
 160                 "cannot set sygus type to a finalized Datatype");
 161   d_sygus_type = st;
 162   d_sygus_bvl = bvl;
 163   d_sygus_allow_const = allow_const || allow_all;
 164   d_sygus_allow_all = allow_all;
 165 }
 166
 167 void Datatype::setTuple() {
 168   PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
 169   d_isTuple = true;
 170 }
 171
 172 void Datatype::setRecord() {
 173   PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype");
 174   d_isRecord = true;
 175 }
 176
 177 Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
 178   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 179   std::vector< Type > processing;
 180   computeCardinality( processing );
 181   return d_card;
 182 }
 183
 184 Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
 185   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 186   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
 187     d_card = Cardinality::INTEGERS;
 188   }else{
 189     processing.push_back( d_self );
 190     Cardinality c = 0;
 191     for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 192       c += (*i).computeCardinality( processing );
 193     }
 194     d_card = c;
 195     processing.pop_back();
 196   }
 197   return d_card;
 198 }
 199
 200 bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
 201   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 202   if( d_card_rec_singleton==0 ){
 203     if( isCodatatype() ){
 204       Assert( d_card_u_assume.empty() );
 205       std::vector< Type > processing;
 206       if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
 207         d_card_rec_singleton = 1;
 208       }else{
 209         d_card_rec_singleton = -1;
 210       }
 211       if( d_card_rec_singleton==1 ){
 212         Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
 213         for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
 214           Trace("dt-card") << "  " << d_card_u_assume [i] << std::endl;
 215         }
 216         Trace("dt-card") << std::endl;
 217       }
 218     }else{
 219       d_card_rec_singleton = -1;
 220     }
 221   }
 222   return d_card_rec_singleton==1;
 223 }
 224
 225 unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) {
 226   return d_card_u_assume.size();
 227 }
 228 Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) {
 229   return d_card_u_assume[i];
 230 }
 231
 232 bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){
 233   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
 234     return true;
 235   }else{
 236     if( d_card_rec_singleton==0 ){
 237       //if not yet computed
 238       if( d_constructors.size()==1 ){
 239         bool success = false;
 240         processing.push_back( d_self );
 241         for(unsigned i = 0; i<d_constructors[0].getNumArgs(); i++ ) {
 242           Type t = ((SelectorType)d_constructors[0][i].getType()).getRangeType();
 243           //if it is an uninterpreted sort, then we depend on it having cardinality one
 244           if( t.isSort() ){
 245             if( std::find( u_assume.begin(), u_assume.end(), t )==u_assume.end() ){
 246               u_assume.push_back( t );
 247             }
 248           //if it is a datatype, recurse
 249           }else if( t.isDatatype() ){
 250             const Datatype & dt = ((DatatypeType)t).getDatatype();
 251             if( !dt.computeCardinalityRecSingleton( processing, u_assume ) ){
 252               return false;
 253             }else{
 254               success = true;
 255             }
 256           //if it is a builtin type, it must have cardinality one
 257           }else if( !t.getCardinality().isOne() ){
 258             return false;
 259           }
 260         }
 261         processing.pop_back();
 262         return success;
 263       }else{
 264         return false;
 265       }
 266     }else if( d_card_rec_singleton==-1 ){
 267       return false;
 268     }else{
 269       for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
 270         if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[i] )==u_assume.end() ){
 271           u_assume.push_back( d_card_u_assume[i] );
 272         }
 273       }
 274       return true;
 275     }
 276   }
 277 }
 278
 279 bool Datatype::isFinite() const throw(IllegalArgumentException) {
 280   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 281
 282   // we're using some internals, so we have to set up this library context
 283   ExprManagerScope ems(d_self);
 284   TypeNode self = TypeNode::fromType(d_self);
 285   // is this already in the cache ?
 286   if(self.getAttribute(DatatypeFiniteComputedAttr())) {
 287     return self.getAttribute(DatatypeFiniteAttr());
 288   }
 289   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 290     if(! (*i).isFinite()) {
 291       self.setAttribute(DatatypeFiniteComputedAttr(), true);
 292       self.setAttribute(DatatypeFiniteAttr(), false);
 293       return false;
 294     }
 295   }
 296   self.setAttribute(DatatypeFiniteComputedAttr(), true);
 297   self.setAttribute(DatatypeFiniteAttr(), true);
 298   return true;
 299 }
 300
 301 bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) {
 302   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 303   // we're using some internals, so we have to set up this library context
 304   ExprManagerScope ems(d_self);
 305   TypeNode self = TypeNode::fromType(d_self);
 306   // is this already in the cache ?
 307   if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
 308     return self.getAttribute(DatatypeUFiniteAttr());
 309   }
 310   //start by assuming it is not
 311   self.setAttribute(DatatypeUFiniteComputedAttr(), true);
 312   self.setAttribute(DatatypeUFiniteAttr(), false);
 313   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 314     if(! (*i).isInterpretedFinite()) {
 315       return false;
 316     }
 317   }
 318   self.setAttribute(DatatypeUFiniteComputedAttr(), true);
 319   self.setAttribute(DatatypeUFiniteAttr(), true);
 320   return true;
 321 }
 322
 323 bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
 324   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 325   if( d_well_founded==0 ){
 326     // we're using some internals, so we have to set up this library context
 327     ExprManagerScope ems(d_self);
 328     std::vector< Type > processing;
 329     if( computeWellFounded( processing ) ){
 330       d_well_founded = 1;
 331     }else{
 332       d_well_founded = -1;
 333     }
 334   }
 335   return d_well_founded==1;
 336 }
 337
 338 bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) {
 339   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 340   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
 341     return d_isCo;
 342   }else{
 343     processing.push_back( d_self );
 344     for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 345       if( (*i).computeWellFounded( processing ) ){
 346         processing.pop_back();
 347         return true;
 348       }else{
 349         Trace("dt-wf") << "Constructor " << (*i).getName() << " is not well-founded." << std::endl;
 350       }
 351     }
 352     processing.pop_back();
 353     Trace("dt-wf") << "Datatype " << getName() << " is not well-founded." << std::endl;
 354     return false;
 355   }
 356 }
 357
 358 Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
 359   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 360   ExprManagerScope ems(d_self);
 361
 362
 363   // is this already in the cache ?
 364   std::map< Type, Expr >::iterator it = d_ground_term.find( t );
 365   if( it != d_ground_term.end() ){
 366     Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl;
 367     return it->second;
 368   } else {
 369     std::vector< Type > processing;
 370     Expr groundTerm = computeGroundTerm( t, processing );
 371     if(!groundTerm.isNull() ) {
 372       // we found a ground-term-constructing constructor!
 373       d_ground_term[t] = groundTerm;
 374       Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
 375     }
 376     if( groundTerm.isNull() ){
 377       if( !d_isCo ){
 378         // if we get all the way here, we aren't well-founded
 379         IllegalArgument(*this, "datatype is not well-founded, cannot construct a ground term!");
 380       }else{
 381         return groundTerm;
 382       }
 383     }else{
 384       return groundTerm;
 385     }
 386   }
 387 }
 388
 389 Expr getSubtermWithType( Expr e, Type t, bool isTop ){
 390   if( !isTop && e.getType()==t ){
 391     return e;
 392   }else{
 393     for( unsigned i=0; i<e.getNumChildren(); i++ ){
 394       Expr se = getSubtermWithType( e[i], t, false );
 395       if( !se.isNull() ){
 396         return se;
 397       }
 398     }
 399     return Expr();
 400   }
 401 }
 402
 403 Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
 404   if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){
 405     processing.push_back( d_self );
 406     for( unsigned r=0; r<2; r++ ){
 407       for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 408         //do nullary constructors first
 409         if( ((*i).getNumArgs()==0)==(r==0)){
 410           Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl;
 411           Expr e = (*i).computeGroundTerm( t, processing, d_ground_term );
 412           if( !e.isNull() ){
 413             //must check subterms for the same type to avoid infinite loops in type enumeration
 414             Expr se = getSubtermWithType( e, t, true );
 415             if( !se.isNull() ){
 416               Debug("datatypes") << "Take subterm " << se << std::endl;
 417               e = se;
 418             }
 419             processing.pop_back();
 420             return e;
 421           }else{
 422             Debug("datatypes") << "...failed." << std::endl;
 423           }
 424         }
 425       }
 426     }
 427     processing.pop_back();
 428   }else{
 429     Debug("datatypes") << "...already processing " << t << std::endl;
 430   }
 431   return Expr();
 432 }
 433
 434 DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
 435   PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
 436   PrettyCheckArgument(!d_self.isNull(), *this);
 437   return DatatypeType(d_self);
 438 }
 439
 440 DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
 441   const throw(IllegalArgumentException) {
 442   PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
 443   PrettyCheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
 444   return DatatypeType(d_self).instantiate(params);
 445 }
 446
 447 bool Datatype::operator==(const Datatype& other) const throw() {
 448   // two datatypes are == iff the name is the same and they have
 449   // exactly matching constructors (in the same order)
 450
 451   if(this == &other) {
 452     return true;
 453   }
 454
 455   if(isResolved() != other.isResolved()) {
 456     return false;
 457   }
 458
 459   if( d_name != other.d_name ||
 460       getNumConstructors() != other.getNumConstructors() ) {
 461     return false;
 462   }
 463   for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) {
 464     Assert(j != other.end());
 465     // two constructors are == iff they have the same name, their
 466     // constructors and testers are equal and they have exactly
 467     // matching args (in the same order)
 468     if((*i).getName() != (*j).getName() ||
 469        (*i).getNumArgs() != (*j).getNumArgs()) {
 470       return false;
 471     }
 472     // testing equivalence of constructors and testers is harder b/c
 473     // this constructor might not be resolved yet; only compare them
 474     // if they are both resolved
 475     Assert(isResolved() == !(*i).d_constructor.isNull() &&
 476            isResolved() == !(*i).d_tester.isNull() &&
 477            (*i).d_constructor.isNull() == (*j).d_constructor.isNull() &&
 478            (*i).d_tester.isNull() == (*j).d_tester.isNull());
 479     if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) {
 480       return false;
 481     }
 482     if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) {
 483       return false;
 484     }
 485     for(DatatypeConstructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) {
 486       Assert(l != (*j).end());
 487       if((*k).getName() != (*l).getName()) {
 488         return false;
 489       }
 490       // testing equivalence of selectors is harder b/c args might not
 491       // be resolved yet
 492       Assert(isResolved() == (*k).isResolved() &&
 493              (*k).isResolved() == (*l).isResolved());
 494       if((*k).isResolved()) {
 495         // both are resolved, so simply compare the selectors directly
 496         if((*k).d_selector != (*l).d_selector) {
 497           return false;
 498         }
 499       } else {
 500         // neither is resolved, so compare their (possibly unresolved)
 501         // types; we don't know if they'll be resolved the same way,
 502         // so we can't ever say unresolved types are equal
 503         if(!(*k).d_selector.isNull() && !(*l).d_selector.isNull()) {
 504           if((*k).d_selector.getType() != (*l).d_selector.getType()) {
 505             return false;
 506           }
 507         } else {
 508           if((*k).isUnresolvedSelf() && (*l).isUnresolvedSelf()) {
 509             // Fine, the selectors are equal if the rest of the
 510             // enclosing datatypes are equal...
 511           } else {
 512             return false;
 513           }
 514         }
 515       }
 516     }
 517   }
 518   return true;
 519 }
 520
 521 const DatatypeConstructor& Datatype::operator[](size_t index) const {
 522   PrettyCheckArgument(index < getNumConstructors(), index, "index out of bounds");
 523   return d_constructors[index];
 524 }
 525
 526 const DatatypeConstructor& Datatype::operator[](std::string name) const {
 527   for(const_iterator i = begin(); i != end(); ++i) {
 528     if((*i).getName() == name) {
 529       return *i;
 530     }
 531   }
 532   IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
 533 }
 534
 535 Expr Datatype::getConstructor(std::string name) const {
 536   return (*this)[name].getConstructor();
 537 }
 538
 539 Type Datatype::getSygusType() const {
 540   return d_sygus_type;
 541 }
 542
 543 Expr Datatype::getSygusVarList() const {
 544   return d_sygus_bvl;
 545 }
 546
 547 bool Datatype::getSygusAllowConst() const {
 548   return d_sygus_allow_const;
 549 }
 550
 551 bool Datatype::getSygusAllowAll() const {
 552   return d_sygus_allow_const;
 553 }
 554
 555 bool Datatype::involvesExternalType() const{
 556   return d_involvesExt;
 557 }
 558
 559 bool Datatype::involvesUninterpretedType() const{
 560   return d_involvesUt;
 561 }
 562
 563 void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
 564                                   const std::map<std::string, DatatypeType>& resolutions,
 565                                   const std::vector<Type>& placeholders,
 566                                   const std::vector<Type>& replacements,
 567                                   const std::vector< SortConstructorType >& paramTypes,
 568                                   const std::vector< DatatypeType >& paramReplacements, size_t cindex)
 569   throw(IllegalArgumentException, DatatypeResolutionException) {
 570
 571   PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
 572   PrettyCheckArgument(!isResolved(),
 573                 "cannot resolve a Datatype constructor twice; "
 574                 "perhaps the same constructor was added twice, "
 575                 "or to two datatypes?");
 576
 577   // we're using some internals, so we have to set up this library context
 578   ExprManagerScope ems(*em);
 579
 580   NodeManager* nm = NodeManager::fromExprManager(em);
 581   TypeNode selfTypeNode = TypeNode::fromType(self);
 582   size_t index = 0;
 583   for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
 584     if((*i).d_selector.isNull()) {
 585       // the unresolved type wasn't created here; do name resolution
 586       string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
 587       (*i).d_name.resize((*i).d_name.find('\0'));
 588       if(typeName == "") {
 589         (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
 590       } else {
 591         map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
 592         if(j == resolutions.end()) {
 593           stringstream msg;
 594           msg << "cannot resolve type \"" << typeName << "\" "
 595               << "in selector \"" << (*i).d_name << "\" "
 596               << "of constructor \"" << d_name << "\"";
 597           throw DatatypeResolutionException(msg.str());
 598         } else {
 599           (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
 600         }
 601       }
 602     } else {
 603       // the type for the selector already exists; may need
 604       // complex-type substitution
 605       Type range = (*i).d_selector.getType();
 606       if(!placeholders.empty()) {
 607         range = range.substitute(placeholders, replacements);
 608       }
 609       if(!paramTypes.empty() ) {
 610         range = doParametricSubstitution( range, paramTypes, paramReplacements );
 611       }
 612       (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
 613     }
 614     Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex);
 615     Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
 616     (*i).d_resolved = true;
 617   }
 618
 619   Assert(index == getNumArgs());
 620
 621   // Set constructor/tester last, since DatatypeConstructor::isResolved()
 622   // returns true when d_tester is not the null Expr.  If something
 623   // fails above, we want Constuctor::isResolved() to remain "false".
 624   // Further, mkConstructorType() iterates over the selectors, so
 625   // should get the results of any resolutions we did above.
 626   d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
 627   d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
 628   // associate constructor with all selectors
 629   for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
 630     (*i).d_constructor = d_constructor;
 631   }
 632 }
 633
 634 Type DatatypeConstructor::doParametricSubstitution( Type range,
 635                                   const std::vector< SortConstructorType >& paramTypes,
 636                                   const std::vector< DatatypeType >& paramReplacements ) {
 637   TypeNode typn = TypeNode::fromType( range );
 638   if(typn.getNumChildren() == 0) {
 639     return range;
 640   } else {
 641     std::vector< Type > origChildren;
 642     std::vector< Type > children;
 643     for(TypeNode::const_iterator i = typn.begin(), iend = typn.end();i != iend; ++i) {
 644       origChildren.push_back( (*i).toType() );
 645       children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) );
 646     }
 647     for( unsigned i = 0; i < paramTypes.size(); ++i ) {
 648       if( paramTypes[i].getArity() == origChildren.size() ) {
 649         Type tn = paramTypes[i].instantiate( origChildren );
 650         if( range == tn ) {
 651           return paramReplacements[i].instantiate( children );
 652         }
 653       }
 654     }
 655     NodeBuilder<> nb(typn.getKind());
 656     for( unsigned i = 0; i < children.size(); ++i ) {
 657       nb << TypeNode::fromType( children[i] );
 658     }
 659     return nb.constructTypeNode().toType();
 660   }
 661 }
 662
 663 DatatypeConstructor::DatatypeConstructor(std::string name) :
 664   // We don't want to introduce a new data member, because eventually
 665   // we're going to be a constant stuffed inside a node.  So we stow
 666   // the tester name away inside the constructor name until
 667   // resolution.
 668   d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
 669   d_tester(),
 670   d_args() {
 671   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 672 }
 673
 674 DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
 675   // We don't want to introduce a new data member, because eventually
 676   // we're going to be a constant stuffed inside a node.  So we stow
 677   // the tester name away inside the constructor name until
 678   // resolution.
 679   d_name(name + '\0' + tester),
 680   d_tester(),
 681   d_args() {
 682   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 683   PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 684 }
 685
 686 void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){
 687   d_sygus_op = op;
 688   d_sygus_let_body = let_body;
 689   d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() );
 690   d_sygus_num_let_input_args = num_let_input_args;
 691 }
 692
 693 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
 694   // We don't want to introduce a new data member, because eventually
 695   // we're going to be a constant stuffed inside a node.  So we stow
 696   // the selector type away inside a var until resolution (when we can
 697   // create the proper selector type)
 698   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 699   PrettyCheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
 700
 701   // we're using some internals, so we have to set up this library context
 702   ExprManagerScope ems(selectorType);
 703
 704   Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName, TypeNode::fromType(selectorType), "is an unresolved selector type placeholder", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
 705   Debug("datatypes") << type << endl;
 706   d_args.push_back(DatatypeConstructorArg(selectorName, type));
 707 }
 708
 709 void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) {
 710   // We don't want to introduce a new data member, because eventually
 711   // we're going to be a constant stuffed inside a node.  So we stow
 712   // the selector type away after a NUL in the name string until
 713   // resolution (when we can create the proper selector type)
 714   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 715   PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
 716   d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
 717 }
 718
 719 void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
 720   // We don't want to introduce a new data member, because eventually
 721   // we're going to be a constant stuffed inside a node.  So we mark
 722   // the name string with a NUL to indicate that we have a
 723   // self-selecting selector until resolution (when we can create the
 724   // proper selector type)
 725   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 726   d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
 727 }
 728
 729 std::string DatatypeConstructor::getName() const throw() {
 730   return d_name.substr(0, d_name.find('\0'));
 731 }
 732
 733 std::string DatatypeConstructor::getTesterName() const throw() {
 734   return d_name.substr(d_name.find('\0') + 1);
 735 }
 736
 737 Expr DatatypeConstructor::getConstructor() const {
 738   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 739   return d_constructor;
 740 }
 741
 742 Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
 743   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 744   ExprManagerScope ems(d_constructor);
 745   const Datatype& dt = Datatype::datatypeOf(d_constructor);
 746   PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
 747   DatatypeType dtt = dt.getDatatypeType();
 748   Matcher m(dtt);
 749   m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );
 750   vector<Type> subst;
 751   m.getMatches(subst);
 752   vector<Type> params = dt.getParameters();
 753   return d_constructor.getType().substitute(params, subst);
 754 }
 755
 756 Expr DatatypeConstructor::getTester() const {
 757   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 758   return d_tester;
 759 }
 760
 761 Expr DatatypeConstructor::getSygusOp() const {
 762   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 763   return d_sygus_op;
 764 }
 765
 766 Expr DatatypeConstructor::getSygusLetBody() const {
 767   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 768   return d_sygus_let_body;
 769 }
 770
 771 unsigned DatatypeConstructor::getNumSygusLetArgs() const {
 772   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 773   return d_sygus_let_args.size();
 774 }
 775
 776 Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
 777   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 778   return d_sygus_let_args[i];
 779 }
 780
 781 unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
 782   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 783   return d_sygus_num_let_input_args;
 784 }
 785
 786 bool DatatypeConstructor::isSygusIdFunc() const {
 787   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 788   return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
 789 }
 790
 791 Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
 792   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 793
 794   Cardinality c = 1;
 795
 796   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 797     c *= SelectorType((*i).getSelector().getType()).getRangeType().getCardinality();
 798   }
 799
 800   return c;
 801 }
 802
 803 /** compute the cardinality of this datatype */
 804 Cardinality DatatypeConstructor::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
 805   Cardinality c = 1;
 806   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 807     Type t = SelectorType((*i).getSelector().getType()).getRangeType();
 808     if( t.isDatatype() ){
 809       const Datatype& dt = ((DatatypeType)t).getDatatype();
 810       c *= dt.computeCardinality( processing );
 811     }else{
 812       c *= t.getCardinality();
 813     }
 814   }
 815   return c;
 816 }
 817
 818 bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException){
 819   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 820     Type t = SelectorType((*i).getSelector().getType()).getRangeType();
 821     if( t.isDatatype() ){
 822       const Datatype& dt = ((DatatypeType)t).getDatatype();
 823       if( !dt.computeWellFounded( processing ) ){
 824         return false;
 825       }
 826     }
 827   }
 828   return true;
 829 }
 830
 831
 832 bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
 833   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 834
 835   // we're using some internals, so we have to set up this library context
 836   ExprManagerScope ems(d_constructor);
 837   TNode self = Node::fromExpr(d_constructor);
 838   // is this already in the cache ?
 839   if(self.getAttribute(DatatypeFiniteComputedAttr())) {
 840     return self.getAttribute(DatatypeFiniteAttr());
 841   }
 842   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 843     if(! (*i).getRangeType().getCardinality().isFinite()) {
 844       self.setAttribute(DatatypeFiniteComputedAttr(), true);
 845       self.setAttribute(DatatypeFiniteAttr(), false);
 846       return false;
 847     }
 848   }
 849   self.setAttribute(DatatypeFiniteComputedAttr(), true);
 850   self.setAttribute(DatatypeFiniteAttr(), true);
 851   return true;
 852 }
 853
 854 bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentException) {
 855   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 856   // we're using some internals, so we have to set up this library context
 857   ExprManagerScope ems(d_constructor);
 858   TNode self = Node::fromExpr(d_constructor);
 859   // is this already in the cache ?
 860   if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
 861     return self.getAttribute(DatatypeUFiniteAttr());
 862   }
 863   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 864     TypeNode t = TypeNode::fromType( (*i).getRangeType() );
 865     if(!t.isInterpretedFinite()) {
 866       self.setAttribute(DatatypeUFiniteComputedAttr(), true);
 867       self.setAttribute(DatatypeUFiniteAttr(), false);
 868       return false;
 869     }
 870   }
 871   self.setAttribute(DatatypeUFiniteComputedAttr(), true);
 872   self.setAttribute(DatatypeUFiniteAttr(), true);
 873   return true;
 874 }
 875
 876 Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) {
 877 // we're using some internals, so we have to set up this library context
 878   ExprManagerScope ems(d_constructor);
 879
 880   std::vector<Expr> groundTerms;
 881   groundTerms.push_back(getConstructor());
 882
 883   // for each selector, get a ground term
 884   std::vector< Type > instTypes;
 885   std::vector< Type > paramTypes;
 886   if( DatatypeType(t).isParametric() ){
 887     paramTypes = DatatypeType(t).getDatatype().getParameters();
 888     instTypes = DatatypeType(t).getParamTypes();
 889   }
 890   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
 891     Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
 892     if( DatatypeType(t).isParametric() ){
 893       selType = selType.substitute( paramTypes, instTypes );
 894     }
 895     Expr arg;
 896     if( selType.isDatatype() ){
 897       std::map< Type, Expr >::iterator itgt = gt.find( selType );
 898       if( itgt != gt.end() ){
 899         arg = itgt->second;
 900       }else{
 901         const Datatype & dt = DatatypeType(selType).getDatatype();
 902         arg = dt.computeGroundTerm( selType, processing );
 903       }
 904     }else{
 905       arg = selType.mkGroundTerm();
 906     }
 907     if( arg.isNull() ){
 908       Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl;
 909       return Expr();
 910     }else{
 911       Debug("datatypes") << "...constructed arg " << arg.getType() << std::endl;
 912       groundTerms.push_back(arg);
 913     }
 914   }
 915
 916   Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
 917   if( groundTerm.getType()!=t ){
 918     Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
 919     //type is ambiguous, must apply type ascription
 920     Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
 921     groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
 922                        getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
 923                        groundTerms[0]);
 924     groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
 925   }
 926   return groundTerm;
 927 }
 928
 929
 930 const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
 931   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
 932   return d_args[index];
 933 }
 934
 935 const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const {
 936   for(const_iterator i = begin(); i != end(); ++i) {
 937     if((*i).getName() == name) {
 938       return *i;
 939     }
 940   }
 941   IllegalArgument(name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
 942 }
 943
 944 Expr DatatypeConstructor::getSelector(std::string name) const {
 945   return (*this)[name].getSelector();
 946 }
 947
 948 bool DatatypeConstructor::involvesExternalType() const{
 949   for(const_iterator i = begin(); i != end(); ++i) {
 950     if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) {
 951       return true;
 952     }
 953   }
 954   return false;
 955 }
 956
 957 bool DatatypeConstructor::involvesUninterpretedType() const{
 958   for(const_iterator i = begin(); i != end(); ++i) {
 959     if(SelectorType((*i).getSelector().getType()).getRangeType().isSort()) {
 960       return true;
 961     }
 962   }
 963   return false;
 964 }
 965
 966 DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) :
 967   d_name(name),
 968   d_selector(selector),
 969   d_resolved(false) {
 970   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
 971 }
 972
 973 std::string DatatypeConstructorArg::getName() const throw() {
 974   string name = d_name;
 975   const size_t nul = name.find('\0');
 976   if(nul != string::npos) {
 977     name.resize(nul);
 978   }
 979   return name;
 980 }
 981
 982 Expr DatatypeConstructorArg::getSelector() const {
 983   PrettyCheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
 984   return d_selector;
 985 }
 986
 987 Expr DatatypeConstructorArg::getConstructor() const {
 988   PrettyCheckArgument(isResolved(), this,
 989                 "cannot get a associated constructor for argument of an unresolved datatype constructor");
 990   return d_constructor;
 991 }
 992
 993 SelectorType DatatypeConstructorArg::getType() const {
 994   return getSelector().getType();
 995 }
 996
 997 Type DatatypeConstructorArg::getRangeType() const {
 998   return getType().getRangeType();
 999 }
1000
1001 bool DatatypeConstructorArg::isUnresolvedSelf() const throw() {
1002   return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
1003 }
1004
1005 static const int s_printDatatypeNamesOnly = std::ios_base::xalloc();
1006
1007 std::string DatatypeConstructorArg::getTypeName() const {
1008   Type t;
1009   if(isResolved()) {
1010     t = SelectorType(d_selector.getType()).getRangeType();
1011   } else {
1012     if(d_selector.isNull()) {
1013       string typeName = d_name.substr(d_name.find('\0') + 1);
1014       return (typeName == "") ? "[self]" : typeName;
1015     } else {
1016       t = d_selector.getType();
1017     }
1018   }
1019
1020   // Unfortunately, in the case of complex selector types, we can
1021   // enter nontrivial recursion here.  Make sure that doesn't happen.
1022   stringstream ss;
1023   ss << language::SetLanguage(language::output::LANG_CVC4);
1024   ss.iword(s_printDatatypeNamesOnly) = 1;
1025   t.toStream(ss);
1026   return ss.str();
1027 }
1028
1029 std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
1030   // These datatype things are recursive!  Be very careful not to
1031   // print an infinite chain of them.
1032   long& printNameOnly = os.iword(s_printDatatypeNamesOnly);
1033   Debug("datatypes-output") << "printNameOnly is " << printNameOnly << std::endl;
1034   if(printNameOnly) {
1035     return os << dt.getName();
1036   }
1037
1038   class Scope {
1039     long& d_ref;
1040     long d_oldValue;
1041   public:
1042     Scope(long& ref, long value) : d_ref(ref), d_oldValue(ref) { d_ref = value; }
1043     ~Scope() { d_ref = d_oldValue; }
1044   } scope(printNameOnly, 1);
1045   // when scope is destructed, the value pops back
1046
1047   Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl;
1048
1049   // can only output datatypes in the CVC4 native language
1050   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
1051
1052   os << "DATATYPE " << dt.getName();
1053   if(dt.isParametric()) {
1054     os << '[';
1055     for(size_t i = 0; i < dt.getNumParameters(); ++i) {
1056       if(i > 0) {
1057         os << ',';
1058       }
1059       os << dt.getParameter(i);
1060     }
1061     os << ']';
1062   }
1063   os << " =" << endl;
1064   Datatype::const_iterator i = dt.begin(), i_end = dt.end();
1065   if(i != i_end) {
1066     os << "  ";
1067     do {
1068       os << *i << endl;
1069       if(++i != i_end) {
1070         os << "| ";
1071       }
1072     } while(i != i_end);
1073   }
1074   os << "END;" << endl;
1075
1076   return os;
1077 }
1078
1079 std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
1080   // can only output datatypes in the CVC4 native language
1081   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
1082
1083   os << ctor.getName();
1084
1085   DatatypeConstructor::const_iterator i = ctor.begin(), i_end = ctor.end();
1086   if(i != i_end) {
1087     os << "(";
1088     do {
1089       os << *i;
1090       if(++i != i_end) {
1091         os << ", ";
1092       }
1093     } while(i != i_end);
1094     os << ")";
1095   }
1096
1097   return os;
1098 }
1099
1100 std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
1101   // can only output datatypes in the CVC4 native language
1102   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
1103
1104   os << arg.getName() << ": " << arg.getTypeName();
1105
1106   return os;
1107 }
1108
1109 DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException) : d_index(index){
1110
1111 }
1112
1113 std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
1114   return out << "index_" << dic.getIndex();
1115 }
1116
1117 }/* CVC4 namespace */