From: Aina Niemetz Date: Tue, 23 Feb 2021 22:34:20 +0000 (-0800) Subject: google test: theory: Migrate strings_rewriter_white. (#5976) X-Git-Tag: cvc5-1.0.0~2233 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03b53ca0374440bb0fe81c3cc85c2e374ac10f71;p=cvc5.git google test: theory: Migrate strings_rewriter_white. (#5976) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index e7528453e..12546f8bb 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -13,7 +13,7 @@ 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) cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory) -cvc4_add_cxx_unit_test_white(strings_rewriter_white theory) +cvc4_add_unit_test_white(strings_rewriter_white theory) cvc4_add_cxx_unit_test_white(theory_arith_white theory) cvc4_add_cxx_unit_test_white(theory_bags_normal_form_white theory) cvc4_add_cxx_unit_test_white(theory_bags_rewriter_white theory) diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp new file mode 100644 index 000000000..c7ed3e97d --- /dev/null +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -0,0 +1,67 @@ +/********************* */ +/*! \file strings_rewriter_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Not Committed Yet + ** 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 the strings rewriter + ** + ** Unit tests for the strings rewriter. + **/ + +#include +#include +#include + +#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" + +namespace CVC4 { + +using namespace kind; +using namespace smt; +using namespace theory; +using namespace theory::strings; + +namespace test { + +class TestTheoryWhiteStringsRewriter : public TestSmt +{ +}; + +TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node bc = d_nodeManager->mkConst(::CVC4::String("BC")); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + + Node ax = d_nodeManager->mkNode(STRING_CONCAT, a, x); + Node bcy = d_nodeManager->mkNode(STRING_CONCAT, bc, y); + + { + Node leq = d_nodeManager->mkNode(STRING_LEQ, ax, bcy); + ASSERT_EQ(Rewriter::rewrite(leq), d_nodeManager->mkConst(true)); + } + + { + Node leq = d_nodeManager->mkNode(STRING_LEQ, bcy, ax); + ASSERT_EQ(Rewriter::rewrite(leq), d_nodeManager->mkConst(false)); + } +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/strings_rewriter_white.h b/test/unit/theory/strings_rewriter_white.h deleted file mode 100644 index f5c7cced8..000000000 --- a/test/unit/theory/strings_rewriter_white.h +++ /dev/null @@ -1,89 +0,0 @@ -/********************* */ -/*! \file strings_rewriter_white.h - ** \verbatim - ** Top contributors (to current version): - ** 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 the strings rewriter - ** - ** Unit tests for the strings rewriter. - **/ - -#include - -#include -#include -#include - -#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/strings_rewriter.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::smt; -using namespace CVC4::theory; -using namespace CVC4::theory::strings; - -class StringsRewriterWhite : public CxxTest::TestSuite -{ - public: - StringsRewriterWhite() {} - - void setUp() override - { - Options opts; - opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager; - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm, &opts); - d_scope = new SmtScope(d_smt); - d_smt->finishInit(); - } - - void tearDown() override - { - delete d_scope; - delete d_smt; - delete d_em; - } - - void testRewriteLeq() - { - TypeNode intType = d_nm->integerType(); - TypeNode strType = d_nm->stringType(); - - Node a = d_nm->mkConst(::CVC4::String("A")); - Node bc = d_nm->mkConst(::CVC4::String("BC")); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - - Node ax = d_nm->mkNode(STRING_CONCAT, a, x); - Node bcy = d_nm->mkNode(STRING_CONCAT, bc, y); - - { - Node leq = d_nm->mkNode(STRING_LEQ, ax, bcy); - TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(true)); - } - - { - Node leq = d_nm->mkNode(STRING_LEQ, bcy, ax); - TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(false)); - } - } - - private: - ExprManager* d_em; - SmtEngine* d_smt; - SmtScope* d_scope; - - NodeManager* d_nm; -};