src/expr/datatype.cpp

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