From: Morgan Deters Date: Fri, 3 Aug 2012 21:49:20 +0000 (+0000) Subject: ArrayStoreAll infrastructure X-Git-Tag: cvc5-1.0.0~7892 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39a66fe81b66498c82d1638c58c3c4ccc8f586db;p=cvc5.git ArrayStoreAll infrastructure --- diff --git a/src/expr/type.cpp b/src/expr/type.cpp index df222b684..bd8e29a44 100644 --- 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 a813aec02..bd6a6a298 100644 --- 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 bfbedde88..83bbb25a7 100644 --- 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 eaef3746e..4a8695ec4 100644 --- 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 39945e081..57baa82cd 100644 --- 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 9b0611ed8..d443b8452 100644 --- 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().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 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() { diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 5f5a1e75e..88d21cac5 100644 --- 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 index 000000000..915f853d6 --- /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 + +#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 */