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