From 82aebfb5c8c30e778453fc818d132a9158349d55 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 24 Feb 2021 10:24:14 -0800 Subject: [PATCH] google test: theory: Migrate theory_black. (#5985) --- test/unit/theory/CMakeLists.txt | 2 +- test/unit/theory/theory_black.cpp | 133 +++++++++++++++++++++++++ test/unit/theory/theory_black.h | 158 ------------------------------ 3 files changed, 134 insertions(+), 159 deletions(-) create mode 100644 test/unit/theory/theory_black.cpp delete mode 100644 test/unit/theory/theory_black.h diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 1af33ff19..f972efd47 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -9,7 +9,7 @@ ## directory for licensing information. ## cvc4_add_unit_test_black(regexp_operation_black theory) -cvc4_add_cxx_unit_test_black(theory_black theory) +cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_unit_test_white(sequences_rewriter_white theory) diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp new file mode 100644 index 000000000..0aba243b5 --- /dev/null +++ b/test/unit/theory/theory_black.cpp @@ -0,0 +1,133 @@ +/********************* */ +/*! \file theory_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. 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 +#include + +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_value.h" +#include "test_smt.h" +#include "theory/rewriter.h" + +namespace CVC4 { + +using namespace kind; +using namespace context; +using namespace theory; +using namespace smt; + +namespace test { + +class TestTheoryBlack : public TestSmt +{ +}; + +TEST_F(TestTheoryBlack, array_const) +{ + TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->integerType()); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + ASSERT_TRUE(storeAll.isConst()); + + Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + ASSERT_FALSE(arr.isConst()); + arr = Rewriter::rewrite(arr); + ASSERT_TRUE(arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + ASSERT_TRUE(arr.isConst()); + Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + ASSERT_FALSE(arr2.isConst()); + arr2 = Rewriter::rewrite(arr2); + ASSERT_TRUE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, one); + ASSERT_TRUE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + ASSERT_FALSE(arr2.isConst()); + arr2 = Rewriter::rewrite(arr2); + ASSERT_TRUE(arr2.isConst()); + + arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), + d_nodeManager->mkBitVectorType(1)); + zero = d_nodeManager->mkConst(BitVector(1, 0u)); + one = d_nodeManager->mkConst(BitVector(1, 1u)); + storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + ASSERT_TRUE(storeAll.isConst()); + + arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + ASSERT_FALSE(arr.isConst()); + arr = Rewriter::rewrite(arr); + ASSERT_TRUE(arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + arr = Rewriter::rewrite(arr); + ASSERT_TRUE(arr.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + ASSERT_FALSE(arr2.isConst()); + arr2 = Rewriter::rewrite(arr2); + ASSERT_TRUE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, one); + ASSERT_FALSE(arr2.isConst()); + arr2 = Rewriter::rewrite(arr2); + ASSERT_TRUE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + ASSERT_FALSE(arr2.isConst()); + arr2 = Rewriter::rewrite(arr2); + ASSERT_TRUE(arr2.isConst()); + + arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(2), + d_nodeManager->mkBitVectorType(2)); + zero = d_nodeManager->mkConst(BitVector(2, 0u)); + one = d_nodeManager->mkConst(BitVector(2, 1u)); + Node two = d_nodeManager->mkConst(BitVector(2, 2u)); + Node three = d_nodeManager->mkConst(BitVector(2, 3u)); + storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, one)); + ASSERT_TRUE(storeAll.isConst()); + + arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + ASSERT_TRUE(arr.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + ASSERT_FALSE(arr2.isConst()); + arr2 = Rewriter::rewrite(arr2); + ASSERT_TRUE(arr2.isConst()); + + arr = d_nodeManager->mkNode(STORE, storeAll, one, three); + ASSERT_TRUE(arr.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, one); + ASSERT_FALSE(arr2.isConst()); + arr2 = Rewriter::rewrite(arr2); + ASSERT_TRUE(arr2 == storeAll); + + arr2 = d_nodeManager->mkNode(STORE, arr, zero, zero); + ASSERT_FALSE(arr2.isConst()); + ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr2, two, two); + ASSERT_FALSE(arr2.isConst()); + ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr2, three, one); + ASSERT_FALSE(arr2.isConst()); + ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr2, three, three); + ASSERT_FALSE(arr2.isConst()); + ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr2, two, zero); + ASSERT_FALSE(arr2.isConst()); + arr2 = Rewriter::rewrite(arr2); + ASSERT_TRUE(arr2.isConst()); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h deleted file mode 100644 index bd843eb16..000000000 --- a/test/unit/theory/theory_black.h +++ /dev/null @@ -1,158 +0,0 @@ -/********************* */ -/*! \file theory_black.h - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Andres Noetzli, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. 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 "api/cvc4cpp.h" -#include "expr/expr_manager.h" -#include "expr/node.h" -#include "expr/node_builder.h" -#include "expr/node_manager.h" -#include "expr/node_value.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 { - public: - void setUp() override - { - d_slv = new api::Solver(); - d_em = d_slv->getExprManager(); - d_smt = d_slv->getSmtEngine(); - d_scope = new SmtScope(d_smt); - // Ensure that the SMT engine is fully initialized (required for the - // rewriter) - d_smt->push(); - - d_nm = NodeManager::fromExprManager(d_em); - } - - void tearDown() override - { - delete d_scope; - delete d_slv; - } - - 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, zero)); - 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, zero)); - 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); - arr = Rewriter::rewrite(arr); - 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, one)); - 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()); - - } - - private: - api::Solver* d_slv; - ExprManager* d_em; - SmtEngine* d_smt; - NodeManager* d_nm; - SmtScope* d_scope; -}; -- 2.30.2