diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-04-01 14:26:23 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-01 14:26:23 -0700 |
commit | 41355e412a142809f63a1939a4515486ccd4c6fb (patch) | |
tree | b8b7ee334c8cdc52c72a10356adfaf769793c539 /test | |
parent | ae536749a2342e51c450deb62a13d5cfda965881 (diff) |
Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)
`TheoryBVRewriter::RewriteITEBv()` is currently always returning the
status `REWRITE_DONE`. This can result in a situation where a rewritten
node can be rewritten again (which breaks the contract of our rewriter).
The unit test in this commit illustrates the issue. The commit fixes the
issue by returning `REWRITE_AGAIN` or `REWRITE_AGAIN_FULL` if a node
changed. `REWRITE_AGAIN_FULL` is needed if the resulting node may have a
child that is not a subterm of the original expression.
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; +}; |