Introduce smt2 parsing utility ParseOp and refactor (#3165)

5 files changed, 512 insertions, 369 deletions

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 03e194b90..8ac8baf1b 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -41,6 +41,7 @@ set(libcvc4parser_src_files
   smt1/smt1.h
   smt1/smt1_input.cpp
   smt1/smt1_input.h
+  smt2/parse_op.h
   smt2/smt2.cpp
   smt2/smt2.h
   smt2/smt2_input.cpp
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a5109361b..9e7bc74ee 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -79,8 +79,9 @@ using namespace CVC4::parser;
 
 #include <memory>
 
-#include "parser/parser.h"
 #include "parser/antlr_tracing.h"
+#include "parser/parser.h"
+#include "parser/smt2/parse_op.h"
 #include "smt/command.h"
 
 namespace CVC4 {
@@ -1833,42 +1834,15 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   Expr f;
   std::string name;
   Type type;
+  ParseOp p;
 }
 : termNonVariable[expr, expr2]
 
   // a qualified identifier (section 3.6 of SMT-LIB version 2.6)
 
-  | qualIdentifier[kind,name,f,type]
+  | qualIdentifier[p]
     {
-      if (kind != kind::NULL_EXPR || !type.isNull())
-      {
-        PARSER_STATE->parseError(
-            "Bad syntax for qualified identifier operator in term position.");
-      }
-      else if (!f.isNull())
-      {
-        expr = f;
-      }
-      else if (!PARSER_STATE->isDeclared(name,SYM_VARIABLE))
-      {
-        if (PARSER_STATE->sygus_v1() && name[0] == '-'
-            && name.find_first_not_of("0123456789", 1) == std::string::npos)
-        {
-          // allow unary minus in sygus version 1
-          expr = MK_CONST(Rational(name));
-        }
-        else
-        {
-          std::stringstream ss;
-          ss << "Symbol " << name << " is not declared.";
-          PARSER_STATE->parseError(ss.str());
-        }
-      }
-      else
-      {
-        expr = PARSER_STATE->getExpressionForName(name);
-      }
-      assert(!expr.isNull());
+      expr = PARSER_STATE->parseOpToExpr(p);
     }
   ;
 
@@ -1881,26 +1855,22 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
 @init {
   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Kind kind = kind::NULL_EXPR;
-  Kind qkind = kind::NULL_EXPR;
   std::string name;
   std::vector<Expr> args;
   std::vector< std::pair<std::string, Type> > sortedVarNames;
   Expr f, f2, f3;
-  Expr qexpr;
-  Type qtype;
   std::string attr;
   Expr attexpr;
   std::vector<Expr> patexprs;
   std::vector<Expr> patconds;
   std::unordered_set<std::string> names;
   std::vector< std::pair<std::string, Expr> > binders;
-  bool isBuiltinOperator = false;
-  bool isOverloadedFunction = false;
   int match_vindex = -1;
   std::vector<Type> match_ptypes;
   Type type;
   Type type2;
   api::Term atomTerm;
+  ParseOp p;
 }
   : LPAREN_TOK quantOp[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
@@ -1939,241 +1909,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-  | LPAREN_TOK qualIdentifier[qkind,name,qexpr,qtype]
-    {
-      // process the operator
-      Debug("parser") << "Parsed qual id: " << qkind << "/" << name << "/"
-                      << qexpr << "/" << qtype << std::endl;
-      if (qkind != kind::NULL_EXPR)
-      {
-        // It is a special case, e.g. tupSel or array constant specification.
-        // We have to wait until the arguments are parsed to resolve it.
-      }
-      else if (!qexpr.isNull())
-      {
-        // An explicit operator, e.g. an indexed symbol.
-        args.push_back(qexpr);
-        if (qexpr.getType().isTester())
-        {
-          kind = kind::APPLY_TESTER;
-        }
-      }
-      else
-      {
-        isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
-        if (isBuiltinOperator)
-        {
-          // a builtin operator, convert to kind
-          kind = PARSER_STATE->getOperatorKind(name);
-        }
-        else
-        {
-          // A non-built-in function application, get the expression
-          PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
-          expr = PARSER_STATE->getVariable(name);
-          if (!expr.isNull())
-          {
-            PARSER_STATE->checkFunctionLike(expr);
-            kind = PARSER_STATE->getKindForFunction(expr);
-            args.push_back(expr);
-          }
-          else
-          {
-            // Could not find the expression. It may be an overloaded symbol,
-            // in which case we may find it after knowing the types of its
-            // arguments.
-            isOverloadedFunction = true;
-          }
-        }
-      }
-    }
+  | LPAREN_TOK qualIdentifier[p]
     termList[args,expr] RPAREN_TOK
-    { Debug("parser") << "args has size " << args.size() << std::endl
-                      << "expr is " << expr << std::endl;
-      for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
-        Debug("parser") << "++ " << *i << std::endl;
-      }
-      // We now can figure out what the operator is, if we guessed it was
-      // overloaded.
-      if(isOverloadedFunction) {
-        std::vector< Type > argTypes;
-        for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
-          argTypes.push_back( (*i).getType() );
-        }
-        expr = PARSER_STATE->getOverloadedFunctionForTypes(name, argTypes);
-        if(!expr.isNull()) {
-          PARSER_STATE->checkFunctionLike(expr);
-          kind = PARSER_STATE->getKindForFunction(expr);
-          args.insert(args.begin(),expr);
-        }else{
-          PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types.");
-        }
-      }
-      // handle special cases
-      if (qkind == kind::STORE_ALL)
-      {
-        if (args.size() != 1)
-        {
-          PARSER_STATE->parseError("Too many arguments to array constant.");
-        }
-        if (!args[0].isConst())
-        {
-          std::stringstream ss;
-          ss << "expected constant term inside array constant, but found "
-             << "nonconstant term:" << std::endl
-             << "the term: " << args[0];
-          PARSER_STATE->parseError(ss.str());
-        }
-        ArrayType aqtype = static_cast<ArrayType>(qtype);
-        if (!aqtype.getConstituentType().isComparableTo(args[0].getType()))
-        {
-          std::stringstream ss;
-          ss << "type mismatch inside array constant term:" << std::endl
-             << "array type:          " << qtype << std::endl
-             << "expected const type: " << aqtype.getConstituentType()
-             << std::endl
-             << "computed const type: " << args[0].getType();
-          PARSER_STATE->parseError(ss.str());
-        }
-        expr = MK_CONST(CVC4::ArrayStoreAll(qtype, args[0]));
-      }
-      else if (qkind == kind::APPLY_SELECTOR)
-      {
-        if (qexpr.isNull())
-        {
-          PARSER_STATE->parseError("Could not process parsed tuple selector.");
-        }
-        // tuple selector case
-        Integer x = qexpr.getConst<CVC4::Rational>().getNumerator();
-        if (!x.fitsUnsignedInt())
-        {
-          PARSER_STATE->parseError(
-              "index of tupSel is larger than size of unsigned int");
-        }
-        unsigned int n = x.toUnsignedInt();
-        if (args.size() > 1)
-        {
-          PARSER_STATE->parseError(
-              "tupSel applied to more than one tuple argument");
-        }
-        Type t = args[0].getType();
-        if (!t.isTuple())
-        {
-          PARSER_STATE->parseError("tupSel applied to non-tuple");
-        }
-        size_t length = ((DatatypeType)t).getTupleLength();
-        if (n >= length)
-        {
-          std::stringstream ss;
-          ss << "tuple is of length " << length << "; cannot access index "
-             << n;
-          PARSER_STATE->parseError(ss.str());
-        }
-        const Datatype& dt = ((DatatypeType)t).getDatatype();
-        expr = dt[0][n].getSelector();
-        expr = MK_EXPR(kind::APPLY_SELECTOR, expr, args);
-      }
-      else if (qkind != kind::NULL_EXPR)
-      {
-        std::stringstream ss;
-        ss << "Could not process parsed qualified identifier kind " << qkind;
-        PARSER_STATE->parseError(ss.str());
-      }
-      else if (isBuiltinOperator)
-      {
-        bool done = false;
-        if (args.size() > 2)
-        {
-          if (kind == CVC4::kind::INTS_DIVISION || kind == CVC4::kind::XOR
-              || kind == CVC4::kind::MINUS || kind == CVC4::kind::DIVISION
-              || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6()))
-          {
-            // Builtin operators that are not tokenized, are left associative,
-            // but not internally variadic must set this.
-            expr =
-                EXPR_MANAGER->mkLeftAssociative(kind, args);
-            done = true;
-          }
-          else if (kind == CVC4::kind::IMPLIES)
-          {
-            /* right-associative, but CVC4 internally only supports 2 args */
-            expr = EXPR_MANAGER->mkRightAssociative(kind, args);
-            done = true;
-          }
-          else if (kind == CVC4::kind::EQUAL || kind == CVC4::kind::LT
-                   || kind == CVC4::kind::GT || kind == CVC4::kind::LEQ
-                   || kind == CVC4::kind::GEQ)
-          {
-            /* "chainable", but CVC4 internally only supports 2 args */
-            expr = MK_EXPR(MK_CONST(Chain(kind)), args);
-            done = true;
-          }
-        }
-
-        if (!done)
-        {
-          if (CVC4::kind::isAssociative(kind)
-              && args.size() > EXPR_MANAGER->maxArity(kind))
-          {
-            /* Special treatment for associative operators with lots of children
-             */
-            expr = EXPR_MANAGER->mkAssociative(kind, args);
-          }
-          else if (!PARSER_STATE->strictModeEnabled()
-                   && (kind == CVC4::kind::AND || kind == CVC4::kind::OR)
-                   && args.size() == 1)
-          {
-            /* Unary AND/OR can be replaced with the argument.
-             * It just so happens expr should already be the only argument. */
-            assert(expr == args[0]);
-          }
-          else if (kind == CVC4::kind::MINUS && args.size() == 1)
-          {
-            expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
-          }
-          else
-          {
-            PARSER_STATE->checkOperator(kind, args.size());
-            expr = MK_EXPR(kind, args);
-          }
-        }
-      }
-      else
-      {
-        bool done = false;
-        if (args.size() >= 2)
-        {
-          // may be partially applied function, in this case we use HO_APPLY
-          Type argt = args[0].getType();
-          if (argt.isFunction())
-          {
-            unsigned arity = static_cast<FunctionType>(argt).getArity();
-            if (args.size() - 1 < arity)
-            {
-              Debug("parser") << "Partial application of " << args[0];
-              Debug("parser") << " : #argTypes = " << arity;
-              Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
-              // must curry the partial application
-              expr =
-                  EXPR_MANAGER->mkLeftAssociative(CVC4::kind::HO_APPLY, args);
-              done = true;
-            }
-          }
-        }
-
-        if (!done)
-        {
-          if (kind == kind::NULL_EXPR)
-          {
-            std::vector<Expr> eargs(args.begin() + 1, args.end());
-            expr = MK_EXPR(args[0], eargs);
-          }
-          else
-          {
-            expr = MK_EXPR(kind, args);
-          }
-        }
-      }
+    { 
+      expr = PARSER_STATE->applyParseOp(p,args);
     }
   | /* a let or sygus let binding */
     LPAREN_TOK (
@@ -2422,7 +2161,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
 
 /**
  * Matches a qualified identifier, which can be a combination of one or more of
- * the following:
+ * the following, stored in the ParseOp utility class:
  * (1) A kind.
  * (2) A string name.
  * (3) An expression expr.
@@ -2470,107 +2209,24 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
  * expression (3), which may involve disambiguating f based on type T if it is
  * overloaded.
  */
-qualIdentifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr, CVC4::Type& t]
+qualIdentifier[CVC4::ParseOp& p]
 @init {
   Kind k;
   std::string baseName;
   Expr f;
   Type type;
 }
-: identifier[kind,name,expr]
+: identifier[p]
   | LPAREN_TOK AS_TOK
-    ( CONST_TOK sortSymbol[t, CHECK_DECLARED]
+    ( CONST_TOK sortSymbol[type, CHECK_DECLARED]
       {
-        if (!t.isArray())
-        {
-          std::stringstream ss;
-          ss << "expected array constant term, but cast is not of array type"
-             << std::endl
-             << "cast type: " << t;
-          PARSER_STATE->parseError(ss.str());
-        }
-        kind = kind::STORE_ALL;
+        p.d_kind = kind::STORE_ALL;
+        PARSER_STATE->applyTypeAscription(p, type);
       }
-    | identifier[k,baseName,f]
+    | identifier[p]
       sortSymbol[type, CHECK_DECLARED]
       {
-        if (f.isNull())
-        {
-          Trace("parser-overloading")
-              << "Getting variable expression with name " << baseName
-              << " and type " << type << std::endl;
-          // get the variable expression for the type
-          if (PARSER_STATE->isDeclared(baseName, SYM_VARIABLE))
-          {
-            f = PARSER_STATE->getExpressionForNameAndType(baseName, type);
-          }
-          if(f.isNull())
-          {
-            std::stringstream ss;
-            ss << "Could not resolve expression with name " << baseName
-               << " and type " << type << std::endl;
-            PARSER_STATE->parseError(ss.str());
-          }
-        }
-        Trace("parser-qid") << "Resolve ascription " << type << " on " << f;
-        Trace("parser-qid") << " " << f.getKind() << " " << f.getType();
-        Trace("parser-qid") << std::endl;
-        // by default, we take f itself
-        expr = f;
-        if (f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype())
-        {
-          // nullary constructors with a type ascription
-          // could be a parametric constructor or just an overloaded constructor
-          DatatypeType dtype = static_cast<DatatypeType>(type);
-          if (dtype.isParametric())
-          {
-            std::vector<CVC4::Expr> v;
-            Expr e = f.getOperator();
-            const DatatypeConstructor& dtc =
-                Datatype::datatypeOf(e)[Datatype::indexOf(e)];
-            v.push_back(MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION,
-                                MK_CONST(AscriptionType(
-                                    dtc.getSpecializedConstructorType(type))),
-                                f.getOperator()));
-            v.insert(v.end(), f.begin(), f.end());
-            expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
-          }
-        }
-        else if (f.getType().isConstructor())
-        {
-          // a non-nullary constructor with a type ascription
-          DatatypeType dtype = static_cast<DatatypeType>(type);
-          if (dtype.isParametric())
-          {
-            const DatatypeConstructor& dtc =
-                Datatype::datatypeOf(f)[Datatype::indexOf(f)];
-            expr = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION,
-                           MK_CONST(AscriptionType(
-                               dtc.getSpecializedConstructorType(type))),
-                           f);
-          }
-        }
-        else if (f.getKind() == CVC4::kind::EMPTYSET)
-        {
-          Debug("parser") << "Empty set encountered: " << f << " " << type
-                          << std::endl;
-          expr = MK_CONST(::CVC4::EmptySet(type));
-        }
-        else if (f.getKind() == CVC4::kind::UNIVERSE_SET)
-        {
-          expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET);
-        }
-        else if (f.getKind() == CVC4::kind::SEP_NIL)
-        {
-          // We don't want the nil reference to be a constant: for instance, it
-          // could be of type Int but is not a const rational. However, the
-          // expression has 0 children. So we convert to a SEP_NIL variable.
-          expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL);
-        }
-        else if (f.getType() != type)
-        {
-          PARSER_STATE->parseError("Type ascription not satisfied.");
-        }
+        PARSER_STATE->applyTypeAscription(p, type);
       }
     )
     RPAREN_TOK
