summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h16
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h48
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/expr/expr_public.h35
-rw-r--r--test/unit/theory/theory_black.h152
5 files changed, 220 insertions, 32 deletions
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 4402c43ea..d120f8feb 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -119,14 +119,10 @@ class TheoryArraysRewriter {
TNode mostFrequentValue;
unsigned mostFrequentValueCount = 0;
- bool recompute CVC4_UNUSED = false;
- if (node[0].getKind() == kind::STORE) {
- // TODO: look up most frequent value and count
- mostFrequentValue = node.getAttribute(ArrayConstantMostFrequentValueAttr());
- mostFrequentValueCount = node.getAttribute(ArrayConstantMostFrequentValueCountAttr());
- if (!replacedValue.isNull() && mostFrequentValue == replacedValue) {
- recompute = true;
- }
+ store = node[0];
+ if (store.getKind() == kind::STORE) {
+ mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr());
+ mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
}
// Compute the most frequently written value for n
@@ -134,7 +130,6 @@ class TheoryArraysRewriter {
(valCount == mostFrequentValueCount && value < mostFrequentValue)) {
mostFrequentValue = value;
mostFrequentValueCount = valCount;
- recompute = false;
}
// Need to make sure the default value count is larger, or the same and the default value is expression-order-less-than nextValue
@@ -180,7 +175,7 @@ class TheoryArraysRewriter {
Assert(compare != Cardinality::UNKNOWN);
if (compare == Cardinality::GREATER ||
(compare == Cardinality::EQUAL && (defaultValue < maxValue))) {
- Assert(recompute);
+ Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
return n;
}
@@ -283,6 +278,7 @@ public:
if (store.isConst() && index.isConst() && value.isConst()) {
// normalize constant
Node n = normalizeConstant(node);
+ Assert(n.isConst());
Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
return RewriteResponse(REWRITE_DONE, n);
}
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 2cad1fa43..8b31a31f9 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -48,24 +48,31 @@ struct ArraySelectTypeRule {
struct ArrayStoreTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
- Assert(n.getKind() == kind::STORE);
- TypeNode arrayType = n[0].getType(check);
- if( check ) {
- if(!arrayType.isArray()) {
- throw TypeCheckingExceptionPrivate(n, "array store operating on non-array");
- }
- TypeNode indexType = n[1].getType(check);
- TypeNode valueType = n[2].getType(check);
- if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
- throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
- }
- if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){
- Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
- Debug("array-types") << "value types: " << valueType << std::endl;
- throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
+ if (n.getKind() == kind::STORE) {
+ TypeNode arrayType = n[0].getType(check);
+ if( check ) {
+ if(!arrayType.isArray()) {
+ throw TypeCheckingExceptionPrivate(n, "array store operating on non-array");
+ }
+ TypeNode indexType = n[1].getType(check);
+ TypeNode valueType = n[2].getType(check);
+ if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
+ throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
+ }
+ if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){
+ Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
+ Debug("array-types") << "value types: " << valueType << std::endl;
+ throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
+ }
}
+ return arrayType;
+ }
+ else {
+ Assert(n.getKind() == kind::STORE_ALL);
+ ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
+ ArrayType arrayType = storeAll.getType();
+ return TypeNode::fromType(arrayType);
}
- return arrayType;
}
inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
@@ -116,14 +123,13 @@ struct ArrayStoreTypeRule {
// that is written to more than the default value. If so, it is not in
// normal form.
- // Get the most frequently written value from n[0]
+ // Get the most frequently written value for n[0]
TNode mostFrequentValue;
unsigned mostFrequentValueCount = 0;
store = n[0];
if (store.getKind() == kind::STORE) {
- // TODO: look up most frequent value and count
- mostFrequentValue = n.getAttribute(ArrayConstantMostFrequentValueAttr());
- mostFrequentValueCount = n.getAttribute(ArrayConstantMostFrequentValueCountAttr());
+ mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr());
+ mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
}
// Compute the most frequently written value for n
@@ -140,8 +146,6 @@ struct ArrayStoreTypeRule {
(compare == Cardinality::EQUAL && (!(defaultValue < mostFrequentValue)))) {
return false;
}
-
- // TODO: store mostFrequentValue and mostFrequentValueCount for this node
n.setAttribute(ArrayConstantMostFrequentValueAttr(), mostFrequentValue);
n.setAttribute(ArrayConstantMostFrequentValueCountAttr(), mostFrequentValueCount);
return true;
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 470fdac3d..716b8959e 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -2,6 +2,7 @@
UNIT_TESTS = \
theory/logic_info_white \
theory/theory_engine_white \
+ theory/theory_black \
theory/theory_white \
theory/theory_arith_white \
theory/theory_bv_white \
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index d4a968e96..279d4bebe 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -373,6 +373,41 @@ public:
TS_ASSERT(!cons_x_nil.isConst());
TS_ASSERT(cons_1_nil.isConst());
TS_ASSERT(cons_1_cons_2_nil.isConst());
+
+ ArrayType arrType = d_em->mkArrayType(d_em->integerType(), d_em->integerType());
+ Expr zero = d_em->mkConst(Rational(0));
+ Expr one = d_em->mkConst(Rational(1));
+ Expr storeAll = d_em->mkConst(ArrayStoreAll(arrType, zero));
+ TS_ASSERT(storeAll.isConst());
+
+ Expr arr = d_em->mkExpr(STORE, storeAll, zero, zero);
+ TS_ASSERT(!arr.isConst());
+ arr = d_em->mkExpr(STORE, storeAll, zero, one);
+ TS_ASSERT(arr.isConst());
+ Expr arr2 = d_em->mkExpr(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, one);
+ TS_ASSERT(arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, zero, one);
+ TS_ASSERT(!arr2.isConst());
+
+ arrType = d_em->mkArrayType(d_em->mkBitVectorType(1), d_em->mkBitVectorType(1));
+ zero = d_em->mkConst(BitVector(1,unsigned(0)));
+ one = d_em->mkConst(BitVector(1,unsigned(1)));
+ storeAll = d_em->mkConst(ArrayStoreAll(arrType, zero));
+ TS_ASSERT(storeAll.isConst());
+
+ arr = d_em->mkExpr(STORE, storeAll, zero, zero);
+ TS_ASSERT(!arr.isConst());
+ arr = d_em->mkExpr(STORE, storeAll, zero, one);
+ TS_ASSERT(arr.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, one);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, zero, one);
+ TS_ASSERT(!arr2.isConst());
+
}
void testGetConst() {
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
new file mode 100644
index 000000000..4af34dba5
--- /dev/null
+++ b/test/unit/theory/theory_black.h
@@ -0,0 +1,152 @@
+/********************* */
+/*! \file theory_black.h
+ ** \verbatim
+ ** Original author: barrett
+ ** Major contributors: barrett
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011, 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::theory
+ **
+ ** Black box testing of CVC4::theory
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+//Used in some of the tests
+#include <vector>
+#include <sstream>
+
+#include "expr/expr_manager.h"
+#include "expr/node_value.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::smt;
+
+class TheoryBlack : public CxxTest::TestSuite {
+private:
+
+ ExprManager* d_em;
+ SmtEngine* d_smt;
+ NodeManager* d_nm;
+ SmtScope* d_scope;
+
+public:
+
+ void setUp() {
+ d_em = new ExprManager();
+ d_smt = new SmtEngine(d_em);
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_scope = new SmtScope(d_smt);
+ }
+
+ void tearDown() {
+ delete d_em;
+ }
+
+ void testArrayConst() {
+ TypeNode arrType = d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType());
+ Node zero = d_nm->mkConst(Rational(0));
+ Node one = d_nm->mkConst(Rational(1));
+ Node storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), zero.toExpr()));
+ TS_ASSERT(storeAll.isConst());
+
+ Node arr = d_nm->mkNode(STORE, storeAll, zero, zero);
+ TS_ASSERT(!arr.isConst());
+ arr = Rewriter::rewrite(arr);
+ TS_ASSERT(arr.isConst());
+ arr = d_nm->mkNode(STORE, storeAll, zero, one);
+ TS_ASSERT(arr.isConst());
+ Node arr2 = d_nm->mkNode(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = Rewriter::rewrite(arr2);
+ TS_ASSERT(arr2.isConst());
+ arr2 = d_nm->mkNode(STORE, arr, one, one);
+ TS_ASSERT(arr2.isConst());
+ arr2 = d_nm->mkNode(STORE, arr, zero, one);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = Rewriter::rewrite(arr2);
+ TS_ASSERT(arr2.isConst());
+
+ arrType = d_nm->mkArrayType(d_nm->mkBitVectorType(1), d_nm->mkBitVectorType(1));
+ zero = d_nm->mkConst(BitVector(1,unsigned(0)));
+ one = d_nm->mkConst(BitVector(1,unsigned(1)));
+ storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), zero.toExpr()));
+ TS_ASSERT(storeAll.isConst());
+
+ arr = d_nm->mkNode(STORE, storeAll, zero, zero);
+ TS_ASSERT(!arr.isConst());
+ arr = Rewriter::rewrite(arr);
+ TS_ASSERT(arr.isConst());
+ arr = d_nm->mkNode(STORE, storeAll, zero, one);
+ TS_ASSERT(arr.isConst());
+ arr2 = d_nm->mkNode(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = Rewriter::rewrite(arr2);
+ TS_ASSERT(arr2.isConst());
+ arr2 = d_nm->mkNode(STORE, arr, one, one);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = Rewriter::rewrite(arr2);
+ TS_ASSERT(arr2.isConst());
+ arr2 = d_nm->mkNode(STORE, arr, zero, one);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = Rewriter::rewrite(arr2);
+ TS_ASSERT(arr2.isConst());
+
+ arrType = d_nm->mkArrayType(d_nm->mkBitVectorType(2), d_nm->mkBitVectorType(2));
+ zero = d_nm->mkConst(BitVector(2,unsigned(0)));
+ one = d_nm->mkConst(BitVector(2,unsigned(1)));
+ Node two = d_nm->mkConst(BitVector(2,unsigned(2)));
+ Node three = d_nm->mkConst(BitVector(2,unsigned(3)));
+ storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), one.toExpr()));
+ TS_ASSERT(storeAll.isConst());
+
+ arr = d_nm->mkNode(STORE, storeAll, zero, zero);
+ TS_ASSERT(arr.isConst());
+ arr2 = d_nm->mkNode(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = Rewriter::rewrite(arr2);
+ TS_ASSERT(arr2.isConst());
+
+ arr = d_nm->mkNode(STORE, storeAll, one, three);
+ TS_ASSERT(arr.isConst());
+ arr2 = d_nm->mkNode(STORE, arr, one, one);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = Rewriter::rewrite(arr2);
+ TS_ASSERT(arr2 == storeAll);
+
+ arr2 = d_nm->mkNode(STORE, arr, zero, zero);
+ TS_ASSERT(!arr2.isConst());
+ TS_ASSERT(Rewriter::rewrite(arr2).isConst());
+ arr2 = d_nm->mkNode(STORE, arr2, two, two);
+ TS_ASSERT(!arr2.isConst());
+ TS_ASSERT(Rewriter::rewrite(arr2).isConst());
+ arr2 = d_nm->mkNode(STORE, arr2, three, one);
+ TS_ASSERT(!arr2.isConst());
+ TS_ASSERT(Rewriter::rewrite(arr2).isConst());
+ arr2 = d_nm->mkNode(STORE, arr2, three, three);
+ TS_ASSERT(!arr2.isConst());
+ TS_ASSERT(Rewriter::rewrite(arr2).isConst());
+ arr2 = d_nm->mkNode(STORE, arr2, two, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = Rewriter::rewrite(arr2);
+ TS_ASSERT(arr2.isConst());
+
+ }
+
+};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback