From: Aina Niemetz Date: Thu, 25 Feb 2021 12:27:15 +0000 (-0800) Subject: google test: theory: Migrate theory_bv_rewriter_white. (#5986) X-Git-Tag: cvc5-1.0.0~2214 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bac328252d9bc1053917ae3bfb02bad37f8f6130;p=cvc5.git google test: theory: Migrate theory_bv_rewriter_white. (#5986) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 8e7951f17..f9c2d3141 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -18,7 +18,7 @@ cvc4_add_unit_test_white(theory_arith_white theory) cvc4_add_unit_test_white(theory_bags_normal_form_white theory) cvc4_add_unit_test_white(theory_bags_rewriter_white theory) cvc4_add_unit_test_white(theory_bags_type_rules_white theory) -cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory) +cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_cxx_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) diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp new file mode 100644 index 000000000..e2e4d1ddb --- /dev/null +++ b/test/unit/theory/theory_bv_rewriter_white.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file theory_bv_rewriter_white.cpp + ** \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 Unit tests for the bit-vector rewriter + ** + ** Unit tests for the bit-vector rewriter. + **/ + +#include +#include +#include + +#include "expr/node.h" +#include "test_smt.h" +#include "theory/rewriter.h" +#include "util/bitvector.h" + +namespace CVC4 { + +using namespace kind; +using namespace smt; +using namespace theory; + +namespace test { + +class TestTheoryWhiteBvRewriter : public TestSmt +{ + protected: + Node boolToBv(Node b) + { + return d_nodeManager->mkNode(ITE, + b, + d_nodeManager->mkConst(BitVector(1, 1u)), + d_nodeManager->mkConst(BitVector(1, 0u))); + } +}; + +TEST_F(TestTheoryWhiteBvRewriter, rewrite_to_fixpoint) +{ + TypeNode boolType = d_nodeManager->booleanType(); + TypeNode bvType = d_nodeManager->mkBitVectorType(1); + + Node zero = d_nodeManager->mkConst(BitVector(1, 0u)); + Node b1 = d_nodeManager->mkVar("b1", boolType); + Node b2 = d_nodeManager->mkVar("b2", boolType); + Node b3 = d_nodeManager->mkVar("b3", boolType); + Node bv = d_nodeManager->mkVar("bv", bvType); + + Node n = d_nodeManager->mkNode( + BITVECTOR_ITE, + boolToBv(b1), + d_nodeManager->mkNode( + BITVECTOR_ITE, + boolToBv(b2), + d_nodeManager->mkNode(BITVECTOR_ITE, boolToBv(b3), zero, bv), + bv), + bv); + Node nr = Rewriter::rewrite(n); + ASSERT_EQ(nr, Rewriter::rewrite(nr)); +} + +TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite) +{ + TypeNode boolType = d_nodeManager->booleanType(); + TypeNode bvType = d_nodeManager->mkBitVectorType(1); + + Node zero = d_nodeManager->mkConst(BitVector(1, 0u)); + Node c1 = d_nodeManager->mkVar("c1", bvType); + Node c2 = d_nodeManager->mkVar("c2", bvType); + + Node ite = d_nodeManager->mkNode(BITVECTOR_ITE, c2, zero, zero); + Node n = d_nodeManager->mkNode(BITVECTOR_ITE, c1, ite, ite); + Node nr = Rewriter::rewrite(n); + ASSERT_EQ(nr, Rewriter::rewrite(nr)); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h deleted file mode 100644 index 738a51831..000000000 --- a/test/unit/theory/theory_bv_rewriter_white.h +++ /dev/null @@ -1,109 +0,0 @@ -/********************* */ -/*! \file theory_bv_rewriter_white.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 the bit-vector rewriter - ** - ** Unit tests for the bit-vector rewriter. - **/ - -#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 "util/bitvector.h" - -#include -#include -#include -#include - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::smt; -using namespace CVC4::theory; - -class TheoryBvRewriterWhite : public CxxTest::TestSuite -{ - public: - TheoryBvRewriterWhite() {} - - 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; - } - - Node boolToBv(Node b) - { - return d_nm->mkNode(ITE, - b, - d_nm->mkConst(BitVector(1, 1u)), - d_nm->mkConst(BitVector(1, 0u))); - } - - void testRewriteToFixpoint() - { - TypeNode boolType = d_nm->booleanType(); - TypeNode bvType = d_nm->mkBitVectorType(1); - - Node zero = d_nm->mkConst(BitVector(1, 0u)); - Node b1 = d_nm->mkVar("b1", boolType); - Node b2 = d_nm->mkVar("b2", boolType); - Node b3 = d_nm->mkVar("b3", boolType); - Node bv = d_nm->mkVar("bv", bvType); - - Node n = d_nm->mkNode( - BITVECTOR_ITE, - boolToBv(b1), - d_nm->mkNode(BITVECTOR_ITE, - boolToBv(b2), - d_nm->mkNode(BITVECTOR_ITE, boolToBv(b3), zero, bv), - bv), - bv); - Node nr = Rewriter::rewrite(n); - TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr)); - } - - void testRewriteBvIte() - { - TypeNode boolType = d_nm->booleanType(); - TypeNode bvType = d_nm->mkBitVectorType(1); - - Node zero = d_nm->mkConst(BitVector(1, 0u)); - Node c1 = d_nm->mkVar("c1", bvType); - Node c2 = d_nm->mkVar("c2", bvType); - - Node ite = d_nm->mkNode(BITVECTOR_ITE, c2, zero, zero); - Node n = d_nm->mkNode(BITVECTOR_ITE, c1, ite, ite); - Node nr = Rewriter::rewrite(n); - TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr)); - } - - private: - ExprManager* d_em; - SmtEngine* d_smt; - SmtScope* d_scope; - - NodeManager* d_nm; -};