From: Aina Niemetz Date: Wed, 24 Feb 2021 08:17:55 +0000 (-0800) Subject: google test: theory: Migrate evaluator_white. (#5972) X-Git-Tag: cvc5-1.0.0~2227 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=72b71353092c6169d5085e7eb812a4ae80e5fc6a;p=cvc5.git google test: theory: Migrate evaluator_white. (#5972) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 6c4e62765..03968ce75 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -10,7 +10,7 @@ ## 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_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_unit_test_white(strings_rewriter_white theory) diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp new file mode 100644 index 000000000..039a5f12f --- /dev/null +++ b/test/unit/theory/evaluator_white.cpp @@ -0,0 +1,161 @@ +/********************* */ +/*! \file evaluator_white.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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include + +#include "expr/node.h" +#include "test_smt.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/evaluator.h" +#include "theory/rewriter.h" +#include "theory/theory_test_utils.h" +#include "util/rational.h" + +namespace CVC4 { + +using namespace smt; +using namespace theory; + +namespace test { + +class TestTheoryWhiteEvaluator : public TestSmt +{ +}; + +TEST_F(TestTheoryWhiteEvaluator, simple) +{ + TypeNode bv64Type = d_nodeManager->mkBitVectorType(64); + + Node w = d_nodeManager->mkVar("w", bv64Type); + Node x = d_nodeManager->mkVar("x", bv64Type); + Node y = d_nodeManager->mkVar("y", bv64Type); + Node z = d_nodeManager->mkVar("z", bv64Type); + + Node zero = d_nodeManager->mkConst(BitVector(64, (unsigned int)0)); + Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1)); + Node c1 = d_nodeManager->mkConst(BitVector( + 64, + (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111)); + Node c2 = d_nodeManager->mkConst(BitVector( + 64, + (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111)); + + Node t = d_nodeManager->mkNode( + kind::ITE, d_nodeManager->mkNode(kind::EQUAL, y, one), x, w); + + std::vector args = {w, x, y, z}; + std::vector vals = {c1, zero, one, c1}; + + Evaluator eval; + Node r = eval.eval(t, args, vals); + ASSERT_EQ(r, + Rewriter::rewrite(t.substitute( + args.begin(), args.end(), vals.begin(), vals.end()))); +} + +TEST_F(TestTheoryWhiteEvaluator, loop) +{ + TypeNode bv64Type = d_nodeManager->mkBitVectorType(64); + + Node w = d_nodeManager->mkBoundVar(bv64Type); + Node x = d_nodeManager->mkVar("x", bv64Type); + + Node zero = d_nodeManager->mkConst(BitVector(1, (unsigned int)0)); + Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1)); + Node c = d_nodeManager->mkConst(BitVector( + 64, + (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100)); + + Node largs = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, w); + Node lbody = d_nodeManager->mkNode( + kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero); + Node lambda = d_nodeManager->mkNode(kind::LAMBDA, largs, lbody); + Node t = + d_nodeManager->mkNode(kind::BITVECTOR_AND, + d_nodeManager->mkNode(kind::APPLY_UF, lambda, one), + d_nodeManager->mkNode(kind::APPLY_UF, lambda, x)); + + std::vector args = {x}; + std::vector vals = {c}; + Evaluator eval; + Node r = eval.eval(t, args, vals); + ASSERT_EQ(r, + Rewriter::rewrite(t.substitute( + args.begin(), args.end(), vals.begin(), vals.end()))); +} + +TEST_F(TestTheoryWhiteEvaluator, strIdOf) +{ + Node a = d_nodeManager->mkConst(String("A")); + Node empty = d_nodeManager->mkConst(String("")); + Node one = d_nodeManager->mkConst(Rational(1)); + Node two = d_nodeManager->mkConst(Rational(2)); + + std::vector args; + std::vector vals; + Evaluator eval; + + { + Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, one); + Node r = eval.eval(n, args, vals); + ASSERT_EQ(r, Rewriter::rewrite(n)); + } + + { + Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, one); + Node r = eval.eval(n, args, vals); + ASSERT_EQ(r, Rewriter::rewrite(n)); + } + + { + Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, two); + Node r = eval.eval(n, args, vals); + ASSERT_EQ(r, Rewriter::rewrite(n)); + } + + { + Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, two); + Node r = eval.eval(n, args, vals); + ASSERT_EQ(r, Rewriter::rewrite(n)); + } +} + +TEST_F(TestTheoryWhiteEvaluator, code) +{ + Node a = d_nodeManager->mkConst(String("A")); + Node empty = d_nodeManager->mkConst(String("")); + + std::vector args; + std::vector vals; + Evaluator eval; + + // (str.code "A") ---> 65 + { + Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a); + Node r = eval.eval(n, args, vals); + ASSERT_EQ(r, d_nodeManager->mkConst(Rational(65))); + } + + // (str.code "") ---> -1 + { + Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty); + Node r = eval.eval(n, args, vals); + ASSERT_EQ(r, d_nodeManager->mkConst(Rational(-1))); + } +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h deleted file mode 100644 index 1f33d0fbf..000000000 --- a/test/unit/theory/evaluator_white.h +++ /dev/null @@ -1,184 +0,0 @@ -/********************* */ -/*! \file evaluator_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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include -#include - -#include "expr/node.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/evaluator.h" -#include "theory/rewriter.h" -#include "theory/theory_test_utils.h" -#include "util/rational.h" - -using namespace CVC4; -using namespace CVC4::smt; -using namespace CVC4::theory; - -using namespace std; - -class TheoryEvaluatorWhite : public CxxTest::TestSuite -{ - ExprManager *d_em; - NodeManager *d_nm; - SmtEngine *d_smt; - SmtScope *d_scope; - - public: - TheoryEvaluatorWhite() {} - - 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 testSimple() - { - TypeNode bv64Type = d_nm->mkBitVectorType(64); - - Node w = d_nm->mkVar("w", bv64Type); - Node x = d_nm->mkVar("x", bv64Type); - Node y = d_nm->mkVar("y", bv64Type); - Node z = d_nm->mkVar("z", bv64Type); - - Node zero = d_nm->mkConst(BitVector(64, (unsigned int)0)); - Node one = d_nm->mkConst(BitVector(64, (unsigned int)1)); - Node c1 = d_nm->mkConst(BitVector( - 64, - (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111)); - Node c2 = d_nm->mkConst(BitVector( - 64, - (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111)); - - Node t = d_nm->mkNode(kind::ITE, d_nm->mkNode(kind::EQUAL, y, one), x, w); - - std::vector args = {w, x, y, z}; - std::vector vals = {c1, zero, one, c1}; - - Evaluator eval; - Node r = eval.eval(t, args, vals); - TS_ASSERT_EQUALS(r, - Rewriter::rewrite(t.substitute( - args.begin(), args.end(), vals.begin(), vals.end()))); - } - - void testLoop() - { - TypeNode bv64Type = d_nm->mkBitVectorType(64); - - Node w = d_nm->mkBoundVar(bv64Type); - Node x = d_nm->mkVar("x", bv64Type); - - Node zero = d_nm->mkConst(BitVector(1, (unsigned int)0)); - Node one = d_nm->mkConst(BitVector(64, (unsigned int)1)); - Node c = d_nm->mkConst(BitVector( - 64, - (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100)); - - Node largs = d_nm->mkNode(kind::BOUND_VAR_LIST, w); - Node lbody = d_nm->mkNode( - kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero); - Node lambda = d_nm->mkNode(kind::LAMBDA, largs, lbody); - Node t = d_nm->mkNode(kind::BITVECTOR_AND, - d_nm->mkNode(kind::APPLY_UF, lambda, one), - d_nm->mkNode(kind::APPLY_UF, lambda, x)); - - std::vector args = {x}; - std::vector vals = {c}; - Evaluator eval; - Node r = eval.eval(t, args, vals); - TS_ASSERT_EQUALS(r, - Rewriter::rewrite(t.substitute( - args.begin(), args.end(), vals.begin(), vals.end()))); - } - - void testStrIdOf() - { - Node a = d_nm->mkConst(String("A")); - Node empty = d_nm->mkConst(String("")); - Node one = d_nm->mkConst(Rational(1)); - Node two = d_nm->mkConst(Rational(2)); - - std::vector args; - std::vector vals; - Evaluator eval; - - { - Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, empty, one); - Node r = eval.eval(n, args, vals); - TS_ASSERT_EQUALS(r, Rewriter::rewrite(n)); - } - - { - Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, a, one); - Node r = eval.eval(n, args, vals); - TS_ASSERT_EQUALS(r, Rewriter::rewrite(n)); - } - - { - Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, empty, two); - Node r = eval.eval(n, args, vals); - TS_ASSERT_EQUALS(r, Rewriter::rewrite(n)); - } - - { - Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, a, two); - Node r = eval.eval(n, args, vals); - TS_ASSERT_EQUALS(r, Rewriter::rewrite(n)); - } - } - - void testCode() - { - Node a = d_nm->mkConst(String("A")); - Node empty = d_nm->mkConst(String("")); - - std::vector args; - std::vector vals; - Evaluator eval; - - // (str.code "A") ---> 65 - { - Node n = d_nm->mkNode(kind::STRING_TO_CODE, a); - Node r = eval.eval(n, args, vals); - TS_ASSERT_EQUALS(r, d_nm->mkConst(Rational(65))); - } - - // (str.code "") ---> -1 - { - Node n = d_nm->mkNode(kind::STRING_TO_CODE, empty); - Node r = eval.eval(n, args, vals); - TS_ASSERT_EQUALS(r, d_nm->mkConst(Rational(-1))); - } - } -};