Fix parsing array constants (#7617)

This generalizes a fix for parsing array constants.

Fixes #7596.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ef784746ccebf561f0c6f696cc3696762c5c4c91..1fc7a637fb6efb58f4087f6efc8b3b4994cd93c8 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1011,13 +1011,32 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     // 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() == api::DIVISION)
+    // constant and the denominator is non-zero. A similar issue happens for
+    // negative integers and reals, with unary minus.
+    bool isNeg = false;
+    if (constVal.getKind() == api::UMINUS)
+    {
+      isNeg = true;
+      constVal = constVal[0];
+    }
+    if (constVal.getKind() == api::DIVISION
+        && constVal[0].getKind() == api::CONST_RATIONAL
+        && constVal[1].getKind() == api::CONST_RATIONAL)
     {
       std::stringstream sdiv;
-      sdiv << constVal[0] << "/" << constVal[1];
+      sdiv << (isNeg ? "-" : "") << constVal[0] << "/" << constVal[1];
       constVal = d_solver->mkReal(sdiv.str());
     }
+    else if (constVal.getKind() == api::CONST_RATIONAL && isNeg)
+    {
+      std::stringstream sneg;
+      sneg << "-" << constVal;
+      constVal = d_solver->mkInteger(sneg.str());
+    }
+    else
+    {
+      constVal = args[0];
+    }
 
     if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
     {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b08b2f6f5eb34aff502530a3a3ca06a99e939b08..9574628a8b1c3358d3feda64a9f6d323dfed3090 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -109,6 +109,7 @@ set(regress_0_tests
   regress0/arrays/issue3813-massign-assert.smt2
   regress0/arrays/issue3814.smt2
   regress0/arrays/issue4927-unsat-cores.smt2
+  regress0/arrays/issue7596-define-array-uminus.smt2
   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
   regress0/arrays/x2.smtv1.smt2
   regress0/arrays/x3.smtv1.smt2

diff --git a/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2
new file mode 100644 (file)
index 0000000..da21db2
--- /dev/null
+++ b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(define-fun foo () (Array Int Int) ((as const (Array Int Int)) (- 1)))
+(assert (= (select foo 0) (- 1)))
+(check-sat)