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