diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-25 12:09:42 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-25 12:09:42 -0500 |
commit | 91565cda11ad42082a11055514e12ddeee459460 (patch) | |
tree | 56df21e0a0c5d0734cd40b3ce93ced2c2beac54d /src | |
parent | 4f384b6fadd999324d83b4c4ea900de2a0e13dd7 (diff) |
Add isParameterized function to Expr (#3303)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 6 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 19 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 7 | ||||
-rw-r--r-- | src/expr/expr_template.h | 16 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
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()); } |