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. --- test/unit/Makefile.am | 1 + test/unit/expr/expr_public.h | 35 +++++++++ test/unit/theory/theory_black.h | 152 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 188 insertions(+) create mode 100644 test/unit/theory/theory_black.h (limited to 'test/unit') 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