GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/util/boolean_simplification_black.cpp Lines: 133 133 100.0 %
Date: 2021-03-22 Branches: 490 1036 47.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file boolean_simplification_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Morgan Deters, Tim King
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Black box testing of CVC4::BooleanSimplification
13
 **
14
 ** Black box testing of CVC4::BooleanSimplification.
15
 **/
16
17
#include <algorithm>
18
#include <set>
19
#include <vector>
20
21
#include "expr/expr_iomanip.h"
22
#include "expr/kind.h"
23
#include "expr/node.h"
24
#include "options/language.h"
25
#include "options/set_language.h"
26
#include "smt_util/boolean_simplification.h"
27
#include "test_node.h"
28
29
namespace CVC4 {
30
namespace test {
31
32
16
class TestUtilBlackBooleanSimplification : public TestNode
33
{
34
 protected:
35
8
  void SetUp() override
36
  {
37
8
    TestNode::SetUp();
38
39
8
    d_a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
40
8
    d_b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
41
8
    d_c = d_nodeManager->mkSkolem("c", d_nodeManager->booleanType());
42
8
    d_d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
43
8
    d_e = d_nodeManager->mkSkolem("e", d_nodeManager->booleanType());
44
32
    d_f = d_nodeManager->mkSkolem(
45
        "f",
46
24
        d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
47
24
                                      d_nodeManager->booleanType()));
48
32
    d_g = d_nodeManager->mkSkolem(
49
        "g",
50
24
        d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
51
24
                                      d_nodeManager->booleanType()));
52
32
    d_h = d_nodeManager->mkSkolem(
53
        "h",
54
24
        d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
55
24
                                      d_nodeManager->booleanType()));
56
8
    d_fa = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_a);
57
8
    d_fb = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_b);
58
8
    d_fc = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_c);
59
8
    d_ga = d_nodeManager->mkNode(kind::APPLY_UF, d_g, d_a);
60
8
    d_ha = d_nodeManager->mkNode(kind::APPLY_UF, d_h, d_a);
61
8
    d_hc = d_nodeManager->mkNode(kind::APPLY_UF, d_h, d_c);
62
8
    d_ffb = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_fb);
63
8
    d_fhc = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_hc);
64
8
    d_hfc = d_nodeManager->mkNode(kind::APPLY_UF, d_h, d_fc);
65
8
    d_gfb = d_nodeManager->mkNode(kind::APPLY_UF, d_g, d_fb);
66
67
8
    d_ac = d_nodeManager->mkNode(kind::EQUAL, d_a, d_c);
68
8
    d_ffbd = d_nodeManager->mkNode(kind::EQUAL, d_ffb, d_d);
69
8
    d_efhc = d_nodeManager->mkNode(kind::EQUAL, d_e, d_fhc);
70
8
    d_dfa = d_nodeManager->mkNode(kind::EQUAL, d_d, d_fa);
71
72
    // this test is designed for >= 10 removal threshold
73
8
    Assert(BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD >= 10);
74
75
    std::cout << expr::ExprSetDepth(-1)
76
8
              << language::SetLanguage(language::output::LANG_CVC4);
77
8
  }
78
79
  // assert equality up to commuting children
80
30
  void test_nodes_equal(TNode n1, TNode n2)
81
  {
82
60
    std::cout << "ASSERTING: " << n1 << std::endl
83
30
              << "        ~= " << n2 << std::endl;
84
30
    ASSERT_EQ(n1.getKind(), n2.getKind());
85
30
    ASSERT_EQ(n1.getNumChildren(), n2.getNumChildren());
86
60
    std::vector<TNode> v1(n1.begin(), n1.end());
87
60
    std::vector<TNode> v2(n2.begin(), n2.end());
88
30
    sort(v1.begin(), v1.end());
89
30
    sort(v2.begin(), v2.end());
90
30
    ASSERT_EQ(v1, v2);
91
  }
92
93
  // assert that node's children have same elements as the set
94
  // (so no duplicates); also n is asserted to have kind k
95
  void test_node_equals_set(TNode n, Kind k, std::set<TNode> elts)
96
  {
97
    std::vector<TNode> v(n.begin(), n.end());
98
99
    // BooleanSimplification implementation sorts its output nodes, BUT
100
    // that's an implementation detail, not part of the contract, so we
101
    // should be robust to it here; this is a black-box test!
102
    sort(v.begin(), v.end());
103
104
    ASSERT_EQ(n.getKind(), k);
105
    ASSERT_EQ(elts.size(), n.getNumChildren());
106
    ASSERT_TRUE(equal(n.begin(), n.end(), elts.begin()));
107
  }
108
109
  Node d_a, d_b, d_c, d_d, d_e, d_f, d_g, d_h;
110
  Node d_fa, d_fb, d_fc, d_ga, d_ha, d_hc, d_ffb, d_fhc, d_hfc, d_gfb;
111
  Node d_ac, d_ffbd, d_efhc, d_dfa;
