1 files changed, 24 insertions, 0 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8447eb4dc..d40236208 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -678,6 +678,30 @@ public:
    */
   Expr mkHoApply(Expr expr, std::vector<Expr>& args);
 
+  /** Apply type ascription
+   *
+   * Return term t with a type ascription applied to it. This is used for
+   * syntax like (as t T) in smt2 and t::T in the CVC language. This includes:
+   * - (as emptyset (Set T))
+   * - (as univset (Set T))
+   * - (as sep.nil T)
+   * - (cons T)
+   * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor.
+   *
+   * The term to ascribe t is a term whose kind and children (but not type)
+   * are equivalent to that of the term returned by this method.
+   *
+   * Notice that method is not necessarily a cast. In actuality, the above terms
+   * should be understood as symbols indexed by types. However, SMT-LIB does not
+   * permit types as indices, so we must use, e.g. (as emptyset (Set T))
+   * instead of (_ emptyset (Set T)).
+   *
+   * @param t The term to ascribe a type
+   * @param s The sort to ascribe
+   * @return Term t with sort s ascribed.
+   */
+  api::Term applyTypeAscription(api::Term t, api::Sort s);
+
   /**
    * Add an operator to the current legal set.
    *