diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 37 |
1 files changed, 28 insertions, 9 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 151ecbfb4..3dd039775 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1772,25 +1772,44 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) { parseError("Too many arguments to array constant."); } - if (!args[0].isConst()) + Expr constVal = args[0]; + if (!constVal.isConst()) { - std::stringstream ss; - ss << "expected constant term inside array constant, but found " - << "nonconstant term:" << std::endl - << "the term: " << args[0]; - parseError(ss.str()); + // To parse array constants taking reals whose values are specified by + // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle + // the fact that (/ 1 3) is the division of constants 1 and 3, and not + // the resulting constant rational value. Thus, we must construct the + // resulting rational here. This also is applied for integral real values + // 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() == kind::DIVISION && constVal[0].isConst() + && constVal[1].isConst() + && !constVal[1].getConst<Rational>().isZero()) + { + constVal = em->mkConst(constVal[0].getConst<Rational>() + / constVal[1].getConst<Rational>()); + } + if (!constVal.isConst()) + { + std::stringstream ss; + ss << "expected constant term inside array constant, but found " + << "nonconstant term:" << std::endl + << "the term: " << constVal; + parseError(ss.str()); + } } ArrayType aqtype = static_cast<ArrayType>(p.d_type); - if (!aqtype.getConstituentType().isComparableTo(args[0].getType())) + if (!aqtype.getConstituentType().isComparableTo(constVal.getType())) { std::stringstream ss; ss << "type mismatch inside array constant term:" << std::endl << "array type: " << p.d_type << std::endl << "expected const type: " << aqtype.getConstituentType() << std::endl - << "computed const type: " << args[0].getType(); + << "computed const type: " << constVal.getType(); parseError(ss.str()); } - return em->mkConst(ArrayStoreAll(p.d_type, args[0])); + return em->mkConst(ArrayStoreAll(p.d_type, constVal)); } else if (p.d_kind == kind::APPLY_SELECTOR) { |