Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

1 files changed, 81 insertions, 24 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 718b862ab..25fb30be6 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -55,18 +55,20 @@ enum DeclarationCheck {
   CHECK_NONE
 };
 
-/** Returns a string representation of the given object (for
- debugging). */
-inline std::string toString(DeclarationCheck check) {
+/**
+ * Returns a string representation of the given object (for
+ * debugging).
+ */
+inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) {
   switch(check) {
   case CHECK_NONE:
-    return "CHECK_NONE";
+    return out << "CHECK_NONE";
   case CHECK_DECLARED:
-    return "CHECK_DECLARED";
+    return out << "CHECK_DECLARED";
   case CHECK_UNDECLARED:
-    return "CHECK_UNDECLARED";
+    return out << "CHECK_UNDECLARED";
   default:
-    Unreachable();
+    return out << "DeclarationCheck!UNKNOWN";
   }
 }
 
@@ -80,16 +82,18 @@ enum SymbolType {
   SYM_SORT
 };
 
-/** Returns a string representation of the given object (for
- debugging). */
-inline std::string toString(SymbolType type) {
+/**
+ * Returns a string representation of the given object (for
+ * debugging).
+ */
+inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
-    return "SYM_VARIABLE";
+    return out << "SYM_VARIABLE";
   case SYM_SORT:
-    return "SYM_SORT";
+    return out << "SYM_SORT";
   default:
-    Unreachable();
+    return out << "SymbolType!UNKNOWN";
   }
 }
 
@@ -133,10 +137,22 @@ class CVC4_PUBLIC Parser {
   /** Are we parsing in strict mode? */
   bool d_strictMode;
 
+  /** Are we only parsing? */
+  bool d_parseOnly;
+
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
   /**
+   * The current set of unresolved types.  We can get by with this NOT
+   * being on the scope, because we can only have one DATATYPE
+   * definition going on at one time.  This is a bit hackish; we
+   * depend on mkMutualDatatypeTypes() to check everything and clear
+   * this out.
+   */
+  std::set<SortType> d_unresolved;
+
+  /**
    * "Preemption commands": extra commands implied by subterms that
    * should be issued before the currently-being-parsed command is
    * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
@@ -155,7 +171,7 @@ protected:
    * @param input the parser input
    * @param strictMode whether to incorporate strict(er) compliance checks
    */
-  Parser(ExprManager* exprManager, Input* input, bool strictMode = false);
+  Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
 
 public:
 
@@ -255,7 +271,7 @@ public:
    * @throws ParserException if checks are enabled and the check fails
    */
   void checkDeclaration(const std::string& name, DeclarationCheck check,
-                        SymbolType type = SYM_VARIABLE) throw (ParserException);
+                        SymbolType type = SYM_VARIABLE) throw(ParserException);
 
   /**
    * Checks whether the given name is bound to a function.
@@ -263,7 +279,7 @@ public:
    * @throws ParserException if checks are enabled and name is not
    * bound to a function
    */
-  void checkFunctionLike(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.
@@ -273,7 +289,7 @@ public:
    * <code>kind</code> cannot be applied to <code>numArgs</code>
    * arguments.
    */
-  void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
+  void checkArity(Kind kind, unsigned numArgs) throw(ParserException);
 
   /**
    * Check that <code>kind</code> is a legal operator in the current
@@ -284,7 +300,7 @@ public:
    * @throws ParserException if the parser mode is strict and the
    * operator <code>kind</code> has not been enabled
    */
-  void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException);
+  void checkOperator(Kind kind, unsigned numArgs) throw(ParserException);
 
   /**
    * Returns the type for the variable with the given name.
@@ -300,7 +316,7 @@ public:
   /**
    * Create a set of new CVC4 variable expressions of the given type.
    */
-  const std::vector<Expr>
+  std::vector<Expr>
   mkVars(const std::vector<std::string> names, const Type& type);
 
   /** Create a new CVC4 function expression of the given type. */
@@ -327,17 +343,27 @@ public:
   /**
    * Creates a new sort with the given name.
    */
-  Type mkSort(const std::string& name);
+  SortType mkSort(const std::string& name);
 
   /**
    * Creates a new sort constructor with the given name and arity.
    */
-  Type mkSortConstructor(const std::string& name, size_t arity);
+  SortConstructorType mkSortConstructor(const std::string& name, size_t arity);
 
   /**
    * Creates new sorts with the given names (all of arity 0).
    */
-  std::vector<Type> mkSorts(const std::vector<std::string>& names);
+  std::vector<SortType> mkSorts(const std::vector<std::string>& names);
+
+  /**
+   * Creates a new "unresolved type," used only during parsing.
+   */
+  SortType mkUnresolvedType(const std::string& name);
+
+  /**
+   * Returns true IFF name is an unresolved type.
+   */
+  bool isUnresolvedType(const std::string& name);
 
   /**
    * Create sorts of mutually-recursive datatypes.
@@ -371,13 +397,37 @@ public:
   /** Is the symbol bound to a predicate? */
   bool isPredicate(const std::string& name);
 
+  /** Parse and return the next command. */
   Command* nextCommand() throw(ParserException);
+
+  /** Parse and return the next expression. */
   Expr nextExpression() throw(ParserException);
 
-  inline void parseError(const std::string& msg) throw (ParserException) {
+  /** Raise a parse error with the given message. */
+  inline void parseError(const std::string& msg) throw(ParserException) {
     d_input->parseError(msg);
   }
 
+  /**
+   * If we are parsing only, don't raise an exception; if we are not,
+   * raise a parse error with the given message.  There is no actual
+   * parse error, everything is as expected, but we cannot create the
+   * Expr, Type, or other requested thing yet due to internal
+   * limitations.  Even though it's not a parse error, we throw a
+   * parse error so that the input line and column information is
+   * available.
+   *
+   * Think quantifiers.  We don't have a TheoryQuantifiers yet, so we
+   * have no kind::FORALL or kind::EXISTS.  But we might want to
+   * support parsing quantifiers (just not doing anything with them).
+   * So this mechanism gives you a way to do it with --parse-only.
+   */
+  inline void unimplementedFeature(const std::string& msg) throw(ParserException) {
+    if(!d_parseOnly) {
+      parseError(msg);
+    }
+  }
+
   inline void pushScope() { d_declScope->pushScope(); }
   inline void popScope() { d_declScope->popScope(); }
 
@@ -405,7 +455,7 @@ public:
    *
    * In short, caveat emptor.
    */
-  void useDeclarationsFrom(Parser* parser) {
+  inline void useDeclarationsFrom(Parser* parser) {
     if(parser == NULL) {
       d_declScope = &d_declScopeAllocated;
     } else {
@@ -414,6 +464,13 @@ public:
   }
 
   /**
+   * Gets the current declaration level.
+   */
+  inline size_t getDeclarationLevel() const throw() {
+    return d_declScope->getLevel();
+  }
+
+  /**
    * An expression stream interface for a parser.  This stream simply
    * pulls expressions from the given Parser object.
    *