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