src/expr/datatype.cpp

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