Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

1 files changed, 10 insertions, 5 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 15fe5126c..718b862ab 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -263,7 +263,7 @@ public:
    * @throws ParserException if checks are enabled and name is not
    * bound to a function
    */
-  void checkFunction(const std::string& name) throw (ParserException);
+  void checkFunctionLike(const std::string& name) throw (ParserException);
 
   /**
    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
@@ -337,8 +337,13 @@ public:
   /**
    * Creates new sorts with the given names (all of arity 0).
    */
-  const std::vector<Type>
-  mkSorts(const std::vector<std::string>& names);
+  std::vector<Type> mkSorts(const std::vector<std::string>& names);
+
+  /**
+   * Create sorts of mutually-recursive datatypes.
+   */
+  std::vector<DatatypeType>
+  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
 
   /**
    * Add an operator to the current legal set.
@@ -357,8 +362,8 @@ public:
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
 
-  /** Is the symbol bound to a function? */
-  bool isFunction(const std::string& name);
+  /** Is the symbol bound to a function (or function-like thing)? */
+  bool isFunctionLike(const std::string& name);
 
   /** Is the symbol bound to a defined function? */
   bool isDefinedFunction(const std::string& name);