Marging from types 404:415, changes: Massive

* Types are now represented as nodes in the attribute table and are managed, i.e. you can say
    Type booleanType = d_nodeManager->booleanType();
    Type t = d_nodeManager->mkFunctionType(booleanType, booleanType);
    FunctionType ft = (FunctionType)t;
    Assert(ft.getArgTypes()[0], booleanType);
* The attributes now have a table for Nodes and a table for TNodes (both should be used with caution)
* Changes the way nodes are extracted from NodeBuilder, added several methods to
  extract a Node, NodeValue, or Node*, with corresponding methods for extraction
* Used the above in the construction of Expr and Type objects
* The NodeManager now destroys the attributes in the destructor by pausing the
  garbage collection
* To achive destruction a flag d_inDesctruction has been added to loosen the assertion
  in NodeValue::dec() (there might be -refcount TNodes leftover)
* Beginnings of the Bitvector constants using GMP

Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs.

I hate branching and merging.

1 files changed, 52 insertions, 0 deletions

diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
new file mode 100644
index 000000000..38f8fc787
--- /dev/null
+++ b/src/expr/expr_manager_scope.h
@@ -0,0 +1,52 @@
+/*
+ * expr_manager_scope.h
+ *
+ *  Created on: Apr 7, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__EXPR_MANAGER_SCOPE_H
+#define __CVC4__EXPR_MANAGER_SCOPE_H
+
+#include "expr/expr.h"
+#include "expr/node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * Creates a <code>NodeManagerScope</code> with the underlying
+ * <code>NodeManager</code> of a given <code>Expr</code> or
+ * <code>ExprManager</code>.  The <code>NodeManagerScope</code> is
+ * destroyed when the <code>ExprManagerScope</code> is destroyed. See
+ * <code>NodeManagerScope</code> for more information.
+ */
+// NOTE: Here, it seems ExprManagerScope is redundant, since we have
+// NodeManagerScope already.  However, without this class, we'd need
+// Expr to be a friend of ExprManager, because in the implementation
+// of Expr functions, it needs to set the current NodeManager
+// correctly (and to do that it needs access to
+// ExprManager::getNodeManager()).  So, we make ExprManagerScope a
+// friend of ExprManager's, since its implementation is simple to
+// read and understand (and verify that it doesn't do any mischief).
+//
+// ExprManager::getNodeManager() can't just be made public, since
+// ExprManager is exposed to clients of the library and NodeManager is
+// not.  Similarly, ExprManagerScope shouldn't go in expr_manager.h,
+// since that's a public header.
+class ExprManagerScope {
+  NodeManagerScope d_nms;
+public:
+  inline ExprManagerScope(const Expr& e) :
+    d_nms(e.getExprManager() == NULL
+          ? NodeManager::currentNM()
+          : e.getExprManager()->getNodeManager()) {
+  }
+  inline ExprManagerScope(const ExprManager& exprManager) :
+    d_nms(exprManager.getNodeManager()) {
+  }
+};
+
+}
+
+
+#endif /* __CVC4__EXPR_MANAGER_SCOPE_H */