diff options
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 37 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/array-const-real-parse.smt2 | 7 |
3 files changed, 36 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) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f4937f8f3..b05393258 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -36,6 +36,7 @@ set(regress_0_tests regress0/arith/mod-simp.smt2 regress0/arith/mod.01.smt2 regress0/arith/mult.01.smt2 + regress0/array-const-real-parse.smt2 regress0/arrayinuf_declare.smt2 regress0/arrays/arrays0.smt2 regress0/arrays/arrays1.smt2 diff --git a/test/regress/regress0/array-const-real-parse.smt2 b/test/regress/regress0/array-const-real-parse.smt2 new file mode 100644 index 000000000..0246380f8 --- /dev/null +++ b/test/regress/regress0/array-const-real-parse.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_AUFLIRA) +(set-info :status sat) +(declare-fun a () (Array Int Real)) +(assert (= a ((as const (Array Int Real)) 0.0))) +(declare-fun b () (Array Int Real)) +(assert (= b ((as const (Array Int Real)) (/ 1 3)))) +(check-sat) |