@@ -2578,19 +2234,19 @@ qualIdentifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr, CVC4::Type
 
 /**
  * Matches an identifier, which can be a combination of one or more of the
- * following:
+ * following, stored in the ParseOp utility class:
  * (1) A kind.
  * (2) A string name.
  * (3) An expression expr.
  * For examples, see documentation of qualIdentifier.
  */
-identifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr]
+identifier[CVC4::ParseOp& p]
 @init {
   Expr f;
   Expr f2;
   std::vector<uint64_t> numerals;
 }
-: functionName[name, CHECK_NONE]
+: functionName[p.d_name, CHECK_NONE]
 
   // indexed functions
 
@@ -2607,18 +2263,18 @@ identifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr]
           PARSER_STATE->parseError(
               "Bad syntax for test (_ is X), X must be a constructor.");
         }
-        expr = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getTester();
+        p.d_expr = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getTester();
       }
     | TUPLE_SEL_TOK m=INTEGER_LITERAL
       {
         // we adopt a special syntax (_ tupSel n)
-        kind = CVC4::kind::APPLY_SELECTOR;
+        p.d_kind = CVC4::kind::APPLY_SELECTOR;
         // put m in expr so that the caller can deal with this case
-        expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
+        p.d_expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
       }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
-        expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals)
+        p.d_expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals)
                    .getExpr();
       }
     )
