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