1 files changed, 64 insertions, 1 deletions
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;