From: Aina Niemetz Date: Tue, 23 Feb 2021 23:16:41 +0000 (-0800) Subject: google test: theory: Migrate regexp_operation_black. (#5974) X-Git-Tag: cvc5-1.0.0~2232 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eeb74f13bdf16aeda2e4d5fe7b4880cb17702fe4;p=cvc5.git google test: theory: Migrate regexp_operation_black. (#5974) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 12546f8bb..6c4e62765 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -8,7 +8,7 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -cvc4_add_cxx_unit_test_black(regexp_operation_black theory) +cvc4_add_unit_test_black(regexp_operation_black theory) cvc4_add_cxx_unit_test_black(theory_black theory) cvc4_add_cxx_unit_test_white(evaluator_white theory) cvc4_add_cxx_unit_test_white(logic_info_white theory) diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp new file mode 100644 index 000000000..9c419a28d --- /dev/null +++ b/test/unit/theory/regexp_operation_black.cpp @@ -0,0 +1,148 @@ +/********************* */ +/*! \file regexp_operation_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 Unit tests for symbolic regular expression operations + ** + ** Unit tests for symbolic regular expression operations. + **/ + +#include +#include +#include + +#include "api/cvc4cpp.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "smt/smt_engine_scope.h" +#include "test_smt.h" +#include "theory/rewriter.h" +#include "theory/strings/regexp_operation.h" +#include "theory/strings/skolem_cache.h" + +namespace CVC4 { + +using namespace kind; +using namespace smt; +using namespace theory; +using namespace theory::strings; + +namespace test { + +class TestTheoryBlackRegexpOperation : public TestSmt +{ + protected: + void SetUp() override + { + TestSmt::SetUp(); + d_skolemCache.reset(new SkolemCache()); + d_regExpOpr.reset(new RegExpOpr(d_skolemCache.get())); + } + + void includes(Node r1, Node r2) + { + r1 = Rewriter::rewrite(r1); + r2 = Rewriter::rewrite(r2); + std::cout << r1 << " includes " << r2 << std::endl; + ASSERT_TRUE(d_regExpOpr->regExpIncludes(r1, r2)); + } + + void doesNotInclude(Node r1, Node r2) + { + r1 = Rewriter::rewrite(r1); + r2 = Rewriter::rewrite(r2); + std::cout << r1 << " does not include " << r2 << std::endl; + ASSERT_FALSE(d_regExpOpr->regExpIncludes(r1, r2)); + } + + std::unique_ptr d_skolemCache; + std::unique_ptr d_regExpOpr; +}; + +TEST_F(TestTheoryBlackRegexpOperation, basic) +{ + Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA, std::vector{}); + Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma); + Node a = d_nodeManager->mkNode(STRING_TO_REGEXP, + d_nodeManager->mkConst(String("a"))); + Node c = d_nodeManager->mkNode(STRING_TO_REGEXP, + d_nodeManager->mkConst(String("c"))); + Node abc = d_nodeManager->mkNode(STRING_TO_REGEXP, + d_nodeManager->mkConst(String("abc"))); + Node sigma3 = d_nodeManager->mkNode(REGEXP_CONCAT, sigma, sigma, sigma); + Node asc = d_nodeManager->mkNode(REGEXP_CONCAT, a, sigma, c); + Node asw = d_nodeManager->mkNode(REGEXP_CONCAT, a, sigma, sigmaStar); + + includes(sigma3, abc); + doesNotInclude(abc, sigma3); + + includes(sigma3, asc); + doesNotInclude(asc, sigma3); + + includes(asc, abc); + doesNotInclude(abc, asc); + + includes(asw, asc); + doesNotInclude(asc, asw); +} + +TEST_F(TestTheoryBlackRegexpOperation, star_wildcards) +{ + Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA, std::vector{}); + Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma); + Node a = d_nodeManager->mkNode(STRING_TO_REGEXP, + d_nodeManager->mkConst(String("a"))); + Node c = d_nodeManager->mkNode(STRING_TO_REGEXP, + d_nodeManager->mkConst(String("c"))); + Node abc = d_nodeManager->mkNode(STRING_TO_REGEXP, + d_nodeManager->mkConst(String("abc"))); + + Node _abc_ = d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, abc, sigmaStar); + Node _asc_ = + d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, c, sigmaStar); + Node _sc_ = Rewriter::rewrite( + d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, sigma, c, sigmaStar)); + Node _as_ = Rewriter::rewrite( + d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, sigmaStar)); + Node _assc_ = d_nodeManager->mkNode( + REGEXP_CONCAT, + std::vector{sigmaStar, a, sigma, sigma, c, sigmaStar}); + Node _csa_ = + d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, c, sigma, a, sigmaStar); + Node _c_a_ = d_nodeManager->mkNode( + REGEXP_CONCAT, sigmaStar, c, sigmaStar, a, sigmaStar); + Node _s_s_ = Rewriter::rewrite(d_nodeManager->mkNode( + REGEXP_CONCAT, sigmaStar, sigma, sigmaStar, sigma, sigmaStar)); + Node _a_abc_ = Rewriter::rewrite(d_nodeManager->mkNode( + REGEXP_CONCAT, sigmaStar, a, sigmaStar, abc, sigmaStar)); + + includes(_asc_, _abc_); + doesNotInclude(_abc_, _asc_); + doesNotInclude(_csa_, _abc_); + doesNotInclude(_assc_, _asc_); + doesNotInclude(_asc_, _assc_); + includes(_sc_, abc); + includes(_sc_, _abc_); + includes(_sc_, _asc_); + includes(_sc_, _assc_); + doesNotInclude(_sc_, _csa_); + includes(_as_, abc); + includes(_as_, _abc_); + includes(_as_, _asc_); + includes(_as_, _assc_); + doesNotInclude(_sc_, _csa_); + includes(_s_s_, _c_a_); + doesNotInclude(_c_a_, _s_s_); + includes(_abc_, _a_abc_); + doesNotInclude(_a_abc_, _abc_); +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h deleted file mode 100644 index ec00464f1..000000000 --- a/test/unit/theory/regexp_operation_black.h +++ /dev/null @@ -1,164 +0,0 @@ -/********************* */ -/*! \file regexp_operation_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 Unit tests for symbolic regular expression operations - ** - ** Unit tests for symbolic regular expression operations. - **/ - -#include - -#include -#include -#include - -#include "api/cvc4cpp.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/rewriter.h" -#include "theory/strings/regexp_operation.h" -#include "theory/strings/skolem_cache.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::smt; -using namespace CVC4::theory; -using namespace CVC4::theory::strings; - -class RegexpOperationBlack : public CxxTest::TestSuite -{ - public: - RegexpOperationBlack() {} - - void setUp() override - { - Options opts; - opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_slv = new api::Solver(); - d_em = d_slv->getExprManager(); - d_smt = d_slv->getSmtEngine(); - d_scope = new SmtScope(d_smt); - d_skc = new SkolemCache(); - d_regExpOpr = new RegExpOpr(d_skc); - - // Ensure that the SMT engine is fully initialized (required for the - // rewriter) - d_smt->push(); - - d_nm = NodeManager::currentNM(); - } - - void tearDown() override - { - delete d_regExpOpr; - delete d_skc; - delete d_scope; - delete d_slv; - } - - void includes(Node r1, Node r2) - { - r1 = Rewriter::rewrite(r1); - r2 = Rewriter::rewrite(r2); - std::cout << r1 << " includes " << r2 << std::endl; - TS_ASSERT(d_regExpOpr->regExpIncludes(r1, r2)); - } - - void doesNotInclude(Node r1, Node r2) - { - r1 = Rewriter::rewrite(r1); - r2 = Rewriter::rewrite(r2); - std::cout << r1 << " does not include " << r2 << std::endl; - TS_ASSERT(!d_regExpOpr->regExpIncludes(r1, r2)); - } - - void testBasic() - { - Node sigma = d_nm->mkNode(REGEXP_SIGMA, std::vector{}); - Node sigmaStar = d_nm->mkNode(REGEXP_STAR, sigma); - Node a = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("a"))); - Node c = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("c"))); - Node abc = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("abc"))); - Node sigma3 = d_nm->mkNode(REGEXP_CONCAT, sigma, sigma, sigma); - Node asc = d_nm->mkNode(REGEXP_CONCAT, a, sigma, c); - Node asw = d_nm->mkNode(REGEXP_CONCAT, a, sigma, sigmaStar); - - includes(sigma3, abc); - doesNotInclude(abc, sigma3); - - includes(sigma3, asc); - doesNotInclude(asc, sigma3); - - includes(asc, abc); - doesNotInclude(abc, asc); - - includes(asw, asc); - doesNotInclude(asc, asw); - } - - void testStarWildcards() - { - Node sigma = d_nm->mkNode(REGEXP_SIGMA, std::vector{}); - Node sigmaStar = d_nm->mkNode(REGEXP_STAR, sigma); - Node a = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("a"))); - Node c = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("c"))); - Node abc = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("abc"))); - - Node _abc_ = d_nm->mkNode(REGEXP_CONCAT, sigmaStar, abc, sigmaStar); - Node _asc_ = d_nm->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, c, sigmaStar); - Node _sc_ = Rewriter::rewrite( - d_nm->mkNode(REGEXP_CONCAT, sigmaStar, sigma, c, sigmaStar)); - Node _as_ = Rewriter::rewrite( - d_nm->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, sigmaStar)); - Node _assc_ = d_nm->mkNode( - REGEXP_CONCAT, - std::vector{sigmaStar, a, sigma, sigma, c, sigmaStar}); - Node _csa_ = d_nm->mkNode(REGEXP_CONCAT, sigmaStar, c, sigma, a, sigmaStar); - Node _c_a_ = - d_nm->mkNode(REGEXP_CONCAT, sigmaStar, c, sigmaStar, a, sigmaStar); - Node _s_s_ = Rewriter::rewrite(d_nm->mkNode( - REGEXP_CONCAT, sigmaStar, sigma, sigmaStar, sigma, sigmaStar)); - Node _a_abc_ = Rewriter::rewrite( - d_nm->mkNode(REGEXP_CONCAT, sigmaStar, a, sigmaStar, abc, sigmaStar)); - - includes(_asc_, _abc_); - doesNotInclude(_abc_, _asc_); - doesNotInclude(_csa_, _abc_); - doesNotInclude(_assc_, _asc_); - doesNotInclude(_asc_, _assc_); - includes(_sc_, abc); - includes(_sc_, _abc_); - includes(_sc_, _asc_); - includes(_sc_, _assc_); - doesNotInclude(_sc_, _csa_); - includes(_as_, abc); - includes(_as_, _abc_); - includes(_as_, _asc_); - includes(_as_, _assc_); - doesNotInclude(_sc_, _csa_); - includes(_s_s_, _c_a_); - doesNotInclude(_c_a_, _s_s_); - includes(_abc_, _a_abc_); - doesNotInclude(_a_abc_, _abc_); - } - - private: - api::Solver* d_slv; - ExprManager* d_em; - SmtEngine* d_smt; - SmtScope* d_scope; - SkolemCache* d_skc; - RegExpOpr* d_regExpOpr; - - NodeManager* d_nm; -};