From: Aina Niemetz Date: Mon, 22 Feb 2021 18:20:17 +0000 (-0800) Subject: google test: preprocessing: Migrate pass_foreign_theory_rewrite_white. (#5936) X-Git-Tag: cvc5-1.0.0~2249 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dea7a1fc8360735f90618f005509306c7c45bd30;p=cvc5.git google test: preprocessing: Migrate pass_foreign_theory_rewrite_white. (#5936) --- diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt index f9518bd2e..ebb0a5189 100644 --- a/test/unit/preprocessing/CMakeLists.txt +++ b/test/unit/preprocessing/CMakeLists.txt @@ -12,4 +12,4 @@ # Add unit tests cvc4_add_cxx_unit_test_white(pass_bv_gauss_white preprocessing) -cvc4_add_cxx_unit_test_white(pass_foreign_theory_rewrite_white preprocessing) +cvc4_add_unit_test_white(pass_foreign_theory_rewrite_white preprocessing) diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp new file mode 100644 index 000000000..af20766aa --- /dev/null +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -0,0 +1,50 @@ +/********************* */ +/*! \file pass_foreign_theory_rewrite_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Yoni Zohar + ** 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 Foreign Theory Rerwrite prepricessing pass + ** Unit tests for Foreign Theory Rerwrite prepricessing pass + **/ + +#include "expr/node_manager.h" +#include "preprocessing/passes/foreign_theory_rewrite.h" +#include "smt/smt_engine.h" +#include "test_smt.h" + +namespace CVC4 { + +using namespace preprocessing::passes; + +namespace test { + +class TestPPWhiteForeignTheoryRewrite : public TestSmt +{ +}; + +TEST_F(TestPPWhiteForeignTheoryRewrite, simplify) +{ + std::cout << "len(x) >= 0 is simplified to true" << std::endl; + Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType()); + Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x); + Node zero = d_nodeManager->mkConst(0); + Node geq1 = d_nodeManager->mkNode(kind::GEQ, len_x, zero); + Node tt = d_nodeManager->mkConst(true); + Node simplified1 = ForeignTheoryRewrite::foreignRewrite(geq1); + ASSERT_EQ(simplified1, tt); + + std::cout << "len(x) >= n is not simplified to true" << std::endl; + Node n = d_nodeManager->mkVar("n", d_nodeManager->integerType()); + Node geq2 = d_nodeManager->mkNode(kind::GEQ, len_x, n); + Node simplified2 = ForeignTheoryRewrite::foreignRewrite(geq2); + ASSERT_NE(simplified2, tt); +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.h b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.h deleted file mode 100644 index 5416cf304..000000000 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file pass_foreign_theory_rewrite.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, 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 Foreign Theory Rerwrite prepricessing pass - ** Unit tests for Foreign Theory Rerwrite prepricessing pass - **/ - -#include - -#include "expr/node_manager.h" -#include "preprocessing/passes/foreign_theory_rewrite.h" -#include "smt/smt_engine.h" -#include "test_utils.h" - -using namespace CVC4; -using namespace CVC4::preprocessing::passes; - -class ForeignTheoryRewriteWhite : public CxxTest::TestSuite -{ - public: - ForeignTheoryRewriteWhite() {} - - void setUp() override - { - d_em = new ExprManager(); - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm); - d_smt->finishInit(); - } - - void tearDown() override - { - delete d_smt; - delete d_em; - } - - void testSimplify() - { - std::cout << "len(x) >= 0 is simplified to true" << std::endl; - Node x = d_nm->mkVar("x", d_nm->stringType()); - Node len_x = d_nm->mkNode(kind::STRING_LENGTH, x); - Node zero = d_nm->mkConst(0); - Node geq1 = d_nm->mkNode(kind::GEQ, len_x, zero); - Node tt = d_nm->mkConst(true); - Node simplified1 = ForeignTheoryRewrite::foreignRewrite(geq1); - TS_ASSERT_EQUALS(simplified1, tt); - - std::cout << "len(x) >= n is not simplified to true" << std::endl; - Node n = d_nm->mkVar("n", d_nm->integerType()); - Node geq2 = d_nm->mkNode(kind::GEQ, len_x, n); - Node simplified2 = ForeignTheoryRewrite::foreignRewrite(geq2); - TS_ASSERT(simplified2 != tt); - } - - private: - ExprManager* d_em; - NodeManager* d_nm; - SmtEngine* d_smt; -}; diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h new file mode 100644 index 000000000..937111fe4 --- /dev/null +++ b/test/unit/test_smt.h @@ -0,0 +1,43 @@ +/********************* */ +/*! \file test_smt.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** 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 Common header for unit tests that need an SmtEngine. + **/ + +#ifndef CVC4__TEST__UNIT__TEST_SMT_H +#define CVC4__TEST__UNIT__TEST_SMT_H + +#include "expr/node_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "test.h" + +namespace CVC4 { +namespace test { + +class TestSmt : public TestInternal +{ + protected: + void SetUp() override + { + d_nodeManager.reset(new NodeManager(nullptr)); + d_scope.reset(new NodeManagerScope(d_nodeManager.get())); + d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); + d_smtEngine->finishInit(); + } + + std::unique_ptr d_scope; + std::unique_ptr d_nodeManager; + std::unique_ptr d_smtEngine; +}; +} // namespace test +} // namespace CVC4 +#endif