From: Aina Niemetz Date: Wed, 24 Feb 2021 22:35:22 +0000 (-0800) Subject: google test: theory: Migrate theory_bags_type_rules_white. (#5984) X-Git-Tag: cvc5-1.0.0~2217 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3e16e447aed037806f874a54ae74d6850415fd7;p=cvc5.git google test: theory: Migrate theory_bags_type_rules_white. (#5984) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index c135c4a94..8e7951f17 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -17,7 +17,7 @@ cvc4_add_unit_test_white(strings_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) cvc4_add_unit_test_white(theory_bags_normal_form_white theory) cvc4_add_unit_test_white(theory_bags_rewriter_white theory) -cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory) +cvc4_add_unit_test_white(theory_bags_type_rules_white theory) cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_cxx_unit_test_white(theory_bv_white theory) cvc4_add_unit_test_white(theory_engine_white theory) diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp new file mode 100644 index 000000000..6e2a818e0 --- /dev/null +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -0,0 +1,114 @@ +/********************* */ +/*! \file theory_bags_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 Black box testing of bags typing rules + **/ + +#include "expr/dtype.h" +#include "test_smt.h" +#include "theory/bags/theory_bags_type_rules.h" +#include "theory/strings/type_enumerator.h" + +namespace CVC4 { + +using namespace smt; +using namespace theory; +using namespace kind; +using namespace theory::bags; + +namespace test { + +typedef expr::Attribute attribute; + +class TestTheoryWhiteBagsTypeRule : public TestSmt +{ + protected: + std::vector getNStrings(size_t n) + { + std::vector elements(n); + CVC4::theory::strings::StringEnumerator enumerator( + d_nodeManager->stringType()); + + for (size_t i = 0; i < n; i++) + { + ++enumerator; + elements[i] = *enumerator; + } + + return elements; + } +}; + +TEST_F(TestTheoryWhiteBagsTypeRule, count_operator) +{ + std::vector elements = getNStrings(1); + Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(Rational(100))); + + Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag); + Node node = d_nodeManager->mkConst(Rational(10)); + + // node of type Int is not compatible with bag of type (Bag String) + ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true), + TypeCheckingExceptionPrivate); +} + +TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) +{ + std::vector elements = getNStrings(1); + Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(Rational(10))); + ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag)); + ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(), + bag.getType()); +} + +TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) +{ + std::vector elements = getNStrings(1); + Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(Rational(-1))); + Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(Rational(0))); + Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(Rational(1))); + + // only positive multiplicity are constants + ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), negative)); + ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), zero)); + ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), positive)); +} + +TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) +{ + std::vector elements = getNStrings(1); + Node set = + d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]); + ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_FROM_SET, set)); + ASSERT_TRUE(d_nodeManager->mkNode(BAG_FROM_SET, set).getType().isBag()); +} + +TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) +{ + std::vector elements = getNStrings(1); + Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(Rational(10))); + ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag)); + ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet()); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h deleted file mode 100644 index 825e52669..000000000 --- a/test/unit/theory/theory_bags_type_rules_white.h +++ /dev/null @@ -1,123 +0,0 @@ -/********************* */ -/*! \file theory_bags_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 Black box testing of bags typing rules - **/ - -#include - -#include "expr/dtype.h" -#include "smt/smt_engine.h" -#include "theory/bags/theory_bags_type_rules.h" -#include "theory/strings/type_enumerator.h" - -using namespace CVC4; -using namespace CVC4::smt; -using namespace CVC4::theory; -using namespace CVC4::kind; -using namespace CVC4::theory::bags; -using namespace std; - -typedef expr::Attribute attribute; - -class BagsTypeRuleWhite : public CxxTest::TestSuite -{ - public: - void setUp() override - { - 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_smt.reset(); - d_nm.release(); - d_em.reset(); - } - - std::vector getNStrings(size_t n) - { - std::vector elements(n); - CVC4::theory::strings::StringEnumerator enumerator(d_nm->stringType()); - - for (size_t i = 0; i < n; i++) - { - ++enumerator; - elements[i] = *enumerator; - } - - return elements; - } - - void testCountOperator() - { - vector elements = getNStrings(1); - Node bag = d_nm->mkBag( - d_nm->stringType(), elements[0], d_nm->mkConst(Rational(100))); - - Node count = d_nm->mkNode(BAG_COUNT, elements[0], bag); - Node node = d_nm->mkConst(Rational(10)); - - // node of type Int is not compatible with bag of type (Bag String) - TS_ASSERT_THROWS(d_nm->mkNode(BAG_COUNT, node, bag).getType(true), - TypeCheckingExceptionPrivate&); - } - - void testDuplicateRemovalOperator() - { - vector elements = getNStrings(1); - Node bag = d_nm->mkBag( - d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10))); - TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(DUPLICATE_REMOVAL, bag)); - TS_ASSERT(d_nm->mkNode(DUPLICATE_REMOVAL, bag).getType() == bag.getType()); - } - - void testMkBagOperator() - { - vector elements = getNStrings(1); - Node negative = d_nm->mkBag( - d_nm->stringType(), elements[0], d_nm->mkConst(Rational(-1))); - Node zero = d_nm->mkBag( - d_nm->stringType(), elements[0], d_nm->mkConst(Rational(0))); - Node positive = d_nm->mkBag( - d_nm->stringType(), elements[0], d_nm->mkConst(Rational(1))); - - // only positive multiplicity are constants - TS_ASSERT(!MkBagTypeRule::computeIsConst(d_nm.get(), negative)); - TS_ASSERT(!MkBagTypeRule::computeIsConst(d_nm.get(), zero)); - TS_ASSERT(MkBagTypeRule::computeIsConst(d_nm.get(), positive)); - } - - void testFromSetOperator() - { - vector elements = getNStrings(1); - Node set = d_nm->mkSingleton(d_nm->stringType(), elements[0]); - TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(BAG_FROM_SET, set)); - TS_ASSERT(d_nm->mkNode(BAG_FROM_SET, set).getType().isBag()); - } - - void testToSetOperator() - { - vector elements = getNStrings(1); - Node bag = d_nm->mkBag( - d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10))); - TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(BAG_TO_SET, bag)); - TS_ASSERT(d_nm->mkNode(BAG_TO_SET, bag).getType().isSet()); - } - - private: - std::unique_ptr d_em; - std::unique_ptr d_smt; - std::unique_ptr d_nm; -}; /* class BagsTypeRuleBlack */