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