From: Aina Niemetz Date: Fri, 26 Feb 2021 22:11:49 +0000 (-0800) Subject: google test: theory: Migrate theory_sets_type_rules_white. (#6001) X-Git-Tag: cvc5-1.0.0~2199 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e9116e5e3962ccda697b05cef65f3f31bb794ce;p=cvc5.git google test: theory: Migrate theory_sets_type_rules_white. (#6001) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index d2e9b2e92..90155518e 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -24,7 +24,7 @@ cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) -cvc4_add_cxx_unit_test_white(theory_sets_type_rules_white theory) +cvc4_add_unit_test_white(theory_sets_type_rules_white theory) cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_cxx_unit_test_white(theory_strings_word_white theory) cvc4_add_cxx_unit_test_white(theory_white theory) diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp new file mode 100644 index 000000000..3c1d64b84 --- /dev/null +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -0,0 +1,86 @@ +/********************* */ +/*! \file theory_sets_type_rules_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Mudathir Mohamed + ** 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 White box testing of sets typing rules + **/ + +#include "expr/dtype.h" +#include "test_api.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace CVC4::api; + +namespace test { + +class TestTheoryWhiteSetsTypeRuleApi : public TestApi +{ +}; +class TestTheoryWhiteSetsTypeRuleInternal : public TestNode +{ +}; + +TEST_F(TestTheoryWhiteSetsTypeRuleInternal, is_comparable_to) +{ + TypeNode setRealType = d_nodeManager->mkSetType(d_nodeManager->realType()); + TypeNode setIntType = d_nodeManager->mkSetType(d_nodeManager->integerType()); + ASSERT_FALSE(setIntType.isComparableTo(setRealType)); + ASSERT_FALSE(setIntType.isSubtypeOf(setRealType)); + ASSERT_FALSE(setRealType.isComparableTo(setIntType)); + ASSERT_FALSE(setRealType.isComparableTo(setIntType)); +} + +TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term) +{ + Sort realSort = d_solver.getRealSort(); + Sort intSort = d_solver.getIntegerSort(); + Term emptyReal = d_solver.mkEmptySet(d_solver.mkSetSort(realSort)); + Term integerOne = d_solver.mkInteger(1); + Term realOne = d_solver.mkReal(1); + Term singletonInt = d_solver.mkTerm(api::SINGLETON, integerOne); + Term singletonReal = d_solver.mkTerm(api::SINGLETON, realOne); + // (union + // (singleton (singleton_op Int) 1) + // (as emptyset (Set Real))) + ASSERT_THROW(d_solver.mkTerm(UNION, singletonInt, emptyReal), + CVC4ApiException); + // (union + // (singleton (singleton_op Real) 1) + // (as emptyset (Set Real))) + ASSERT_NO_THROW(d_solver.mkTerm(UNION, singletonReal, emptyReal)); +} + +TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node) +{ + Node singletonInt = + d_nodeManager->mkConst(SingletonOp(d_nodeManager->integerType())); + Node singletonReal = + d_nodeManager->mkConst(SingletonOp(d_nodeManager->realType())); + Node intConstant = d_nodeManager->mkConst(Rational(1)); + Node realConstant = d_nodeManager->mkConst(Rational(1, 5)); + // (singleton (singleton_op Real) 1) + ASSERT_NO_THROW( + d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant)); + // (singleton (singleton_op Int) (/ 1 5)) + ASSERT_DEATH( + d_nodeManager->mkSingleton(d_nodeManager->integerType(), realConstant), + "Invalid operands for mkSingleton"); + + Node n = d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant); + // the type of (singleton (singleton_op Real) 1) is (Set Real) + ASSERT_TRUE(n.getType() + == d_nodeManager->mkSetType(d_nodeManager->realType())); + // (singleton (singleton_op Real) 1) is a constant in normal form + ASSERT_TRUE(n.isConst()); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h deleted file mode 100644 index 4d60dea52..000000000 --- a/test/unit/theory/theory_sets_type_rules_white.h +++ /dev/null @@ -1,100 +0,0 @@ -/********************* */ -/*! \file theory_sets_type_rules_white.h - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, Andrew Reynolds - ** 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 White box testing of sets typing rules - **/ - -#include - -#include "api/cvc4cpp.h" -#include "expr/dtype.h" -#include "smt/smt_engine.h" - -using namespace CVC4; -using namespace CVC4::api; - -class SetsTypeRuleWhite : public CxxTest::TestSuite -{ - public: - void setUp() override - { - d_slv.reset(new Solver()); - d_em.reset(new ExprManager()); - d_nm.reset(NodeManager::fromExprManager(d_em.get())); - d_smt.reset(new SmtEngine(d_nm.get())); - d_smt->finishInit(); - } - - void tearDown() override - { - d_slv.reset(); - d_smt.reset(); - d_nm.release(); - d_em.reset(); - } - - void testIsisComparableTo() - { - TypeNode setRealType = d_nm->mkSetType(d_nm->realType()); - TypeNode setIntType = d_nm->mkSetType(d_nm->integerType()); - TS_ASSERT(!setIntType.isComparableTo(setRealType)); - TS_ASSERT(!setIntType.isSubtypeOf(setRealType)); - TS_ASSERT(!setRealType.isComparableTo(setIntType)); - TS_ASSERT(!setRealType.isComparableTo(setIntType)); - } - - void testSingletonTerm() - { - Sort realSort = d_slv->getRealSort(); - Sort intSort = d_slv->getIntegerSort(); - Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort)); - Term integerOne = d_slv->mkInteger(1); - Term realOne = d_slv->mkReal(1); - Term singletonInt = d_slv->mkTerm(api::SINGLETON, integerOne); - Term singletonReal = d_slv->mkTerm(api::SINGLETON, realOne); - // (union - // (singleton (singleton_op Int) 1) - // (as emptyset (Set Real))) - TS_ASSERT_THROWS(d_slv->mkTerm(UNION, singletonInt, emptyReal), - CVC4ApiException&); - // (union - // (singleton (singleton_op Real) 1) - // (as emptyset (Set Real))) - TS_ASSERT_THROWS_NOTHING(d_slv->mkTerm(UNION, singletonReal, emptyReal)); - } - - void testSingletonNode() - { - Node singletonInt = d_nm->mkConst(SingletonOp(d_nm->integerType())); - Node singletonReal = d_nm->mkConst(SingletonOp(d_nm->realType())); - Node intConstant = d_nm->mkConst(Rational(1)); - Node realConstant = d_nm->mkConst(Rational(1, 5)); - // (singleton (singleton_op Real) 1) - TS_ASSERT_THROWS_NOTHING( - d_nm->mkSingleton(d_nm->realType(), intConstant)); - // (singleton (singleton_op Int) (/ 1 5)) - // This fails now with the assertions. cxxtest does not catch that. - // TS_ASSERT_THROWS(d_nm->mkSingleton(d_nm->integerType(), realConstant), - // Exception); - - Node n = d_nm->mkSingleton(d_nm->realType(), intConstant); - // the type of (singleton (singleton_op Real) 1) is (Set Real) - TS_ASSERT(n.getType() == d_nm->mkSetType(d_nm->realType())); - // (singleton (singleton_op Real) 1) is a constant in normal form - TS_ASSERT(n.isConst()); - } - - private: - std::unique_ptr d_slv; - std::unique_ptr d_em; - std::unique_ptr d_smt; - std::unique_ptr d_nm; -}; /* class SetsTypeRuleWhite */