src/expr/expr_manager_template.cpp

   1 /*********************                                                        */
   2 /*! \file expr_manager_template.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters, cconway
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Public-facing expression manager interface, implementation.
  15  **
  16  ** Public-facing expression manager interface, implementation.
  17  **/
  18
  19 #include "expr/node.h"
  20 #include "expr/expr.h"
  21 #include "expr/kind.h"
  22 #include "expr/metakind.h"
  23 #include "expr/type.h"
  24 #include "expr/node_manager.h"
  25 #include "expr/expr_manager.h"
  26 #include "context/context.h"
  27
  28 ${includes}
  29
  30 // This is a hack, but an important one: if there's an error, the
  31 // compiler directs the user to the template file instead of the
  32 // generated one.  We don't want the user to modify the generated one,
  33 // since it'll get overwritten on a later build.
  34 #line 35 "${template}"
  35
  36 using namespace std;
  37 using namespace CVC4::context;
  38 using namespace CVC4::kind;
  39
  40 namespace CVC4 {
  41
  42 ExprManager::ExprManager() :
  43   d_ctxt(new Context),
  44   d_nodeManager(new NodeManager(d_ctxt)) {
  45 }
  46
  47 ExprManager::~ExprManager() {
  48   delete d_nodeManager;
  49   delete d_ctxt;
  50 }
  51
  52 BooleanType ExprManager::booleanType() const {
  53   NodeManagerScope nms(d_nodeManager);
  54   return Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()));
  55 }
  56
  57 KindType ExprManager::kindType() const {
  58   NodeManagerScope nms(d_nodeManager);
  59   return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()));
  60 }
  61
  62 RealType ExprManager::realType() const {
  63   NodeManagerScope nms(d_nodeManager);
  64   return Type(d_nodeManager, new TypeNode(d_nodeManager->realType()));
  65 }
  66
  67 IntegerType ExprManager::integerType() const {
  68   NodeManagerScope nms(d_nodeManager);
  69   return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()));
  70 }
  71
  72 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
  73   const unsigned n = 1;
  74   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
  75                 "Exprs with kind %s must have at least %u children and "
  76                 "at most %u children (the one under construction has %u)",
  77                 kind::kindToString(kind).c_str(),
  78                 minArity(kind), maxArity(kind), n);
  79   NodeManagerScope nms(d_nodeManager);
  80   try {
  81     return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
  82   } catch (const TypeCheckingExceptionPrivate& e) {
  83     throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
  84   }
  85 }
  86
  87 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
  88   const unsigned n = 2;
  89   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
  90                 "Exprs with kind %s must have at least %u children and "
  91                 "at most %u children (the one under construction has %u)",
  92                 kind::kindToString(kind).c_str(),
  93                 minArity(kind), maxArity(kind), n);
  94   NodeManagerScope nms(d_nodeManager);
  95   try {
  96     return Expr(this, d_nodeManager->mkNodePtr(kind,
  97                                                child1.getNode(),
  98                                                child2.getNode()));
  99   } catch (const TypeCheckingExceptionPrivate& e) {
 100     throw TypeCheckingException(Expr(this, new Node(e.getNode())),
 101                                 e.getMessage());
 102   }
 103 }
 104
 105 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 106                          const Expr& child3) {
 107   const unsigned n = 3;
 108   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 109                 "Exprs with kind %s must have at least %u children and "
 110                 "at most %u children (the one under construction has %u)",
 111                 kind::kindToString(kind).c_str(),
 112                 minArity(kind), maxArity(kind), n);
 113   NodeManagerScope nms(d_nodeManager);
 114   try {
 115     return Expr(this, d_nodeManager->mkNodePtr(kind,
 116                                                child1.getNode(),
 117                                                child2.getNode(),
 118                                                child3.getNode()));
 119   } catch (const TypeCheckingExceptionPrivate& e) {
 120     throw TypeCheckingException(Expr(this, new Node(e.getNode())),
 121                                 e.getMessage());
 122   }
 123 }
 124
 125 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 126                          const Expr& child3, const Expr& child4) {
 127   const unsigned n = 4;
 128   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 129                 "Exprs with kind %s must have at least %u children and "
 130                 "at most %u children (the one under construction has %u)",
 131                 kind::kindToString(kind).c_str(),
 132                 minArity(kind), maxArity(kind), n);
 133   NodeManagerScope nms(d_nodeManager);
 134   try {
 135     return Expr(this, d_nodeManager->mkNodePtr(kind,
 136                                                child1.getNode(),
 137                                                child2.getNode(),
 138                                                child3.getNode(),
 139                                                child4.getNode()));
 140   } catch (const TypeCheckingExceptionPrivate& e) {
 141     throw TypeCheckingException(Expr(this, new Node(e.getNode())),
 142                                 e.getMessage());
 143   }
 144 }
 145
 146 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 147                          const Expr& child3, const Expr& child4,
 148                          const Expr& child5) {
 149   const unsigned n = 5;
 150   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 151                 "Exprs with kind %s must have at least %u children and "
 152                 "at most %u children (the one under construction has %u)",
 153                 kind::kindToString(kind).c_str(),
 154                 minArity(kind), maxArity(kind), n);
 155   NodeManagerScope nms(d_nodeManager);
 156   try {
 157     return Expr(this, d_nodeManager->mkNodePtr(kind,
 158                                                child1.getNode(),
 159                                                child2.getNode(),
 160                                                child3.getNode(),
 161                                                child4.getNode(),
 162                                                child5.getNode()));
 163   } catch (const TypeCheckingExceptionPrivate& e) {
 164     throw TypeCheckingException(Expr(this, new Node(e.getNode())),
 165                                 e.getMessage());
 166   }
 167 }
 168
 169 Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
 170   const unsigned n = children.size();
 171   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 172                 "Exprs with kind %s must have at least %u children and "
 173                 "at most %u children (the one under construction has %u)",
 174                 kind::kindToString(kind).c_str(),
 175                 minArity(kind), maxArity(kind), n);
 176
 177   NodeManagerScope nms(d_nodeManager);
 178
 179   vector<Node> nodes;
 180   vector<Expr>::const_iterator it = children.begin();
 181   vector<Expr>::const_iterator it_end = children.end();
 182   while(it != it_end) {
 183     nodes.push_back(it->getNode());
 184     ++it;
 185   }
 186   try {
 187     return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
 188   } catch (const TypeCheckingExceptionPrivate& e) {
 189     throw TypeCheckingException(Expr(this, new Node(e.getNode())),
 190                                 e.getMessage());
 191   }
 192 }
 193
 194 Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
 195   const unsigned n = children.size();
 196   Kind kind = kind::operatorKindToKind(opExpr.getKind());
 197   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
 198                 "Exprs with kind %s must have at least %u children and "
 199                 "at most %u children (the one under construction has %u)",
 200                 kind::kindToString(kind).c_str(),
 201                 minArity(kind), maxArity(kind), n);
 202
 203   NodeManagerScope nms(d_nodeManager);
 204
 205   vector<Node> nodes;
 206   vector<Expr>::const_iterator it = children.begin();
 207   vector<Expr>::const_iterator it_end = children.end();
 208   while(it != it_end) {
 209     nodes.push_back(it->getNode());
 210     ++it;
 211   }
 212   try {
 213     return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
 214   } catch (const TypeCheckingExceptionPrivate& e) {
 215     throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
 216   }
 217 }
 218
 219 /** Make a function type from domain to range. */
 220 FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) {
 221   NodeManagerScope nms(d_nodeManager);
 222   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)));
 223 }
 224
 225 /** Make a function type with input types from argTypes. */
 226 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
 227   Assert( argTypes.size() >= 1 );
 228   NodeManagerScope nms(d_nodeManager);
 229   std::vector<TypeNode> argTypeNodes;
 230   for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
 231     argTypeNodes.push_back(*argTypes[i].d_typeNode);
 232   }
 233   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode)));
 234 }
 235
 236 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
 237   Assert( sorts.size() >= 2 );
 238   NodeManagerScope nms(d_nodeManager);
 239   std::vector<TypeNode> sortNodes;
 240   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
 241      sortNodes.push_back(*sorts[i].d_typeNode);
 242   }
 243   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes)));
 244 }
 245
 246 FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
 247   Assert( sorts.size() >= 1 );
 248   NodeManagerScope nms(d_nodeManager);
 249   std::vector<TypeNode> sortNodes;
 250   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
 251      sortNodes.push_back(*sorts[i].d_typeNode);
 252   }
 253   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)));
 254 }
 255
 256 TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
 257   Assert( types.size() >= 2 );
 258   NodeManagerScope nms(d_nodeManager);
 259   std::vector<TypeNode> typeNodes;
 260   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
 261      typeNodes.push_back(*types[i].d_typeNode);
 262   }
 263   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)));
 264 }
 265
 266 BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
 267   NodeManagerScope nms(d_nodeManager);
 268   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)));
 269 }
 270
 271 ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
 272   NodeManagerScope nms(d_nodeManager);
 273   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)));
 274 }
 275
 276 SortType ExprManager::mkSort(const std::string& name) const {
 277   NodeManagerScope nms(d_nodeManager);
 278   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
 279 }
 280
 281 /**
 282  * Get the type for the given Expr and optionally do type checking.
 283  *
 284  * Initial type computation will be near-constant time if
 285  * type checking is not requested. Results are memoized, so that
 286  * subsequent calls to getType() without type checking will be
 287  * constant time.
 288  *
 289  * Initial type checking is linear in the size of the expression.
 290  * Again, the results are memoized, so that subsequent calls to
 291  * getType(), with or without type checking, will be constant
 292  * time.
 293  *
 294  * NOTE: A TypeCheckingException can be thrown even when type
 295  * checking is not requested. getType() will always return a
 296  * valid and correct type and, thus, an exception will be thrown
 297  * when no valid or correct type can be computed (e.g., if the
 298  * arguments to a bit-vector operation aren't bit-vectors). When
 299  * type checking is not requested, getType() will do the minimum
 300  * amount of checking required to return a valid result.
 301  *
 302  * @param n the Expr for which we want a type
 303  * @param check whether we should check the type as we compute it
 304  * (default: false)
 305  */
 306 Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) {
 307   NodeManagerScope nms(d_nodeManager);
 308   Type t;
 309   try {
 310     t = Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode(), check)));
 311   } catch (const TypeCheckingExceptionPrivate& e) {
 312     throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
 313   }
 314   return t;
 315 }
 316
 317 Expr ExprManager::mkVar(const std::string& name, const Type& type) {
 318   NodeManagerScope nms(d_nodeManager);
 319   return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode));
 320 }
 321
 322 Expr ExprManager::mkVar(const Type& type) {
 323   NodeManagerScope nms(d_nodeManager);
 324   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
 325 }
 326
 327 Expr ExprManager::mkAssociative(Kind kind,
 328                                 const std::vector<Expr>& children) {
 329   CheckArgument( kind::isAssociative(kind), kind,
 330                  "Illegal kind in mkAssociative: %s",
 331                  kind::kindToString(kind).c_str());
 332
 333   NodeManagerScope nms(d_nodeManager);
 334   const unsigned int max = maxArity(kind);
 335   const unsigned int min = minArity(kind);
 336   unsigned int numChildren = children.size();
 337
 338   /* If the number of children is within bounds, then there's nothing to do. */
 339   if( numChildren <= max ) {
 340     return mkExpr(kind,children);
 341   }
 342
 343   std::vector<Expr>::const_iterator it = children.begin() ;
 344   std::vector<Expr>::const_iterator end = children.end() ;
 345
 346   /* The new top-level children and the children of each sub node */
 347   std::vector<Node> newChildren;
 348   std::vector<Node> subChildren;
 349
 350   while( it != end && numChildren > max ) {
 351     /* Grab the next max children and make a node for them. */
 352     for( std::vector<Expr>::const_iterator next = it + max;
 353          it != next;
 354          ++it, --numChildren ) {
 355       subChildren.push_back(it->getNode());
 356     }
 357     Node subNode = d_nodeManager->mkNode(kind,subChildren);
 358     newChildren.push_back(subNode);
 359
 360     subChildren.clear();
 361   }
 362
 363   /* If there's children left, "top off" the Expr. */
 364   if(numChildren > 0) {
 365     /* If the leftovers are too few, just copy them into newChildren;
 366      * otherwise make a new sub-node  */
 367     if(numChildren < min) {
 368       for(; it != end; ++it) {
 369         newChildren.push_back(it->getNode());
 370       }
 371     } else {
 372       for(; it != end; ++it) {
 373         subChildren.push_back(it->getNode());
 374       }
 375       Node subNode = d_nodeManager->mkNode(kind, subChildren);
 376       newChildren.push_back(subNode);
 377     }
 378   }
 379
 380   /* It's inconceivable we could have enough children for this to fail
 381    * (more than 2^32, in most cases?). */
 382   AlwaysAssert( newChildren.size() <= max,
 383                 "Too many new children in mkAssociative" );
 384
 385   /* It would be really weird if this happened (it would require
 386    * min > 2, for one thing), but let's make sure. */
 387   AlwaysAssert( newChildren.size() >= min,
 388                 "Too few new children in mkAssociative" );
 389
 390   return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
 391 }
 392
 393 unsigned ExprManager::minArity(Kind kind) {
 394   return metakind::getLowerBoundForKind(kind);
 395 }
 396
 397 unsigned ExprManager::maxArity(Kind kind) {
 398   return metakind::getUpperBoundForKind(kind);
 399 }
 400
 401 NodeManager* ExprManager::getNodeManager() const {
 402   return d_nodeManager;
 403 }
 404
 405 Context* ExprManager::getContext() const {
 406   return d_ctxt;
 407 }
 408
 409 ${mkConst_implementations}
 410
 411 }/* CVC4 namespace */