src/expr/datatype.cpp

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