Add isParameterized function to Expr (#3303)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 6a6088007158ab66f0b3d7f184c204212109e827..b40a58e3700892f57179ec0855baad8623b5546c 100644 (file)
--- 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 7fee35afd57d4adf4cce6ca96c62e1a6c96f4a14..bb7b48f97d04e3c335442ad431e46e01a839f1f7 100644 (file)
--- 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 d6a6f47bb4938264f72f8bb28fe264f7e631353c..04466a4c6933086d9bc62cf338aaeff0801d4a6f 100644 (file)
--- 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 458255c062a3e3df1711b12da6efd5b8c3ca7057..d03efdd52574d69d18512bfb27a66cd613ef6a40 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -449,6 +449,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.
    *

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bbfaf186e8cb93213bde1a66ac06e03a957ddf14..bb0881030b79e86256f186144cc98ef0e483cd7f 100644 (file)
--- 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 6dc44e3145e057484edb699e4dc901af5288a734..bcae83b0a29b16652a36569d4d597cf79fb1c6d0 100644 (file)
--- 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 (file)
index 0000000..7d66908
--- /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 )