From: Aina Niemetz Date: Mon, 1 Mar 2021 12:22:48 +0000 (-0800) Subject: google test: util: Migrate array_store_all_white. (#6008) X-Git-Tag: cvc5-1.0.0~2189 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2dec0e1ed6eb413e6af3496fcc2aaa297d2a9f66;p=cvc5.git google test: util: Migrate array_store_all_white. (#6008) --- diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 52719e6f4..ab7bf25f5 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -11,7 +11,7 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_cxx_unit_test_white(array_store_all_white util) +cvc4_add_unit_test_white(array_store_all_white util) cvc4_add_unit_test_white(assert_white util) cvc4_add_unit_test_black(binary_heap_black util) cvc4_add_cxx_unit_test_black(bitvector_black util) diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp new file mode 100644 index 000000000..a0a954008 --- /dev/null +++ b/test/unit/util/array_store_all_white.cpp @@ -0,0 +1,81 @@ +/********************* */ +/*! \file array_store_all_white.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::ArrayStoreAll + ** + ** Black box testing of CVC4::ArrayStoreAll. + **/ + +#include "expr/array_store_all.h" +#include "expr/expr.h" +#include "expr/type.h" +#include "test_smt.h" +#include "test_utils.h" + +namespace CVC4 { +namespace test { + +class TestUtilWhiteArrayStoreAll : public TestSmt +{ +}; + +TEST_F(TestUtilWhiteArrayStoreAll, store_all) +{ + TypeNode usort = d_nodeManager->mkSort("U"); + ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->realType()), + d_nodeManager->mkConst(Rational(9, 2))); + ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort), + d_nodeManager->mkConst(UninterpretedConstant(usort, 0))); + ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), + d_nodeManager->realType()), + d_nodeManager->mkConst(Rational(0))); + ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), + d_nodeManager->integerType()), + d_nodeManager->mkConst(Rational(0))); +} + +TEST_F(TestUtilWhiteArrayStoreAll, type_errors) +{ + ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkConst(UninterpretedConstant( + d_nodeManager->mkSort("U"), 0))), + IllegalArgumentException); + ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkConst(Rational(9, 2))), + IllegalArgumentException); + ASSERT_THROW( + ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->mkSort("U")), + d_nodeManager->mkConst(Rational(9, 2))), + IllegalArgumentException); +} + +TEST_F(TestUtilWhiteArrayStoreAll, const_error) +{ + TypeNode usort = d_nodeManager->mkSort("U"); + ASSERT_THROW(ArrayStoreAll(d_nodeManager->mkArrayType( + d_nodeManager->mkSort("U"), usort), + d_nodeManager->mkVar(usort)), + IllegalArgumentException); + ASSERT_THROW( + ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkVar("x", d_nodeManager->integerType())), + IllegalArgumentException); + ASSERT_THROW( + ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkNode(kind::PLUS, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkConst(Rational(0)))), + IllegalArgumentException); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/util/array_store_all_white.h b/test/unit/util/array_store_all_white.h deleted file mode 100644 index 2e107f668..000000000 --- a/test/unit/util/array_store_all_white.h +++ /dev/null @@ -1,94 +0,0 @@ -/********************* */ -/*! \file array_store_all_white.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Morgan Deters, Clark Barrett - ** 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::ArrayStoreAll - ** - ** Black box testing of CVC4::ArrayStoreAll. - **/ - -#include - -#include "api/cvc4cpp.h" -#include "expr/array_store_all.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "expr/type.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "test_utils.h" - -using namespace CVC4; -using namespace std; - -class ArrayStoreAllWhite : public CxxTest::TestSuite -{ - public: - void setUp() override - { - d_slv = new api::Solver(); - d_scope = new smt::SmtScope(d_slv->getSmtEngine()); - d_nm = d_slv->getSmtEngine()->d_nodeManager; - } - - void tearDown() override - { - delete d_scope; - delete d_slv; - } - - void testStoreAll() - { - TypeNode usort = d_nm->mkSort("U"); - ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->realType()), - d_nm->mkConst(Rational(9, 2))); - ArrayStoreAll(d_nm->mkArrayType(d_nm->mkSort("U"), usort), - d_nm->mkConst(UninterpretedConstant(usort, 0))); - ArrayStoreAll(d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->realType()), - d_nm->mkConst(Rational(0))); - ArrayStoreAll( - d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->integerType()), - d_nm->mkConst(Rational(0))); - } - - void testTypeErrors() - { - TS_ASSERT_THROWS(ArrayStoreAll(d_nm->integerType(), - d_nm->mkConst(UninterpretedConstant( - d_nm->mkSort("U"), 0))), - IllegalArgumentException&); - TS_ASSERT_THROWS( - ArrayStoreAll(d_nm->integerType(), d_nm->mkConst(Rational(9, 2))), - IllegalArgumentException&); - TS_ASSERT_THROWS( - ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->mkSort("U")), - d_nm->mkConst(Rational(9, 2))), - IllegalArgumentException&); - } - - void testConstError() - { - TypeNode usort = d_nm->mkSort("U"); - TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( - d_nm->mkArrayType(d_nm->mkSort("U"), usort), d_nm->mkVar(usort))); - TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( - d_nm->integerType(), d_nm->mkVar("x", d_nm->integerType()))); - TS_ASSERT_THROWS_ANYTHING( - ArrayStoreAll(d_nm->integerType(), - d_nm->mkNode(kind::PLUS, - d_nm->mkConst(Rational(1)), - d_nm->mkConst(Rational(0))))); - } - - private: - api::Solver* d_slv; - smt::SmtScope* d_scope; - NodeManager* d_nm; -}; /* class ArrayStoreAllBlack */