2 files changed, 23 insertions, 0 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index d6a6f47bb..04466a4c6 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -410,6 +410,13 @@ Expr Expr::getOperator() const {
   return Expr(d_exprManager, new Node(d_node->getOperator()));
 }
 
+bool Expr::isParameterized() const
+{
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->getMetaKind() == kind::metakind::PARAMETERIZED;
+}
+
 Type Expr::getType(bool check) const
 {
   ExprManagerScope ems(*this);
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 458255c06..d03efdd52 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -450,6 +450,22 @@ public:
   Expr getOperator() const;
 
   /**
+   * Check if this is an expression is parameterized.
+   *
+   * @return true if this expression is parameterized.
+   *
+   * In detail, an expression that is parameterized is one that has an operator
+   * that must be provided in addition to its kind to construct it. For example,
+   * say we want to re-construct an Expr e where its children a1, ..., an are
+   * replaced by b1 ... bn. Then there are two cases:
+   * (1) If e is parametric, call:
+   *   ExprManager::mkExpr(e.getKind(), e.getOperator(), b1, ..., bn )
+   * (2) If e is not parametric, call:
+   *   ExprManager::mkExpr(e.getKind(), b1, ..., bn )
+   */
+  bool isParameterized() const;
+
+  /**
    * Get the type for this Expr and optionally do type checking.
    *
    * Initial type computation will be near-constant time if