From: Aina Niemetz Date: Mon, 1 Mar 2021 09:31:23 +0000 (-0800) Subject: google test: theory: Migrate theory_strings_skolem_cache_black. (#6002) X-Git-Tag: cvc5-1.0.0~2191 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fce23101ad8e1ada10acc2e5807b9392c5e6ee6c;p=cvc5.git google test: theory: Migrate theory_strings_skolem_cache_black. (#6002) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 0d24da50b..c52b41966 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -25,7 +25,7 @@ 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_unit_test_white(theory_sets_type_rules_white theory) -cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory) +cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_unit_test_white(theory_strings_word_white theory) cvc4_add_unit_test_white(theory_white theory) cvc4_add_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp new file mode 100644 index 000000000..fbe976147 --- /dev/null +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -0,0 +1,62 @@ +/********************* */ +/*! \file theory_strings_skolem_cache_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, 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 Black box testing of the skolem cache of the theory of strings. + **/ + +#include + +#include "expr/node.h" +#include "test_smt.h" +#include "theory/strings/skolem_cache.h" +#include "util/rational.h" +#include "util/string.h" + +namespace CVC4 { + +using namespace theory::strings; + +namespace test { + +class TestTheoryBlackStringsSkolemCache : public TestSmt +{ +}; + +TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached) +{ + Node zero = d_nodeManager->mkConst(Rational(0)); + Node n = d_nodeManager->mkSkolem("n", d_nodeManager->integerType()); + Node a = d_nodeManager->mkSkolem("a", d_nodeManager->stringType()); + Node b = d_nodeManager->mkSkolem("b", d_nodeManager->stringType()); + Node c = d_nodeManager->mkSkolem("c", d_nodeManager->stringType()); + Node d = d_nodeManager->mkSkolem("d", d_nodeManager->stringType()); + Node sa = d_nodeManager->mkNode( + kind::STRING_SUBSTR, + a, + zero, + d_nodeManager->mkNode(kind::STRING_STRIDOF, a, b, zero)); + Node sc = d_nodeManager->mkNode(kind::STRING_SUBSTR, c, zero, n); + + SkolemCache sk; + + // Check that skolems are shared between: + // + // SK_FIRST_CTN(a, b) + // + // SK_FIRST_CTN(a, b) + { + Node s1 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); + Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); + ASSERT_EQ(s1, s2); + } +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h deleted file mode 100644 index 72a9b7e64..000000000 --- a/test/unit/theory/theory_strings_skolem_cache_black.h +++ /dev/null @@ -1,82 +0,0 @@ -/********************* */ -/*! \file theory_strings_skolem_cache_black.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, 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 the skolem cache of the theory of strings. - **/ - -#include - -#include - -#include "expr/expr_manager.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/strings/skolem_cache.h" -#include "util/rational.h" -#include "util/string.h" - -using namespace CVC4; -using namespace CVC4::smt; -using namespace CVC4::theory::strings; - -class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite -{ - public: - void setUp() override - { - d_em.reset(new ExprManager()); - d_nm = NodeManager::fromExprManager(d_em.get()); - d_smt.reset(new SmtEngine(d_nm)); - d_scope.reset(new SmtScope(d_smt.get())); - // Ensure that the SMT engine is fully initialized (required for the - // rewriter) - d_smt->push(); - - } - - void tearDown() override {} - - void testMkSkolemCached() - { - Node zero = d_nm->mkConst(Rational(0)); - Node n = d_nm->mkSkolem("n", d_nm->integerType()); - Node a = d_nm->mkSkolem("a", d_nm->stringType()); - Node b = d_nm->mkSkolem("b", d_nm->stringType()); - Node c = d_nm->mkSkolem("c", d_nm->stringType()); - Node d = d_nm->mkSkolem("d", d_nm->stringType()); - Node sa = d_nm->mkNode(kind::STRING_SUBSTR, - a, - zero, - d_nm->mkNode(kind::STRING_STRIDOF, a, b, zero)); - Node sc = d_nm->mkNode(kind::STRING_SUBSTR, c, zero, n); - - SkolemCache sk; - - // Check that skolems are shared between: - // - // SK_FIRST_CTN(a, b) - // - // SK_FIRST_CTN(a, b) - { - Node s1 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); - Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); - TS_ASSERT_EQUALS(s1, s2); - } - } - - private: - std::unique_ptr d_em; - std::unique_ptr d_smt; - NodeManager* d_nm; - std::unique_ptr d_scope; -};