112
};
113
114
13
TEST_F(TestUtilBlackBooleanSimplification, negate)
115
{
116
4
  Node in, out;
117
118
2
  in = d_nodeManager->mkNode(kind::NOT, d_a);
119
2
  out = d_a;
120
2
  test_nodes_equal(out, BooleanSimplification::negate(in));
121
2
  test_nodes_equal(in, BooleanSimplification::negate(out));
122
123
2
  in = d_fa.andNode(d_ac).notNode().notNode().notNode().notNode();
124
2
  out = d_fa.andNode(d_ac).notNode();
125
2
  test_nodes_equal(out, BooleanSimplification::negate(in));
126
127
#ifdef CVC4_ASSERTIONS
128
2
  in = Node();
129
4
  ASSERT_THROW(BooleanSimplification::negate(in), AssertArgumentException);
130
#endif
131
}
132
133
13
TEST_F(TestUtilBlackBooleanSimplification, simplifyClause)
134
{
135
4
  Node in, out;
136
137
2
  in = d_a.orNode(d_b);
138
2
  out = in;
139
2
  test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
140
141
2
  in = d_nodeManager->mkNode(kind::OR, d_a, d_d.andNode(d_b));
142
2
  out = in;
143
2
  test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
144
145
2
  in = d_nodeManager->mkNode(kind::OR, d_a, d_d.orNode(d_b));
146
2
  out = d_nodeManager->mkNode(kind::OR, d_a, d_d, d_b);
147
2
  test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
148
149
8
  in = d_nodeManager->mkNode(kind::OR,
150
                             d_fa,
151
4
                             d_ga.orNode(d_c).notNode(),
152
                             d_hfc,
153
                             d_ac,
154
4
                             d_d.andNode(d_b));
155
6
  out = NodeBuilder<>(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc
156
4
                                << d_ac << d_d.andNode(d_b);
157
2
  test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
158
159
8
  in = d_nodeManager->mkNode(kind::OR,
160
                             d_fa,
161
4
                             d_ga.andNode(d_c).notNode(),
162
                             d_hfc,
163
                             d_ac,
164
4
                             d_d.andNode(d_b));
165
6
  out = NodeBuilder<>(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode()
166
4
                                << d_hfc << d_ac << d_d.andNode(d_b);
167
2
  test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
168
169
#ifdef CVC4_ASSERTIONS
170
2
  in = d_nodeManager->mkNode(kind::AND, d_a, d_b);
171
4
  ASSERT_THROW(BooleanSimplification::simplifyClause(in),
172
2
               AssertArgumentException);
173
#endif
174
}
175
176
13
TEST_F(TestUtilBlackBooleanSimplification, simplifyHornClause)
177
{
178
4
  Node in, out;
179
180
2
  in = d_a.impNode(d_b);
181
2
  out = d_a.notNode().orNode(d_b);
182
2
  test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
183
184
2
  in = d_a.notNode().impNode(d_ac.andNode(d_b));
185
2
  out = d_nodeManager->mkNode(kind::OR, d_a, d_ac.andNode(d_b));
186
2
  test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
187
188
2
  in =
189
16
      d_a.andNode(d_b).impNode(d_nodeManager->mkNode(kind::AND,
190
                                                     d_fa,
191
4
                                                     d_ga.orNode(d_c).notNode(),
192
4
                                                     d_hfc.orNode(d_ac),
193
4
                                                     d_d.andNode(d_b)));
194
12
  out = d_nodeManager->mkNode(kind::OR,
195
4
                              d_a.notNode(),
196
4
                              d_b.notNode(),
197
14
                              d_nodeManager->mkNode(kind::AND,
198
                                                    d_fa,
199
4
                                                    d_ga.orNode(d_c).notNode(),
200
4
                                                    d_hfc.orNode(d_ac),
201
4
                                                    d_d.andNode(d_b)));
202
2
  test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
203
204
6
  in = d_a.andNode(d_b).impNode(
205
14
      d_nodeManager->mkNode(kind::OR,
206
                            d_fa,
207
4
                            d_ga.orNode(d_c).notNode(),
208
4
                            d_hfc.orNode(d_ac),
209
4
                            d_d.andNode(d_b).notNode()));
210
6
  out = NodeBuilder<>(kind::OR)
211
4
        << d_a.notNode() << d_b.notNode() << d_fa << d_ga.orNode(d_c).notNode()
212
4
        << d_hfc << d_ac << d_d.notNode();
213
2
  test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
214
215
#ifdef CVC4_ASSERTIONS
216
2
  in = d_nodeManager->mkNode(kind::OR, d_a, d_b);
217
4
  ASSERT_THROW(BooleanSimplification::simplifyHornClause(in),
218
2
               AssertArgumentException);
219
#endif
220
}
221
222
13
TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict)
223
{
224
4
  Node in, out;
225
226
2
  in = d_a.andNode(d_b);
227
2
  out = in;
228
2
  test_nodes_equal(out, BooleanSimplification::simplifyConflict(in));
229
230
2
  in = d_nodeManager->mkNode(kind::AND, d_a, d_d.andNode(d_b));
231
2
  out = d_nodeManager->mkNode(kind::AND, d_a, d_d, d_b);
232
2
  test_nodes_equal(out, BooleanSimplification::simplifyConflict(in));
233
234
12
  in = d_nodeManager->mkNode(kind::AND,
235
                             d_fa,
236
4
                             d_ga.orNode(d_c).notNode(),
237
                             d_fa,
238
4
                             d_hfc.orNode(d_ac),
239
4
                             d_d.andNode(d_b));
240
6
  out = NodeBuilder<>(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode()
241
4
                                 << d_hfc.orNode(d_ac) << d_d << d_b;
242
2
  test_nodes_equal(out, BooleanSimplification::simplifyConflict(in));
243
244
#ifdef CVC4_ASSERTIONS
245
2
  in = d_nodeManager->mkNode(kind::OR, d_a, d_b);
246
4
  ASSERT_THROW(BooleanSimplification::simplifyConflict(in),
247
2
               AssertArgumentException);
248
#endif
249
}
250
}  // namespace test
251
71717
}  // namespace CVC4