src/expr/node_manager.cpp

   1 /*********************                                                        */
   2 /** node_manager.cpp
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   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  ** Expression manager implementation.
  14  **/
  15
  16 #include "node_builder.h"
  17 #include "node_manager.h"
  18 #include "expr/node.h"
  19 #include "expr/attribute.h"
  20 #include "util/output.h"
  21
  22 using namespace std;
  23 using namespace CVC4::expr;
  24
  25 namespace CVC4 {
  26
  27 __thread NodeManager* NodeManager::s_current = 0;
  28
  29 NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
  30   NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
  31   if (find == d_nodeValueSet.end()) {
  32     return NULL;
  33   } else {
  34     return *find;
  35   }
  36 }
  37
  38 void NodeManager::poolInsert(NodeValue* nv) {
  39   Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in"
  40          "the pool!");
  41   d_nodeValueSet.insert(nv);
  42 }
  43
  44 // general expression-builders
  45
  46 Node NodeManager::mkNode(Kind kind) {
  47   return NodeBuilder<>(this, kind);
  48 }
  49
  50 Node NodeManager::mkNode(Kind kind, const Node& child1) {
  51   return NodeBuilder<>(this, kind) << child1;
  52 }
  53
  54 Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) {
  55   return NodeBuilder<>(this, kind) << child1 << child2;
  56 }
  57
  58 Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
  59   return NodeBuilder<>(this, kind) << child1 << child2 << child3;
  60 }
  61
  62 Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
  63   return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
  64 }
  65
  66 Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
  67   return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
  68 }
  69
  70 // N-ary version
  71 Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
  72   return NodeBuilder<>(this, kind).append(children);
  73 }
  74
  75 Node NodeManager::mkVar(const Type* type, string name) {
  76   Node n = mkVar(type);
  77   n.setAttribute(VarNameAttr(), name);
  78   return n;
  79 }
  80
  81 Node NodeManager::mkVar(const Type* type) {
  82   Node n = NodeBuilder<>(this, VARIABLE);
  83   n.setAttribute(TypeAttr(), type);
  84   return n;
  85 }
  86
  87 Node NodeManager::mkVar() {
  88   return NodeBuilder<>(this, VARIABLE);
  89 }
  90
  91 }/* CVC4 namespace */