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