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