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