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