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/parser | |
parent | 4f384b6fadd999324d83b4c4ea900de2a0e13dd7 (diff) |
Add isParameterized function to Expr (#3303)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
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()); } |