* test/unit/Makefile.am, test/unit/expr/attribute_white.h,

  test/unit/expr/node_white.h: add whitebox attribute test (pulled out
  attribute stuff from node_white)

* test/unit/parser/parser_black.h: fix memory leaks uncovered by
  valgrind

* src/theory/interrupted.h: actually make this "lightweight" (not
  derived from CVC4::Exception), as promised in my last commit

* src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match
  the new-style cleanup function definition

* src/expr/attribute.cpp, src/expr/attribute.h: support for attribute
  deletion, custom cleanup functions, clearer cleanup function
  definition.

* src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim
  remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool",
  and enable freeing of NodeValues

* src/expr/type.h, src/expr/type.cpp: reference-counting for types,
  customized cleanup function for types, also code cleanup

* (various): changed "const Type*" to "Type*" (to enable
  reference-counting etc.  Types are still immutable.)

* src/util/output.h: add ::isOn()-- which queries whether a
  Debug/Trace flag is currently on or not.

* src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp,
  src/expr/type.cpp, src/expr/expr_manager.cpp, various others:
  minor code cleanup

5 files changed, 121 insertions, 130 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 593a89873..d20e59db3 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -60,7 +60,7 @@ Expr AntlrParser::getSymbol(const std::string& name, SymbolType type) {
     return d_varSymbolTable.getObject(name);
 
   default:
-    Unhandled("Unhandled symbol type!");
+    Unhandled(type);
   }
 }
 
@@ -72,17 +72,16 @@ Expr AntlrParser::getFunction(const std::string& name) {
   return getSymbol(name, SYM_FUNCTION);
 }
 
