From: Aina Niemetz Date: Fri, 26 Feb 2021 21:28:22 +0000 (-0800) Subject: google test: theory: Migrate theory_sets_type_enumerator_white. (#6000) X-Git-Tag: cvc5-1.0.0~2200 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9295f225d86319626ca31975ec9ee53dc8788a2e;p=cvc5.git google test: theory: Migrate theory_sets_type_enumerator_white. (#6000) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 14ae782e4..d2e9b2e92 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -23,7 +23,7 @@ cvc4_add_unit_test_white(theory_bv_white theory) 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_cxx_unit_test_white(theory_sets_type_enumerator_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_cxx_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_cxx_unit_test_white(theory_strings_word_white theory) diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index 039a5f12f..1ced4a584 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -27,7 +27,6 @@ namespace CVC4 { -using namespace smt; using namespace theory; namespace test { diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index 9c419a28d..59f2cadb2 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -30,7 +30,6 @@ namespace CVC4 { using namespace kind; -using namespace smt; using namespace theory; using namespace theory::strings; diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 590fa2ace..14c04c69c 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -30,7 +30,6 @@ namespace CVC4 { -using namespace smt; using namespace theory; using namespace theory::quantifiers; using namespace theory::strings; diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index c7ed3e97d..80cbce88d 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -20,8 +20,6 @@ #include "expr/node.h" #include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "test_smt.h" #include "theory/rewriter.h" #include "theory/strings/strings_rewriter.h" @@ -29,7 +27,6 @@ namespace CVC4 { using namespace kind; -using namespace smt; using namespace theory; using namespace theory::strings; diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 658571b00..2c6e00a11 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -20,7 +20,6 @@ namespace CVC4 { -using namespace smt; using namespace theory; using namespace kind; using namespace theory::bags; diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index db8e430f3..110ab5a64 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -19,7 +19,6 @@ namespace CVC4 { -using namespace smt; using namespace theory; using namespace kind; using namespace theory::bags; diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 6e2a818e0..2c28d5b2c 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -19,7 +19,6 @@ namespace CVC4 { -using namespace smt; using namespace theory; using namespace kind; using namespace theory::bags; diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index 0aba243b5..9864e60af 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -28,7 +28,6 @@ namespace CVC4 { using namespace kind; using namespace context; using namespace theory; -using namespace smt; namespace test { diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp index e2e4d1ddb..9a5e7bf8f 100644 --- a/test/unit/theory/theory_bv_rewriter_white.cpp +++ b/test/unit/theory/theory_bv_rewriter_white.cpp @@ -26,7 +26,6 @@ namespace CVC4 { using namespace kind; -using namespace smt; using namespace theory; namespace test { diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 0f304bfcf..92e359c8f 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -33,7 +33,6 @@ using namespace theory::bv; using namespace theory::bv::utils; using namespace expr; using namespace context; -using namespace smt; namespace test { diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index c888fbf0d..baf8f4d9c 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -43,7 +43,6 @@ using namespace theory; using namespace expr; using namespace context; using namespace kind; -using namespace smt; using namespace theory::bv; namespace test { diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp new file mode 100644 index 000000000..4338e9fa2 --- /dev/null +++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp @@ -0,0 +1,155 @@ +/********************* */ +/*! \file theory_sets_type_enumerator_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andrew Reynolds, 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 CVC4::theory::sets::SetsTypeEnumerator + ** + ** White box testing of CVC4::theory::sets::SetsTypeEnumerator. (These tests + ** depends on the ordering that the SetsTypeEnumerator use, so it's a + *white-box + ** test.) + **/ + +#include "expr/dtype.h" +#include "test_smt.h" +#include "theory/sets/theory_sets_type_enumerator.h" + +namespace CVC4 { + +using namespace theory; +using namespace kind; +using namespace theory::sets; + +namespace test { + +class TestTheoryWhiteSetsTypeEnumerator : public TestSmt +{ + protected: + void addAndCheckUnique(Node n, std::vector& elems) + { + ASSERT_TRUE(n.isConst()); + ASSERT_TRUE(std::find(elems.begin(), elems.end(), n) == elems.end()); + elems.push_back(n); + } +}; + +TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_booleans) +{ + TypeNode boolType = d_nodeManager->booleanType(); + SetEnumerator setEnumerator(d_nodeManager->mkSetType(boolType)); + ASSERT_FALSE(setEnumerator.isFinished()); + + std::vector elems; + + Node actual0 = *setEnumerator; + addAndCheckUnique(actual0, elems); + ASSERT_FALSE(setEnumerator.isFinished()); + + Node actual1 = *++setEnumerator; + addAndCheckUnique(actual1, elems); + ASSERT_FALSE(setEnumerator.isFinished()); + + Node actual2 = *++setEnumerator; + addAndCheckUnique(actual2, elems); + ASSERT_FALSE(setEnumerator.isFinished()); + + Node actual3 = Rewriter::rewrite(*++setEnumerator); + addAndCheckUnique(actual3, elems); + ASSERT_FALSE(setEnumerator.isFinished()); + + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); +} + +TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_UF) +{ + TypeNode sort = d_nodeManager->mkSort("Atom"); + SetEnumerator setEnumerator(d_nodeManager->mkSetType(sort)); + + Node actual0 = *setEnumerator; + Node expected0 = + d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(sort))); + ASSERT_EQ(expected0, actual0); + ASSERT_FALSE(setEnumerator.isFinished()); + + std::vector elems; + for (unsigned i = 0; i < 7; i++) + { + Node actual = *setEnumerator; + addAndCheckUnique(actual, elems); + ASSERT_FALSE(setEnumerator.isFinished()); + ++setEnumerator; + } +} + +TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_finite_dataype) +{ + DType dt("Colors"); + dt.addConstructor(std::make_shared("red")); + dt.addConstructor(std::make_shared("green")); + dt.addConstructor(std::make_shared("blue")); + TypeNode datatype = d_nodeManager->mkDatatypeType(dt); + const std::vector >& dtcons = + datatype.getDType().getConstructors(); + SetEnumerator setEnumerator(d_nodeManager->mkSetType(datatype)); + + Node red = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor()); + + Node green = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor()); + + Node blue = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor()); + + std::vector elems; + for (unsigned i = 0; i < 8; i++) + { + Node actual = *setEnumerator; + addAndCheckUnique(actual, elems); + ASSERT_FALSE(setEnumerator.isFinished()); + ++setEnumerator; + } + + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); +} + +TEST_F(TestTheoryWhiteSetsTypeEnumerator, bv) +{ + TypeNode bitVector2 = d_nodeManager->mkBitVectorType(2); + SetEnumerator setEnumerator(d_nodeManager->mkSetType(bitVector2)); + + std::vector elems; + for (unsigned i = 0; i < 16; i++) + { + Node actual = *setEnumerator; + addAndCheckUnique(actual, elems); + ASSERT_FALSE(setEnumerator.isFinished()); + ++setEnumerator; + } + + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); + ASSERT_THROW(*++setEnumerator, NoMoreValuesException); + ASSERT_TRUE(setEnumerator.isFinished()); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h deleted file mode 100644 index a100984ba..000000000 --- a/test/unit/theory/theory_sets_type_enumerator_white.h +++ /dev/null @@ -1,172 +0,0 @@ -/********************* */ -/*! \file theory_sets_type_enumerator_white.h - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, Andrew Reynolds, Andres Noetzli - ** 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 CVC4::theory::sets::SetEnumerator - ** - ** White box testing of CVC4::theory::sets::SetEnumerator. (These tests - ** depends on the ordering that the SetEnumerator use, so it's a white-box - * test.) - **/ - -#include - -#include "expr/dtype.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/sets/theory_sets_type_enumerator.h" - -using namespace CVC4; -using namespace CVC4::smt; -using namespace CVC4::theory; -using namespace CVC4::kind; -using namespace CVC4::theory::sets; -using namespace std; - -class SetEnumeratorWhite : public CxxTest::TestSuite -{ - public: - void setUp() override - { - d_em = new ExprManager(); - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm); - d_scope = new SmtScope(d_smt); - d_smt->finishInit(); - } - - void tearDown() override - { - delete d_scope; - delete d_smt; - delete d_em; - } - - void addAndCheckUnique(Node n, std::vector& elems) - { - TS_ASSERT(n.isConst()); - TS_ASSERT(std::find(elems.begin(), elems.end(), n) == elems.end()); - elems.push_back(n); - } - - void testSetOfBooleans() - { - TypeNode boolType = d_nm->booleanType(); - SetEnumerator setEnumerator(d_nm->mkSetType(boolType)); - TS_ASSERT(!setEnumerator.isFinished()); - - std::vector elems; - - Node actual0 = *setEnumerator; - addAndCheckUnique(actual0, elems); - TS_ASSERT(!setEnumerator.isFinished()); - - Node actual1 = *++setEnumerator; - addAndCheckUnique(actual1, elems); - TS_ASSERT(!setEnumerator.isFinished()); - - Node actual2 = *++setEnumerator; - addAndCheckUnique(actual2, elems); - TS_ASSERT(!setEnumerator.isFinished()); - - Node actual3 = Rewriter::rewrite(*++setEnumerator); - addAndCheckUnique(actual3, elems); - TS_ASSERT(!setEnumerator.isFinished()); - - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - } - - void testSetOfUF() - { - TypeNode sort = d_nm->mkSort("Atom"); - SetEnumerator setEnumerator(d_nm->mkSetType(sort)); - - Node actual0 = *setEnumerator; - Node expected0 = d_nm->mkConst(EmptySet(d_nm->mkSetType(sort))); - TS_ASSERT_EQUALS(expected0, actual0); - TS_ASSERT(!setEnumerator.isFinished()); - - std::vector elems; - for (unsigned i = 0; i < 7; i++) - { - Node actual = *setEnumerator; - addAndCheckUnique(actual, elems); - TS_ASSERT(!setEnumerator.isFinished()); - ++setEnumerator; - } - } - - void testSetOfFiniteDatatype() - { - DType dt("Colors"); - dt.addConstructor(std::make_shared("red")); - dt.addConstructor(std::make_shared("green")); - dt.addConstructor(std::make_shared("blue")); - TypeNode datatype = d_nm->mkDatatypeType(dt); - const std::vector >& dtcons = - datatype.getDType().getConstructors(); - SetEnumerator setEnumerator(d_nm->mkSetType(datatype)); - - Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor()); - - Node green = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor()); - - Node blue = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor()); - - std::vector elems; - for (unsigned i = 0; i < 8; i++) - { - Node actual = *setEnumerator; - addAndCheckUnique(actual, elems); - TS_ASSERT(!setEnumerator.isFinished()); - ++setEnumerator; - } - - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - } - - void testBV() - { - TypeNode bitVector2 = d_nm->mkBitVectorType(2); - SetEnumerator setEnumerator(d_nm->mkSetType(bitVector2)); - - std::vector elems; - for (unsigned i = 0; i < 16; i++) - { - Node actual = *setEnumerator; - addAndCheckUnique(actual, elems); - TS_ASSERT(!setEnumerator.isFinished()); - ++setEnumerator; - } - - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); - TS_ASSERT(setEnumerator.isFinished()); - } - - private: - ExprManager* d_em; - SmtEngine* d_smt; - NodeManager* d_nm; - SmtScope* d_scope; -}; /* class SetEnumeratorWhite */