src/expr/datatype.cpp

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