Add isParameterized function to Expr (#3303)

5 files changed, 51 insertions, 4 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 6a6088007..b40a58e37 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1050,6 +1050,12 @@ Kind Term::getKind() const
   return intToExtKind(d_expr->getKind());
 }
 
+bool Term::isParameterized() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  return d_expr->isParameterized();
+}
+
 Sort Term::getSort() const
 {
   CVC4_API_CHECK_NOT_NULL;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 7fee35afd..bb7b48f97 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -579,7 +579,24 @@ class CVC4_PUBLIC Term
    * @return the kind of this term
    */
   Kind getKind() const;
-
+  
+  /**
+   * @return true if this expression is parameterized.
+   *
+   * !!! The below documentation is not accurate until we have a way of getting
+   * operators from terms.
+   *
+   * In detail, a term 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 a Term t where its children a1, ..., an are
+   * replaced by b1 ... bn. Then there are two cases:
+   * (1) If t is parametric, call:
+   *   mkTerm(t.getKind(), t.getOperator(), b1, ..., bn )
+   * (2) If t is not parametric, call:
+   *   mkTerm(t.getKind(), b1, ..., bn )
+   */
+  bool isParameterized() const;
+  
   /**
    * @return the sort of this term
    */
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
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bbfaf186e..bb0881030 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1392,9 +1392,10 @@ Expr Smt2::purifySygusGTerm(Expr term,
   }
   std::vector<Expr> pchildren;
   // To test whether the operator should be passed to mkExpr below, we check
-  // whether this term has an operator which is not constant. This includes
-  // APPLY_UF terms, but excludes applications of interpreted symbols.
-  if (term.hasOperator() && !term.getOperator().isConst())
+  // whether this term is parameterized. This includes APPLY_UF terms and BV
+  // extraction terms, but excludes applications of most interpreted symbols
+  // like PLUS.
+  if (term.isParameterized())
   {
     pchildren.push_back(term.getOperator());
   }