diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-10-07 10:55:29 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-07 12:55:29 -0500 |
| commit | a6817647ee9bae0df0f1922c0d521d7f100d0245 (patch) | |
| tree | 192655da9dedc67a04ef29d4eabd4c1e67c7a143 /src/parser/smt2/smt2.cpp | |
| parent | eb4321c5040258ac1ac41eb955aa5b6b5199011e (diff) | |
New C++ API: Rename Term::isConst() to Term::isValue(). (#5211)
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 84e25c36b..b9b7de149 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1101,7 +1101,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) parseError("Too many arguments to array constant."); } api::Term constVal = args[0]; - if (!constVal.isConst()) + if (!constVal.isValue()) { // To parse array constants taking reals whose values are specified by // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle @@ -1111,15 +1111,15 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) // like 5.0 which are converted to (/ 5 1) to distinguish them from // integer constants. We must ensure numerator and denominator are // constant and the denominator is non-zero. - if (constVal.getKind() == api::DIVISION && constVal[0].isConst() - && constVal[1].isConst() + if (constVal.getKind() == api::DIVISION && constVal[0].isValue() + && constVal[1].isValue() && !constVal[1].getExpr().getConst<Rational>().isZero()) { std::stringstream sdiv; sdiv << constVal[0] << "/" << constVal[1]; constVal = d_solver->mkReal(sdiv.str()); } - if (!constVal.isConst()) + if (!constVal.isValue()) { std::stringstream ss; ss << "expected constant term inside array constant, but found " |