diff --git a/src/parser/smt2/parse_op.h b/src/parser/smt2/parse_op.h
new file mode 100644
index 000000000..40b42d0bb
--- /dev/null
+++ b/src/parser/smt2/parse_op.h
@@ -0,0 +1,74 @@
+/*********************                                                        */
+/*! \file parse_op.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Definitions of parsed operators in smt2.
+ **/
+
+#include "cvc4parser_private.h"
+
+#ifndef CVC4__PARSER__SMT2__PARSE_OP_H
+#define CVC4__PARSER__SMT2__PARSE_OP_H
+
+#include <string>
+
+#include "expr/expr.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+
+/** A parsed operator
+ *
+ * The purpose of this struct is to store information regarding a parsed term
+ * in the smt2 language that might not be ready to associate with an
+ * expression.
+ *
+ * While parsing terms in smt2, we may store a combination of one or more of
+ * the following to track how to process this term:
+ * (1) A kind.
+ * (2) A string name.
+ * (3) An expression expr.
+ * (4) A type t.
+ *
+ * Examples:
+ *
+ * - For declared functions f that we have not yet looked up in a symbol table,
+ * we store (2). We may store a name in a state if f is overloaded and we have
+ * not yet parsed its arguments to know how to disambiguate f.
+ * - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to
+ * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
+ * caller as the n^th generic tuple selector. We do this since there is no
+ * AST expression representing generic tuple select, and we do not have enough
+ * type information at this point to know the type of the tuple we will be
+ * selecting from.
+ * - For array constant specifications prior to type ascription e.g. when we
+ * have parsed "const", we store (1), setting the kind to STORE_ALL.
+ * - For array constant specifications (as const (Array T1 T2)), we store (1)
+ * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2).
+ * When parsing this as an operator e.g. ((as const (Array T1 T2)) t), we
+ * interpret this operator by converting the next parsed constant of type T2 to
+ * an Array of type (Array T1 T2) over that constant.
+ */
+struct ParseOp
+{
+  ParseOp() : d_kind(kind::NULL_EXPR) {}
+  /** The kind associated with the parsed operator, if it exists */
+  Kind d_kind;
+  /** The name associated with the parsed operator, if it exists */
+  std::string d_name;
+  /** The expression associated with the parsed operator, if it exists */
+  Expr d_expr;
+  /** The type associated with the parsed operator, if it exists */
+  Type d_type;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__PARSER__SMT2__PARSE_OP_H */
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d1fb3fe32..346675b6b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1566,6 +1566,355 @@ InputLanguage Smt2::getLanguage() const
   return em->getOptions().getInputLanguage();
 }
 