-const Type* 
-AntlrParser::getType(const std::string& var_name,
-                     SymbolType type) {
+Type* AntlrParser::getType(const std::string& var_name,
+                           SymbolType type) {
   Assert( isDeclared(var_name, type) );
-  const Type* t = getSymbol(var_name,type).getType();
+  Type* t = getSymbol(var_name, type).getType();
   return t;
 }
 
-const Type* AntlrParser::getSort(const std::string& name) {
+Type* AntlrParser::getSort(const std::string& name) {
   Assert( isDeclared(name, SYM_SORT) );
-  const Type* t = d_sortTable.getObject(name);
+  Type* t = d_sortTable.getObject(name);
   return t;
 }
 
@@ -134,33 +133,30 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
   return result;
 }
 
-const Type* 
-AntlrParser::functionType(const Type* domainType, 
-                          const Type* rangeType) {
-  return d_exprManager->mkFunctionType(domainType,rangeType);
+Type* AntlrParser::functionType(Type* domainType,
+                                Type* rangeType) {
+  return d_exprManager->mkFunctionType(domainType, rangeType);
 }
 
-const Type* 
-AntlrParser::functionType(const std::vector<const Type*>& argTypes, 
-                          const Type* rangeType) {
+Type* AntlrParser::functionType(const std::vector<Type*>& argTypes,
+                                Type* rangeType) {
   Assert( argTypes.size() > 0 );
-  return d_exprManager->mkFunctionType(argTypes,rangeType);
+  return d_exprManager->mkFunctionType(argTypes, rangeType);
 }
 
-const Type* 
-AntlrParser::functionType(const std::vector<const Type*>& sorts) {
+Type* AntlrParser::functionType(const std::vector<Type*>& sorts) {
   Assert( sorts.size() > 0 );
   if( sorts.size() == 1 ) {
     return sorts[0];
   } else {
-    std::vector<const Type*> argTypes(sorts);
-    const Type* rangeType = argTypes.back();
+    std::vector<Type*> argTypes(sorts);
+    Type* rangeType = argTypes.back();
     argTypes.pop_back();
-    return functionType(argTypes,rangeType);
+    return functionType(argTypes, rangeType);
   }
 }
 
-const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
+Type* AntlrParser::predicateType(const std::vector<Type*>& sorts) {
   if(sorts.size() == 0) {
     return d_exprManager->booleanType();
   } else {
@@ -168,17 +164,16 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
   }
 }
 
-Expr 
-AntlrParser::mkVar(const std::string& name, const Type* type) {
+Expr AntlrParser::mkVar(const std::string& name, Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(type, name);
-  defineVar(name,expr);
+  defineVar(name, expr);
   return expr;
 }
 
-const std::vector<Expr> 
-AntlrParser::mkVars(const std::vector<std::string> names, 
-                    const Type* type) {
+const std::vector<Expr>
+AntlrParser::mkVars(const std::vector<std::string> names,
+                    Type* type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
     vars.push_back(mkVar(names[i], type));
@@ -186,55 +181,51 @@ AntlrParser::mkVars(const std::vector<std::string> names,
   return vars;
 }
 
-void
-AntlrParser::defineVar(const std::string& name, const Expr& val) {
+void AntlrParser::defineVar(const std::string& name, const Expr& val) {
   Assert(!isDeclared(name));
-  d_varSymbolTable.bindName(name,val);
+  d_varSymbolTable.bindName(name, val);
   Assert(isDeclared(name));
 }
 
-void
-AntlrParser::undefineVar(const std::string& name) {
+void AntlrParser::undefineVar(const std::string& name) {
   Assert(isDeclared(name));
   d_varSymbolTable.unbindName(name);
   Assert(!isDeclared(name));
 }
 
 
-const Type* 
-AntlrParser::newSort(const std::string& name) {
+Type* AntlrParser::newSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Assert( !isDeclared(name, SYM_SORT) );
-  const Type* type = d_exprManager->mkSort(name);
+  Type* type = d_exprManager->mkSort(name);
   d_sortTable.bindName(name, type);
   Assert( isDeclared(name, SYM_SORT) );
   return type;
 }
 
-const std::vector<const Type*>
+const std::vector<Type*>
 AntlrParser::newSorts(const std::vector<std::string>& names) {
-  std::vector<const Type*> types;
+  std::vector<Type*> types;
   for(unsigned i = 0; i < names.size(); ++i) {
     types.push_back(newSort(names[i]));
   }
   return types;
 }
 
-void
-AntlrParser::setLogic(const std::string& name) {
+void AntlrParser::setLogic(const std::string& name) {
   if( name == "QF_UF" ) {
     newSort("U");
   } else {
-    Unhandled("setLogic: " + name);
+    Unhandled(name);
   }
 }
 
-const BooleanType* AntlrParser::booleanType() {
-  return d_exprManager->booleanType(); 
+BooleanType* AntlrParser::booleanType() {
+  return d_exprManager->booleanType();
 }
 
-const KindType* AntlrParser::kindType() {
-  return d_exprManager->kindType(); 
+KindType* AntlrParser::kindType() {
+  return d_exprManager->kindType();
 }
 
 unsigned int AntlrParser::minArity(Kind kind) {
@@ -251,7 +242,7 @@ unsigned int AntlrParser::minArity(Kind kind) {
     return 1;
 
   case APPLY:
-  case EQUAL: 
+  case EQUAL:
   case IFF:
   case IMPLIES:
   case PLUS:
@@ -262,7 +253,7 @@ unsigned int AntlrParser::minArity(Kind kind) {
     return 3;
 
   default:
-    Unhandled("kind in minArity");
+    Unhandled(kind);
   }
 }
 
@@ -277,7 +268,7 @@ unsigned int AntlrParser::maxArity(Kind kind) {
   case NOT:
     return 1;
 
-  case EQUAL: 
+  case EQUAL:
   case IFF:
   case IMPLIES:
   case XOR:
@@ -293,7 +284,7 @@ unsigned int AntlrParser::maxArity(Kind kind) {
     return UINT_MAX;
 
   default:
-    Unhandled("kind in maxArity");
+    Unhandled(kind);
   }
 }
 
@@ -309,7 +300,7 @@ bool AntlrParser::isDeclared(const std::string& name, SymbolType type) {
   case SYM_SORT:
     return d_sortTable.isBound(name);
   default:
-    Unhandled("Unhandled symbol type!");
+    Unhandled(type);
   }
 }
 
@@ -345,7 +336,7 @@ void AntlrParser::checkDeclaration(const std::string& varName,
     break;
 
   default:
-    Unhandled("Unknown check type!");
+    Unhandled(check);
   }
 }
 
@@ -353,7 +344,7 @@ void AntlrParser::checkFunction(const std::string& name)
   throw (antlr::SemanticException) {
   if( d_checksEnabled && !isFunction(name) ) {
     parseError("Expecting function symbol, found '" + name + "'");
-  } 
+  }
 }
 
 void AntlrParser::checkArity(Kind kind, unsigned int numArgs)
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 94d919555..e970ebd52 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -137,7 +137,7 @@ protected:
   /**
    * Returns a sort, given a name
    */
-  const Type* getSort(const std::string& sort_name);
+  Type* getSort(const std::string& sort_name);
 
   /**
    * Types of symbols. Used to define namespaces.
@@ -193,7 +193,7 @@ protected:
    * @param name the symbol to lookup 
    * @param type the (namespace) type of the symbol
    */
-  const Type* getType(const std::string& var_name,
+  Type* getType(const std::string& var_name,
                       SymbolType type = SYM_VARIABLE);
 
   /**
@@ -244,13 +244,13 @@ protected:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /** Create a new CVC4 variable expression of the given type. */
-  Expr mkVar(const std::string& name, const Type* type);
+  Expr mkVar(const std::string& name, 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, 
-         const Type* type);
+         Type* type);
 
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val);
@@ -258,12 +258,12 @@ protected:
   void undefineVar(const std::string& name);
 
   /** Returns a function type over the given domain and range types. */
-  const Type* functionType(const Type* domain, const Type* range);
+  Type* functionType(Type* domain, Type* range);
 
   /** Returns a function type over the given types. argTypes must be
       non-empty. */
-  const Type* functionType(const std::vector<const Type*>& argTypes,
-                           const Type* rangeType);
+  Type* functionType(const std::vector<Type*>& argTypes,
+                     Type* rangeType);
 
   /** 
    * Returns a function type over the given types. If types has only
@@ -271,7 +271,7 @@ protected:
    *
    * @param types a non-empty list of input and output types. 
    */
-  const Type* functionType(const std::vector<const Type*>& types);
+  Type* functionType(const std::vector<Type*>& types);
 
   /** 
    * Returns a predicate type over the given sorts. If sorts is empty,
@@ -279,17 +279,17 @@ protected:
 
    * @param sorts a list of input types
    */
-  const Type* predicateType(const std::vector<const Type*>& sorts);
+  Type* predicateType(const std::vector<Type*>& sorts);
 
   /**
    * Creates a new sort with the given name.
    */
-  const Type* newSort(const std::string& name);
+  Type* newSort(const std::string& name);
 
   /**
    * Creates a new sorts with the given names.
    */
-  const std::vector<const Type*>
+  const std::vector<Type*>
   newSorts(const std::vector<std::string>& names);
 
   /** Is the symbol bound to a boolean variable? */
@@ -302,10 +302,10 @@ protected:
   bool isPredicate(const std::string& name);
 
   /** Returns the boolean type. */
-  const BooleanType* booleanType();
+  BooleanType* booleanType();
 
   /** Returns the kind type (i.e., the type of types). */
-  const KindType* kindType();
+  KindType* kindType();
 
   /** Returns the minimum arity of the given kind. */
   static unsigned int minArity(Kind kind);
@@ -346,7 +346,7 @@ private:
   SymbolTable<Expr> d_varSymbolTable;
 
   /** The sort table */
-  SymbolTable<const Type*> d_sortTable;
+  SymbolTable<Type*> d_sortTable;
 
   /** Are semantic checks enabled during parsing? */
   bool d_checksEnabled;
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 9492b36d9..55ae0ff73 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -89,15 +89,15 @@ command returns [CVC4::Command* cmd = 0]
 declaration returns [CVC4::DeclarationCommand* cmd]
 {
   vector<string> ids;
-  const Type* t;
+  Type* t;
   Debug("parser") << "declaration: " << LT(1)->getText() << endl;
-} 
+}
   : identifierList[ids, CHECK_UNDECLARED] COLON t = declType[ids] SEMICOLON
     { cmd = new DeclarationCommand(ids,t); }
   ;
 
 /** Match the right-hand side of a declaration. Returns the type. */
-declType[std::vector<std::string>& idList] returns [const CVC4::Type* t]
+declType[std::vector<std::string>& idList] returns [CVC4::Type* t]
 {
   Debug("parser") << "declType: " << LT(1)->getText() << endl;
 }
@@ -111,9 +111,9 @@ declType[std::vector<std::string>& idList] returns [const CVC4::Type* t]
  * Match the type in a declaration and do the declaration binding.
  * TODO: Actually parse sorts into Type objects.
  */
-type returns  [const CVC4::Type* t]
+type returns  [CVC4::Type* t]
 {
-  const Type *t1, *t2;
+  Type *t1, *t2;
   Debug("parser") << "type: " << LT(1)->getText() << endl;
 }
   : /* Simple type */
@@ -122,10 +122,10 @@ type returns  [const CVC4::Type* t]
     t1 = baseType RIGHT_ARROW t2 = baseType
     { t = functionType(t1,t2); }
   | /* Multi-parameter function type */
-    LPAREN t1 = baseType 
-    { std::vector<const Type*> argTypes;
+    LPAREN t1 = baseType
+    { std::vector<Type*> argTypes;
       argTypes.push_back(t1); }
-    (COMMA t1 = baseType { argTypes.push_back(t1); } )+ 
+    (COMMA t1 = baseType { argTypes.push_back(t1); } )+
     RPAREN RIGHT_ARROW t2 = baseType
     { t = functionType(argTypes,t2); }
   ;
@@ -136,7 +136,7 @@ type returns  [const CVC4::Type* t]
  * @param idList the list to fill with identifiers.
  * @param check what kinds of check to perform on the symbols
  */
-identifierList[std::vector<std::string>& idList, 
+identifierList[std::vector<std::string>& idList,
                DeclarationCheck check = CHECK_NONE]
 {
   string id;
@@ -150,10 +150,10 @@ identifierList[std::vector<std::string>& idList,
  * Matches an identifier and returns a string.
  */
 identifier[DeclarationCheck check = CHECK_NONE,
-           SymbolType type = SYM_VARIABLE] 
+           SymbolType type = SYM_VARIABLE]
 returns [std::string id]
   : x:IDENTIFIER
-    { id = x->getText(); 
+    { id = x->getText();
       checkDeclaration(id, check, type); }
   ;
 
@@ -161,7 +161,7 @@ returns [std::string id]
  * Matches a type.
  * TODO: parse more types
  */
-baseType returns [const CVC4::Type* t]
+baseType returns [CVC4::Type* t]
 {
   std::string id;
   Debug("parser") << "base type: " << LT(1)->getText() << endl;
@@ -173,7 +173,7 @@ baseType returns [const CVC4::Type* t]
 /**
  * Matches a type identifier
  */
-typeSymbol returns [const CVC4::Type* t]
+typeSymbol returns [CVC4::Type* t]
 {
   std::string id;
   Debug("parser") << "type symbol: " << LT(1)->getText() << endl;
@@ -228,7 +228,7 @@ impliesFormula returns [CVC4::Expr f]
   Expr e;
   Debug("parser") << "=> Formula: " << LT(1)->getText() << endl;
 }
-  : f = orFormula 
+  : f = orFormula
     ( IMPLIES e = impliesFormula
         { f = mkExpr(CVC4::kind::IMPLIES, f, e); }
     )?
@@ -259,7 +259,7 @@ xorFormula returns [CVC4::Expr f]
   Debug("parser") << "XOR formula: " << LT(1)->getText() << endl;
 }
   : f = andFormula
-    ( XOR e = andFormula 
+    ( XOR e = andFormula
       { f = mkExpr(CVC4::kind::XOR,f, e); }
     )*
   ;
@@ -289,7 +289,7 @@ notFormula returns [CVC4::Expr f]
   Debug("parser") << "NOT formula: " << LT(1)->getText() << endl;
 }
   : /* negation */
-    NOT f = notFormula 
+    NOT f = notFormula
     { f = mkExpr(CVC4::kind::NOT, f); }
   | /* a boolean atom */
     f = predFormula
@@ -300,7 +300,7 @@ predFormula returns [CVC4::Expr f]
   Debug("parser") << "predicate formula: " << LT(1)->getText() << endl;
 }
   : { Expr e; }
-    f = term 
+    f = term
     (EQUAL e = term
       { f = mkExpr(CVC4::kind::EQUAL, f, e); }
     )?
@@ -315,8 +315,8 @@ term returns [CVC4::Expr t]
   Debug("parser") << "term: " << LT(1)->getText() << endl;
 }
   : /* function application */
-    // { isFunction(LT(1)->getText()) }? 
-    { Expr f; 
+    // { isFunction(LT(1)->getText()) }?
+    { Expr f;
       std::vector<CVC4::Expr> args; }
     f = functionSymbol[CHECK_DECLARED]
     { args.push_back( f ); }
@@ -343,16 +343,16 @@ term returns [CVC4::Expr t]
 /**
  * Parses an ITE term.
  */
-iteTerm returns [CVC4::Expr t] 
+iteTerm returns [CVC4::Expr t]
 {
   Expr iteCondition, iteThen, iteElse;
   Debug("parser") << "ite: " << LT(1)->getText() << endl;
 }
-  : IF iteCondition = formula 
+  : IF iteCondition = formula
     THEN iteThen = formula
     iteElse = iteElseTerm
-    ENDIF     
-    { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); }  
+    ENDIF
+    { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); }
   ;
 
 /**
@@ -379,8 +379,8 @@ functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f]
 {
   Debug("parser") << "function symbol: " << LT(1)->getText() << endl;
   std::string name;
-}  
+}
   : name = identifier[check,SYM_FUNCTION]
-    { checkFunction(name);  
+    { checkFunction(name);
       f = getFunction(name); }
   ;
diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index e3985818c..d694cd93f 100644
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -115,11 +115,11 @@ C_IDENTIFIER options { paraphrase = "an attribute (e.g., ':x')"; testLiterals =
   ;
 
 VAR_IDENTIFIER options { paraphrase = "a variable (e.g., '?x')"; testLiterals = false; }
-  :  '?' IDENTIFIER 
+  :  '?' IDENTIFIER
   ;
 
 FUN_IDENTIFIER options { paraphrase = "a function variable (e.g, '$x')"; testLiterals = false; }
-  :  '$' IDENTIFIER 
+  :  '$' IDENTIFIER
   ;
 
 
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index d1ac50651..f9758dc5c 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -102,12 +102,12 @@ benchAttribute returns [Command* smt_command = 0]
     { smt_command = new AssertCommand(formula);   }
   | FORMULA_ATTR formula = annotatedFormula
     { smt_command = new CheckSatCommand(formula); }
-  | STATUS_ATTR b_status = status                   
-    { smt_command = new SetBenchmarkStatusCommand(b_status); }        
-  | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN  
-  | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN  
-  | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN  
-  | NOTES_ATTR STRING_LITERAL        
+  | STATUS_ATTR b_status = status
+    { smt_command = new SetBenchmarkStatusCommand(b_status); }
+  | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN
+  | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
+  | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN
+  | NOTES_ATTR STRING_LITERAL
   | annotation
   ;
 
@@ -119,12 +119,12 @@ annotatedFormula returns [CVC4::Expr formula]
 {
   Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
   Kind kind = CVC4::kind::UNDEFINED_KIND;
-  vector<Expr> args; 
+  vector<Expr> args;
   std::string name;
   Expr expr1, expr2, expr3;
 }
   : /* a built-in operator application */
-    LPAREN kind = builtinOp annotatedFormulas[args] RPAREN 
+    LPAREN kind = builtinOp annotatedFormulas[args] RPAREN
     { checkArity(kind, args.size());
       formula = mkExpr(kind,args); }
 
@@ -134,16 +134,16 @@ annotatedFormula returns [CVC4::Expr formula]
     { std::vector<Expr> diseqs;
       for(unsigned i = 0; i < args.size(); ++i) {
         for(unsigned j = i+1; j < args.size(); ++j) {
-          diseqs.push_back(mkExpr(CVC4::kind::NOT, 
+          diseqs.push_back(mkExpr(CVC4::kind::NOT,
                                   mkExpr(CVC4::kind::EQUAL,args[i],args[j])));
         }
       }
       formula = mkExpr(CVC4::kind::AND, diseqs); }
 
   | /* An ite expression */
-    LPAREN (ITE | IF_THEN_ELSE) 
+    LPAREN (ITE | IF_THEN_ELSE)
     { Expr test, trueExpr, falseExpr; }
-    test = annotatedFormula 
+    test = annotatedFormula
     trueExpr = annotatedFormula
     falseExpr = annotatedFormula
     RPAREN
@@ -164,12 +164,12 @@ annotatedFormula returns [CVC4::Expr formula]
     formula=annotatedFormula
     { undefineVar(name); }
     RPAREN
-    
+
   | /* A non-built-in function application */
 
     // Semantic predicate not necessary if parenthesized subexpressions
     // are disallowed
-    // { isFunction(LT(2)->getText()) }? 
+    // { isFunction(LT(2)->getText()) }?
 
     { Expr f; }
     LPAREN f = functionSymbol
@@ -180,7 +180,7 @@ annotatedFormula returns [CVC4::Expr formula]
 
   | /* a variable */
     { std::string name; }
-    ( name = identifier[CHECK_DECLARED] 
+    ( name = identifier[CHECK_DECLARED]
       | name = variable[CHECK_DECLARED]
       | name = function_var[CHECK_DECLARED] )
     { formula = getVariable(name); }
@@ -195,7 +195,7 @@ annotatedFormula returns [CVC4::Expr formula]
  * Matches a sequence of annotaed formulas and puts them into the formulas
  * vector.
  * @param formulas the vector to fill with formulas
- */   
+ */
 annotatedFormulas[std::vector<Expr>& formulas]
 {
   Expr f;
@@ -222,7 +222,7 @@ builtinOp returns [CVC4::Kind kind]
   ;
 
 /**
- * Matches a (possibly undeclared) predicate identifier (returning the string). 
+ * Matches a (possibly undeclared) predicate identifier (returning the string).
  * @param check what kind of check to do with the symbol
  */
 predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p]
@@ -241,14 +241,14 @@ functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
  * Matches an previously declared function symbol (returning an Expr)
  */
 functionSymbol returns [CVC4::Expr fun]
-{ 
+{
   string name;
 }
   : name = functionName[CHECK_DECLARED]
     { checkFunction(name);
       fun = getFunction(name); }
   ;
-  
+
 /**
  * Matches an attribute name from the input (:attribute_name).
  */
@@ -272,12 +272,12 @@ function_var[DeclarationCheck check = CHECK_NONE] returns [std::string name]
  * Matches the sort symbol, which can be an arbitrary identifier.
  * @param check the check to perform on the name
  */
-sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] 
-  : name = identifier[check,SYM_SORT] 
+sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+  : name = identifier[check,SYM_SORT]
   ;
 
-sortSymbol returns [const CVC4::Type* t]
-{ 
+sortSymbol returns [CVC4::Type* t]
+{
   std::string name;
 }
   : name = sortName { t = getSort(name); }
@@ -286,47 +286,47 @@ sortSymbol returns [const CVC4::Type* t]
 functionDeclaration
 {
   string name;
-  const Type* t;
-  std::vector<const Type*> sorts;
+  Type* t;
+  std::vector<Type*> sorts;
 }
-  : LPAREN name = functionName[CHECK_UNDECLARED] 
+  : LPAREN name = functionName[CHECK_UNDECLARED]
       t = sortSymbol // require at least one sort
     { sorts.push_back(t); }
       sortList[sorts] RPAREN
     { t = functionType(sorts);
-      mkVar(name, t); } 
+      mkVar(name, t); }
   ;
-              
+
 /**
  * Matches the declaration of a predicate and declares it
  */
 predicateDeclaration
 {
   string p_name;
-  std::vector<const Type*> p_sorts;
-  const Type *t;
+  std::vector<Type*> p_sorts;
+  Type *t;
 }
   : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN
     { t = predicateType(p_sorts);
-      mkVar(p_name, t); } 
+      mkVar(p_name, t); }
   ;
 
-sortDeclaration 
+sortDeclaration
 {
   string name;
 }
   : name = sortName[CHECK_UNDECLARED]
     { newSort(name); }
   ;
-  
+
 /**
  * Matches a sequence of sort symbols and fills them into the given vector.
  */
-sortList[std::vector<const Type*>& sorts]
+sortList[std::vector<Type*>& sorts]
 {
-  const Type* t;
+  Type* t;
 }
-  : ( t = sortSymbol { sorts.push_back(t); })* 
+  : ( t = sortSymbol { sorts.push_back(t); })*
   ;
 
 /**
@@ -350,11 +350,11 @@ annotation
  * @param check what kinds of check to do on the symbol
  * @return the id string
  */
-identifier[DeclarationCheck check = CHECK_NONE, 
-           SymbolType type = SYM_VARIABLE] 
+identifier[DeclarationCheck check = CHECK_NONE,
+           SymbolType type = SYM_VARIABLE]
 returns [std::string id]
 {
-  Debug("parser") << "identifier: " << LT(1)->getText() 
+  Debug("parser") << "identifier: " << LT(1)->getText()
                   << " check? " << toString(check)
                   << " type? " << toString(type) << endl;
 }