diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-03 21:49:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-03 21:49:20 +0000 |
commit | 39a66fe81b66498c82d1638c58c3c4ccc8f586db (patch) | |
tree | 5b423aabea9494abac34dad5bb5846cc7c1496c6 /src/util | |
parent | 3daaecd22fe5f6147cb08e5a4e08177b33a2daa2 (diff) |
ArrayStoreAll infrastructure
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/array_store_all.h | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h index 5647ed53d..834eec2c3 100644 --- a/src/util/array_store_all.h +++ b/src/util/array_store_all.h @@ -35,22 +35,26 @@ namespace CVC4 { namespace CVC4 { class CVC4_PUBLIC ArrayStoreAll { - const Type d_type; + const ArrayType d_type; const Expr d_expr; public: - ArrayStoreAll(Type type, Expr expr) throw(IllegalArgumentException) : + ArrayStoreAll(ArrayType type, Expr expr) throw(IllegalArgumentException) : d_type(type), d_expr(expr) { + + // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types + // because this check is done in production builds too CheckArgument(type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str()); - CheckArgument(expr.getType() == ArrayType(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.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()); } ~ArrayStoreAll() throw() { } - Type getType() const throw() { + ArrayType getType() const throw() { return d_type; } Expr getExpr() const throw() { |