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.

4 files changed, 32 insertions, 32 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 16bde1de3..3f4435966 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -123,7 +123,7 @@ command returns [CVC4::Command* cmd = 0]
 declaration[CVC4::Command*& cmd]
 @init {
   std::vector<std::string> ids;
-  Type* t;
+  Type t;
   Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : // FIXME: These could be type or function declarations, if that matters.
@@ -132,7 +132,7 @@ declaration[CVC4::Command*& cmd]
   ;
 
 /** Match the right-hand side of a declaration. Returns the type. */
-declType[CVC4::Type*& t, std::vector<std::string>& idList]
+declType[CVC4::Type& t, std::vector<std::string>& idList]
 @init {
   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
@@ -148,10 +148,10 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
  * Match the type in a declaration and do the declaration binding.
  * TODO: Actually parse sorts into Type objects.
  */
-type[CVC4::Type*& t]
+type[CVC4::Type& t]
 @init {
-  Type* t2;
-  std::vector<Type*> typeList;
+  Type t2;
+  std::vector<Type> typeList;
   Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* Simple type */
@@ -199,7 +199,7 @@ identifier[std::string& id,
  * Matches a type.
  * TODO: parse more types
  */
-baseType[CVC4::Type*& t]
+baseType[CVC4::Type& t]
 @init {
   std::string id;
   Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
@@ -211,7 +211,7 @@ baseType[CVC4::Type*& t]
 /**
  * Matches a type identifier
  */
-typeSymbol[CVC4::Type*& t]
+typeSymbol[CVC4::Type& t]
 @init {
   std::string id;
   Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 5f07b16b7..57914c9de 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -62,38 +62,38 @@ Expr ParserState::getVariable(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
-Type*
+Type
 ParserState::getType(const std::string& var_name,
                      SymbolType type) {
   Assert( isDeclared(var_name, type) );
-  Type* t = getSymbol(var_name,type).getType();
+  Type t = getSymbol(var_name,type).getType();
   return t;
 }
 
-Type* ParserState::getSort(const std::string& name) {
+Type ParserState::getSort(const std::string& name) {
   Assert( isDeclared(name, SYM_SORT) );
-  Type *t = d_declScope.lookupType(name);
+  Type t = d_declScope.lookupType(name);
   return t;
 }
 
 /* Returns true if name is bound to a boolean variable. */
 bool ParserState::isBoolean(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean();
+  return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
 }
 
 /* Returns true if name is bound to a function. */
 bool ParserState::isFunction(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction();
+  return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
 }
 
 /* Returns true if name is bound to a function returning boolean. */
 bool ParserState::isPredicate(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
+  return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 }
 
 Expr 
-ParserState::mkVar(const std::string& name, Type* type) {
-  Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
+ParserState::mkVar(const std::string& name, const Type& type) {
+  Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
   defineVar(name,expr);
   return expr;
@@ -101,7 +101,7 @@ ParserState::mkVar(const std::string& name, Type* type) {
 
 const std::vector<Expr>
 ParserState::mkVars(const std::vector<std::string> names,
-                    Type* type) {
+                    const Type& type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
     vars.push_back(mkVar(names[i],type));
@@ -134,19 +134,19 @@ ParserState::setLogic(const std::string& name) {
   }
 }
 
-Type*
+Type
 ParserState::mkSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Assert( !isDeclared(name, SYM_SORT) ) ;
-  Type* type = d_exprManager->mkSort(name);
+  Type type = d_exprManager->mkSort(name);
   d_declScope.bindType(name, type);
   Assert( isDeclared(name, SYM_SORT) ) ;
   return type;
 }
 
-const std::vector<Type*>
+const std::vector<Type>
 ParserState::mkSorts(const std::vector<std::string>& names) {
-  std::vector<Type*> types;
+  std::vector<Type> types;
   for(unsigned i = 0; i < names.size(); ++i) {
     types.push_back(mkSort(names[i]));
   }
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index de624e3a0..3ca9c2c0e 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -174,7 +174,7 @@ public:
   /**
    * Returns a sort, given a name
    */
-  Type* getSort(const std::string& sort_name);
+  Type getSort(const std::string& sort_name);
 
   /**
    * Checks if a symbol has been declared.
@@ -216,15 +216,15 @@ public:
    * @param var_name the symbol to lookup
    * @param type the (namespace) type of the symbol
    */
-  Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
+  Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
 
   /** Create a new CVC4 variable expression of the given type. */
-  Expr mkVar(const std::string& name, Type* type);
+  Expr mkVar(const std::string& name, const Type& type);
 
   /** Create a set of new CVC4 variable expressions of the given
    type. */
   const std::vector<Expr>
-  mkVars(const std::vector<std::string> names, Type* type);
+  mkVars(const std::vector<std::string> names, const Type& type);
 
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val);
@@ -234,12 +234,12 @@ public:
   /**
    * Creates a new sort with the given name.
    */
-  Type* mkSort(const std::string& name);
+  Type mkSort(const std::string& name);
 
   /**
    * Creates a new sorts with the given names.
    */
-  const std::vector<Type*>
+  const std::vector<Type>
   mkSorts(const std::vector<std::string>& names);
 
   /** Is the symbol bound to a boolean variable? */
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 25c2fbc89..15f0c8844 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -285,7 +285,7 @@ attribute
 functionDeclaration
 @declarations {
   std::string name;
-  std::vector<Type*> sorts;
+  std::vector<Type> sorts;
 }
   : LPAREN_TOK functionName[name,CHECK_UNDECLARED] 
       t = sortSymbol // require at least one sort
@@ -305,10 +305,10 @@ functionDeclaration
 predicateDeclaration
 @declarations {
   std::string name;
-  std::vector<Type*> p_sorts;
+  std::vector<Type> p_sorts;
 }
   : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
-    { Type *t;
+    { Type t;
       if( p_sorts.empty() ) {
         t = EXPR_MANAGER->booleanType();
       } else { 
@@ -329,7 +329,7 @@ sortDeclaration
 /**
  * Matches a sequence of sort symbols and fills them into the given vector.
  */
-sortList[std::vector<CVC4::Type*>& sorts]
+sortList[std::vector<CVC4::Type>& sorts]
   : ( t = sortSymbol { sorts.push_back(t); })* 
   ;
 
@@ -341,7 +341,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check]
   : identifier[name,check,SYM_SORT] 
   ;
 
-sortSymbol returns [CVC4::Type* t]
+sortSymbol returns [CVC4::Type t]
 @declarations {
   std::string name;
 }