src/expr/expr_manager.cpp

   1 /*********************                                                        */
   2 /** expr_manager.cpp
   3  ** Original author: dejan
   4  ** Major contributors: cconway, mdeters
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** [[ Add file-specific comments here ]]
  14  **/
  15
  16 /*
  17  * expr_manager.cpp
  18  *
  19  *  Created on: Dec 10, 2009
  20  *      Author: dejan
  21  */
  22
  23 #include "expr/node.h"
  24 #include "expr/expr.h"
  25 #include "expr/type.h"
  26 #include "expr/node_manager.h"
  27 #include "expr/expr_manager.h"
  28
  29 using namespace std;
  30
  31 namespace CVC4 {
  32
  33 ExprManager::ExprManager() :
  34   d_nodeManager(new NodeManager()) {
  35 }
  36
  37 ExprManager::~ExprManager() {
  38   delete d_nodeManager;
  39 }
  40
  41 const BooleanType* ExprManager::booleanType() {
  42   NodeManagerScope nms(d_nodeManager);
  43   return BooleanType::getInstance();
  44 }
  45
  46 const KindType* ExprManager::kindType() {
  47   NodeManagerScope nms(d_nodeManager);
  48   return KindType::getInstance();
  49 }
  50
  51 Expr ExprManager::mkExpr(Kind kind) {
  52   NodeManagerScope nms(d_nodeManager);
  53   return Expr(this, new Node(d_nodeManager->mkNode(kind)));
  54 }
  55
  56 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
  57   NodeManagerScope nms(d_nodeManager);
  58   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode())));
  59 }
  60
  61 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
  62   NodeManagerScope nms(d_nodeManager);
  63   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
  64                                           child2.getNode())));
  65 }
  66
  67 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
  68                          const Expr& child3) {
  69   NodeManagerScope nms(d_nodeManager);
  70   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
  71                                           child2.getNode(), child3.getNode())));
  72 }
  73
  74 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
  75                          const Expr& child3, const Expr& child4) {
  76   NodeManagerScope nms(d_nodeManager);
  77   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
  78                                           child2.getNode(), child3.getNode(),
  79                                           child4.getNode())));
  80 }
  81
  82 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
  83                          const Expr& child3, const Expr& child4,
  84                          const Expr& child5) {
  85   NodeManagerScope nms(d_nodeManager);
  86   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
  87                                           child2.getNode(), child3.getNode(),
  88                                           child5.getNode())));
  89 }
  90
  91 Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
  92   NodeManagerScope nms(d_nodeManager);
  93
  94   vector<Node> nodes;
  95   vector<Expr>::const_iterator it = children.begin();
  96   vector<Expr>::const_iterator it_end = children.end();
  97   while(it != it_end) {
  98     nodes.push_back(it->getNode());
  99     ++it;
 100   }
 101   return Expr(this, new Node(d_nodeManager->mkNode(kind, nodes)));
 102 }
 103
 104 /** Make a function type from domain to range. */
 105 const FunctionType*
 106 ExprManager::mkFunctionType(const Type* domain,
 107                             const Type* range) {
 108   NodeManagerScope nms(d_nodeManager);
 109   return FunctionType::getInstance(this, domain, range);
 110 }
 111
 112 /** Make a function type with input types from argTypes. */
 113 const FunctionType*
 114 ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes,
 115                             const Type* range) {
 116   NodeManagerScope nms(d_nodeManager);
 117   return FunctionType::getInstance(this, argTypes, range);
 118 }
 119
 120 const Type* ExprManager::mkSort(std::string name) {
 121   // FIXME: Sorts should be unique per-ExprManager
 122   NodeManagerScope nms(d_nodeManager);
 123   return new SortType(this, name);
 124 }
 125
 126 Expr ExprManager::mkVar(const Type* type, string name) {
 127   NodeManagerScope nms(d_nodeManager);
 128   return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
 129 }
 130
 131 Expr ExprManager::mkVar(const Type* type) {
 132   NodeManagerScope nms(d_nodeManager);
 133   return Expr(this, new Node(d_nodeManager->mkVar(type)));
 134 }
 135
 136 NodeManager* ExprManager::getNodeManager() const {
 137   return d_nodeManager;
 138 }
 139
 140 } // End namespace CVC4