Fix spurious parse error for rational real array constants (#3554)

Currently we can't parse constant arrays that store real values that are given as rationals `(/ n m)`. We throw a spurious parse error for `((as const (Array Int Real)) (/ 1 3))`, indicating that the argument of the array is not constant. This is caused by the fact that `(/ 1 3)` is parsed as a *division* term not a rational value.

This adds a special case to constant array construction so that we compute the result of a constant division instead of using the division term `(/ n m)` when constructing an array constant.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 151ecbfb4885d90bddf64ddcffb57009948c21a3..3dd03977565d4a9fdee0969dbdb51f0bce8d4e00 100644 (file)
--- 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 f4937f8f3be6e933433609404d5fb6bd44f67037..b0539325885dfb94789aa34bdf2ad6215cf47701 100644 (file)
--- 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 (file)
index 0000000..0246380
--- /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)