+void Smt2::applyTypeAscription(ParseOp& p, Type type)
+{
+  // (as const (Array T1 T2))
+  if (p.d_kind == kind::STORE_ALL)
+  {
+    if (!type.isArray())
+    {
+      std::stringstream ss;
+      ss << "expected array constant term, but cast is not of array type"
+         << std::endl
+         << "cast type: " << type;
+      parseError(ss.str());
+    }
+    p.d_type = type;
+    return;
+  }
+  if (p.d_expr.isNull())
+  {
+    Trace("parser-overloading")
+        << "Getting variable expression with name " << p.d_name << " and type "
+        << type << std::endl;
+    // get the variable expression for the type
+    if (isDeclared(p.d_name, SYM_VARIABLE))
+    {
+      p.d_expr = getExpressionForNameAndType(p.d_name, type);
+    }
+    if (p.d_expr.isNull())
+    {
+      std::stringstream ss;
+      ss << "Could not resolve expression with name " << p.d_name
+         << " and type " << type << std::endl;
+      parseError(ss.str());
+    }
+  }
+  ExprManager* em = getExprManager();
+  Type etype = p.d_expr.getType();
+  Kind ekind = p.d_expr.getKind();
+  Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
+  Trace("parser-qid") << " " << ekind << " " << etype;
+  Trace("parser-qid") << std::endl;
+  if (ekind == kind::APPLY_CONSTRUCTOR && type.isDatatype())
+  {
+    // nullary constructors with a type ascription
+    // could be a parametric constructor or just an overloaded constructor
+    DatatypeType dtype = static_cast<DatatypeType>(type);
+    if (dtype.isParametric())
+    {
+      std::vector<Expr> v;
+      Expr e = p.d_expr.getOperator();
+      const DatatypeConstructor& dtc =
+          Datatype::datatypeOf(e)[Datatype::indexOf(e)];
+      v.push_back(em->mkExpr(
+          kind::APPLY_TYPE_ASCRIPTION,
+          em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
+          p.d_expr.getOperator()));
+      v.insert(v.end(), p.d_expr.begin(), p.d_expr.end());
+      p.d_expr = em->mkExpr(kind::APPLY_CONSTRUCTOR, v);
+    }
+  }
+  else if (etype.isConstructor())
+  {
+    // a non-nullary constructor with a type ascription
+    DatatypeType dtype = static_cast<DatatypeType>(type);
+    if (dtype.isParametric())
+    {
+      const DatatypeConstructor& dtc =
+          Datatype::datatypeOf(p.d_expr)[Datatype::indexOf(p.d_expr)];
+      p.d_expr = em->mkExpr(
+          kind::APPLY_TYPE_ASCRIPTION,
+          em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
+          p.d_expr);
+    }
+  }
+  else if (ekind == kind::EMPTYSET)
+  {
+    Debug("parser") << "Empty set encountered: " << p.d_expr << " " << type
+                    << std::endl;
+    p.d_expr = em->mkConst(EmptySet(type));
+  }
+  else if (ekind == kind::UNIVERSE_SET)
+  {
+    p.d_expr = em->mkNullaryOperator(type, kind::UNIVERSE_SET);
+  }
+  else if (ekind == kind::SEP_NIL)
+  {
+    // We don't want the nil reference to be a constant: for instance, it
+    // could be of type Int but is not a const rational. However, the
+    // expression has 0 children. So we convert to a SEP_NIL variable.
+    p.d_expr = em->mkNullaryOperator(type, kind::SEP_NIL);
+  }
+  else if (etype != type)
+  {
+    parseError("Type ascription not satisfied.");
+  }
+}
+
+Expr Smt2::parseOpToExpr(ParseOp& p)
+{
+  Expr expr;
+  if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull())
+  {
+    parseError(
+        "Bad syntax for qualified identifier operator in term position.");
+  }
+  else if (!p.d_expr.isNull())
+  {
+    expr = p.d_expr;
+  }
+  else if (!isDeclared(p.d_name, SYM_VARIABLE))
+  {
+    if (sygus_v1() && p.d_name[0] == '-'
+        && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos)
+    {
+      // allow unary minus in sygus version 1
+      expr = getExprManager()->mkConst(Rational(p.d_name));
+    }
+    else
+    {
+      std::stringstream ss;
+      ss << "Symbol " << p.d_name << " is not declared.";
+      parseError(ss.str());
+    }
+  }
+  else
+  {
+    expr = getExpressionForName(p.d_name);
+  }
+  assert(!expr.isNull());
+  return expr;
+}
+
+Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
+{
+  bool isBuiltinOperator = false;
+  // the builtin kind of the overall return expression
+  Kind kind = kind::NULL_EXPR;
+  // First phase: process the operator
+  if (Debug.isOn("parser"))
+  {
+    Debug("parser") << "Apply parse op to:" << std::endl;
+    Debug("parser") << "args has size " << args.size() << std::endl;
+    for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+    {
+      Debug("parser") << "++ " << *i << std::endl;
+    }
+  }
+  if (p.d_kind != kind::NULL_EXPR)
+  {
+    // It is a special case, e.g. tupSel or array constant specification.
+    // We have to wait until the arguments are parsed to resolve it.
+  }
+  else if (!p.d_expr.isNull())
+  {
+    // An explicit operator, e.g. an indexed symbol.
+    args.insert(args.begin(), p.d_expr);
+    if (p.d_expr.getType().isTester())
+    {
+      // Testers are handled differently than other indexed operators,
+      // since they require a kind.
+      kind = kind::APPLY_TESTER;
+    }
+  }
+  else
+  {
+    isBuiltinOperator = isOperatorEnabled(p.d_name);
+    if (isBuiltinOperator)
+    {
+      // a builtin operator, convert to kind
+      kind = getOperatorKind(p.d_name);
+    }
+    else
+    {
+      // A non-built-in function application, get the expression
+      checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
+      Expr v = getVariable(p.d_name);
+      if (!v.isNull())
+      {
+        checkFunctionLike(v);
+        kind = getKindForFunction(v);
+        args.insert(args.begin(), v);
+      }
+      else
+      {
+        // Overloaded symbol?
+        // Could not find the expression. It may be an overloaded symbol,
+        // in which case we may find it after knowing the types of its
+        // arguments.
+        std::vector<Type> argTypes;
+        for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+        {
+          argTypes.push_back((*i).getType());
+        }
+        Expr op = getOverloadedFunctionForTypes(p.d_name, argTypes);
+        if (!op.isNull())
+        {
+          checkFunctionLike(op);
+          kind = getKindForFunction(op);
+          args.insert(args.begin(), op);
+        }
+        else
+        {
+          parseError(
+              "Cannot find unambiguous overloaded function for argument "
+              "types.");
+        }
+      }
+    }
+  }
+
+  // Second phase: apply the arguments to the parse op
+  ExprManager* em = getExprManager();
+  // handle special cases
+  if (p.d_kind == kind::STORE_ALL)
+  {
+    if (args.size() != 1)
+    {
+      parseError("Too many arguments to array constant.");
+    }
+    if (!args[0].isConst())
+    {
+      std::stringstream ss;
+      ss << "expected constant term inside array constant, but found "
+         << "nonconstant term:" << std::endl
+         << "the term: " << args[0];
+      parseError(ss.str());
+    }
+    ArrayType aqtype = static_cast<ArrayType>(p.d_type);
+    if (!aqtype.getConstituentType().isComparableTo(args[0].getType()))
+    {
+      std::stringstream ss;
+      ss << "type mismatch inside array constant term:" << std::endl
+         << "array type:          " << p.d_type << std::endl
+         << "expected const type: " << aqtype.getConstituentType() << std::endl
+         << "computed const type: " << args[0].getType();
+      parseError(ss.str());
+    }
+    return em->mkConst(ArrayStoreAll(p.d_type, args[0]));
+  }
+  else if (p.d_kind == kind::APPLY_SELECTOR)
+  {
+    if (p.d_expr.isNull())
+    {
+      parseError("Could not process parsed tuple selector.");
+    }
+    // tuple selector case
+    Integer x = p.d_expr.getConst<Rational>().getNumerator();
+    if (!x.fitsUnsignedInt())
+    {
+      parseError("index of tupSel is larger than size of unsigned int");
+    }
+    unsigned int n = x.toUnsignedInt();
+    if (args.size() > 1)
+    {
+      parseError("tupSel applied to more than one tuple argument");
+    }
+    Type t = args[0].getType();
+    if (!t.isTuple())
+    {
+      parseError("tupSel applied to non-tuple");
+    }
+    size_t length = ((DatatypeType)t).getTupleLength();
+    if (n >= length)
+    {
+      std::stringstream ss;
+      ss << "tuple is of length " << length << "; cannot access index " << n;
+      parseError(ss.str());
+    }
+    const Datatype& dt = ((DatatypeType)t).getDatatype();
+    return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args);
+  }
+  else if (p.d_kind != kind::NULL_EXPR)
+  {
+    std::stringstream ss;
+    ss << "Could not process parsed qualified identifier kind " << p.d_kind;
+    parseError(ss.str());
+  }
+  else if (isBuiltinOperator)
+  {
+    if (args.size() > 2)
+    {
+      if (kind == kind::INTS_DIVISION || kind == kind::XOR
+          || kind == kind::MINUS || kind == kind::DIVISION
+          || (kind == kind::BITVECTOR_XNOR && v2_6()))
+      {
+        // Builtin operators that are not tokenized, are left associative,
+        // but not internally variadic must set this.
+        return em->mkLeftAssociative(kind, args);
+      }
+      else if (kind == kind::IMPLIES)
+      {
+        /* right-associative, but CVC4 internally only supports 2 args */
+        return em->mkRightAssociative(kind, args);
+      }
+      else if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT
+               || kind == kind::LEQ || kind == kind::GEQ)
+      {
+        /* "chainable", but CVC4 internally only supports 2 args */
+        return em->mkExpr(em->mkConst(Chain(kind)), args);
+      }
+    }
+
+    if (kind::isAssociative(kind) && args.size() > em->maxArity(kind))
+    {
+      /* Special treatment for associative operators with lots of children
+       */
+      return em->mkAssociative(kind, args);
+    }
+    else if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
+             && args.size() == 1)
+    {
+      // Unary AND/OR can be replaced with the argument.
+      return args[0];
+    }
+    else if (kind == kind::MINUS && args.size() == 1)
+    {
+      return em->mkExpr(kind::UMINUS, args[0]);
+    }
+    else
+    {
+      checkOperator(kind, args.size());
+      return em->mkExpr(kind, args);
+    }
+  }
+
+  if (args.size() >= 2)
+  {
+    // may be partially applied function, in this case we use HO_APPLY
+    Type argt = args[0].getType();
+    if (argt.isFunction())
+    {
+      unsigned arity = static_cast<FunctionType>(argt).getArity();
+      if (args.size() - 1 < arity)
+      {
+        Debug("parser") << "Partial application of " << args[0];
+        Debug("parser") << " : #argTypes = " << arity;
+        Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
+        // must curry the partial application
+        return em->mkLeftAssociative(kind::HO_APPLY, args);
+      }
+    }
+  }
+  if (kind == kind::NULL_EXPR)
+  {
+    std::vector<Expr> eargs(args.begin() + 1, args.end());
+    return em->mkExpr(args[0], eargs);
+  }
+  return em->mkExpr(kind, args);
+}
+
 Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
 {
   if (!sexpr.isKeyword())
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 669104954..7c7f290a5 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -28,6 +28,7 @@
 #include "api/cvc4cpp.h"
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
+#include "parser/smt2/parse_op.h"
 #include "smt/command.h"
 #include "theory/logic_info.h"
 #include "util/abstract_value.h"
@@ -444,7 +445,69 @@ class Smt2 : public Parser
     parseError(withLogic);
   }
 
