src/expr/expr_manager_template.cpp

   1 /*********************                                                        */
   2 /*! \file expr_manager_template.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Dejan Jovanovic, Christopher L. Conway
   6  ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Public-facing expression manager interface, implementation
  13  **
  14  ** Public-facing expression manager interface, implementation.
  15  **/
  16
  17 #include "expr/node_manager.h"
  18 #include "expr/expr_manager.h"
  19 #include "expr/variable_type_map.h"
  20 #include "context/context.h"
  21 #include "options/options.h"
  22 #include "util/statistics_registry.h"
  23
  24 #include <map>
  25
  26 ${includes}
  27
  28 // This is a hack, but an important one: if there's an error, the
  29 // compiler directs the user to the template file instead of the
  30 // generated one.  We don't want the user to modify the generated one,
  31 // since it'll get overwritten on a later build.
  32 #line 33 "${template}"
  33
  34 #ifdef CVC4_STATISTICS_ON
  35   #define INC_STAT(kind) \
  36   { \
  37     if (d_exprStatistics[kind] == NULL) { \
  38       stringstream statName; \
  39       statName << "expr::ExprManager::" << kind; \
  40       d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
  41       d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \
  42     } \
  43     ++ *(d_exprStatistics[kind]); \
  44   }
  45   #define INC_STAT_VAR(type, bound_var) \
  46   { \
  47     TypeNode* typeNode = Type::getTypeNode(type); \
  48     TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \
  49     if (d_exprStatisticsVars[type] == NULL) { \
  50       stringstream statName; \
  51       if (type == LAST_TYPE) { \
  52         statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \
  53       } else { \
  54         statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
  55       } \
  56       d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
  57       d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
  58     } \
  59     ++ *(d_exprStatisticsVars[type]); \
  60   }
  61 #else
  62   #define INC_STAT(kind)
  63   #define INC_STAT_VAR(type, bound_var)
  64 #endif
  65
  66 using namespace std;
  67 using namespace CVC4::context;
  68 using namespace CVC4::kind;
  69
  70 namespace CVC4 {
  71
  72 ExprManager::ExprManager() :
  73   d_ctxt(new Context()),
  74   d_nodeManager(new NodeManager(d_ctxt, this)) {
  75 #ifdef CVC4_STATISTICS_ON
  76   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
  77     d_exprStatistics[i] = NULL;
  78   }
  79   for (unsigned i = 0; i < LAST_TYPE; ++ i) {
  80     d_exprStatisticsVars[i] = NULL;
  81   }
  82 #endif
  83 }
  84
  85 ExprManager::ExprManager(const Options& options) :
  86   d_ctxt(new Context()),
  87   d_nodeManager(new NodeManager(d_ctxt, this, options)) {
  88 #ifdef CVC4_STATISTICS_ON
  89   for (unsigned i = 0; i < LAST_TYPE; ++ i) {
  90     d_exprStatisticsVars[i] = NULL;
  91   }
  92   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
  93     d_exprStatistics[i] = NULL;
  94   }
  95 #endif
  96 }
  97
  98 ExprManager::~ExprManager() throw() {
  99   NodeManagerScope nms(d_nodeManager);
 100
 101   try {
 102
 103 #ifdef CVC4_STATISTICS_ON
 104     for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
 105       if (d_exprStatistics[i] != NULL) {
 106         d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]);
 107         delete d_exprStatistics[i];
 108       }
 109     }
 110     for (unsigned i = 0; i < LAST_TYPE; ++ i) {
 111       if (d_exprStatisticsVars[i] != NULL) {
 112         d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]);
 113         delete d_exprStatisticsVars[i];
 114       }
 115     }
 116 #endif
 117
 118     delete d_nodeManager;
 119     delete d_ctxt;
 120
 121   } catch(Exception& e) {
 122     Warning() << "CVC4 threw an exception during cleanup." << std::endl
 123               << e << std::endl;
 124   }
 125 }
 126
 127 StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() {
 128   return d_nodeManager->getStatisticsRegistry();
 129 }
 130
 131 const Options& ExprManager::getOptions() const {
 132   return d_nodeManager->getOptions();
 133 }
 134
 135 BooleanType ExprManager::booleanType() const {
 136   NodeManagerScope nms(d_nodeManager);
 137   return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
 138 }
 139
 140 StringType ExprManager::stringType() const {
 141   NodeManagerScope nms(d_nodeManager);
 142   return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
 143 }
 144
 145 RealType ExprManager::realType() const {
 146   NodeManagerScope nms(d_nodeManager);
 147   return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));
 148 }
 149
 150 IntegerType ExprManager::integerType() const {
 151   NodeManagerScope nms(d_nodeManager);
 152   return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())));
 153 }
 154
 155 Expr ExprManager::mkExpr(Kind kind, Expr child1) {
 156   const unsigned n = 1 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
 157   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 158                 "Exprs with kind %s must have at least %u children and "
 159                 "at most %u children (the one under construction has %u)",
 160                 kind::kindToString(kind).c_str(),
 161                 minArity(kind), maxArity(kind), n);
 162   NodeManagerScope nms(d_nodeManager);
 163   try {
 164     INC_STAT(kind);
 165     return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
 166   } catch (const TypeCheckingExceptionPrivate& e) {
 167     throw TypeCheckingException(this, &e);
 168   }
 169 }
 170
 171 Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
 172   const unsigned n = 2 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
 173   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 174                 "Exprs with kind %s must have at least %u children and "
 175                 "at most %u children (the one under construction has %u)",
 176                 kind::kindToString(kind).c_str(),
 177                 minArity(kind), maxArity(kind), n);
 178   NodeManagerScope nms(d_nodeManager);
 179   try {
 180     INC_STAT(kind);
 181     return Expr(this, d_nodeManager->mkNodePtr(kind,
 182                                                child1.getNode(),
 183                                                child2.getNode()));
 184   } catch (const TypeCheckingExceptionPrivate& e) {
 185     throw TypeCheckingException(this, &e);
 186   }
 187 }
 188
 189 Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
 190                          Expr child3) {
 191   const unsigned n = 3 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
 192   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 193                 "Exprs with kind %s must have at least %u children and "
 194                 "at most %u children (the one under construction has %u)",
 195                 kind::kindToString(kind).c_str(),
 196                 minArity(kind), maxArity(kind), n);
 197   NodeManagerScope nms(d_nodeManager);
 198   try {
 199     INC_STAT(kind);
 200     return Expr(this, d_nodeManager->mkNodePtr(kind,
 201                                                child1.getNode(),
 202                                                child2.getNode(),
 203                                                child3.getNode()));
 204   } catch (const TypeCheckingExceptionPrivate& e) {
 205     throw TypeCheckingException(this, &e);
 206   }
 207 }
 208
 209 Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
 210                          Expr child3, Expr child4) {
 211   const unsigned n = 4 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
 212   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 213                 "Exprs with kind %s must have at least %u children and "
 214                 "at most %u children (the one under construction has %u)",
 215                 kind::kindToString(kind).c_str(),
 216                 minArity(kind), maxArity(kind), n);
 217   NodeManagerScope nms(d_nodeManager);
 218   try {
 219     INC_STAT(kind);
 220     return Expr(this, d_nodeManager->mkNodePtr(kind,
 221                                                child1.getNode(),
 222                                                child2.getNode(),
 223                                                child3.getNode(),
 224                                                child4.getNode()));
 225   } catch (const TypeCheckingExceptionPrivate& e) {
 226     throw TypeCheckingException(this, &e);
 227   }
 228 }
 229
 230 Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
 231                          Expr child3, Expr child4,
 232                          Expr child5) {
 233   const unsigned n = 5 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
 234   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 235                 "Exprs with kind %s must have at least %u children and "
 236                 "at most %u children (the one under construction has %u)",
 237                 kind::kindToString(kind).c_str(),
 238                 minArity(kind), maxArity(kind), n);
 239   NodeManagerScope nms(d_nodeManager);
 240   try {
 241     INC_STAT(kind);
 242     return Expr(this, d_nodeManager->mkNodePtr(kind,
 243                                                child1.getNode(),
 244                                                child2.getNode(),
 245                                                child3.getNode(),
 246                                                child4.getNode(),
 247                                                child5.getNode()));
 248   } catch (const TypeCheckingExceptionPrivate& e) {
 249     throw TypeCheckingException(this, &e);
 250   }
 251 }
 252
 253 Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
 254   const unsigned n = children.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
 255   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 256                 "Exprs with kind %s must have at least %u children and "
 257                 "at most %u children (the one under construction has %u)",
 258                 kind::kindToString(kind).c_str(),
 259                 minArity(kind), maxArity(kind), n);
 260
 261   NodeManagerScope nms(d_nodeManager);
 262
 263   vector<Node> nodes;
 264   vector<Expr>::const_iterator it = children.begin();
 265   vector<Expr>::const_iterator it_end = children.end();
 266   while(it != it_end) {
 267     nodes.push_back(it->getNode());
 268     ++it;
 269   }
 270   try {
 271     INC_STAT(kind);
 272     return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
 273   } catch (const TypeCheckingExceptionPrivate& e) {
 274     throw TypeCheckingException(this, &e);
 275   }
 276 }
 277
 278 Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren) {
 279   const unsigned n = otherChildren.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
 280   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 281                 "Exprs with kind %s must have at least %u children and "
 282                 "at most %u children (the one under construction has %u)",
 283                 kind::kindToString(kind).c_str(),
 284                 minArity(kind), maxArity(kind), n);
 285
 286   NodeManagerScope nms(d_nodeManager);
 287
 288   vector<Node> nodes;
 289   nodes.push_back(child1.getNode());
 290
 291   vector<Expr>::const_iterator it = otherChildren.begin();
 292   vector<Expr>::const_iterator it_end = otherChildren.end();
 293   while(it != it_end) {
 294     nodes.push_back(it->getNode());
 295     ++it;
 296   }
 297   try {
 298     INC_STAT(kind);
 299     return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
 300   } catch (const TypeCheckingExceptionPrivate& e) {
 301     throw TypeCheckingException(this, &e);
 302   }
 303 }
 304
 305 Expr ExprManager::mkExpr(Expr opExpr) {
 306   const unsigned n = 0;
 307   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
 308   CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
 309                 "This Expr constructor is for parameterized kinds only");
 310   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 311                 "Exprs with kind %s must have at least %u children and "
 312                 "at most %u children (the one under construction has %u)",
 313                 kind::kindToString(kind).c_str(),
 314                 minArity(kind), maxArity(kind), n);
 315   NodeManagerScope nms(d_nodeManager);
 316   try {
 317     INC_STAT(kind);
 318     return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode()));
 319   } catch (const TypeCheckingExceptionPrivate& e) {
 320     throw TypeCheckingException(this, &e);
 321   }
 322 }
 323
 324 Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
 325   const unsigned n = 1;
 326   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
 327   CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
 328                 "This Expr constructor is for parameterized kinds only");
 329   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 330                 "Exprs with kind %s must have at least %u children and "
 331                 "at most %u children (the one under construction has %u)",
 332                 kind::kindToString(kind).c_str(),
 333                 minArity(kind), maxArity(kind), n);
 334   NodeManagerScope nms(d_nodeManager);
 335   try {
 336     INC_STAT(kind);
 337     return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode()));
 338   } catch (const TypeCheckingExceptionPrivate& e) {
 339     throw TypeCheckingException(this, &e);
 340   }
 341 }
 342
 343 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
 344   const unsigned n = 2;
 345   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
 346   CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
 347                 "This Expr constructor is for parameterized kinds only");
 348   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 349                 "Exprs with kind %s must have at least %u children and "
 350                 "at most %u children (the one under construction has %u)",
 351                 kind::kindToString(kind).c_str(),
 352                 minArity(kind), maxArity(kind), n);
 353   NodeManagerScope nms(d_nodeManager);
 354   try {
 355     INC_STAT(kind);
 356     return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
 357                                                child1.getNode(),
 358                                                child2.getNode()));
 359   } catch (const TypeCheckingExceptionPrivate& e) {
 360     throw TypeCheckingException(this, &e);
 361   }
 362 }
 363
 364 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
 365   const unsigned n = 3;
 366   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
 367   CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
 368                 "This Expr constructor is for parameterized kinds only");
 369   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 370                 "Exprs with kind %s must have at least %u children and "
 371                 "at most %u children (the one under construction has %u)",
 372                 kind::kindToString(kind).c_str(),
 373                 minArity(kind), maxArity(kind), n);
 374   NodeManagerScope nms(d_nodeManager);
 375   try {
 376     INC_STAT(kind);
 377     return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
 378                                                child1.getNode(),
 379                                                child2.getNode(),
 380                                                child3.getNode()));
 381   } catch (const TypeCheckingExceptionPrivate& e) {
 382     throw TypeCheckingException(this, &e);
 383   }
 384 }
 385
 386 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
 387                          Expr child4) {
 388   const unsigned n = 4;
 389   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
 390   CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
 391                 "This Expr constructor is for parameterized kinds only");
 392   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 393                 "Exprs with kind %s must have at least %u children and "
 394                 "at most %u children (the one under construction has %u)",
 395                 kind::kindToString(kind).c_str(),
 396                 minArity(kind), maxArity(kind), n);
 397   NodeManagerScope nms(d_nodeManager);
 398   try {
 399     INC_STAT(kind);
 400     return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
 401                                                child1.getNode(),
 402                                                child2.getNode(),
 403                                                child3.getNode(),
 404                                                child4.getNode()));
 405   } catch (const TypeCheckingExceptionPrivate& e) {
 406     throw TypeCheckingException(this, &e);
 407   }
 408 }
 409
 410 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
 411                          Expr child4, Expr child5) {
 412   const unsigned n = 5;
 413   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
 414   CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
 415                 "This Expr constructor is for parameterized kinds only");
 416   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 417                 "Exprs with kind %s must have at least %u children and "
 418                 "at most %u children (the one under construction has %u)",
 419                 kind::kindToString(kind).c_str(),
 420                 minArity(kind), maxArity(kind), n);
 421   NodeManagerScope nms(d_nodeManager);
 422   try {
 423     INC_STAT(kind);
 424     return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
 425                                                child1.getNode(),
 426                                                child2.getNode(),
 427                                                child3.getNode(),
 428                                                child4.getNode(),
 429                                                child5.getNode()));
 430   } catch (const TypeCheckingExceptionPrivate& e) {
 431     throw TypeCheckingException(this, &e);
 432   }
 433 }
 434
 435 Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
 436   const unsigned n = children.size();
 437   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
 438   CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
 439                 "This Expr constructor is for parameterized kinds only");
 440   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 441                 "Exprs with kind %s must have at least %u children and "
 442                 "at most %u children (the one under construction has %u)",
 443                 kind::kindToString(kind).c_str(),
 444                 minArity(kind), maxArity(kind), n);
 445
 446   NodeManagerScope nms(d_nodeManager);
 447
 448   vector<Node> nodes;
 449   vector<Expr>::const_iterator it = children.begin();
 450   vector<Expr>::const_iterator it_end = children.end();
 451   while(it != it_end) {
 452     nodes.push_back(it->getNode());
 453     ++it;
 454   }
 455   try {
 456     INC_STAT(kind);
 457     return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
 458   } catch (const TypeCheckingExceptionPrivate& e) {
 459     throw TypeCheckingException(this, &e);
 460   }
 461 }
 462
 463 bool ExprManager::hasOperator(Kind k) {
 464   return NodeManager::hasOperator(k);
 465 }
 466
 467 Expr ExprManager::operatorOf(Kind k) {
 468   NodeManagerScope nms(d_nodeManager);
 469
 470   return d_nodeManager->operatorOf(k).toExpr();
 471 }
 472
 473 /** Make a function type from domain to range. */
 474 FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
 475   NodeManagerScope nms(d_nodeManager);
 476   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))));
 477 }
 478
 479 /** Make a function type with input types from argTypes. */
 480 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
 481   NodeManagerScope nms(d_nodeManager);
 482   Assert( argTypes.size() >= 1 );
 483   std::vector<TypeNode> argTypeNodes;
 484   for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
 485     argTypeNodes.push_back(*argTypes[i].d_typeNode);
 486   }
 487   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode))));
 488 }
 489
 490 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
 491   NodeManagerScope nms(d_nodeManager);
 492   Assert( sorts.size() >= 2 );
 493   std::vector<TypeNode> sortNodes;
 494   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
 495      sortNodes.push_back(*sorts[i].d_typeNode);
 496   }
 497   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes))));
 498 }
 499
 500 FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
 501   NodeManagerScope nms(d_nodeManager);
 502   Assert( sorts.size() >= 1 );
 503   std::vector<TypeNode> sortNodes;
 504   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
 505      sortNodes.push_back(*sorts[i].d_typeNode);
 506   }
 507   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
 508 }
 509
 510 TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
 511   NodeManagerScope nms(d_nodeManager);
 512   Assert( types.size() >= 1 );
 513   std::vector<TypeNode> typeNodes;
 514   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
 515      typeNodes.push_back(*types[i].d_typeNode);
 516   }
 517   return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
 518 }
 519
 520 RecordType ExprManager::mkRecordType(const Record& rec) {
 521   NodeManagerScope nms(d_nodeManager);
 522   return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
 523 }
 524
 525 SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
 526   NodeManagerScope nms(d_nodeManager);
 527   std::vector<TypeNode> typeNodes;
 528   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
 529      typeNodes.push_back(*types[i].d_typeNode);
 530   }
 531   return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes))));
 532 }
 533
 534 BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
 535   NodeManagerScope nms(d_nodeManager);
 536   return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))));
 537 }
 538
 539 ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
 540   NodeManagerScope nms(d_nodeManager);
 541   return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
 542 }
 543
 544 DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
 545   // Not worth a special implementation; this doesn't need to be fast
 546   // code anyway..
 547   vector<Datatype> datatypes;
 548   datatypes.push_back(datatype);
 549   vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
 550   Assert(result.size() == 1);
 551   return result.front();
 552 }
 553
 554 std::vector<DatatypeType>
 555 ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 556   return mkMutualDatatypeTypes(datatypes, set<Type>());
 557 }
 558
 559 std::vector<DatatypeType>
 560 ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
 561                                    const std::set<Type>& unresolvedTypes) {
 562   NodeManagerScope nms(d_nodeManager);
 563   std::map<std::string, DatatypeType> nameResolutions;
 564   std::vector<DatatypeType> dtts;
 565
 566   // First do some sanity checks, set up the final Type to be used for
 567   // each datatype, and set up the "named resolutions" used to handle
 568   // simple self- and mutual-recursion, for example in the definition
 569   // "nat = succ(pred:nat) | zero", a named resolution can handle the
 570   // pred selector.
 571   for(std::vector<Datatype>::const_iterator i = datatypes.begin(),
 572         i_end = datatypes.end();
 573       i != i_end;
 574       ++i) {
 575     TypeNode* typeNode;
 576     if( (*i).getNumParameters() == 0 ) {
 577       typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
 578     } else {
 579       TypeNode cons = d_nodeManager->mkTypeConst(*i);
 580       std::vector< TypeNode > params;
 581       params.push_back( cons );
 582       for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
 583         params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
 584       }
 585
 586       typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
 587     }
 588     Type type(d_nodeManager, typeNode);
 589     DatatypeType dtt(type);
 590     CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
 591                   datatypes,
 592                   "cannot construct two datatypes at the same time "
 593                   "with the same name `%s'",
 594                   (*i).getName().c_str());
 595     nameResolutions.insert(std::make_pair((*i).getName(), dtt));
 596     dtts.push_back(dtt);
 597   }
 598
 599   // Second, set up the type substitution map for complex type
 600   // resolution (e.g. if "list" is the type we're defining, and it has
 601   // a selector of type "ARRAY INT OF list", this can't be taken care
 602   // of using the named resolutions that we set up above.  A
 603   // preliminary array type was set up, and now needs to have "list"
 604   // substituted in it for the correct type.
 605   //
 606   // @TODO get rid of named resolutions altogether and handle
 607   // everything with these resolutions?
 608   std::vector< SortConstructorType > paramTypes;
 609   std::vector< DatatypeType > paramReplacements;
 610   std::vector<Type> placeholders;// to hold the "unresolved placeholders"
 611   std::vector<Type> replacements;// to hold our final, resolved types
 612   for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
 613         i_end = unresolvedTypes.end();
 614       i != i_end;
 615       ++i) {
 616     std::string name;
 617     if( (*i).isSort() ) {
 618       name = SortType(*i).getName();
 619     } else {
 620       Assert( (*i).isSortConstructor() );
 621       name = SortConstructorType(*i).getName();
 622     }
 623     std::map<std::string, DatatypeType>::const_iterator resolver =
 624       nameResolutions.find(name);
 625     CheckArgument(resolver != nameResolutions.end(),
 626                   unresolvedTypes,
 627                   "cannot resolve type `%s'; it's not among "
 628                   "the datatypes being defined", name.c_str());
 629     // We will instruct the Datatype to substitute "*i" (the
 630     // unresolved SortType used as a placeholder in complex types)
 631     // with "(*resolver).second" (the DatatypeType we created in the
 632     // first step, above).
 633     if( (*i).isSort() ) {
 634       placeholders.push_back(*i);
 635       replacements.push_back( (*resolver).second );
 636     } else {
 637       Assert( (*i).isSortConstructor() );
 638       paramTypes.push_back( SortConstructorType(*i) );
 639       paramReplacements.push_back( (*resolver).second );
 640     }
 641   }
 642
 643   // Lastly, perform the final resolutions and checks.
 644   for(std::vector<DatatypeType>::iterator i = dtts.begin(),
 645         i_end = dtts.end();
 646       i != i_end;
 647       ++i) {
 648     const Datatype& dt = (*i).getDatatype();
 649     if(!dt.isResolved()) {
 650       const_cast<Datatype&>(dt).resolve(this, nameResolutions,
 651                                         placeholders, replacements,
 652                                         paramTypes, paramReplacements);
 653     }
 654
 655     // Now run some checks, including a check to make sure that no
 656     // selector is function-valued.
 657     checkResolvedDatatype(*i);
 658   }
 659
 660   for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
 661     (*i)->nmNotifyNewDatatypes(dtts);
 662   }
 663
 664   return dtts;
 665 }
 666
 667 void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
 668   const Datatype& dt = dtt.getDatatype();
 669
 670   AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved");
 671
 672   // for all constructors...
 673   for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
 674       i != i_end;
 675       ++i) {
 676     const DatatypeConstructor& c = *i;
 677     Type testerType CVC4_UNUSED = c.getTester().getType();
 678     Assert(c.isResolved() &&
 679            testerType.isTester() &&
 680            TesterType(testerType).getDomain() == dtt &&
 681            TesterType(testerType).getRangeType() == booleanType(),
 682            "malformed tester in datatype post-resolution");
 683     Type ctorType CVC4_UNUSED = c.getConstructor().getType();
 684     Assert(ctorType.isConstructor() &&
 685            ConstructorType(ctorType).getArity() == c.getNumArgs() &&
 686            ConstructorType(ctorType).getRangeType() == dtt,
 687            "malformed constructor in datatype post-resolution");
 688     // for all selectors...
 689     for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
 690         j != j_end;
 691         ++j) {
 692       const DatatypeConstructorArg& a = *j;
 693       Type selectorType = a.getSelector().getType();
 694       Assert(a.isResolved() &&
 695              selectorType.isSelector() &&
 696              SelectorType(selectorType).getDomain() == dtt,
 697              "malformed selector in datatype post-resolution");
 698       // This next one's a "hard" check, performed in non-debug builds
 699       // as well; the other ones should all be guaranteed by the
 700       // CVC4::Datatype class, but this actually needs to be checked.
 701       AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
 702                    "cannot put function-like things in datatypes");
 703     }
 704   }
 705 }
 706
 707 ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const {
 708   NodeManagerScope nms(d_nodeManager);
 709   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
 710 }
 711
 712 SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
 713   NodeManagerScope nms(d_nodeManager);
 714   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
 715 }
 716
 717 TesterType ExprManager::mkTesterType(Type domain) const {
 718   NodeManagerScope nms(d_nodeManager);
 719   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
 720 }
 721
 722 SortType ExprManager::mkSort(const std::string& name) const {
 723   NodeManagerScope nms(d_nodeManager);
 724   return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))));
 725 }
 726
 727 SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
 728                                                    size_t arity) const {
 729   NodeManagerScope nms(d_nodeManager);
 730   return SortConstructorType(Type(d_nodeManager,
 731               new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
 732 }
 733
 734 /* - not in release 1.0
 735 Type ExprManager::mkPredicateSubtype(Expr lambda)
 736   throw(TypeCheckingException) {
 737   NodeManagerScope nms(d_nodeManager);
 738   try {
 739     return PredicateSubtype(Type(d_nodeManager,
 740                 new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
 741   } catch (const TypeCheckingExceptionPrivate& e) {
 742     throw TypeCheckingException(this, &e);
 743   }
 744 }
 745 */
 746
 747 /* - not in release 1.0
 748 Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
 749   throw(TypeCheckingException) {
 750   NodeManagerScope nms(d_nodeManager);
 751   try {
 752     return PredicateSubtype(Type(d_nodeManager,
 753                 new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
 754   } catch (const TypeCheckingExceptionPrivate& e) {
 755     throw TypeCheckingException(this, &e);
 756   }
 757 }
 758 */
 759
 760 Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
 761   throw(TypeCheckingException) {
 762   NodeManagerScope nms(d_nodeManager);
 763   try {
 764     return SubrangeType(Type(d_nodeManager,
 765                 new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
 766   } catch (const TypeCheckingExceptionPrivate& e) {
 767     throw TypeCheckingException(this, &e);
 768   }
 769 }
 770
 771 /**
 772  * Get the type for the given Expr and optionally do type checking.
 773  *
 774  * Initial type computation will be near-constant time if
 775  * type checking is not requested. Results are memoized, so that
 776  * subsequent calls to getType() without type checking will be
 777  * constant time.
 778  *
 779  * Initial type checking is linear in the size of the expression.
 780  * Again, the results are memoized, so that subsequent calls to
 781  * getType(), with or without type checking, will be constant
 782  * time.
 783  *
 784  * NOTE: A TypeCheckingException can be thrown even when type
 785  * checking is not requested. getType() will always return a
 786  * valid and correct type and, thus, an exception will be thrown
 787  * when no valid or correct type can be computed (e.g., if the
 788  * arguments to a bit-vector operation aren't bit-vectors). When
 789  * type checking is not requested, getType() will do the minimum
 790  * amount of checking required to return a valid result.
 791  *
 792  * @param e the Expr for which we want a type
 793  * @param check whether we should check the type as we compute it
 794  * (default: false)
 795  */
 796 Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
 797   NodeManagerScope nms(d_nodeManager);
 798   Type t;
 799   try {
 800     t = Type(d_nodeManager,
 801              new TypeNode(d_nodeManager->getType(e.getNode(), check)));
 802   } catch (const TypeCheckingExceptionPrivate& e) {
 803     throw TypeCheckingException(this, &e);
 804   }
 805   return t;
 806 }
 807
 808 Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
 809   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
 810   NodeManagerScope nms(d_nodeManager);
 811   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
 812   Debug("nm") << "set " << name << " on " << *n << std::endl;
 813   INC_STAT_VAR(type, false);
 814   return Expr(this, n);
 815 }
 816
 817 Expr ExprManager::mkVar(Type type, uint32_t flags) {
 818   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
 819   NodeManagerScope nms(d_nodeManager);
 820   INC_STAT_VAR(type, false);
 821   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
 822 }
 823
 824 Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
 825   NodeManagerScope nms(d_nodeManager);
 826   Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode);
 827   Debug("nm") << "set " << name << " on " << *n << std::endl;
 828   INC_STAT_VAR(type, true);
 829   return Expr(this, n);
 830 }
 831
 832 Expr ExprManager::mkBoundVar(Type type) {
 833   NodeManagerScope nms(d_nodeManager);
 834   INC_STAT_VAR(type, true);
 835   return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
 836 }
 837
 838 Expr ExprManager::mkAssociative(Kind kind,
 839                                 const std::vector<Expr>& children) {
 840   CheckArgument( kind::isAssociative(kind), kind,
 841                  "Illegal kind in mkAssociative: %s",
 842                  kind::kindToString(kind).c_str());
 843
 844   NodeManagerScope nms(d_nodeManager);
 845   const unsigned int max = maxArity(kind);
 846   const unsigned int min = minArity(kind);
 847   unsigned int numChildren = children.size();
 848
 849   /* If the number of children is within bounds, then there's nothing to do. */
 850   if( numChildren <= max ) {
 851     return mkExpr(kind,children);
 852   }
 853
 854   std::vector<Expr>::const_iterator it = children.begin() ;
 855   std::vector<Expr>::const_iterator end = children.end() ;
 856
 857   /* The new top-level children and the children of each sub node */
 858   std::vector<Node> newChildren;
 859   std::vector<Node> subChildren;
 860
 861   while( it != end && numChildren > max ) {
 862     /* Grab the next max children and make a node for them. */
 863     for( std::vector<Expr>::const_iterator next = it + max;
 864          it != next;
 865          ++it, --numChildren ) {
 866       subChildren.push_back(it->getNode());
 867     }
 868     Node subNode = d_nodeManager->mkNode(kind,subChildren);
 869     newChildren.push_back(subNode);
 870
 871     subChildren.clear();
 872   }
 873
 874   /* If there's children left, "top off" the Expr. */
 875   if(numChildren > 0) {
 876     /* If the leftovers are too few, just copy them into newChildren;
 877      * otherwise make a new sub-node  */
 878     if(numChildren < min) {
 879       for(; it != end; ++it) {
 880         newChildren.push_back(it->getNode());
 881       }
 882     } else {
 883       for(; it != end; ++it) {
 884         subChildren.push_back(it->getNode());
 885       }
 886       Node subNode = d_nodeManager->mkNode(kind, subChildren);
 887       newChildren.push_back(subNode);
 888     }
 889   }
 890
 891   /* It's inconceivable we could have enough children for this to fail
 892    * (more than 2^32, in most cases?). */
 893   AlwaysAssert( newChildren.size() <= max,
 894                 "Too many new children in mkAssociative" );
 895
 896   /* It would be really weird if this happened (it would require
 897    * min > 2, for one thing), but let's make sure. */
 898   AlwaysAssert( newChildren.size() >= min,
 899                 "Too few new children in mkAssociative" );
 900
 901   return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
 902 }
 903
 904 unsigned ExprManager::minArity(Kind kind) {
 905   return metakind::getLowerBoundForKind(kind);
 906 }
 907
 908 unsigned ExprManager::maxArity(Kind kind) {
 909   return metakind::getUpperBoundForKind(kind);
 910 }
 911
 912 NodeManager* ExprManager::getNodeManager() const {
 913   return d_nodeManager;
 914 }
 915
 916 Context* ExprManager::getContext() const {
 917   return d_ctxt;
 918 }
 919
 920 Statistics ExprManager::getStatistics() const throw() {
 921   return Statistics(*d_nodeManager->getStatisticsRegistry());
 922 }
 923
 924 SExpr ExprManager::getStatistic(const std::string& name) const throw() {
 925   return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
 926 }
 927
 928 namespace expr {
 929
 930 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
 931
 932 TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
 933   Debug("export") << "type: " << n << std::endl;
 934   if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
 935     throw ExportUnsupportedException
 936       ("export of types belonging to theory of DATATYPES kinds unsupported");
 937   }
 938   if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
 939      n.getKind() != kind::SORT_TYPE) {
 940     throw ExportUnsupportedException
 941       ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
 942   }
 943   if(n.getKind() == kind::TYPE_CONSTANT) {
 944     return to->mkTypeConst(n.getConst<TypeConstant>());
 945   } else if(n.getKind() == kind::BITVECTOR_TYPE) {
 946     return to->mkBitVectorType(n.getConst<BitVectorSize>());
 947   } else if(n.getKind() == kind::SUBRANGE_TYPE) {
 948     return to->mkSubrangeType(n.getSubrangeBounds());
 949   }
 950   Type from_t = from->toType(n);
 951   Type& to_t = vmap.d_typeMap[from_t];
 952   if(! to_t.isNull()) {
 953     Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl;
 954     return *Type::getTypeNode(to_t);
 955   }
 956   NodeBuilder<> children(to, n.getKind());
 957   if(n.getKind() == kind::SORT_TYPE) {
 958     Debug("export") << "type: operator: " << n.getOperator() << std::endl;
 959     // make a new sort tag in target node manager
 960     Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG);
 961     children << sortTag;
 962   }
 963   for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
 964     Debug("export") << "type: child: " << *i << std::endl;
 965     children << exportTypeInternal(*i, from, to, vmap);
 966   }
 967   TypeNode out = children.constructTypeNode();// FIXME thread safety
 968   to_t = to->toType(out);
 969   return out;
 970 }/* exportTypeInternal() */
 971
 972 }/* CVC4::expr namespace */
 973
 974 Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
 975   Assert(t.d_nodeManager != em->d_nodeManager,
 976          "Can't export a Type to the same ExprManager");
 977   NodeManagerScope ems(t.d_nodeManager);
 978   return Type(em->d_nodeManager,
 979               new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
 980 }
 981
 982 ${mkConst_implementations}
 983
 984 }/* CVC4 namespace */