1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
/***
* Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
*
* Copyright (C) 2023 by the authors listed in the AUTHORS file at
* https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
*
* This file is part of Bitwuzla under the MIT license. See COPYING for more
* information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
*/
#include "test/unit/rewrite/test_rewriter.h"
namespace bzla::test {
using namespace bzla::node;
class TestRewriterBvNorm : public TestRewriter
{
};
TEST_F(TestRewriterBvNorm, norm_bv_add_mul)
{
constexpr RewriteRuleKind kind = RewriteRuleKind::NORM_BV_ADD_MUL;
//// applies
test_rule<kind>(
d_nm.mk_node(Kind::BV_ADD,
{d_nm.invert_node(d_nm.mk_node(
Kind::BV_MUL, {d_bv4_a, d_nm.invert_node(d_bv4_b)})),
d_bv4_one}));
//// does not apply
test_rule_does_not_apply<kind>(
RewriteRule<RewriteRuleKind::BV_NEG_ELIM>::apply(
d_rewriter,
d_nm.mk_node(Kind::BV_NEG,
{d_nm.mk_node(Kind::BV_MUL, {d_bv4_a, d_bv4_b})}))
.first);
}
TEST_F(TestRewriterBvNorm, norm_bv_not_or_shl)
{
constexpr RewriteRuleKind kind = RewriteRuleKind::NORM_BV_NOT_OR_SHL;
//// applies
test_rule<kind>(d_nm.invert_node(d_nm.mk_node(
Kind::BV_AND,
{d_nm.invert_node(d_bv4_a),
d_nm.invert_node(d_nm.mk_node(Kind::BV_SHL, {d_bv4_b, d_bv4_a}))})));
test_rule<kind>(d_nm.invert_node(d_nm.mk_node(
Kind::BV_AND,
{d_nm.invert_node(d_nm.mk_node(Kind::BV_SHL, {d_bv4_b, d_bv4_a})),
d_nm.invert_node(d_bv4_a)})));
//// does not apply
test_rule_does_not_apply<kind>(d_nm.invert_node(
d_nm.mk_node(Kind::BV_AND,
{d_nm.mk_node(Kind::BV_SHL, {d_bv4_b, d_bv4_a}),
d_nm.invert_node(d_bv4_a)})));
}
TEST_F(TestRewriterBvNorm, norm_bv_shl_neg)
{
constexpr RewriteRuleKind kind = RewriteRuleKind::NORM_BV_SHL_NEG;
//// applies
test_rule<kind>(
d_nm.mk_node(Kind::BV_SHL,
{RewriteRule<RewriteRuleKind::BV_NEG_ELIM>::apply(
d_rewriter, d_nm.mk_node(Kind::BV_NEG, {d_bv4_a}))
.first,
d_bv4_b}));
}
} // namespace bzla::test
|
