src/expr/datatype.cpp

   1 /*********************                                                        */
   2 /*! \file datatype.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A class representing a Datatype definition
  13  **
  14  ** A class representing a Datatype definition for the theory of
  15  ** inductive datatypes.
  16  **/
  17 #include "expr/datatype.h"
  18
  19 #include <string>
  20 #include <sstream>
  21
  22 #include "base/check.h"
  23 #include "expr/attribute.h"
  24 #include "expr/dtype.h"
  25 #include "expr/expr_manager.h"
  26 #include "expr/expr_manager_scope.h"
  27 #include "expr/node.h"
  28 #include "expr/node_algorithm.h"
  29 #include "expr/node_manager.h"
  30 #include "expr/type.h"
  31 #include "expr/type_matcher.h"
  32 #include "options/datatypes_options.h"
  33 #include "options/set_language.h"
  34 #include "theory/type_enumerator.h"
  35
  36 using namespace std;
  37
  38 namespace CVC4 {
  39
  40 Datatype::~Datatype()
  41 {
  42   ExprManagerScope ems(*d_em);
  43   d_internal.reset();
  44   d_constructors.clear();
  45   delete d_record;
  46 }
  47
  48 Datatype::Datatype(ExprManager* em, std::string name, bool isCo)
  49     : d_em(em),
  50       d_internal(nullptr),
  51       d_record(NULL),
  52       d_isRecord(false),
  53       d_constructors()
  54 {
  55   ExprManagerScope ems(*d_em);
  56   d_internal = std::make_shared<DType>(name, isCo);
  57 }
  58
  59 Datatype::Datatype(ExprManager* em,
  60                    std::string name,
  61                    const std::vector<Type>& params,
  62                    bool isCo)
  63     : d_em(em),
  64       d_internal(nullptr),
  65       d_record(NULL),
  66       d_isRecord(false),
  67       d_constructors()
  68 {
  69   ExprManagerScope ems(*d_em);
  70   std::vector<TypeNode> paramsn;
  71   for (const Type& t : params)
  72   {
  73     paramsn.push_back(TypeNode::fromType(t));
  74   }
  75   d_internal = std::make_shared<DType>(name, paramsn, isCo);
  76 }
  77
  78 const Datatype& Datatype::datatypeOf(Expr item) {
  79   ExprManagerScope ems(item);
  80   TypeNode t = Node::fromExpr(item).getType();
  81   switch(t.getKind()) {
  82   case kind::CONSTRUCTOR_TYPE:
  83     return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype();
  84   case kind::SELECTOR_TYPE:
  85   case kind::TESTER_TYPE:
  86     return DatatypeType(t[0].toType()).getDatatype();
  87   default:
  88     Unhandled() << "arg must be a datatype constructor, selector, or tester";
  89   }
  90 }
  91
  92 size_t Datatype::indexOf(Expr item) {
  93   ExprManagerScope ems(item);
  94   PrettyCheckArgument(item.getType().isConstructor() ||
  95                 item.getType().isTester() ||
  96                 item.getType().isSelector(),
  97                 item,
  98                 "arg must be a datatype constructor, selector, or tester");
  99   return indexOfInternal(item);
 100 }
 101
 102 size_t Datatype::indexOfInternal(Expr item)
 103 {
 104   TNode n = Node::fromExpr(item);
 105   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
 106     return indexOf( item[0] );
 107   }else{
 108     Assert(n.hasAttribute(DTypeIndexAttr()));
 109     return n.getAttribute(DTypeIndexAttr());
 110   }
 111 }
 112
 113 size_t Datatype::cindexOf(Expr item) {
 114   ExprManagerScope ems(item);
 115   PrettyCheckArgument(item.getType().isSelector(),
 116                 item,
 117                 "arg must be a datatype selector");
 118   return cindexOfInternal(item);
 119 }
 120 size_t Datatype::cindexOfInternal(Expr item)
 121 {
 122   TNode n = Node::fromExpr(item);
 123   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
 124     return cindexOf( item[0] );
 125   }else{
 126     Assert(n.hasAttribute(DTypeConsIndexAttr()));
 127     return n.getAttribute(DTypeConsIndexAttr());
 128   }
 129 }
 130
 131 void Datatype::resolve(const std::map<std::string, DatatypeType>& resolutions,
 132                        const std::vector<Type>& placeholders,
 133                        const std::vector<Type>& replacements,
 134                        const std::vector<SortConstructorType>& paramTypes,
 135                        const std::vector<DatatypeType>& paramReplacements)
 136 {
 137   PrettyCheckArgument(!isResolved(), this, "cannot resolve a Datatype twice");
 138   PrettyCheckArgument(resolutions.find(getName()) != resolutions.end(),
 139                       resolutions,
 140                       "Datatype::resolve(): resolutions doesn't contain me!");
 141   PrettyCheckArgument(placeholders.size() == replacements.size(), placeholders,
 142                 "placeholders and replacements must be the same size");
 143   PrettyCheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
 144                 "paramTypes and paramReplacements must be the same size");
 145   PrettyCheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
 146
 147   // we're using some internals, so we have to make sure that the Datatype's
 148   // ExprManager is active
 149   ExprManagerScope ems(*d_em);
 150
 151   Trace("datatypes") << "Datatype::resolve: " << getName()
 152                      << ", #placeholders=" << placeholders.size() << std::endl;
 153
 154   std::map<std::string, TypeNode> resolutionsn;
 155   std::vector<TypeNode> placeholdersn;
 156   std::vector<TypeNode> replacementsn;
 157   std::vector<TypeNode> paramTypesn;
 158   std::vector<TypeNode> paramReplacementsn;
 159   for (const std::pair<const std::string, DatatypeType>& r : resolutions)
 160   {
 161     resolutionsn[r.first] = TypeNode::fromType(r.second);
 162   }
 163   for (const Type& t : placeholders)
 164   {
 165     placeholdersn.push_back(TypeNode::fromType(t));
 166   }
 167   for (const Type& t : replacements)
 168   {
 169     replacementsn.push_back(TypeNode::fromType(t));
 170   }
 171   for (const Type& t : paramTypes)
 172   {
 173     paramTypesn.push_back(TypeNode::fromType(t));
 174   }
 175   for (const Type& t : paramReplacements)
 176   {
 177     paramReplacementsn.push_back(TypeNode::fromType(t));
 178   }
 179   bool res = d_internal->resolve(resolutionsn,
 180                                  placeholdersn,
 181                                  replacementsn,
 182                                  paramTypesn,
 183                                  paramReplacementsn);
 184   if (!res)
 185   {
 186     IllegalArgument(*this,
 187                     "could not resolve datatype that is not well formed");
 188   }
 189   Trace("dt-debug") << "Datatype::resolve: finished " << getName() << " "
 190                     << d_constructors.size() << std::endl;
 191   AlwaysAssert(isResolved());
 192   //
 193   d_self = d_internal->getTypeNode().toType();
 194   for (DatatypeConstructor& c : d_constructors)
 195   {
 196     AlwaysAssert(c.isResolved());
 197     c.d_constructor = c.d_internal->getConstructor().toExpr();
 198     for (size_t i = 0, nargs = c.getNumArgs(); i < nargs; i++)
 199     {
 200       AlwaysAssert(c.d_args[i].isResolved());
 201       c.d_args[i].d_selector = c.d_args[i].d_internal->getSelector().toExpr();
 202     }
 203   }
 204
 205   if( d_isRecord ){
 206     std::vector< std::pair<std::string, Type> > fields;
 207     for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){
 208       fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) );
 209     }
 210     d_record = new Record(fields);
 211   }
 212 }
 213
 214 void Datatype::addConstructor(const DatatypeConstructor& c) {
 215   Trace("dt-debug") << "Datatype::addConstructor" << std::endl;
 216   PrettyCheckArgument(
 217       !isResolved(), this, "cannot add a constructor to a finalized Datatype");
 218   d_constructors.push_back(c);
 219   d_internal->addConstructor(c.d_internal);
 220   Trace("dt-debug") << "Datatype::addConstructor: finished" << std::endl;
 221 }
 222
 223
 224 void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
 225   PrettyCheckArgument(
 226       !isResolved(), this, "cannot set sygus type to a finalized Datatype");
 227   TypeNode stn = TypeNode::fromType(st);
 228   Node bvln = Node::fromExpr(bvl);
 229   d_internal->setSygus(stn, bvln, allow_const, allow_all);
 230 }
 231
 232 void Datatype::addSygusConstructor(Expr op,
 233                                    const std::string& cname,
 234                                    const std::vector<Type>& cargs,
 235                                    std::shared_ptr<SygusPrintCallback> spc,
 236                                    int weight)
 237 {
 238   // avoid name clashes
 239   std::stringstream ss;
 240   ss << getName() << "_" << getNumConstructors() << "_" << cname;
 241   std::string name = ss.str();
 242   std::string testerId("is-");
 243   testerId.append(name);
 244   unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
 245   DatatypeConstructor c(name, testerId, cweight);
 246   c.setSygus(op, spc);
 247   for( unsigned j=0; j<cargs.size(); j++ ){
 248     Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
 249     std::stringstream sname;
 250     sname << name << "_" << j;
 251     c.addArg(sname.str(), cargs[j]);
 252   }
 253   addConstructor(c);
 254 }
 255
 256 void Datatype::addSygusConstructor(Kind k,
 257                                    const std::string& cname,
 258                                    const std::vector<Type>& cargs,
 259                                    std::shared_ptr<SygusPrintCallback> spc,
 260                                    int weight)
 261 {
 262   ExprManagerScope ems(*d_em);
 263   Expr op = d_em->operatorOf(k);
 264   addSygusConstructor(op, cname, cargs, spc, weight);
 265 }
 266
 267 void Datatype::setTuple() {
 268   PrettyCheckArgument(
 269       !isResolved(), this, "cannot set tuple to a finalized Datatype");
 270   d_internal->setTuple();
 271 }
 272
 273 void Datatype::setRecord() {
 274   PrettyCheckArgument(
 275       !isResolved(), this, "cannot set record to a finalized Datatype");
 276   d_isRecord = true;
 277 }
 278
 279 Cardinality Datatype::getCardinality(Type t) const
 280 {
 281   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 282   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 283   ExprManagerScope ems(d_self);
 284   TypeNode tn = TypeNode::fromType(t);
 285   return d_internal->getCardinality(tn);
 286 }
 287
 288 Cardinality Datatype::getCardinality() const
 289 {
 290   PrettyCheckArgument(!isParametric(), this, "for getCardinality, this datatype cannot be parametric");
 291   ExprManagerScope ems(d_self);
 292   return d_internal->getCardinality();
 293 }
 294
 295 bool Datatype::isRecursiveSingleton(Type t) const
 296 {
 297   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 298   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 299   ExprManagerScope ems(d_self);
 300   TypeNode tn = TypeNode::fromType(t);
 301   return d_internal->isRecursiveSingleton(tn);
 302 }
 303
 304 bool Datatype::isRecursiveSingleton() const
 305 {
 306   PrettyCheckArgument(!isParametric(), this, "for isRecursiveSingleton, this datatype cannot be parametric");
 307   ExprManagerScope ems(d_self);
 308   return d_internal->isRecursiveSingleton();
 309 }
 310
 311 unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const
 312 {
 313   Assert(isRecursiveSingleton(t));
 314   ExprManagerScope ems(d_self);
 315   TypeNode tn = TypeNode::fromType(t);
 316   return d_internal->getNumRecursiveSingletonArgTypes(tn);
 317 }
 318
 319 unsigned Datatype::getNumRecursiveSingletonArgTypes() const
 320 {
 321   PrettyCheckArgument(!isParametric(), this, "for getNumRecursiveSingletonArgTypes, this datatype cannot be parametric");
 322   ExprManagerScope ems(d_self);
 323   return d_internal->getNumRecursiveSingletonArgTypes();
 324 }
 325
 326 Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const
 327 {
 328   Assert(isRecursiveSingleton(t));
 329   ExprManagerScope ems(d_self);
 330   TypeNode tn = TypeNode::fromType(t);
 331   return d_internal->getRecursiveSingletonArgType(tn, i).toType();
 332 }
 333
 334 Type Datatype::getRecursiveSingletonArgType(unsigned i) const
 335 {
 336   PrettyCheckArgument(!isParametric(), this, "for getRecursiveSingletonArgType, this datatype cannot be parametric");
 337   ExprManagerScope ems(d_self);
 338   return d_internal->getRecursiveSingletonArgType(i).toType();
 339 }
 340
 341 bool Datatype::isFinite(Type t) const
 342 {
 343   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 344   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 345   ExprManagerScope ems(d_self);
 346   TypeNode tn = TypeNode::fromType(t);
 347   return d_internal->isFinite(tn);
 348 }
 349 bool Datatype::isFinite() const
 350 {
 351   PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
 352   ExprManagerScope ems(d_self);
 353   return d_internal->isFinite();
 354 }
 355
 356 bool Datatype::isInterpretedFinite(Type t) const
 357 {
 358   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 359   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 360   ExprManagerScope ems(d_self);
 361   TypeNode tn = TypeNode::fromType(t);
 362   return d_internal->isInterpretedFinite(tn);
 363 }
 364 bool Datatype::isInterpretedFinite() const
 365 {
 366   PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
 367   ExprManagerScope ems(d_self);
 368   return d_internal->isInterpretedFinite();
 369 }
 370
 371 bool Datatype::isWellFounded() const
 372 {
 373   ExprManagerScope ems(d_self);
 374   return d_internal->isWellFounded();
 375 }
 376
 377 Expr Datatype::mkGroundTerm(Type t) const
 378 {
 379   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 380   ExprManagerScope ems(d_self);
 381   TypeNode tn = TypeNode::fromType(t);
 382   Node gterm = d_internal->mkGroundTerm(tn);
 383   PrettyCheckArgument(
 384       !gterm.isNull(),
 385       this,
 386       "datatype is not well-founded, cannot construct a ground term!");
 387   return gterm.toExpr();
 388 }
 389
 390 Expr Datatype::mkGroundValue(Type t) const
 391 {
 392   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 393   ExprManagerScope ems(d_self);
 394   TypeNode tn = TypeNode::fromType(t);
 395   Node gvalue = d_internal->mkGroundValue(tn);
 396   PrettyCheckArgument(
 397       !gvalue.isNull(),
 398       this,
 399       "datatype is not well-founded, cannot construct a ground value!");
 400   return gvalue.toExpr();
 401 }
 402
 403 DatatypeType Datatype::getDatatypeType() const
 404 {
 405   PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
 406   ExprManagerScope ems(d_self);
 407   Type self = d_internal->getTypeNode().toType();
 408   PrettyCheckArgument(!self.isNull(), *this);
 409   return DatatypeType(self);
 410 }
 411
 412 DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const
 413 {
 414   PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
 415   ExprManagerScope ems(d_self);
 416   Type self = d_internal->getTypeNode().toType();
 417   PrettyCheckArgument(!self.isNull() && DatatypeType(self).isParametric(),
 418                       this);
 419   return DatatypeType(self).instantiate(params);
 420 }
 421
 422 bool Datatype::operator==(const Datatype& other) const
 423 {
 424   // two datatypes are == iff the name is the same and they have
 425   // exactly matching constructors (in the same order)
 426
 427   if(this == &other) {
 428     return true;
 429   }
 430   return true;
 431 }
 432
 433 const DatatypeConstructor& Datatype::operator[](size_t index) const {
 434   PrettyCheckArgument(index < getNumConstructors(), index, "index out of bounds");
 435   return d_constructors[index];
 436 }
 437
 438 const DatatypeConstructor& Datatype::operator[](std::string name) const {
 439   for(const_iterator i = begin(); i != end(); ++i) {
 440     if((*i).getName() == name) {
 441       return *i;
 442     }
 443   }
 444   std::string dname = getName();
 445   IllegalArgument(name,
 446                   "No such constructor `%s' of datatype `%s'",
 447                   name.c_str(),
 448                   dname.c_str());
 449 }
 450
 451 Expr Datatype::getConstructor(std::string name) const {
 452   return (*this)[name].getConstructor();
 453 }
 454
 455 Type Datatype::getSygusType() const {
 456   return d_internal->getSygusType().toType();
 457 }
 458
 459 Expr Datatype::getSygusVarList() const {
 460   return d_internal->getSygusVarList().toExpr();
 461 }
 462
 463 bool Datatype::getSygusAllowConst() const {
 464   return d_internal->getSygusAllowConst();
 465 }
 466
 467 bool Datatype::getSygusAllowAll() const {
 468   return d_internal->getSygusAllowAll();
 469 }
 470
 471 bool Datatype::involvesExternalType() const{
 472   return d_internal->involvesExternalType();
 473 }
 474
 475 bool Datatype::involvesUninterpretedType() const{
 476   return d_internal->involvesUninterpretedType();
 477 }
 478
 479 const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
 480 {
 481   return &d_constructors;
 482 }
 483
 484 DatatypeConstructor::DatatypeConstructor(std::string name)
 485     : d_internal(nullptr),
 486       d_testerName("is_" + name)  // default tester name is "is_FOO"
 487 {
 488   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 489   d_internal = std::make_shared<DTypeConstructor>(name, 1);
 490 }
 491
 492 DatatypeConstructor::DatatypeConstructor(std::string name,
 493                                          std::string tester,
 494                                          unsigned weight)
 495     : d_internal(nullptr), d_testerName(tester)
 496 {
 497   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 498   PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 499   d_internal = std::make_shared<DTypeConstructor>(name, weight);
 500 }
 501
 502 void DatatypeConstructor::setSygus(Expr op,
 503                                    std::shared_ptr<SygusPrintCallback> spc)
 504 {
 505   PrettyCheckArgument(
 506       !isResolved(), this, "cannot modify a finalized Datatype constructor");
 507   Node opn = Node::fromExpr(op);
 508   d_internal->setSygus(op);
 509   // print callback lives at the expression level currently
 510   d_sygus_pc = spc;
 511 }
 512
 513 const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs()
 514     const
 515 {
 516   return &d_args;
 517 }
 518
 519 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
 520   // We don't want to introduce a new data member, because eventually
 521   // we're going to be a constant stuffed inside a node.  So we stow
 522   // the selector type away inside a var until resolution (when we can
 523   // create the proper selector type)
 524   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 525   PrettyCheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
 526
 527   // we're using some internals, so we have to set up this library context
 528   ExprManagerScope ems(selectorType);
 529
 530   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();
 531   Debug("datatypes") << type << endl;
 532   d_args.push_back(DatatypeConstructorArg(selectorName, type));
 533   d_internal->addArg(d_args.back().d_internal);
 534 }
 535
 536 void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) {
 537   // We don't want to introduce a new data member, because eventually
 538   // we're going to be a constant stuffed inside a node.  So we stow
 539   // the selector type away after a NUL in the name string until
 540   // resolution (when we can create the proper selector type)
 541   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 542   PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
 543   d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
 544   d_internal->addArg(d_args.back().d_internal);
 545 }
 546
 547 void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
 548   // We don't want to introduce a new data member, because eventually
 549   // we're going to be a constant stuffed inside a node.  So we mark
 550   // the name string with a NUL to indicate that we have a
 551   // self-selecting selector until resolution (when we can create the
 552   // proper selector type)
 553   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 554   d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
 555   d_internal->addArg(d_args.back().d_internal);
 556 }
 557
 558 std::string DatatypeConstructor::getName() const
 559 {
 560   return d_internal->getName();
 561 }
 562
 563 std::string DatatypeConstructor::getTesterName() const
 564 {
 565   // not stored internally, since tester names only pertain to parsing
 566   return d_testerName;
 567 }
 568
 569 Expr DatatypeConstructor::getConstructor() const {
 570   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 571   return d_constructor;
 572 }
 573
 574 Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
 575   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 576   PrettyCheckArgument(returnType.isDatatype(), this, "cannot get specialized constructor type for non-datatype type");
 577   ExprManagerScope ems(d_constructor);
 578   TypeNode tn = TypeNode::fromType(returnType);
 579   return d_internal->getSpecializedConstructorType(tn).toType();
 580 }
 581
 582 Expr DatatypeConstructor::getTester() const {
 583   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 584   ExprManagerScope ems(d_constructor);
 585   return d_internal->getTester().toExpr();
 586 }
 587
 588 Expr DatatypeConstructor::getSygusOp() const {
 589   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 590   ExprManagerScope ems(d_constructor);
 591   return d_internal->getSygusOp().toExpr();
 592 }
 593
 594 bool DatatypeConstructor::isSygusIdFunc() const {
 595   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 596   ExprManagerScope ems(d_constructor);
 597   return d_internal->isSygusIdFunc();
 598 }
 599
 600 unsigned DatatypeConstructor::getWeight() const
 601 {
 602   PrettyCheckArgument(
 603       isResolved(), this, "this datatype constructor is not yet resolved");
 604   ExprManagerScope ems(d_constructor);
 605   return d_internal->getWeight();
 606 }
 607
 608 std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
 609 {
 610   PrettyCheckArgument(
 611       isResolved(), this, "this datatype constructor is not yet resolved");
 612   return d_sygus_pc;
 613 }
 614
 615 Cardinality DatatypeConstructor::getCardinality(Type t) const
 616 {
 617   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 618   ExprManagerScope ems(d_constructor);
 619   TypeNode tn = TypeNode::fromType(t);
 620   return d_internal->getCardinality(tn);
 621 }
 622
 623 bool DatatypeConstructor::isFinite(Type t) const
 624 {
 625   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 626   ExprManagerScope ems(d_constructor);
 627   TypeNode tn = TypeNode::fromType(t);
 628   return d_internal->isFinite(tn);
 629 }
 630
 631 bool DatatypeConstructor::isInterpretedFinite(Type t) const
 632 {
 633   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 634   ExprManagerScope ems(d_constructor);
 635   TypeNode tn = TypeNode::fromType(t);
 636   return d_internal->isInterpretedFinite(tn);
 637 }
 638
 639 const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
 640   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
 641   return d_args[index];
 642 }
 643
 644 const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const {
 645   for(const_iterator i = begin(); i != end(); ++i) {
 646     if((*i).getName() == name) {
 647       return *i;
 648     }
 649   }
 650   std::string dname = getName();
 651   IllegalArgument(name,
 652                   "No such arg `%s' of constructor `%s'",
 653                   name.c_str(),
 654                   dname.c_str());
 655 }
 656
 657 Expr DatatypeConstructor::getSelector(std::string name) const {
 658   return (*this)[name].d_selector;
 659 }
 660
 661 Type DatatypeConstructor::getArgType(unsigned index) const
 662 {
 663   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
 664   ExprManagerScope ems(d_constructor);
 665   return d_internal->getArgType(index).toType();
 666 }
 667
 668 bool DatatypeConstructor::involvesExternalType() const{
 669   ExprManagerScope ems(d_constructor);
 670   return d_internal->involvesExternalType();
 671 }
 672
 673 bool DatatypeConstructor::involvesUninterpretedType() const{
 674   ExprManagerScope ems(d_constructor);
 675   return d_internal->involvesUninterpretedType();
 676 }
 677
 678 DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector)
 679     : d_internal(nullptr)
 680 {
 681   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
 682   d_internal = std::make_shared<DTypeSelector>(name, Node::fromExpr(selector));
 683 }
 684
 685 std::string DatatypeConstructorArg::getName() const
 686 {
 687   string name = d_internal->getName();
 688   const size_t nul = name.find('\0');
 689   if(nul != string::npos) {
 690     name.resize(nul);
 691   }
 692   return name;
 693 }
 694
 695 Expr DatatypeConstructorArg::getSelector() const {
 696   PrettyCheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
 697   return d_selector;
 698 }
 699
 700 Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) const {
 701   PrettyCheckArgument(isResolved(), this, "cannot get an internal selector for an unresolved datatype constructor");
 702   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
 703   ExprManagerScope ems(d_constructor);
 704   TypeNode dtn = TypeNode::fromType(domainType);
 705   return d_internal->getSelectorInternal(dtn, index).toExpr();
 706 }
 707
 708 int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const {
 709   PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor");
 710   ExprManagerScope ems(d_constructor);
 711   Node seln = Node::fromExpr(sel);
 712   return d_internal->getSelectorIndexInternal(seln);
 713 }
 714
 715 Expr DatatypeConstructorArg::getConstructor() const {
 716   PrettyCheckArgument(isResolved(), this,
 717                 "cannot get a associated constructor for argument of an unresolved datatype constructor");
 718   ExprManagerScope ems(d_selector);
 719   return d_internal->getConstructor().toExpr();
 720 }
 721
 722 SelectorType DatatypeConstructorArg::getType() const {
 723   return d_selector.getType();
 724 }
 725
 726 Type DatatypeConstructorArg::getRangeType() const {
 727   return getType().getRangeType();
 728 }
 729
 730 bool DatatypeConstructorArg::isUnresolvedSelf() const
 731 {
 732   return d_selector.isNull();
 733 }
 734
 735 bool DatatypeConstructorArg::isResolved() const
 736 {
 737   // We could just write:
 738   //
 739   //   return !d_selector.isNull() && d_selector.getType().isSelector();
 740   //
 741   // HOWEVER, this causes problems in ExprManager tear-down, because
 742   // the attributes are removed before the pool is purged.  When the
 743   // pool is purged, this triggers an equality test between Datatypes,
 744   // and this triggers a call to isResolved(), which breaks because
 745   // d_selector has no type after attributes are stripped.
 746   //
 747   // This problem, coupled with the fact that this function is called
 748   // _often_, means we should just use a boolean flag.
 749   //
 750   return d_internal->isResolved();
 751 }
 752
 753 std::ostream& operator<<(std::ostream& os, const Datatype& dt)
 754 {
 755   // can only output datatypes in the CVC4 native language
 756   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 757   dt.toStream(os);
 758   return os;
 759 }
 760
 761 void Datatype::toStream(std::ostream& out) const
 762 {
 763   out << "DATATYPE " << getName();
 764   if (isParametric())
 765   {
 766     out << '[';
 767     for (size_t i = 0; i < getNumParameters(); ++i)
 768     {
 769       if(i > 0) {
 770         out << ',';
 771       }
 772       out << getParameter(i);
 773     }
 774     out << ']';
 775   }
 776   out << " =" << endl;
 777   Datatype::const_iterator i = begin(), i_end = end();
 778   if(i != i_end) {
 779     out << "  ";
 780     do {
 781       out << *i << endl;
 782       if(++i != i_end) {
 783         out << "| ";
 784       }
 785     } while(i != i_end);
 786   }
 787   out << "END;" << endl;
 788 }
 789
 790 std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
 791   // can only output datatypes in the CVC4 native language
 792   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 793   ctor.toStream(os);
 794   return os;
 795 }
 796
 797 void DatatypeConstructor::toStream(std::ostream& out) const
 798 {
 799   out << getName();
 800
 801   DatatypeConstructor::const_iterator i = begin(), i_end = end();
 802   if(i != i_end) {
 803     out << "(";
 804     do {
 805       out << *i;
 806       if(++i != i_end) {
 807         out << ", ";
 808       }
 809     } while(i != i_end);
 810     out << ")";
 811   }
 812 }
 813
 814 std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
 815   // can only output datatypes in the CVC4 native language
 816   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 817   arg.toStream(os);
 818   return os;
 819 }
 820
 821 void DatatypeConstructorArg::toStream(std::ostream& out) const
 822 {
 823   std::string name = getName();
 824   out << name << ": ";
 825
 826   Type t;
 827   if (isResolved())
 828   {
 829     t = getRangeType();
 830   }
 831   else if (d_selector.isNull())
 832   {
 833     string typeName = name.substr(name.find('\0') + 1);
 834     out << ((typeName == "") ? "[self]" : typeName);
 835     return;
 836   }
 837   else
 838   {
 839     t = d_selector.getType();
 840   }
 841   out << t;
 842 }
 843
 844 DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) : d_index(index) {}
 845 std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
 846   return out << "index_" << dic.getIndex();
 847 }
 848
 849
 850 std::string Datatype::getName() const
 851 {
 852   ExprManagerScope ems(*d_em);
 853   return d_internal->getName();
 854 }
 855 size_t Datatype::getNumConstructors() const { return d_constructors.size(); }
 856
 857 bool Datatype::isParametric() const
 858 {
 859   ExprManagerScope ems(*d_em);
 860   return d_internal->isParametric();
 861 }
 862 size_t Datatype::getNumParameters() const
 863 {
 864   ExprManagerScope ems(*d_em);
 865   return d_internal->getNumParameters();
 866 }
 867 Type Datatype::getParameter(unsigned int i) const
 868 {
 869   CheckArgument(isParametric(),
 870                 this,
 871                 "Cannot get type parameter of a non-parametric datatype.");
 872   CheckArgument(i < getNumParameters(),
 873                 i,
 874                 "Type parameter index out of range for datatype.");
 875   ExprManagerScope ems(*d_em);
 876   return d_internal->getParameter(i).toType();
 877 }
 878
 879 std::vector<Type> Datatype::getParameters() const
 880 {
 881   CheckArgument(isParametric(),
 882                 this,
 883                 "Cannot get type parameters of a non-parametric datatype.");
 884   std::vector<Type> params;
 885   std::vector<TypeNode> paramsn = d_internal->getParameters();
 886   // convert to type
 887   for (unsigned i = 0, nparams = paramsn.size(); i < nparams; i++)
 888   {
 889     params.push_back(paramsn[i].toType());
 890   }
 891   return params;
 892 }
 893
 894 bool Datatype::isCodatatype() const
 895 {
 896   ExprManagerScope ems(*d_em);
 897   return d_internal->isCodatatype();
 898 }
 899
 900 bool Datatype::isSygus() const
 901 {
 902   ExprManagerScope ems(*d_em);
 903   return d_internal->isSygus();
 904 }
 905
 906 bool Datatype::isTuple() const
 907 {
 908   ExprManagerScope ems(*d_em);
 909   return d_internal->isTuple();
 910 }
 911
 912 bool Datatype::isRecord() const { return d_isRecord; }
 913
 914 Record* Datatype::getRecord() const { return d_record; }
 915 bool Datatype::operator!=(const Datatype& other) const
 916 {
 917   return !(*this == other);
 918 }
 919
 920 bool Datatype::isResolved() const
 921 {
 922   ExprManagerScope ems(*d_em);
 923   return d_internal->isResolved();
 924 }
 925 Datatype::iterator Datatype::begin() { return iterator(d_constructors, true); }
 926
 927 Datatype::iterator Datatype::end() { return iterator(d_constructors, false); }
 928
 929 Datatype::const_iterator Datatype::begin() const
 930 {
 931   return const_iterator(d_constructors, true);
 932 }
 933
 934 Datatype::const_iterator Datatype::end() const
 935 {
 936   return const_iterator(d_constructors, false);
 937 }
 938
 939 bool DatatypeConstructor::isResolved() const
 940 {
 941   return d_internal->isResolved();
 942 }
 943
 944 size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); }
 945
 946 DatatypeConstructor::iterator DatatypeConstructor::begin()
 947 {
 948   return iterator(d_args, true);
 949 }
 950
 951 DatatypeConstructor::iterator DatatypeConstructor::end()
 952 {
 953   return iterator(d_args, false);
 954 }
 955
 956 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
 957 {
 958   return const_iterator(d_args, true);
 959 }
 960
 961 DatatypeConstructor::const_iterator DatatypeConstructor::end() const
 962 {
 963   return const_iterator(d_args, false);
 964 }
 965 }/* CVC4 namespace */