From dec12c33bf05638b3e5f69e4b83684524ce6f6aa Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Sun, 26 Aug 2012 17:56:55 +0000 Subject: Array constants finished and working. Unit tests for array constants. --- src/theory/arrays/theory_arrays_rewriter.h | 16 ++- src/theory/arrays/theory_arrays_type_rules.h | 48 +++++---- test/unit/Makefile.am | 1 + test/unit/expr/expr_public.h | 35 ++++++ test/unit/theory/theory_black.h | 152 +++++++++++++++++++++++++++ 5 files changed, 220 insertions(+), 32 deletions(-) create mode 100644 test/unit/theory/theory_black.h 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(); + 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 + +//Used in some of the tests +#include +#include + +#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()); + + } + +}; -- cgit v1.2.3