-private:
+  //------------------------- processing parse operators
+  /**
+   * Given a parse operator p, apply a type ascription to it. This method is run
+   * when we encounter "(as t type)" and information regarding t has been stored
+   * in p.
+   *
+   * This updates p to take into account the ascription. This may include:
+   * - Converting an (pre-ascribed) array constant specification "const" to
+   * an ascribed array constant specification (as const type) where type is
+   * (Array T1 T2) for some T1, T2.
+   * - Converting a (nullary or non-nullary) parametric datatype constructor to
+   * the specialized constructor for the given type.
+   * - Converting an empty set, universe set, or separation nil reference to
+   * the respective term of the given type.
+   * - If p's expression field is set, then we leave p unchanged, check if
+   * that expression has the given type and throw a parse error otherwise.
+   */
+  void applyTypeAscription(ParseOp& p, Type type);
+  /**
+   * This converts a ParseOp to expression, assuming it is a standalone term.
+   *
+   * In particular:
+   * - If p's expression field is set, then that expression is returned.
+   * - If p's name field is set, then we look up that name in the symbol table
+   * of this class.
+   * In other cases, a parse error is thrown.
+   */
+  Expr parseOpToExpr(ParseOp& p);
+  /**
+   * Apply parse operator to list of arguments, and return the resulting
+   * expression.
+   *
+   * This method involves two phases.
+   * (1) Processing the operator represented by p,
+   * (2) Applying that operator to the set of arguments.
+   *
+   * For (1), this involves determining the kind of the overall expression. We
+   * may be in one the following cases:
+   * - If p's expression field is set, we may choose to prepend it to args, or
+   * otherwise determine the appropriate kind of the overall expression based on
+   * this expression.
+   * - If p's name field is set, then we get the appropriate symbol for that
+   * name, which may involve disambiguating that name if it is overloaded based
+   * on the types of args. We then determine the overall kind of the return
+   * expression based on that symbol.
+   * - p's kind field may be already set.
+   *
+   * For (2), we construct the overall expression, which may involve the
+   * following:
+   * - If p is an array constant specification (as const (Array T1 T2)), then
+   * we return the appropriate array constant based on args[0].
+   * - If p represents a tuple selector, then we infer the appropriate tuple
+   * selector expression based on the type of args[0].
+   * - If the overall kind of the expression is chainable, we may convert it
+   * to a left- or right-associative chain.
+   * - If the overall kind is MINUS and args has size 1, then we return an
+   * application of UMINUS.
+   * - If the overall expression is a partial application, then we process this
+   * as a chain of HO_APPLY terms.
+   */
+  Expr applyParseOp(ParseOp& p, std::vector<Expr>& args);
+  //------------------------- end processing parse operators
+ private:
   std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type;
   std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars;
   std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body;