ArrayStoreAll infrastructure

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index df222b684d6ecca9aa8891c8d174b3fe5b69538c..bd8e29a44119eaf958a17a6fe24be3d79c26696d 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -77,6 +77,16 @@ Expr Type::mkGroundTerm() const {
   return d_typeNode->mkGroundTerm().toExpr();
 }
 
+bool Type::isSubtypeOf(Type t) const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSubtypeOf(*t.d_typeNode);
+}
+
+bool Type::isComparableTo(Type t) const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isComparableTo(*t.d_typeNode);
+}
+
 Type& Type::operator=(const Type& t) {
   Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
   Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");

diff --git a/src/expr/type.h b/src/expr/type.h
index a813aec02d8830253206da14aac55c057ba9e439..bd6a6a298aa8282566a07fe7390e468650287e20 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -145,8 +145,7 @@ public:
   Cardinality getCardinality() const;
 
   /**
-   * Is this a well-founded type?  (I.e., do there exist ground
-   * terms?)
+   * Is this a well-founded type?
    */
   bool isWellFounded() const;
 
@@ -156,6 +155,17 @@ public:
    */
   Expr mkGroundTerm() const;
 
+  /**
+   * Is this type a subtype of the given type?
+   */
+  bool isSubtypeOf(Type t) const;
+
+  /**
+   * Is this type comparable to the given type (i.e., do they share
+   * a common ancestor in the subtype tree)?
+   */
+  bool isComparableTo(Type t) const;
+
   /**
    * Substitution of Types.
    */

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index bfbedde8869fa5082c83cc0dfa0987b40c9eb1b4..83bbb25a78d2028c2a3b0db85480bf62f4f90064 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -430,8 +430,7 @@ public:
   Cardinality getCardinality() const;
 
   /**
-   * Returns whether this type is well-founded.  A type is
-   * well-founded if there exist ground terms.
+   * Returns whether this type is well-founded.
    *
    * @return true iff the type is well-founded
    */
@@ -445,7 +444,9 @@ public:
    */
   Node mkGroundTerm() const;
 
-  /** Is this type a subtype of the given type? */
+  /**
+   * Is this type a subtype of the given type?
+   */
   bool isSubtypeOf(TypeNode t) const;
 
   /**

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index eaef3746eb863461ca15d202182d25745b69148c..4a8695ec4bd3555a74f01af2f6ec34fc1e1979fb 100644 (file)
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -29,11 +29,19 @@ operator SELECT 2 "array select"
 # store a i e  is  a[i] <= e
 operator STORE 3 "array store"
 
+# storeall t e  is  \all i in indexType(t) <= e
+constant STORE_ALL \
+    ::CVC4::ArrayStoreAll \
+    ::CVC4::ArrayStoreAllHashStrategy \
+    "util/array_store_all.h" \
+    "array store-all"
+
 # used internally by array theory
 operator ARR_TABLE_FUN 4 "array table function"
 
 typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
 typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
+typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
 
 endtheory

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 39945e081613d3e29c71b04921c87a6940567996..57baa82cdf886e1820bca67138c9c91cf18bfc10 100644 (file)
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -270,6 +270,7 @@ constant UNINTERPRETED_CONSTANT \
     ::CVC4::UninterpretedConstantHashStrategy \
     "util/uninterpreted_constant.h" \
     "The kind of nodes representing uninterpreted constants"
+typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule
 enumerator SORT_TYPE \
     ::CVC4::theory::builtin::UninterpretedSortEnumerator \
     "theory/builtin/type_enumerator.h"

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 9b0611ed8b628118d11c9611e6a2679504d16e66..d443b8452b302ccd67e4fd5fd74a36ecb180072d 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -130,6 +130,13 @@ public:
   }
 };/* class TupleTypeRule */
 
+class UninterpretedConstantTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    return TypeNode::fromType(n.getConst<UninterpretedConstant>().getType());
+  }
+};/* class UninterpretedConstantTypeRule */
+
 class StringConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {

diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h
index 5647ed53d960f955e7e7c095d215224978490b10..834eec2c3198bb2e16aa648c4b5b79af197b50a9 100644 (file)
--- 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() {

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 5f5a1e75e978b1f7c46b1f1a02bd5058753c924f..88d21cac5f5141eef74b6a5fd6319d43e75e79b7 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -36,6 +36,7 @@ UNIT_TESTS = \
        context/cdvector_black \
        context/stacking_map_black \
        context/stacking_vector_black \
+       util/array_store_all_black \
        util/assert_white \
        util/bitvector_black \
        util/datatype_black \

diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
new file mode 100644 (file)
index 0000000..915f853
--- /dev/null
+++ b/test/unit/util/array_store_all_black.h
@@ -0,0 +1,66 @@
+/*********************                                                        */
+/*! \file array_store_all_black.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::ArrayStoreAll
+ **
+ ** Black box testing of CVC4::ArrayStoreAll.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "util/array_store_all.h"
+#include "expr/expr_manager.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/type.h"
+#include "expr/expr.h"
+
+using namespace CVC4;
+using namespace std;
+
+class ArrayStoreAllBlack : public CxxTest::TestSuite {
+
+  ExprManager* d_em;
+  ExprManagerScope* d_scope;
+
+public:
+
+  void setUp() {
+    d_em = new ExprManager();
+    d_scope = new ExprManagerScope(*d_em);
+  }
+
+  void tearDown() {
+    delete d_scope;
+    delete d_em;
+  }
+
+  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)));
+  }
+
+  void testTypeErrors() {
+    // these two throw an AssertionException in assertions-enabled builds, and an IllegalArgumentException in production builds
+    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0))) );
+    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))) );
+
+    TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->integerType()), d_em->mkConst(Rational(9, 2))), IllegalArgumentException );
+    TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")), d_em->mkConst(Rational(9, 2))), IllegalArgumentException );
+    TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->realType(), d_em->integerType()), d_em->mkConst(Rational(9, 2))), IllegalArgumentException );
+  }
+
+};/* class ArrayStoreAllBlack */