diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_rewriter_white.h | 94 |
2 files changed, 95 insertions, 0 deletions
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 3d29c4de1..963466b09 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -2,6 +2,7 @@ cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_unit_test_white(theory_arith_white theory) +cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_unit_test_white(theory_bv_white theory) cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h new file mode 100644 index 000000000..1f4cc0c2c --- /dev/null +++ b/test/unit/theory/theory_bv_rewriter_white.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file theory_bv_rewriter_white.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 <cxxtest/TestSuite.h> +#include <iostream> +#include <memory> +#include <vector> + +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(opts); + d_smt = new SmtEngine(d_em); + d_scope = new SmtScope(d_smt); + + d_nm = NodeManager::currentNM(); + } + + 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)); + } + + private: + ExprManager* d_em; + SmtEngine* d_smt; + SmtScope* d_scope; + + NodeManager* d_nm; +}; |