From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 16 Aug 2012 19:58:32 +0000 (+0000)
Subject: ArrayStoreAll should (for now) only allow constant expressions, as it is itself a... 
X-Git-Tag: cvc5-1.0.0~7866
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d260caa58d462f7e1eb0d94f73789f844f5f5596;p=cvc5.git

ArrayStoreAll should (for now) only allow constant expressions, as it is itself a CONSTANT.
---

diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h
index 277422ecf..7cfe2eab4 100644
--- a/src/util/array_store_all.h
+++ b/src/util/array_store_all.h
@@ -49,6 +49,7 @@ public:
     CheckArgument(type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str());
 
     CheckArgument(expr.getType().isSubtypeOf(type.getConstituentType()), expr, "expr type `%s' does not match constituent type of array type `%s'", expr.getType().toString().c_str(), type.toString().c_str());
+    CheckArgument(expr.isConst(), expr, "ArrayStoreAll requires a constant expression");
   }
 
   ~ArrayStoreAll() throw() {
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 915f853d6..2c1bd959d 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -47,7 +47,6 @@ public:
   void testStoreAll() {
     Type usort = d_em->mkSort("U");
     ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()), d_em->mkConst(Rational(9, 2)));
-    ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort));
     ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkConst(UninterpretedConstant(usort, 0)));
     ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()), d_em->mkConst(Rational(0)));
     ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()), d_em->mkConst(Rational(0)));
@@ -63,4 +62,11 @@ public:
     TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->realType(), d_em->integerType()), d_em->mkConst(Rational(9, 2))), IllegalArgumentException );
   }
 
+  void testConstError() {
+    Type usort = d_em->mkSort("U");
+    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)) );
+    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkVar("x", d_em->integerType())) );
+    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)), d_em->mkConst(Rational(0)))) );
+  }
+
 };/* class ArrayStoreAllBlack */