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::setTuple() {
 257   PrettyCheckArgument(
 258       !isResolved(), this, "cannot set tuple to a finalized Datatype");
 259   d_internal->setTuple();
 260 }
 261
 262 void Datatype::setRecord() {
 263   PrettyCheckArgument(
 264       !isResolved(), this, "cannot set record to a finalized Datatype");
 265   d_isRecord = true;
 266 }
 267
 268 Cardinality Datatype::getCardinality(Type t) const
 269 {
 270   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 271   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 272   ExprManagerScope ems(d_self);
 273   TypeNode tn = TypeNode::fromType(t);
 274   return d_internal->getCardinality(tn);
 275 }
 276
 277 Cardinality Datatype::getCardinality() const
 278 {
 279   PrettyCheckArgument(!isParametric(), this, "for getCardinality, this datatype cannot be parametric");
 280   ExprManagerScope ems(d_self);
 281   return d_internal->getCardinality();
 282 }
 283
 284 bool Datatype::isRecursiveSingleton(Type t) const
 285 {
 286   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 287   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 288   ExprManagerScope ems(d_self);
 289   TypeNode tn = TypeNode::fromType(t);
 290   return d_internal->isRecursiveSingleton(tn);
 291 }
 292
 293 bool Datatype::isRecursiveSingleton() const
 294 {
 295   PrettyCheckArgument(!isParametric(), this, "for isRecursiveSingleton, this datatype cannot be parametric");
 296   ExprManagerScope ems(d_self);
 297   return d_internal->isRecursiveSingleton();
 298 }
 299
 300 unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const
 301 {
 302   Assert(isRecursiveSingleton(t));
 303   ExprManagerScope ems(d_self);
 304   TypeNode tn = TypeNode::fromType(t);
 305   return d_internal->getNumRecursiveSingletonArgTypes(tn);
 306 }
 307
 308 unsigned Datatype::getNumRecursiveSingletonArgTypes() const
 309 {
 310   PrettyCheckArgument(!isParametric(), this, "for getNumRecursiveSingletonArgTypes, this datatype cannot be parametric");
 311   ExprManagerScope ems(d_self);
 312   return d_internal->getNumRecursiveSingletonArgTypes();
 313 }
 314
 315 Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const
 316 {
 317   Assert(isRecursiveSingleton(t));
 318   ExprManagerScope ems(d_self);
 319   TypeNode tn = TypeNode::fromType(t);
 320   return d_internal->getRecursiveSingletonArgType(tn, i).toType();
 321 }
 322
 323 Type Datatype::getRecursiveSingletonArgType(unsigned i) const
 324 {
 325   PrettyCheckArgument(!isParametric(), this, "for getRecursiveSingletonArgType, this datatype cannot be parametric");
 326   ExprManagerScope ems(d_self);
 327   return d_internal->getRecursiveSingletonArgType(i).toType();
 328 }
 329
 330 bool Datatype::isFinite(Type t) const
 331 {
 332   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 333   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 334   ExprManagerScope ems(d_self);
 335   TypeNode tn = TypeNode::fromType(t);
 336   return d_internal->isFinite(tn);
 337 }
 338 bool Datatype::isFinite() const
 339 {
 340   PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
 341   ExprManagerScope ems(d_self);
 342   return d_internal->isFinite();
 343 }
 344
 345 bool Datatype::isInterpretedFinite(Type t) const
 346 {
 347   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 348   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 349   ExprManagerScope ems(d_self);
 350   TypeNode tn = TypeNode::fromType(t);
 351   return d_internal->isInterpretedFinite(tn);
 352 }
 353 bool Datatype::isInterpretedFinite() const
 354 {
 355   PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
 356   ExprManagerScope ems(d_self);
 357   return d_internal->isInterpretedFinite();
 358 }
 359
 360 bool Datatype::isWellFounded() const
 361 {
 362   ExprManagerScope ems(d_self);
 363   return d_internal->isWellFounded();
 364 }
 365
 366 Expr Datatype::mkGroundTerm(Type t) const
 367 {
 368   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 369   ExprManagerScope ems(d_self);
 370   TypeNode tn = TypeNode::fromType(t);
 371   Node gterm = d_internal->mkGroundTerm(tn);
 372   PrettyCheckArgument(
 373       !gterm.isNull(),
 374       this,
 375       "datatype is not well-founded, cannot construct a ground term!");
 376   return gterm.toExpr();
 377 }
 378
 379 Expr Datatype::mkGroundValue(Type t) const
 380 {
 381   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 382   ExprManagerScope ems(d_self);
 383   TypeNode tn = TypeNode::fromType(t);
 384   Node gvalue = d_internal->mkGroundValue(tn);
 385   PrettyCheckArgument(
 386       !gvalue.isNull(),
 387       this,
 388       "datatype is not well-founded, cannot construct a ground value!");
 389   return gvalue.toExpr();
 390 }
 391
 392 DatatypeType Datatype::getDatatypeType() const
 393 {
 394   PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
 395   ExprManagerScope ems(d_self);
 396   Type self = d_internal->getTypeNode().toType();
 397   PrettyCheckArgument(!self.isNull(), *this);
 398   return DatatypeType(self);
 399 }
 400
 401 DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const
 402 {
 403   PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
 404   ExprManagerScope ems(d_self);
 405   Type self = d_internal->getTypeNode().toType();
 406   PrettyCheckArgument(!self.isNull() && DatatypeType(self).isParametric(),
 407                       this);
 408   return DatatypeType(self).instantiate(params);
 409 }
 410
 411 bool Datatype::operator==(const Datatype& other) const
 412 {
 413   // two datatypes are == iff the name is the same and they have
 414   // exactly matching constructors (in the same order)
 415
 416   if(this == &other) {
 417     return true;
 418   }
 419   return true;
 420 }
 421
 422 const DatatypeConstructor& Datatype::operator[](size_t index) const {
 423   PrettyCheckArgument(index < getNumConstructors(), index, "index out of bounds");
 424   return d_constructors[index];
 425 }
 426
 427 const DatatypeConstructor& Datatype::operator[](std::string name) const {
 428   for(const_iterator i = begin(); i != end(); ++i) {
 429     if((*i).getName() == name) {
 430       return *i;
 431     }
 432   }
 433   std::string dname = getName();
 434   IllegalArgument(name,
 435                   "No such constructor `%s' of datatype `%s'",
 436                   name.c_str(),
 437                   dname.c_str());
 438 }
 439
 440 Expr Datatype::getConstructor(std::string name) const {
 441   return (*this)[name].getConstructor();
 442 }
 443
 444 Type Datatype::getSygusType() const {
 445   return d_internal->getSygusType().toType();
 446 }
 447
 448 Expr Datatype::getSygusVarList() const {
 449   return d_internal->getSygusVarList().toExpr();
 450 }
 451
 452 bool Datatype::getSygusAllowConst() const {
 453   return d_internal->getSygusAllowConst();
 454 }
 455
 456 bool Datatype::getSygusAllowAll() const {
 457   return d_internal->getSygusAllowAll();
 458 }
 459
 460 bool Datatype::involvesExternalType() const{
 461   return d_internal->involvesExternalType();
 462 }
 463
 464 bool Datatype::involvesUninterpretedType() const{
 465   return d_internal->involvesUninterpretedType();
 466 }
 467
 468 const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
 469 {
 470   return &d_constructors;
 471 }
 472
 473 DatatypeConstructor::DatatypeConstructor(std::string name)
 474     : d_internal(nullptr),
 475       d_testerName("is_" + name)  // default tester name is "is_FOO"
 476 {
 477   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 478   d_internal = std::make_shared<DTypeConstructor>(name, 1);
 479 }
 480
 481 DatatypeConstructor::DatatypeConstructor(std::string name,
 482                                          std::string tester,
 483                                          unsigned weight)
 484     : d_internal(nullptr), d_testerName(tester)
 485 {
 486   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 487   PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 488   d_internal = std::make_shared<DTypeConstructor>(name, weight);
 489 }
 490
 491 void DatatypeConstructor::setSygus(Expr op,
 492                                    std::shared_ptr<SygusPrintCallback> spc)
 493 {
 494   PrettyCheckArgument(
 495       !isResolved(), this, "cannot modify a finalized Datatype constructor");
 496   Node opn = Node::fromExpr(op);
 497   d_internal->setSygus(op);
 498   // print callback lives at the expression level currently
 499   d_sygus_pc = spc;
 500 }
 501
 502 const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs()
 503     const
 504 {
 505   return &d_args;
 506 }
 507
 508 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
 509   // We don't want to introduce a new data member, because eventually
 510   // we're going to be a constant stuffed inside a node.  So we stow
 511   // the selector type away inside a var until resolution (when we can
 512   // create the proper selector type)
 513   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 514   PrettyCheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
 515
 516   // we're using some internals, so we have to set up this library context
 517   ExprManagerScope ems(selectorType);
 518
 519   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();
 520   Debug("datatypes") << type << endl;
 521   d_args.push_back(DatatypeConstructorArg(selectorName, type));
 522   d_internal->addArg(d_args.back().d_internal);
 523 }
 524
 525 void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) {
 526   // We don't want to introduce a new data member, because eventually
 527   // we're going to be a constant stuffed inside a node.  So we stow
 528   // the selector type away after a NUL in the name string until
 529   // resolution (when we can create the proper selector type)
 530   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 531   PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
 532   d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
 533   d_internal->addArg(d_args.back().d_internal);
 534 }
 535
 536 void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
 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 mark
 539   // the name string with a NUL to indicate that we have a
 540   // self-selecting selector until resolution (when we can create the
 541   // proper selector type)
 542   PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
 543   d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
 544   d_internal->addArg(d_args.back().d_internal);
 545 }
 546
 547 std::string DatatypeConstructor::getName() const
 548 {
 549   return d_internal->getName();
 550 }
 551
 552 std::string DatatypeConstructor::getTesterName() const
 553 {
 554   // not stored internally, since tester names only pertain to parsing
 555   return d_testerName;
 556 }
 557
 558 Expr DatatypeConstructor::getConstructor() const {
 559   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 560   return d_constructor;
 561 }
 562
 563 Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
 564   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 565   PrettyCheckArgument(returnType.isDatatype(), this, "cannot get specialized constructor type for non-datatype type");
 566   ExprManagerScope ems(d_constructor);
 567   TypeNode tn = TypeNode::fromType(returnType);
 568   return d_internal->getSpecializedConstructorType(tn).toType();
 569 }
 570
 571 Expr DatatypeConstructor::getTester() const {
 572   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 573   ExprManagerScope ems(d_constructor);
 574   return d_internal->getTester().toExpr();
 575 }
 576
 577 Expr DatatypeConstructor::getSygusOp() const {
 578   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 579   ExprManagerScope ems(d_constructor);
 580   return d_internal->getSygusOp().toExpr();
 581 }
 582
 583 bool DatatypeConstructor::isSygusIdFunc() const {
 584   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 585   ExprManagerScope ems(d_constructor);
 586   return d_internal->isSygusIdFunc();
 587 }
 588
 589 unsigned DatatypeConstructor::getWeight() const
 590 {
 591   PrettyCheckArgument(
 592       isResolved(), this, "this datatype constructor is not yet resolved");
 593   ExprManagerScope ems(d_constructor);
 594   return d_internal->getWeight();
 595 }
 596
 597 std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
 598 {
 599   PrettyCheckArgument(
 600       isResolved(), this, "this datatype constructor is not yet resolved");
 601   return d_sygus_pc;
 602 }
 603
 604 Cardinality DatatypeConstructor::getCardinality(Type t) const
 605 {
 606   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 607   ExprManagerScope ems(d_constructor);
 608   TypeNode tn = TypeNode::fromType(t);
 609   return d_internal->getCardinality(tn);
 610 }
 611
 612 bool DatatypeConstructor::isFinite(Type t) const
 613 {
 614   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 615   ExprManagerScope ems(d_constructor);
 616   TypeNode tn = TypeNode::fromType(t);
 617   return d_internal->isFinite(tn);
 618 }
 619
 620 bool DatatypeConstructor::isInterpretedFinite(Type t) const
 621 {
 622   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 623   ExprManagerScope ems(d_constructor);
 624   TypeNode tn = TypeNode::fromType(t);
 625   return d_internal->isInterpretedFinite(tn);
 626 }
 627
 628 const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
 629   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
 630   return d_args[index];
 631 }
 632
 633 const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const {
 634   for(const_iterator i = begin(); i != end(); ++i) {
 635     if((*i).getName() == name) {
 636       return *i;
 637     }
 638   }
 639   std::string dname = getName();
 640   IllegalArgument(name,
 641                   "No such arg `%s' of constructor `%s'",
 642                   name.c_str(),
 643                   dname.c_str());
 644 }
 645
 646 Expr DatatypeConstructor::getSelector(std::string name) const {
 647   return (*this)[name].d_selector;
 648 }
 649
 650 Type DatatypeConstructor::getArgType(unsigned index) const
 651 {
 652   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
 653   ExprManagerScope ems(d_constructor);
 654   return d_internal->getArgType(index).toType();
 655 }
 656
 657 bool DatatypeConstructor::involvesExternalType() const{
 658   ExprManagerScope ems(d_constructor);
 659   return d_internal->involvesExternalType();
 660 }
 661
 662 bool DatatypeConstructor::involvesUninterpretedType() const{
 663   ExprManagerScope ems(d_constructor);
 664   return d_internal->involvesUninterpretedType();
 665 }
 666
 667 DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector)
 668     : d_internal(nullptr)
 669 {
 670   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
 671   d_internal = std::make_shared<DTypeSelector>(name, Node::fromExpr(selector));
 672 }
 673
 674 std::string DatatypeConstructorArg::getName() const
 675 {
 676   string name = d_internal->getName();
 677   const size_t nul = name.find('\0');
 678   if(nul != string::npos) {
 679     name.resize(nul);
 680   }
 681   return name;
 682 }
 683
 684 Expr DatatypeConstructorArg::getSelector() const {
 685   PrettyCheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
 686   return d_selector;
 687 }
 688
 689 Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) const {
 690   PrettyCheckArgument(isResolved(), this, "cannot get an internal selector for an unresolved datatype constructor");
 691   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
 692   ExprManagerScope ems(d_constructor);
 693   TypeNode dtn = TypeNode::fromType(domainType);
 694   return d_internal->getSelectorInternal(dtn, index).toExpr();
 695 }
 696
 697 int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const {
 698   PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor");
 699   ExprManagerScope ems(d_constructor);
 700   Node seln = Node::fromExpr(sel);
 701   return d_internal->getSelectorIndexInternal(seln);
 702 }
 703
 704 Expr DatatypeConstructorArg::getConstructor() const {
 705   PrettyCheckArgument(isResolved(), this,
 706                 "cannot get a associated constructor for argument of an unresolved datatype constructor");
 707   ExprManagerScope ems(d_selector);
 708   return d_internal->getConstructor().toExpr();
 709 }
 710
 711 SelectorType DatatypeConstructorArg::getType() const {
 712   return d_selector.getType();
 713 }
 714
 715 Type DatatypeConstructorArg::getRangeType() const {
 716   return getType().getRangeType();
 717 }
 718
 719 bool DatatypeConstructorArg::isUnresolvedSelf() const
 720 {
 721   return d_selector.isNull();
 722 }
 723
 724 bool DatatypeConstructorArg::isResolved() const
 725 {
 726   // We could just write:
 727   //
 728   //   return !d_selector.isNull() && d_selector.getType().isSelector();
 729   //
 730   // HOWEVER, this causes problems in ExprManager tear-down, because
 731   // the attributes are removed before the pool is purged.  When the
 732   // pool is purged, this triggers an equality test between Datatypes,
 733   // and this triggers a call to isResolved(), which breaks because
 734   // d_selector has no type after attributes are stripped.
 735   //
 736   // This problem, coupled with the fact that this function is called
 737   // _often_, means we should just use a boolean flag.
 738   //
 739   return d_internal->isResolved();
 740 }
 741
 742 std::ostream& operator<<(std::ostream& os, const Datatype& dt)
 743 {
 744   // can only output datatypes in the CVC4 native language
 745   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 746   dt.toStream(os);
 747   return os;
 748 }
 749
 750 void Datatype::toStream(std::ostream& out) const
 751 {
 752   out << "DATATYPE " << getName();
 753   if (isParametric())
 754   {
 755     out << '[';
 756     for (size_t i = 0; i < getNumParameters(); ++i)
 757     {
 758       if(i > 0) {
 759         out << ',';
 760       }
 761       out << getParameter(i);
 762     }
 763     out << ']';
 764   }
 765   out << " =" << endl;
 766   Datatype::const_iterator i = begin(), i_end = end();
 767   if(i != i_end) {
 768     out << "  ";
 769     do {
 770       out << *i << endl;
 771       if(++i != i_end) {
 772         out << "| ";
 773       }
 774     } while(i != i_end);
 775   }
 776   out << "END;" << endl;
 777 }
 778
 779 std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
 780   // can only output datatypes in the CVC4 native language
 781   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 782   ctor.toStream(os);
 783   return os;
 784 }
 785
 786 void DatatypeConstructor::toStream(std::ostream& out) const
 787 {
 788   out << getName();
 789
 790   DatatypeConstructor::const_iterator i = begin(), i_end = end();
 791   if(i != i_end) {
 792     out << "(";
 793     do {
 794       out << *i;
 795       if(++i != i_end) {
 796         out << ", ";
 797       }
 798     } while(i != i_end);
 799     out << ")";
 800   }
 801 }
 802
 803 std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
 804   // can only output datatypes in the CVC4 native language
 805   language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 806   arg.toStream(os);
 807   return os;
 808 }
 809
 810 void DatatypeConstructorArg::toStream(std::ostream& out) const
 811 {
 812   std::string name = getName();
 813   out << name << ": ";
 814
 815   Type t;
 816   if (isResolved())
 817   {
 818     t = getRangeType();
 819   }
 820   else if (d_selector.isNull())
 821   {
 822     string typeName = name.substr(name.find('\0') + 1);
 823     out << ((typeName == "") ? "[self]" : typeName);
 824     return;
 825   }
 826   else
 827   {
 828     t = d_selector.getType();
 829   }
 830   out << t;
 831 }
 832
 833 DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) : d_index(index) {}
 834 std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
 835   return out << "index_" << dic.getIndex();
 836 }
 837
 838
 839 std::string Datatype::getName() const
 840 {
 841   ExprManagerScope ems(*d_em);
 842   return d_internal->getName();
 843 }
 844 size_t Datatype::getNumConstructors() const { return d_constructors.size(); }
 845
 846 bool Datatype::isParametric() const
 847 {
 848   ExprManagerScope ems(*d_em);
 849   return d_internal->isParametric();
 850 }
 851 size_t Datatype::getNumParameters() const
 852 {
 853   ExprManagerScope ems(*d_em);
 854   return d_internal->getNumParameters();
 855 }
 856 Type Datatype::getParameter(unsigned int i) const
 857 {
 858   CheckArgument(isParametric(),
 859                 this,
 860                 "Cannot get type parameter of a non-parametric datatype.");
 861   CheckArgument(i < getNumParameters(),
 862                 i,
 863                 "Type parameter index out of range for datatype.");
 864   ExprManagerScope ems(*d_em);
 865   return d_internal->getParameter(i).toType();
 866 }
 867
 868 std::vector<Type> Datatype::getParameters() const
 869 {
 870   CheckArgument(isParametric(),
 871                 this,
 872                 "Cannot get type parameters of a non-parametric datatype.");
 873   std::vector<Type> params;
 874   std::vector<TypeNode> paramsn = d_internal->getParameters();
 875   // convert to type
 876   for (unsigned i = 0, nparams = paramsn.size(); i < nparams; i++)
 877   {
 878     params.push_back(paramsn[i].toType());
 879   }
 880   return params;
 881 }
 882
 883 bool Datatype::isCodatatype() const
 884 {
 885   ExprManagerScope ems(*d_em);
 886   return d_internal->isCodatatype();
 887 }
 888
 889 bool Datatype::isSygus() const
 890 {
 891   ExprManagerScope ems(*d_em);
 892   return d_internal->isSygus();
 893 }
 894
 895 bool Datatype::isTuple() const
 896 {
 897   ExprManagerScope ems(*d_em);
 898   return d_internal->isTuple();
 899 }
 900
 901 bool Datatype::isRecord() const { return d_isRecord; }
 902
 903 Record* Datatype::getRecord() const { return d_record; }
 904 bool Datatype::operator!=(const Datatype& other) const
 905 {
 906   return !(*this == other);
 907 }
 908
 909 bool Datatype::isResolved() const
 910 {
 911   ExprManagerScope ems(*d_em);
 912   return d_internal->isResolved();
 913 }
 914 Datatype::iterator Datatype::begin() { return iterator(d_constructors, true); }
 915
 916 Datatype::iterator Datatype::end() { return iterator(d_constructors, false); }
 917
 918 Datatype::const_iterator Datatype::begin() const
 919 {
 920   return const_iterator(d_constructors, true);
 921 }
 922
 923 Datatype::const_iterator Datatype::end() const
 924 {
 925   return const_iterator(d_constructors, false);
 926 }
 927
 928 bool DatatypeConstructor::isResolved() const
 929 {
 930   return d_internal->isResolved();
 931 }
 932
 933 size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); }
 934
 935 DatatypeConstructor::iterator DatatypeConstructor::begin()
 936 {
 937   return iterator(d_args, true);
 938 }
 939
 940 DatatypeConstructor::iterator DatatypeConstructor::end()
 941 {
 942   return iterator(d_args, false);
 943 }
 944
 945 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
 946 {
 947   return const_iterator(d_args, true);
 948 }
 949
 950 DatatypeConstructor::const_iterator DatatypeConstructor::end() const
 951 {
 952   return const_iterator(d_args, false);
 953 }
 954 }/* CVC4 namespace */