Add isParameterized function to Expr (#3303)

7 files changed, 74 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());
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6dc44e314..bcae83b0a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1650,6 +1650,7 @@ set(regress_1_tests
   regress1/sygus/clock-inc-tuple.sy
   regress1/sygus/commutative-stream.sy
   regress1/sygus/commutative.sy
+  regress1/sygus/concat_extract_example.sy
   regress1/sygus/constant-bool-si-all.sy
   regress1/sygus/constant-dec-tree-bug.sy
   regress1/sygus/constant-ite-bv.sy
diff --git a/test/regress/regress1/sygus/concat_extract_example.sy b/test/regress/regress1/sygus/concat_extract_example.sy
new file mode 100644
index 000000000..7d6690816
--- /dev/null
+++ b/test/regress/regress1/sygus/concat_extract_example.sy
@@ -0,0 +1,22 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+(set-logic BV)
+(synth-fun f (( x (_ BitVec 32))) (_ BitVec 32)
+	((BV32 (_ BitVec 32)) ( BV16 (_ BitVec 16)))
+	((BV32 (_ BitVec 32) (#x00000000 #x00000001 #xFFFFFFFF
+				x
+				(bvand BV32 BV32)
+				(bvor BV32 BV32)
+				(bvnot BV32)
+				(concat BV16 BV16)
+				))
+	(BV16 (_ BitVec 16) (#x0000 #x0001 #xFFFF
+				(bvand BV16 BV16)
+				(bvor BV16 BV16)
+				(bvnot BV16)
+				((_ extract 31 16) BV32)
+				((_ extract 15 0) BV32)))))
+( constraint (= ( f #x0782ECAD ) #xECAD0000))
+( constraint (= ( f #xFFFF008E ) #x008E0000))
+( constraint (= ( f #x00000000 ) #x00000000))
+( check-synth )