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   std::vector<TypeNode> typeNodes;
 513   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
 514      typeNodes.push_back(*types[i].d_typeNode);
 515   }
 516   return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
 517 }
 518
 519 RecordType ExprManager::mkRecordType(const Record& rec) {
 520   NodeManagerScope nms(d_nodeManager);
 521   return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
 522 }
 523
 524 SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
 525   NodeManagerScope nms(d_nodeManager);
 526   std::vector<TypeNode> typeNodes;
 527   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
 528      typeNodes.push_back(*types[i].d_typeNode);
 529   }
 530   return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes))));
 531 }
 532
 533 BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
 534   NodeManagerScope nms(d_nodeManager);
 535   return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))));
 536 }
 537
 538 ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
 539   NodeManagerScope nms(d_nodeManager);
 540   return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
 541 }
 542
 543 DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
 544   // Not worth a special implementation; this doesn't need to be fast
 545   // code anyway..
 546   vector<Datatype> datatypes;
 547   datatypes.push_back(datatype);
 548   vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
 549   Assert(result.size() == 1);
 550   return result.front();
 551 }
 552
 553 std::vector<DatatypeType>
 554 ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 555   return mkMutualDatatypeTypes(datatypes, set<Type>());
 556 }
 557
 558 std::vector<DatatypeType>
 559 ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
 560                                    const std::set<Type>& unresolvedTypes) {
 561   NodeManagerScope nms(d_nodeManager);
 562   std::map<std::string, DatatypeType> nameResolutions;
 563   std::vector<DatatypeType> dtts;
 564
 565   // First do some sanity checks, set up the final Type to be used for
 566   // each datatype, and set up the "named resolutions" used to handle
 567   // simple self- and mutual-recursion, for example in the definition
 568   // "nat = succ(pred:nat) | zero", a named resolution can handle the
 569   // pred selector.
 570   for(std::vector<Datatype>::const_iterator i = datatypes.begin(),
 571         i_end = datatypes.end();
 572       i != i_end;
 573       ++i) {
 574     TypeNode* typeNode;
 575     if( (*i).getNumParameters() == 0 ) {
 576       typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
 577     } else {
 578       TypeNode cons = d_nodeManager->mkTypeConst(*i);
 579       std::vector< TypeNode > params;
 580       params.push_back( cons );
 581       for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
 582         params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
 583       }
 584
 585       typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
 586     }
 587     Type type(d_nodeManager, typeNode);
 588     DatatypeType dtt(type);
 589     CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
 590                   datatypes,
 591                   "cannot construct two datatypes at the same time "
 592                   "with the same name `%s'",
 593                   (*i).getName().c_str());
 594     nameResolutions.insert(std::make_pair((*i).getName(), dtt));
 595     dtts.push_back(dtt);
 596   }
 597
 598   // Second, set up the type substitution map for complex type
 599   // resolution (e.g. if "list" is the type we're defining, and it has
 600   // a selector of type "ARRAY INT OF list", this can't be taken care
 601   // of using the named resolutions that we set up above.  A
 602   // preliminary array type was set up, and now needs to have "list"
 603   // substituted in it for the correct type.
 604   //
 605   // @TODO get rid of named resolutions altogether and handle
 606   // everything with these resolutions?
 607   std::vector< SortConstructorType > paramTypes;
 608   std::vector< DatatypeType > paramReplacements;
 609   std::vector<Type> placeholders;// to hold the "unresolved placeholders"
 610   std::vector<Type> replacements;// to hold our final, resolved types
 611   for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
 612         i_end = unresolvedTypes.end();
 613       i != i_end;
 614       ++i) {
 615     std::string name;
 616     if( (*i).isSort() ) {
 617       name = SortType(*i).getName();
 618     } else {
 619       Assert( (*i).isSortConstructor() );
 620       name = SortConstructorType(*i).getName();
 621     }
 622     std::map<std::string, DatatypeType>::const_iterator resolver =
 623       nameResolutions.find(name);
 624     CheckArgument(resolver != nameResolutions.end(),
 625                   unresolvedTypes,
 626                   "cannot resolve type `%s'; it's not among "
 627                   "the datatypes being defined", name.c_str());
 628     // We will instruct the Datatype to substitute "*i" (the
 629     // unresolved SortType used as a placeholder in complex types)
 630     // with "(*resolver).second" (the DatatypeType we created in the
 631     // first step, above).
 632     if( (*i).isSort() ) {
 633       placeholders.push_back(*i);
 634       replacements.push_back( (*resolver).second );
 635     } else {
 636       Assert( (*i).isSortConstructor() );
 637       paramTypes.push_back( SortConstructorType(*i) );
 638       paramReplacements.push_back( (*resolver).second );
 639     }
 640   }
 641
 642   // Lastly, perform the final resolutions and checks.
 643   for(std::vector<DatatypeType>::iterator i = dtts.begin(),
 644         i_end = dtts.end();
 645       i != i_end;
 646       ++i) {
 647     const Datatype& dt = (*i).getDatatype();
 648     if(!dt.isResolved()) {
 649       const_cast<Datatype&>(dt).resolve(this, nameResolutions,
 650                                         placeholders, replacements,
 651                                         paramTypes, paramReplacements);
 652     }
 653
 654     // Now run some checks, including a check to make sure that no
 655     // selector is function-valued.
 656     checkResolvedDatatype(*i);
 657   }
 658
 659   for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
 660     (*i)->nmNotifyNewDatatypes(dtts);
 661   }
 662
 663   return dtts;
 664 }
 665
 666 void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
 667   const Datatype& dt = dtt.getDatatype();
 668
 669   AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved");
 670
 671   // for all constructors...
 672   for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
 673       i != i_end;
 674       ++i) {
 675     const DatatypeConstructor& c = *i;
 676     Type testerType CVC4_UNUSED = c.getTester().getType();
 677     Assert(c.isResolved() &&
 678            testerType.isTester() &&
 679            TesterType(testerType).getDomain() == dtt &&
 680            TesterType(testerType).getRangeType() == booleanType(),
 681            "malformed tester in datatype post-resolution");
 682     Type ctorType CVC4_UNUSED = c.getConstructor().getType();
 683     Assert(ctorType.isConstructor() &&
 684            ConstructorType(ctorType).getArity() == c.getNumArgs() &&
 685            ConstructorType(ctorType).getRangeType() == dtt,
 686            "malformed constructor in datatype post-resolution");
 687     // for all selectors...
 688     for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
 689         j != j_end;
 690         ++j) {
 691       const DatatypeConstructorArg& a = *j;
 692       Type selectorType = a.getSelector().getType();
 693       Assert(a.isResolved() &&
 694              selectorType.isSelector() &&
 695              SelectorType(selectorType).getDomain() == dtt,
 696              "malformed selector in datatype post-resolution");
 697       // This next one's a "hard" check, performed in non-debug builds
 698       // as well; the other ones should all be guaranteed by the
 699       // CVC4::Datatype class, but this actually needs to be checked.
 700       AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
 701                    "cannot put function-like things in datatypes");
 702     }
 703   }
 704 }
 705
 706 ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const {
 707   NodeManagerScope nms(d_nodeManager);
 708   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
 709 }
 710
 711 SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
 712   NodeManagerScope nms(d_nodeManager);
 713   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
 714 }
 715
 716 TesterType ExprManager::mkTesterType(Type domain) const {
 717   NodeManagerScope nms(d_nodeManager);
 718   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
 719 }
 720
 721 SortType ExprManager::mkSort(const std::string& name) const {
 722   NodeManagerScope nms(d_nodeManager);
 723   return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))));
 724 }
 725
 726 SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
 727                                                    size_t arity) const {
 728   NodeManagerScope nms(d_nodeManager);
 729   return SortConstructorType(Type(d_nodeManager,
 730               new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
 731 }
 732
 733 /* - not in release 1.0
 734 Type ExprManager::mkPredicateSubtype(Expr lambda)
 735   throw(TypeCheckingException) {
 736   NodeManagerScope nms(d_nodeManager);
 737   try {
 738     return PredicateSubtype(Type(d_nodeManager,
 739                 new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
 740   } catch (const TypeCheckingExceptionPrivate& e) {
 741     throw TypeCheckingException(this, &e);
 742   }
 743 }
 744 */
 745
 746 /* - not in release 1.0
 747 Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
 748   throw(TypeCheckingException) {
 749   NodeManagerScope nms(d_nodeManager);
 750   try {
 751     return PredicateSubtype(Type(d_nodeManager,
 752                 new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
 753   } catch (const TypeCheckingExceptionPrivate& e) {
 754     throw TypeCheckingException(this, &e);
 755   }
 756 }
 757 */
 758
 759 Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
 760   throw(TypeCheckingException) {
 761   NodeManagerScope nms(d_nodeManager);
 762   try {
 763     return SubrangeType(Type(d_nodeManager,
 764                 new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
 765   } catch (const TypeCheckingExceptionPrivate& e) {
 766     throw TypeCheckingException(this, &e);
 767   }
 768 }
 769
 770 /**
 771  * Get the type for the given Expr and optionally do type checking.
 772  *
 773  * Initial type computation will be near-constant time if
 774  * type checking is not requested. Results are memoized, so that
 775  * subsequent calls to getType() without type checking will be
 776  * constant time.
 777  *
 778  * Initial type checking is linear in the size of the expression.
 779  * Again, the results are memoized, so that subsequent calls to
 780  * getType(), with or without type checking, will be constant
 781  * time.
 782  *
 783  * NOTE: A TypeCheckingException can be thrown even when type
 784  * checking is not requested. getType() will always return a
 785  * valid and correct type and, thus, an exception will be thrown
 786  * when no valid or correct type can be computed (e.g., if the
 787  * arguments to a bit-vector operation aren't bit-vectors). When
 788  * type checking is not requested, getType() will do the minimum
 789  * amount of checking required to return a valid result.
 790  *
 791  * @param e the Expr for which we want a type
 792  * @param check whether we should check the type as we compute it
 793  * (default: false)
 794  */
 795 Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
 796   NodeManagerScope nms(d_nodeManager);
 797   Type t;
 798   try {
 799     t = Type(d_nodeManager,
 800              new TypeNode(d_nodeManager->getType(e.getNode(), check)));
 801   } catch (const TypeCheckingExceptionPrivate& e) {
 802     throw TypeCheckingException(this, &e);
 803   }
 804   return t;
 805 }
 806
 807 Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
 808   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
 809   NodeManagerScope nms(d_nodeManager);
 810   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
 811   Debug("nm") << "set " << name << " on " << *n << std::endl;
 812   INC_STAT_VAR(type, false);
 813   return Expr(this, n);
 814 }
 815
 816 Expr ExprManager::mkVar(Type type, uint32_t flags) {
 817   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
 818   NodeManagerScope nms(d_nodeManager);
 819   INC_STAT_VAR(type, false);
 820   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
 821 }
 822
 823 Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
 824   NodeManagerScope nms(d_nodeManager);
 825   Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode);
 826   Debug("nm") << "set " << name << " on " << *n << std::endl;
 827   INC_STAT_VAR(type, true);
 828   return Expr(this, n);
 829 }
 830
 831 Expr ExprManager::mkBoundVar(Type type) {
 832   NodeManagerScope nms(d_nodeManager);
 833   INC_STAT_VAR(type, true);
 834   return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
 835 }
 836
 837 Expr ExprManager::mkAssociative(Kind kind,
 838                                 const std::vector<Expr>& children) {
 839   CheckArgument( kind::isAssociative(kind), kind,
 840                  "Illegal kind in mkAssociative: %s",
 841                  kind::kindToString(kind).c_str());
 842
 843   NodeManagerScope nms(d_nodeManager);
 844   const unsigned int max = maxArity(kind);
 845   const unsigned int min = minArity(kind);
 846   unsigned int numChildren = children.size();
 847
 848   /* If the number of children is within bounds, then there's nothing to do. */
 849   if( numChildren <= max ) {
 850     return mkExpr(kind,children);
 851   }
 852
 853   std::vector<Expr>::const_iterator it = children.begin() ;
 854   std::vector<Expr>::const_iterator end = children.end() ;
 855
 856   /* The new top-level children and the children of each sub node */
 857   std::vector<Node> newChildren;
 858   std::vector<Node> subChildren;
 859
 860   while( it != end && numChildren > max ) {
 861     /* Grab the next max children and make a node for them. */
 862     for( std::vector<Expr>::const_iterator next = it + max;
 863          it != next;
 864          ++it, --numChildren ) {
 865       subChildren.push_back(it->getNode());
 866     }
 867     Node subNode = d_nodeManager->mkNode(kind,subChildren);
 868     newChildren.push_back(subNode);
 869
 870     subChildren.clear();
 871   }
 872
 873   /* If there's children left, "top off" the Expr. */
 874   if(numChildren > 0) {
 875     /* If the leftovers are too few, just copy them into newChildren;
 876      * otherwise make a new sub-node  */
 877     if(numChildren < min) {
 878       for(; it != end; ++it) {
 879         newChildren.push_back(it->getNode());
 880       }
 881     } else {
 882       for(; it != end; ++it) {
 883         subChildren.push_back(it->getNode());
 884       }
 885       Node subNode = d_nodeManager->mkNode(kind, subChildren);
 886       newChildren.push_back(subNode);
 887     }
 888   }
 889
 890   /* It's inconceivable we could have enough children for this to fail
 891    * (more than 2^32, in most cases?). */
 892   AlwaysAssert( newChildren.size() <= max,
 893                 "Too many new children in mkAssociative" );
 894
 895   /* It would be really weird if this happened (it would require
 896    * min > 2, for one thing), but let's make sure. */
 897   AlwaysAssert( newChildren.size() >= min,
 898                 "Too few new children in mkAssociative" );
 899
 900   return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
 901 }
 902
 903 unsigned ExprManager::minArity(Kind kind) {
 904   return metakind::getLowerBoundForKind(kind);
 905 }
 906
 907 unsigned ExprManager::maxArity(Kind kind) {
 908   return metakind::getUpperBoundForKind(kind);
 909 }
 910
 911 NodeManager* ExprManager::getNodeManager() const {
 912   return d_nodeManager;
 913 }
 914
 915 Context* ExprManager::getContext() const {
 916   return d_ctxt;
 917 }
 918
 919 Statistics ExprManager::getStatistics() const throw() {
 920   return Statistics(*d_nodeManager->getStatisticsRegistry());
 921 }
 922
 923 SExpr ExprManager::getStatistic(const std::string& name) const throw() {
 924   return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
 925 }
 926
 927 namespace expr {
 928
 929 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
 930
 931 TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
 932   Debug("export") << "type: " << n << std::endl;
 933   if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
 934     throw ExportUnsupportedException
 935       ("export of types belonging to theory of DATATYPES kinds unsupported");
 936   }
 937   if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
 938      n.getKind() != kind::SORT_TYPE) {
 939     throw ExportUnsupportedException
 940       ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
 941   }
 942   if(n.getKind() == kind::TYPE_CONSTANT) {
 943     return to->mkTypeConst(n.getConst<TypeConstant>());
 944   } else if(n.getKind() == kind::BITVECTOR_TYPE) {
 945     return to->mkBitVectorType(n.getConst<BitVectorSize>());
 946   } else if(n.getKind() == kind::SUBRANGE_TYPE) {
 947     return to->mkSubrangeType(n.getSubrangeBounds());
 948   }
 949   Type from_t = from->toType(n);
 950   Type& to_t = vmap.d_typeMap[from_t];
 951   if(! to_t.isNull()) {
 952     Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl;
 953     return *Type::getTypeNode(to_t);
 954   }
 955   NodeBuilder<> children(to, n.getKind());
 956   if(n.getKind() == kind::SORT_TYPE) {
 957     Debug("export") << "type: operator: " << n.getOperator() << std::endl;
 958     // make a new sort tag in target node manager
 959     Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG);
 960     children << sortTag;
 961   }
 962   for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
 963     Debug("export") << "type: child: " << *i << std::endl;
 964     children << exportTypeInternal(*i, from, to, vmap);
 965   }
 966   TypeNode out = children.constructTypeNode();// FIXME thread safety
 967   to_t = to->toType(out);
 968   return out;
 969 }/* exportTypeInternal() */
 970
 971 }/* CVC4::expr namespace */
 972
 973 Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
 974   Assert(t.d_nodeManager != em->d_nodeManager,
 975          "Can't export a Type to the same ExprManager");
 976   NodeManagerScope ems(t.d_nodeManager);
 977   return Type(em->d_nodeManager,
 978               new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
 979 }
 980
 981 ${mkConst_implementations}
 982
 983 }/* CVC4 namespace */