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

3 files changed, 188 insertions, 0 deletions

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());
+
+  }
+
+};