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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
/***
* Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
*
* Copyright (C) 2022 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 <gtest/gtest.h>
#include "backtrack/backtrackable.h"
#include "preprocess/pass/flatten_and.h"
#include "test/unit/preprocess/test_preprocess_pass.h"
namespace bzla::test {
using namespace backtrack;
using namespace node;
class TestPassFlattenAnd : public TestPreprocessingPass
{
public:
TestPassFlattenAnd() : d_env(d_nm), d_pass(d_env, &d_bm){};
protected:
Env d_env;
preprocess::pass::PassFlattenAnd d_pass;
};
TEST_F(TestPassFlattenAnd, and1)
{
Node a1 = d_nm.mk_const(d_nm.mk_bool_type(), "a1");
Node a2 = d_nm.mk_const(d_nm.mk_bool_type(), "a2");
d_as.push_back(d_nm.mk_node(Kind::AND, {a1, a2}));
ASSERT_EQ(d_as.size(), 1);
preprocess::AssertionVector assertions(d_as.view());
d_pass.apply(assertions);
ASSERT_EQ(d_as.size(), 3);
ASSERT_EQ(d_as[0], d_nm.mk_value(true));
ASSERT_EQ(d_as[1], a1);
ASSERT_EQ(d_as[2], a2);
}
TEST_F(TestPassFlattenAnd, and2)
{
Node a1 = d_nm.mk_const(d_nm.mk_bool_type(), "a1");
Node a2 = d_nm.mk_const(d_nm.mk_bool_type(), "a2");
Node a3 = d_nm.mk_const(d_nm.mk_bool_type(), "a3");
d_as.push_back(
d_nm.mk_node(Kind::AND, {a1, d_nm.mk_node(Kind::AND, {a2, a3})}));
ASSERT_EQ(d_as.size(), 1);
preprocess::AssertionVector assertions(d_as.view());
d_pass.apply(assertions);
ASSERT_EQ(d_as.size(), 4);
ASSERT_EQ(d_as[0], d_nm.mk_value(true));
ASSERT_EQ(d_as[1], a1);
ASSERT_EQ(d_as[2], a2);
ASSERT_EQ(d_as[3], a3);
}
TEST_F(TestPassFlattenAnd, and3)
{
Node a1 = d_nm.mk_const(d_nm.mk_bool_type(), "a1");
Node a2 = d_nm.mk_const(d_nm.mk_bool_type(), "a2");
d_as.push_back(
d_nm.mk_node(Kind::AND, {a2, d_nm.mk_node(Kind::AND, {a1, a2})}));
ASSERT_EQ(d_as.size(), 1);
preprocess::AssertionVector assertions(d_as.view());
d_pass.apply(assertions);
ASSERT_EQ(d_as.size(), 3);
ASSERT_EQ(d_as[0], d_nm.mk_value(true));
ASSERT_EQ(d_as[1], a2);
ASSERT_EQ(d_as[2], a1);
}
} // namespace bzla::test
|
