Array constants finished and working. Unit tests for array constants.

diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 4402c43ea1a2db23bbffc407b5087f49831ff085..d120f8feb4fe00e15d707405261eca4af80cfe2b 100644 (file)
--- 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 2cad1fa439fecebd938bb0d9ab6beac43d5d9aa2..8b31a31f90b4008eb880adbae19c89781fdb9b96 100644 (file)
--- 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 470fdac3df7e80c7810bd6a6f2858de76bd476e0..716b8959eb482568d60977fd746813ada1729867 100644 (file)
--- 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 d4a968e9667fc08be841df5f5a7172b20f95ce94..279d4bebea15383c34265065bdc76b38e8e04f02 100644 (file)
--- 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 (file)
index 0000000..4af34db
--- /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());
+
+  }
+
+};