From ca532e04c4b484bbd5c99e0da62e07814dd77d6d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 25 Feb 2021 05:07:17 -0800 Subject: [PATCH] google test: theory: Migrate theory_bv_white. (#5987) --- test/unit/theory/CMakeLists.txt | 2 +- test/unit/theory/theory_bv_white.cpp | 98 ++++++++++++++++++++++ test/unit/theory/theory_bv_white.h | 119 --------------------------- 3 files changed, 99 insertions(+), 120 deletions(-) create mode 100644 test/unit/theory/theory_bv_white.cpp delete mode 100644 test/unit/theory/theory_bv_white.h diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index f9c2d3141..14ae782e4 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -19,7 +19,7 @@ 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_unit_test_white(theory_bv_rewriter_white theory) -cvc4_add_cxx_unit_test_white(theory_bv_white theory) +cvc4_add_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) cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory) diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp new file mode 100644 index 000000000..0f304bfcf --- /dev/null +++ b/test/unit/theory/theory_bv_white.cpp @@ -0,0 +1,98 @@ +/********************* */ +/*! \file theory_bv_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Mathias Preiner, 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include + +#include "context/context.h" +#include "expr/node.h" +#include "test_smt.h" +#include "theory/bv/bitblast/eager_bitblaster.h" +#include "theory/bv/bv_solver_lazy.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" +#include "theory/theory_test_utils.h" + +namespace CVC4 { + +using namespace theory; +using namespace theory::bv; +using namespace theory::bv::utils; +using namespace expr; +using namespace context; +using namespace smt; + +namespace test { + +class TestTheoryWhiteBv : public TestSmtNoFinishInit +{ +}; + +TEST_F(TestTheoryWhiteBv, bitblaster_core) +{ + d_smtEngine->setLogic("QF_BV"); + + d_smtEngine->setOption("bitblast", SExpr("eager")); + d_smtEngine->setOption("incremental", SExpr("false")); + // Notice that this unit test uses the theory engine of a created SMT + // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized + // via the following call, which constructs its underlying theory engine. + d_smtEngine->finishInit(); + TheoryBV* tbv = dynamic_cast( + d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]); + BVSolverLazy* bvsl = dynamic_cast(tbv->d_internal.get()); + std::unique_ptr bb( + new EagerBitblaster(bvsl, d_smtEngine->getContext())); + + Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)); + Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)); + Node x_plus_y = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x, y); + Node one = d_nodeManager->mkConst(BitVector(16, 1u)); + Node x_shl_one = d_nodeManager->mkNode(kind::BITVECTOR_SHL, x, one); + Node eq = d_nodeManager->mkNode(kind::EQUAL, x_plus_y, x_shl_one); + Node not_x_eq_y = d_nodeManager->mkNode( + kind::NOT, d_nodeManager->mkNode(kind::EQUAL, x, y)); + + bb->bbFormula(eq); + bb->bbFormula(not_x_eq_y); + + ASSERT_EQ(bb->solve(), false); +} + +TEST_F(TestTheoryWhiteBv, mkUmulo) +{ + d_smtEngine->setOption("incremental", SExpr("true")); + for (uint32_t w = 1; w < 16; ++w) + { + d_smtEngine->push(); + Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(w)); + Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(w)); + + Node zx = mkConcat(mkZero(w), x); + Node zy = mkConcat(mkZero(w), y); + Node mul = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zx, zy); + Node lhs = d_nodeManager->mkNode( + kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w)); + Node rhs = mkUmulo(x, y); + Node eq = d_nodeManager->mkNode(kind::DISTINCT, lhs, rhs); + d_smtEngine->assertFormula(eq.toExpr()); + Result res = d_smtEngine->checkSat(); + ASSERT_EQ(res.isSat(), Result::UNSAT); + d_smtEngine->pop(); + } +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h deleted file mode 100644 index 0cfe722a6..000000000 --- a/test/unit/theory/theory_bv_white.h +++ /dev/null @@ -1,119 +0,0 @@ -/********************* */ -/*! \file theory_bv_white.h - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Mathias Preiner - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include - -#include - -#include "context/context.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/bv/bitblast/eager_bitblaster.h" -#include "theory/bv/bv_solver_lazy.h" -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "theory/theory_test_utils.h" - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; -using namespace CVC4::theory::bv::utils; -using namespace CVC4::expr; -using namespace CVC4::context; -using namespace CVC4::smt; - -using namespace std; - -class TheoryBVWhite : public CxxTest::TestSuite { - - ExprManager* d_em; - NodeManager* d_nm; - SmtEngine* d_smt; - SmtScope* d_scope; - -public: - - TheoryBVWhite() {} - - void setUp() override - { - d_em = new ExprManager(); - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm); - d_scope = new SmtScope(d_smt); - } - - void tearDown() override - { - delete d_scope; - delete d_smt; - delete d_em; - } - - void testBitblasterCore() { - d_smt->setLogic("QF_BV"); - - d_smt->setOption("bitblast", SExpr("eager")); - d_smt->setOption("incremental", SExpr("false")); - // Notice that this unit test uses the theory engine of a created SMT - // engine d_smt. We must ensure that d_smt is properly initialized via - // the following call, which constructs its underlying theory engine. - d_smt->finishInit(); - TheoryBV* tbv = dynamic_cast( - d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]); - BVSolverLazy* bvsl = dynamic_cast(tbv->d_internal.get()); - EagerBitblaster* bb = new EagerBitblaster(bvsl, d_smt->getContext()); - - Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); - Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16)); - Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y); - Node one = d_nm->mkConst(BitVector(16, 1u)); - Node x_shl_one = d_nm->mkNode(kind::BITVECTOR_SHL, x, one); - Node eq = d_nm->mkNode(kind::EQUAL, x_plus_y, x_shl_one); - Node not_x_eq_y = d_nm->mkNode(kind::NOT, d_nm->mkNode(kind::EQUAL, x, y)); - - bb->bbFormula(eq); - bb->bbFormula(not_x_eq_y); - - bool res = bb->solve(); - TS_ASSERT (res == false); - delete bb; - } - - void testMkUmulo() { - d_smt->setOption("incremental", SExpr("true")); - for (size_t w = 1; w < 16; ++w) { - d_smt->push(); - Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(w)); - Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(w)); - - Node zx = mkConcat(mkZero(w), x); - Node zy = mkConcat(mkZero(w), y); - Node mul = d_nm->mkNode(kind::BITVECTOR_MULT, zx, zy); - Node lhs = - d_nm->mkNode(kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w)); - Node rhs = mkUmulo(x, y); - Node eq = d_nm->mkNode(kind::DISTINCT, lhs, rhs); - d_smt->assertFormula(eq.toExpr()); - Result res = d_smt->checkSat(); - TS_ASSERT(res.isSat() == Result::UNSAT); - d_smt->pop(); - } - } -};/* class TheoryBVWhite */ -- 2.30.2