From 91565cda11ad42082a11055514e12ddeee459460 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Sep 2019 12:09:42 -0500 Subject: Add isParameterized function to Expr (#3303) --- src/parser/smt2/smt2.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/parser/smt2/smt2.cpp') 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 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()); } -- cgit v1.2.3