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