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 : : * Implementation of algorithm suggested by Deharbe, Fontaine, Merz,
11 : : * and Paleo, "Exploiting symmetry in SMT problems," CADE 2011.
12 : : *
13 : : * From the paper:
14 : : *
15 : : * <pre>
16 : : * \f$ P := guess\_permutations(\phi) \f$
17 : : * foreach \f$ {c_0, ..., c_n} \in P \f$ do
18 : : * if \f$ invariant\_by\_permutations(\phi, {c_0, ..., c_n}) \f$ then
19 : : * T := \f$ select\_terms(\phi, {c_0, ..., c_n}) \f$
20 : : * cts := \f$ \emptyset \f$
21 : : * while T != \f$ \empty \wedge |cts| <= n \f$ do
22 : : * \f$ t := select\_most\_promising\_term(T, \phi) \f$
23 : : * \f$ T := T \setminus {t} \f$
24 : : * cts := cts \f$ \cup used\_in(t, {c_0, ..., c_n}) \f$
25 : : * let \f$ c \in {c_0, ..., c_n} \setminus cts \f$
26 : : * cts := cts \f$ \cup {c} \f$
27 : : * if cts != \f$ {c_0, ..., c_n} \f$ then
28 : : * \f$ \phi := \phi \wedge ( \vee_{c_i \in cts} t = c_i ) \f$
29 : : * end
30 : : * end
31 : : * end
32 : : * end
33 : : * return \f$ \phi \f$
34 : : * </pre>
35 : : */
36 : :
37 : : #include "theory/uf/symmetry_breaker.h"
38 : :
39 : : #include <iterator>
40 : : #include <queue>
41 : :
42 : : #include "theory/rewriter.h"
43 : : #include "util/hash.h"
44 : : #include "util/statistics_registry.h"
45 : :
46 : : using namespace std;
47 : :
48 : : namespace cvc5::internal {
49 : : namespace theory {
50 : : namespace uf {
51 : :
52 : : using namespace cvc5::context;
53 : :
54 : 116081 : SymmetryBreaker::Template::Template(NodeManager* nm)
55 : 116081 : : d_template(), d_assertions(nm), d_sets(), d_reps()
56 : : {
57 : 116081 : }
58 : :
59 : 266388 : TNode SymmetryBreaker::Template::find(TNode n)
60 : : {
61 : 266388 : unordered_map<TNode, TNode>::iterator i = d_reps.find(n);
62 [ + + ]: 266388 : if (i == d_reps.end())
63 : : {
64 : 215690 : return n;
65 : : }
66 : : else
67 : : {
68 : 101396 : return d_reps[n] = find((*i).second);
69 : : }
70 : : }
71 : :
72 : 375693 : bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n)
73 : : {
74 [ + - ]: 751386 : IndentedScope scope(Trace("ufsymm:match"));
75 : :
76 [ + - ]: 751386 : Trace("ufsymm:match") << "UFSYMM matching " << t << endl
77 : 375693 : << "UFSYMM to " << n << endl;
78 : :
79 [ + + ][ + + ]: 375693 : if (t.getKind() != n.getKind() || t.getNumChildren() != n.getNumChildren())
[ + + ]
80 : : {
81 [ + - ]: 140371 : Trace("ufsymm:match") << "UFSYMM BAD MATCH on kind, #children" << endl;
82 : 140371 : return false;
83 : : }
84 : :
85 [ + + ]: 235322 : if (t.getNumChildren() == 0)
86 : : {
87 [ + + ]: 107851 : if (!t.isVar())
88 : : {
89 [ + - ]: 6 : Trace("ufsymm:match") << "UFSYMM non-variables, failing match" << endl;
90 : 6 : return false;
91 : : }
92 : 107845 : t = find(t);
93 : 107845 : n = find(n);
94 [ + - ]: 215690 : Trace("ufsymm:match") << "UFSYMM variable match " << t << " , " << n
95 : 107845 : << endl;
96 [ + - ]: 107845 : Trace("ufsymm:match") << "UFSYMM sets: " << t << " =>";
97 [ + + ]: 107845 : if (d_sets.find(t) != d_sets.end())
98 : : {
99 [ + + ]: 157114 : for (set<TNode>::iterator i = d_sets[t].begin(); i != d_sets[t].end();
100 : 117324 : ++i)
101 : : {
102 [ + - ]: 117324 : Trace("ufsymm:match") << " " << *i;
103 : : }
104 : : }
105 [ + - ]: 107845 : Trace("ufsymm:match") << endl;
106 [ + + ]: 107845 : if (t != n)
107 : : {
108 [ + - ]: 91141 : Trace("ufsymm:match") << "UFSYMM sets: " << n << " =>";
109 [ + + ]: 91141 : if (d_sets.find(n) != d_sets.end())
110 : : {
111 [ + + ]: 238 : for (set<TNode>::iterator i = d_sets[n].begin(); i != d_sets[n].end();
112 : 143 : ++i)
113 : : {
114 [ + - ]: 143 : Trace("ufsymm:match") << " " << *i;
115 : : }
116 : : }
117 [ + - ]: 91141 : Trace("ufsymm:match") << endl;
118 : :
119 [ + + ]: 91141 : if (d_sets.find(t) == d_sets.end())
120 : : {
121 [ + - ]: 136110 : Trace("ufsymm:match")
122 : 68055 : << "UFSYMM inserting " << t << " in with " << n << endl;
123 : 68055 : d_reps[t] = n;
124 : 68055 : d_sets[n].insert(t);
125 : : }
126 : : else
127 : : {
128 [ + + ]: 23086 : if (d_sets.find(n) != d_sets.end())
129 : : {
130 [ + - ]: 64 : Trace("ufsymm:match") << "UFSYMM merging " << n << " and " << t
131 : 32 : << " in with " << n << endl;
132 : 32 : d_sets[n].insert(d_sets[t].begin(), d_sets[t].end());
133 : 32 : d_sets[n].insert(t);
134 : 32 : d_reps[t] = n;
135 : 32 : d_sets.erase(t);
136 : : }
137 : : else
138 : : {
139 [ + - ]: 46108 : Trace("ufsymm:match")
140 : 23054 : << "UFSYMM inserting " << n << " in with " << t << endl;
141 : 23054 : d_sets[t].insert(n);
142 : 23054 : d_reps[n] = t;
143 : : }
144 : : }
145 : : }
146 : 107845 : return true;
147 : : }
148 : :
149 [ + + ]: 127471 : if (t.getMetaKind() == kind::metakind::PARAMETERIZED)
150 : : {
151 [ + + ]: 12279 : if (t.getOperator() != n.getOperator())
152 : : {
153 [ + - ]: 220 : Trace("ufsymm:match")
154 [ - - ]: 110 : << "UFSYMM BAD MATCH on operators: " << t.getOperator()
155 [ - + ][ - + ]: 110 : << " != " << n.getOperator() << endl;
[ - - ]
156 : 110 : return false;
157 : : }
158 : : }
159 : 127361 : TNode::iterator ti = t.begin();
160 : 127361 : TNode::iterator ni = n.begin();
161 [ + + ]: 261287 : while (ti != t.end())
162 : : {
163 [ + + ]: 180565 : if (*ti != *ni)
164 : : { // nothing to do if equal
165 [ + + ]: 163433 : if (!matchRecursive(*ti, *ni))
166 : : {
167 [ + - ]: 46639 : Trace("ufsymm:match") << "UFSYMM BAD MATCH, withdrawing.." << endl;
168 : 46639 : return false;
169 : : }
170 : : }
171 : 133926 : ++ti;
172 : 133926 : ++ni;
173 : : }
174 : :
175 : 80722 : return true;
176 : 375693 : }
177 : :
178 : 378616 : bool SymmetryBreaker::Template::match(TNode n)
179 : : {
180 : : // try to "match" n and d_template
181 [ + + ]: 378616 : if (d_template.isNull())
182 : : {
183 [ + - ]: 166356 : Trace("ufsymm") << "UFSYMM setting template " << n << endl;
184 : 166356 : d_template = n;
185 : 166356 : return true;
186 : : }
187 : : else
188 : : {
189 : 212260 : return matchRecursive(d_template, n);
190 : : }
191 : : }
192 : :
193 : 110475 : void SymmetryBreaker::Template::reset()
194 : : {
195 : 110475 : d_template = Node::null();
196 : 110475 : d_sets.clear();
197 : 110475 : d_reps.clear();
198 : 110475 : }
199 : :
200 : 27723 : SymmetryBreaker::SymmetryBreaker(Env& env, std::string name)
201 : : : EnvObj(env),
202 : 55446 : ContextNotifyObj(userContext()),
203 : 27723 : d_assertionsToRerun(userContext()),
204 : 27723 : d_rerunningAssertions(false),
205 : 27723 : d_phi(),
206 : 27723 : d_phiSet(),
207 : 27723 : d_permutations(),
208 : 27723 : d_terms(),
209 : 27723 : d_template(nodeManager()),
210 : 27723 : d_normalizationCache(),
211 : 27723 : d_termEqs(),
212 : 27723 : d_termEqsOnly(),
213 : 27723 : d_name(name),
214 : 55446 : d_stats(statisticsRegistry(), d_name + "theory::uf::symmetry_breaker::")
215 : : {
216 : 27723 : }
217 : :
218 : : class SBGuard
219 : : {
220 : : bool& d_ref;
221 : : bool d_old;
222 : :
223 : : public:
224 : 0 : SBGuard(bool& b) : d_ref(b), d_old(b) {}
225 : 0 : ~SBGuard()
226 : : {
227 [ - - ]: 0 : Trace("uf") << "reset to " << d_old << std::endl;
228 : 0 : d_ref = d_old;
229 : 0 : }
230 : : }; /* class SBGuard */
231 : :
232 : 92151 : void SymmetryBreaker::rerunAssertionsIfNecessary()
233 : : {
234 [ + - ][ + + ]: 92151 : if (d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty())
[ + - ][ + - ]
235 : : {
236 : 92151 : return;
237 : : }
238 : :
239 : 0 : SBGuard g(d_rerunningAssertions);
240 : 0 : d_rerunningAssertions = true;
241 : :
242 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM: rerunning assertions..." << std::endl;
243 : 0 : for (CDList<Node>::const_iterator i = d_assertionsToRerun.begin();
244 [ - - ]: 0 : i != d_assertionsToRerun.end();
245 : 0 : ++i)
246 : : {
247 : 0 : assertFormula(*i);
248 : : }
249 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM: DONE rerunning assertions..." << std::endl;
250 : 0 : }
251 : :
252 : 29367018 : Node SymmetryBreaker::norm(TNode phi)
253 : : {
254 : 29367018 : Node n = rewrite(phi);
255 : 58734036 : return normInternal(n, 0);
256 : 29367018 : }
257 : :
258 : 29381873 : Node SymmetryBreaker::normInternal(TNode n, size_t level)
259 : : {
260 : 29381873 : Node& result = d_normalizationCache[n];
261 [ + + ]: 29381873 : if (!result.isNull())
262 : : {
263 : 29132665 : return result;
264 : : }
265 : :
266 [ + + ][ + + ]: 249208 : switch (Kind k = n.getKind())
[ - + ]
267 : : {
268 : 4 : case Kind::DISTINCT:
269 : : {
270 : : // commutative N-ary operator handling
271 : 4 : vector<TNode> kids(n.begin(), n.end());
272 : 4 : sort(kids.begin(), kids.end());
273 : 8 : return result = nodeManager()->mkNode(k, kids);
274 : 4 : }
275 : :
276 : 433 : case Kind::AND:
277 : : {
278 : : // commutative+associative N-ary operator handling
279 : 433 : vector<Node> kids;
280 : 433 : kids.reserve(n.getNumChildren());
281 : 433 : queue<TNode> work;
282 : 433 : work.push(n);
283 [ + - ]: 433 : Trace("ufsymm:norm") << "UFSYMM processing " << n << endl;
284 : : do
285 : : {
286 : 433 : TNode m = work.front();
287 : 433 : work.pop();
288 [ + + ]: 1299 : for (TNode::iterator i = m.begin(); i != m.end(); ++i)
289 : : {
290 [ - + ]: 866 : if ((*i).getKind() == k)
291 : : {
292 : 0 : work.push(*i);
293 : : }
294 : : else
295 : : {
296 [ + + ]: 866 : if ((*i).getKind() == Kind::OR)
297 : : {
298 : 1 : kids.push_back(normInternal(*i, level));
299 : : }
300 [ + + ]: 865 : else if ((*i).getKind() == Kind::EQUAL)
301 : : {
302 : 857 : kids.push_back(normInternal(*i, level));
303 : 857 : if ((*i)[0].isVar() || (*i)[1].isVar())
304 : : {
305 : 857 : d_termEqs[(*i)[0]].insert((*i)[1]);
306 : 857 : d_termEqs[(*i)[1]].insert((*i)[0]);
307 [ - + ]: 857 : if (level == 0)
308 : : {
309 : 0 : d_termEqsOnly[(*i)[0]].insert((*i)[1]);
310 : 0 : d_termEqsOnly[(*i)[1]].insert((*i)[0]);
311 [ - - ]: 0 : Trace("ufsymm:eq")
312 : 0 : << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl;
313 : : }
314 : : }
315 : : }
316 : : else
317 : : {
318 : 8 : kids.push_back(*i);
319 : : }
320 : : }
321 : : }
322 [ - + ]: 433 : } while (!work.empty());
323 [ + - ]: 866 : Trace("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the "
324 : 433 : << k << "-kinded Node" << endl;
325 : 433 : sort(kids.begin(), kids.end());
326 : 866 : return result = nodeManager()->mkNode(k, kids);
327 : 433 : }
328 : :
329 : 208616 : case Kind::OR:
330 : : {
331 : : // commutative+associative N-ary operator handling
332 : 208616 : vector<Node> kids;
333 : 208616 : kids.reserve(n.getNumChildren());
334 : 208616 : queue<TNode> work;
335 : 208616 : work.push(n);
336 [ + - ]: 208616 : Trace("ufsymm:norm") << "UFSYMM processing " << n << endl;
337 : 208616 : TNode matchingTerm = TNode::null();
338 : 208616 : vector<TNode> matchingTermEquals;
339 : 208616 : bool first = true, matchedVar = false;
340 : : do
341 : : {
342 : 208616 : TNode m = work.front();
343 : 208616 : work.pop();
344 [ + + ]: 843291 : for (TNode::iterator i = m.begin(); i != m.end(); ++i)
345 : : {
346 [ - + ]: 634675 : if ((*i).getKind() == k)
347 : : {
348 : 0 : work.push(*i);
349 : : }
350 : : else
351 : : {
352 [ + + ]: 634675 : if ((*i).getKind() == Kind::AND)
353 : : {
354 : 757 : first = false;
355 : 757 : matchingTerm = TNode::null();
356 : 757 : kids.push_back(normInternal(*i, level + 1));
357 : : }
358 [ + + ]: 633918 : else if ((*i).getKind() == Kind::EQUAL)
359 : : {
360 : 13240 : kids.push_back(normInternal(*i, level + 1));
361 : 13240 : if ((*i)[0].isVar() || (*i)[1].isVar())
362 : : {
363 : 13120 : d_termEqs[(*i)[0]].insert((*i)[1]);
364 : 13120 : d_termEqs[(*i)[1]].insert((*i)[0]);
365 [ + - ]: 13120 : if (level == 0)
366 : : {
367 [ + + ]: 13120 : if (first)
368 : : {
369 : 2745 : matchingTerm = *i;
370 : : }
371 [ + + ]: 10375 : else if (!matchingTerm.isNull())
372 : : {
373 [ + + ]: 10221 : if (matchedVar)
374 : : {
375 [ + + ]: 7489 : if (matchingTerm == (*i)[0])
376 : : {
377 : 2417 : matchingTermEquals.push_back((*i)[1]);
378 : : }
379 [ + + ]: 5072 : else if (matchingTerm == (*i)[1])
380 : : {
381 : 5068 : matchingTermEquals.push_back((*i)[0]);
382 : : }
383 : : else
384 : : {
385 : 4 : matchingTerm = TNode::null();
386 : : }
387 : : }
388 [ + + ]: 2732 : else if ((*i)[0] == matchingTerm[0])
389 : : {
390 : 777 : matchingTermEquals.push_back(matchingTerm[1]);
391 : 777 : matchingTermEquals.push_back((*i)[1]);
392 : 777 : matchingTerm = matchingTerm[0];
393 : 777 : matchedVar = true;
394 : : }
395 [ - + ]: 1955 : else if ((*i)[1] == matchingTerm[0])
396 : : {
397 : 0 : matchingTermEquals.push_back(matchingTerm[1]);
398 : 0 : matchingTermEquals.push_back((*i)[0]);
399 : 0 : matchingTerm = matchingTerm[0];
400 : 0 : matchedVar = true;
401 : : }
402 [ + + ]: 1955 : else if ((*i)[0] == matchingTerm[1])
403 : : {
404 : 4 : matchingTermEquals.push_back(matchingTerm[0]);
405 : 4 : matchingTermEquals.push_back((*i)[1]);
406 : 4 : matchingTerm = matchingTerm[1];
407 : 4 : matchedVar = true;
408 : : }
409 [ + + ]: 1951 : else if ((*i)[1] == matchingTerm[1])
410 : : {
411 : 1888 : matchingTermEquals.push_back(matchingTerm[0]);
412 : 1888 : matchingTermEquals.push_back((*i)[0]);
413 : 1888 : matchingTerm = matchingTerm[1];
414 : 1888 : matchedVar = true;
415 : : }
416 : : else
417 : : {
418 : 63 : matchingTerm = TNode::null();
419 : : }
420 : : }
421 : : }
422 : : }
423 : : else
424 : : {
425 : 120 : matchingTerm = TNode::null();
426 : : }
427 : 13240 : first = false;
428 : : }
429 : : else
430 : : {
431 : 620678 : first = false;
432 : 620678 : matchingTerm = TNode::null();
433 : 620678 : kids.push_back(*i);
434 : : }
435 : : }
436 : : }
437 [ - + ]: 208616 : } while (!work.empty());
438 [ + + ]: 208616 : if (!matchingTerm.isNull())
439 : : {
440 [ - + ]: 2661 : if (TraceIsOn("ufsymm:eq"))
441 : : {
442 [ - - ]: 0 : Trace("ufsymm:eq") << "UFSYMM here we can conclude that "
443 : 0 : << matchingTerm << " is one of {";
444 : 0 : for (vector<TNode>::const_iterator i = matchingTermEquals.begin();
445 [ - - ]: 0 : i != matchingTermEquals.end();
446 : 0 : ++i)
447 : : {
448 [ - - ]: 0 : Trace("ufsymm:eq") << " " << *i;
449 : : }
450 [ - - ]: 0 : Trace("ufsymm:eq") << " }" << endl;
451 : : }
452 : 2661 : d_termEqsOnly[matchingTerm].insert(matchingTermEquals.begin(),
453 : : matchingTermEquals.end());
454 : : }
455 [ + - ]: 417232 : Trace("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the "
456 : 208616 : << k << "-kinded Node" << endl;
457 : 208616 : sort(kids.begin(), kids.end());
458 : 417232 : return result = nodeManager()->mkNode(k, kids);
459 : 208616 : }
460 : :
461 : 22306 : case Kind::EQUAL:
462 : 22306 : if (n[0].isVar() || n[1].isVar())
463 : : {
464 : 15351 : d_termEqs[n[0]].insert(n[1]);
465 : 15351 : d_termEqs[n[1]].insert(n[0]);
466 [ + + ]: 15351 : if (level == 0)
467 : : {
468 : 1374 : d_termEqsOnly[n[0]].insert(n[1]);
469 : 1374 : d_termEqsOnly[n[1]].insert(n[0]);
470 : 1374 : Trace("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl;
471 : : }
472 : : }
473 : : CVC5_FALLTHROUGH;
474 : : case Kind::XOR:
475 : : // commutative binary operator handling
476 : 22306 : return n[1] < n[0] ? nodeManager()->mkNode(k, n[1], n[0]) : Node(n);
477 : :
478 : 17849 : default:
479 : : // Normally T-rewriting is enough; only special cases (like
480 : : // Boolean-layer stuff) has to go above.
481 : 17849 : return n;
482 : : }
483 : : }
484 : :
485 : 91866 : void SymmetryBreaker::assertFormula(TNode phi)
486 : : {
487 : 91866 : rerunAssertionsIfNecessary();
488 [ + - ]: 91866 : if (!d_rerunningAssertions)
489 : : {
490 : 91866 : d_assertionsToRerun.push_back(phi);
491 : : }
492 : : // use d_phi, put into d_permutations
493 [ + - ]: 91866 : Trace("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl;
494 : 91866 : d_phi.push_back(phi);
495 [ + + ]: 91866 : if (phi.getKind() == Kind::OR)
496 : : {
497 : 88358 : Template t(nodeManager());
498 : 88358 : Node::iterator i = phi.begin();
499 : 88358 : t.match(*i++);
500 [ + + ]: 146263 : while (i != phi.end())
501 : : {
502 [ + + ]: 120604 : if (!t.match(*i++))
503 : : {
504 : 62699 : break;
505 : : }
506 : : }
507 : 88358 : unordered_map<TNode, set<TNode>>& ps = t.partitions();
508 [ + + ]: 129779 : for (auto& kv : ps)
509 : : {
510 [ + - ]: 41421 : Trace("ufsymm") << "UFSYMM partition*: " << kv.first;
511 : 41421 : set<TNode>& p = kv.second;
512 [ + + ]: 99235 : for (set<TNode>::iterator j = p.begin(); j != p.end(); ++j)
513 : : {
514 [ + - ]: 57814 : Trace("ufsymm") << " " << *j;
515 : : }
516 [ + - ]: 41421 : Trace("ufsymm") << endl;
517 : 41421 : p.insert(kv.first);
518 : 41421 : Permutations::iterator pi = d_permutations.find(p);
519 [ + + ]: 41421 : if (pi == d_permutations.end())
520 : : {
521 : 37805 : d_permutations.insert(p);
522 : : }
523 : : }
524 : 88358 : }
525 [ + + ]: 91866 : if (!d_template.match(phi))
526 : : {
527 : : // we hit a bad match, extract the partitions and reset the template
528 : 77788 : unordered_map<TNode, set<TNode>>& ps = d_template.partitions();
529 [ + - ]: 155576 : Trace("ufsymm") << "UFSYMM hit a bad match---have " << ps.size()
530 : 77788 : << " partitions:" << endl;
531 : 77788 : for (unordered_map<TNode, set<TNode>>::iterator i = ps.begin();
532 [ + + ]: 104319 : i != ps.end();
533 : 26531 : ++i)
534 : : {
535 [ + - ]: 26531 : Trace("ufsymm") << "UFSYMM partition: " << (*i).first;
536 : 26531 : set<TNode>& p = (*i).second;
537 [ - + ]: 26531 : if (TraceIsOn("ufsymm"))
538 : : {
539 [ - - ]: 0 : for (set<TNode>::iterator j = p.begin(); j != p.end(); ++j)
540 : : {
541 [ - - ]: 0 : Trace("ufsymm") << " " << *j;
542 : : }
543 : : }
544 [ + - ]: 26531 : Trace("ufsymm") << endl;
545 : 26531 : p.insert((*i).first);
546 : 26531 : d_permutations.insert(p);
547 : : }
548 : 77788 : d_template.reset();
549 : 77788 : bool good CVC5_UNUSED = d_template.match(phi);
550 [ - + ][ - + ]: 77788 : Assert(good);
[ - - ]
551 : : }
552 : 91866 : }
553 : :
554 : 32687 : void SymmetryBreaker::clear()
555 : : {
556 : 32687 : d_phi.clear();
557 : 32687 : d_phiSet.clear();
558 : 32687 : d_permutations.clear();
559 : 32687 : d_terms.clear();
560 : 32687 : d_template.reset();
561 : 32687 : d_normalizationCache.clear();
562 : 32687 : d_termEqs.clear();
563 : 32687 : d_termEqsOnly.clear();
564 : 32687 : }
565 : :
566 : 285 : void SymmetryBreaker::apply(std::vector<Node>& newClauses)
567 : : {
568 : 285 : rerunAssertionsIfNecessary();
569 : 285 : guessPermutations();
570 [ + - ]: 570 : Trace("ufsymm")
571 : 0 : << "UFSYMM =====================================================" << endl
572 : 285 : << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;
573 [ + + ]: 285 : if (!d_permutations.empty())
574 : : {
575 : : {
576 : 115 : TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer);
577 : : // normalize d_phi
578 : :
579 [ + + ]: 90555 : for (vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i)
580 : : {
581 : 90440 : Node n = *i;
582 : 90440 : *i = norm(n);
583 : 90440 : d_phiSet.insert(*i);
584 [ + - ]: 180880 : Trace("ufsymm:norm") << "UFSYMM init-norm-rewrite " << n << endl
585 : 90440 : << "UFSYMM to " << *i << endl;
586 : 90440 : }
587 : 115 : }
588 : :
589 [ + + ]: 62536 : for (const Permutation& p : d_permutations)
590 : : {
591 : 62421 : ++(d_stats.d_permutationSetsConsidered);
592 [ + - ]: 62421 : Trace("ufsymm") << "UFSYMM looking at permutation: " << p << endl;
593 : 62421 : size_t n = p.size() - 1;
594 [ + + ]: 62421 : if (invariantByPermutations(p))
595 : : {
596 : 231 : ++(d_stats.d_permutationSetsInvariant);
597 : 231 : selectTerms(p);
598 : 231 : set<Node> cts;
599 [ + + ][ + + ]: 291 : while (!d_terms.empty() && cts.size() <= n)
[ + + ]
600 : : {
601 [ + - ]: 120 : Trace("ufsymm") << "UFSYMM ==== top of loop, d_terms.size() == "
602 : 60 : << d_terms.size() << " , cts.size() == " << cts.size()
603 : 60 : << " , n == " << n << endl;
604 : 60 : Terms::iterator ti = selectMostPromisingTerm(d_terms);
605 : 60 : Node t = *ti;
606 [ + - ]: 60 : Trace("ufsymm") << "UFSYMM promising term is " << t << endl;
607 : 60 : d_terms.erase(ti);
608 : 60 : insertUsedIn(t, p, cts);
609 [ - + ]: 60 : if (TraceIsOn("ufsymm"))
610 : : {
611 [ - - ]: 0 : if (cts.empty())
612 : : {
613 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM cts is empty" << endl;
614 : : }
615 : : else
616 : : {
617 [ - - ]: 0 : for (set<Node>::iterator ctsi = cts.begin(); ctsi != cts.end();
618 : 0 : ++ctsi)
619 : : {
620 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM cts: " << *ctsi << endl;
621 : : }
622 : : }
623 : : }
624 : 60 : TNode c;
625 [ + - ]: 120 : Trace("ufsymm") << "UFSYMM looking for c \\in " << p << " \\ cts"
626 : 60 : << endl;
627 : 60 : set<TNode>::const_iterator i;
628 [ + + ]: 204 : for (i = p.begin(); i != p.end(); ++i)
629 : : {
630 [ + + ]: 184 : if (cts.find(*i) == cts.end())
631 : : {
632 [ + + ]: 100 : if (c.isNull())
633 : : {
634 : 60 : c = *i;
635 [ + - ]: 60 : Trace("ufsymm") << "UFSYMM found first: " << c << endl;
636 : : }
637 : : else
638 : : {
639 [ + - ]: 40 : Trace("ufsymm") << "UFSYMM found second: " << *i << endl;
640 : 40 : break;
641 : : }
642 : : }
643 : : }
644 [ - + ]: 60 : if (c.isNull())
645 : : {
646 [ - - ]: 0 : Trace("ufsymm")
647 : 0 : << "UFSYMM can't find a c, restart outer loop" << endl;
648 : 0 : break;
649 : : }
650 [ + - ]: 60 : Trace("ufsymm") << "UFSYMM inserting into cts: " << c << endl;
651 : 60 : cts.insert(c);
652 : : // This tests cts != p: if "i == p.end()", we got all the way
653 : : // through p without seeing two elements not in cts (on the
654 : : // second one, we break from the above loop). We know we
655 : : // found at least one (and subsequently added it to cts). So
656 : : // now cts == p.
657 [ + - ]: 60 : Trace("ufsymm") << "UFSYMM p == " << p << endl;
658 [ + + ][ - + ]: 60 : if (i != p.end() || p.size() != cts.size())
[ + + ]
659 : : {
660 [ + - ]: 40 : Trace("ufsymm") << "UFSYMM cts != p" << endl;
661 : 40 : NodeManager* nm = nodeManager();
662 : 40 : NodeBuilder disj(nm, Kind::OR);
663 [ + + ]: 120 : for (const Node& nn : cts)
664 : : {
665 [ + - ]: 80 : if (t != nn)
666 : : {
667 : 80 : disj << nm->mkNode(Kind::EQUAL, t, nn);
668 : : }
669 : : }
670 : 40 : Node d;
671 [ + + ]: 40 : if (disj.getNumChildren() > 1)
672 : : {
673 : 24 : d = disj;
674 : 24 : ++(d_stats.d_clauses);
675 : : }
676 : : else
677 : : {
678 : 16 : d = disj[0];
679 : 16 : disj.clear();
680 : 16 : ++(d_stats.d_units);
681 : : }
682 [ - + ]: 40 : if (TraceIsOn("ufsymm"))
683 : : {
684 [ - - ]: 0 : Trace("ufsymm")
685 : 0 : << "UFSYMM symmetry-breaking clause: " << d << endl;
686 : : }
687 : : else
688 : : {
689 [ + - ]: 80 : Trace("ufsymm:clauses")
690 : 40 : << "UFSYMM symmetry-breaking clause: " << d << endl;
691 : : }
692 : 40 : newClauses.push_back(d);
693 : 40 : }
694 : : else
695 : : {
696 [ + - ]: 20 : Trace("ufsymm") << "UFSYMM cts == p" << endl;
697 : : }
698 [ + - ]: 120 : Trace("ufsymm") << "UFSYMM ==== end of loop, d_terms.size() == "
699 : 60 : << d_terms.size() << " , cts.size() == " << cts.size()
700 : 60 : << " , n == " << n << endl;
701 [ + - ][ + - ]: 60 : }
702 : 231 : }
703 : : }
704 : : }
705 : :
706 : 285 : clear();
707 : 285 : }
708 : :
709 : 285 : void SymmetryBreaker::guessPermutations()
710 : : {
711 : : // use d_phi, put into d_permutations
712 [ + - ]: 285 : Trace("ufsymm") << "UFSYMM guessPermutations()" << endl;
713 : 285 : }
714 : :
715 : 62421 : bool SymmetryBreaker::invariantByPermutations(const Permutation& p)
716 : : {
717 : 62421 : TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer);
718 : :
719 : : // use d_phi
720 [ + - ]: 62421 : Trace("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl;
721 : :
722 [ - + ][ - + ]: 62421 : Assert(p.size() > 1);
[ - - ]
723 : :
724 : : // check that the types match
725 : 62421 : Permutation::iterator permIt = p.begin();
726 : 62421 : TypeNode type = (*permIt++).getType();
727 : : do
728 : : {
729 [ - + ]: 82235 : if (type != (*permIt++).getType())
730 : : {
731 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM types don't match, aborting.." << endl;
732 : 0 : return false;
733 : : }
734 [ + + ]: 82235 : } while (permIt != p.end());
735 : :
736 : : // check P_swap
737 : 62421 : vector<Node> subs;
738 : 62421 : vector<Node> repls;
739 : 62421 : Permutation::iterator i = p.begin();
740 : 62421 : TNode p0 = *i++;
741 : 62421 : TNode p1 = *i;
742 : 62421 : subs.push_back(p0);
743 : 62421 : subs.push_back(p1);
744 : 62421 : repls.push_back(p1);
745 : 62421 : repls.push_back(p0);
746 [ + + ]: 29274191 : for (const Node& nn : d_phi)
747 : : {
748 : : Node s =
749 : 29273948 : nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
750 : 29273948 : Node n = norm(s);
751 [ + + ][ + + ]: 29273948 : if (nn != n && d_phiSet.find(n) == d_phiSet.end())
[ + + ][ + + ]
[ - - ]
752 : : {
753 [ + - ]: 124356 : Trace("ufsymm")
754 : 0 : << "UFSYMM P_swap is NOT an inv perm op for " << p << endl
755 : 0 : << "UFSYMM because this node: " << nn << endl
756 : 0 : << "UFSYMM rewrite-norms to : " << n << endl
757 : 62178 : << "UFSYMM which is not in our set of normalized assertions" << endl;
758 : 62178 : return false;
759 : : }
760 [ - + ]: 29211770 : else if (TraceIsOn("ufsymm:p"))
761 : : {
762 [ - - ]: 0 : if (nn == s)
763 : : {
764 [ - - ]: 0 : Trace("ufsymm:p") << "UFSYMM P_swap passes trivially: " << nn << endl;
765 : : }
766 : : else
767 : : {
768 [ - - ]: 0 : Trace("ufsymm:p") << "UFSYMM P_swap passes: " << nn << endl
769 : 0 : << "UFSYMM rewrites: " << s << endl
770 : 0 : << "UFSYMM norms: " << n << endl;
771 : : }
772 : : }
773 [ + + ][ + + ]: 29336126 : }
774 [ + - ]: 243 : Trace("ufsymm") << "UFSYMM P_swap is an inv perm op for " << p << endl;
775 : :
776 : : // check P_circ, unless size == 2 in which case P_circ == P_swap
777 [ + + ]: 243 : if (p.size() > 2)
778 : : {
779 : 36 : subs.clear();
780 : 36 : repls.clear();
781 : 36 : bool first = true;
782 [ + + ]: 262 : for (TNode nn : p)
783 : : {
784 : 226 : subs.push_back(nn);
785 [ + + ]: 226 : if (!first)
786 : : {
787 : 190 : repls.push_back(nn);
788 : : }
789 : : else
790 : : {
791 : 36 : first = false;
792 : : }
793 : 226 : }
794 : 36 : repls.push_back(*p.begin());
795 [ - + ][ - + ]: 36 : Assert(subs.size() == repls.size());
[ - - ]
796 [ + + ]: 2654 : for (const Node& nn : d_phi)
797 : : {
798 : : Node s =
799 : 2630 : nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
800 : 2630 : Node n = norm(s);
801 [ + + ][ + + ]: 2630 : if (nn != n && d_phiSet.find(n) == d_phiSet.end())
[ + + ][ + + ]
[ - - ]
802 : : {
803 [ + - ]: 24 : Trace("ufsymm")
804 : 0 : << "UFSYMM P_circ is NOT an inv perm op for " << p << endl
805 : 0 : << "UFSYMM because this node: " << nn << endl
806 : 0 : << "UFSYMM rewrite-norms to : " << n << endl
807 : 0 : << "UFSYMM which is not in our set of normalized assertions"
808 : 12 : << endl;
809 : 12 : return false;
810 : : }
811 [ - + ]: 2618 : else if (TraceIsOn("ufsymm:p"))
812 : : {
813 [ - - ]: 0 : if (nn == s)
814 : : {
815 [ - - ]: 0 : Trace("ufsymm:p") << "UFSYMM P_circ passes trivially: " << nn << endl;
816 : : }
817 : : else
818 : : {
819 [ - - ]: 0 : Trace("ufsymm:p") << "UFSYMM P_circ passes: " << nn << endl
820 : 0 : << "UFSYMM rewrites: " << s << endl
821 : 0 : << "UFSYMM norms: " << n << endl;
822 : : }
823 : : }
824 [ + + ][ + + ]: 2642 : }
825 [ + - ]: 24 : Trace("ufsymm") << "UFSYMM P_circ is an inv perm op for " << p << endl;
826 : : }
827 : : else
828 : : {
829 [ + - ]: 414 : Trace("ufsymm") << "UFSYMM no need to check P_circ, since P_circ == P_swap "
830 : 0 : "for perm sets of size 2"
831 : 207 : << endl;
832 : : }
833 : :
834 : 231 : return true;
835 : 62421 : }
836 : :
837 : : // debug-assertion-only function
838 : : template <class T1, class T2>
839 : 1704 : static bool isSubset(const T1& s, const T2& t)
840 : : {
841 [ + + ]: 1704 : if (s.size() > t.size())
842 : : {
843 : : // Trace("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t "
844 : : // << "because size(s) > size(t)" << endl;
845 : 1120 : return false;
846 : : }
847 [ + + ]: 2100 : for (typename T1::const_iterator si = s.begin(); si != s.end(); ++si)
848 : : {
849 [ - + ]: 1516 : if (t.find(*si) == t.end())
850 : : {
851 : : // Trace("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t "
852 : : // << "because s element \"" << *si << "\" not in t" <<
853 : : // endl;
854 : 0 : return false;
855 : : }
856 : : }
857 : :
858 : : // At this point, didn't find any elements from s not in t, so
859 : : // conclude that s \subseteq t
860 : 584 : return true;
861 : : }
862 : :
863 : 231 : void SymmetryBreaker::selectTerms(const Permutation& p)
864 : : {
865 : 231 : TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer);
866 : :
867 : : // use d_phi, put into d_terms
868 [ + - ]: 231 : Trace("ufsymm") << "UFSYMM selectTerms(): " << p << endl;
869 : 231 : d_terms.clear();
870 : 231 : set<Node> terms;
871 [ + + ]: 761 : for (Permutation::iterator i = p.begin(); i != p.end(); ++i)
872 : : {
873 : 530 : const TermEq& teq = d_termEqs[*i];
874 [ + + ]: 4934 : for (TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j)
875 : : {
876 [ + - ]: 4404 : Trace("ufsymm") << "selectTerms: insert in terms " << *j << std::endl;
877 : : }
878 : 530 : terms.insert(teq.begin(), teq.end());
879 : : }
880 [ + + ]: 2257 : for (set<Node>::iterator i = terms.begin(); i != terms.end(); ++i)
881 : : {
882 [ + + ]: 2026 : if (d_termEqsOnly.find(*i) != d_termEqsOnly.end())
883 : : {
884 : 1704 : const TermEq& teq = d_termEqsOnly[*i];
885 [ + + ]: 1704 : if (isSubset(teq, p))
886 : : {
887 [ + - ]: 584 : Trace("ufsymm") << "selectTerms: teq = {";
888 [ + + ]: 2100 : for (TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j)
889 : : {
890 [ + - ]: 1516 : Trace("ufsymm") << " " << *j << std::endl;
891 : : }
892 [ + - ]: 584 : Trace("ufsymm") << " } is subset of p " << p << std::endl;
893 : 584 : d_terms.insert(d_terms.end(), *i);
894 : : }
895 : : else
896 : : {
897 [ - + ]: 1120 : if (TraceIsOn("ufsymm"))
898 : : {
899 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM selectTerms() threw away candidate: " << *i
900 : 0 : << endl;
901 [ - - ]: 0 : Trace("ufsymm:eq") << "UFSYMM selectTerms() #teq == " << teq.size()
902 : 0 : << " #p == " << p.size() << endl;
903 : 0 : TermEq::iterator j;
904 [ - - ]: 0 : for (j = teq.begin(); j != teq.end(); ++j)
905 : : {
906 [ - - ]: 0 : Trace("ufsymm:eq") << "UFSYMM -- teq " << *j << " in "
907 : 0 : << p << " ?" << endl;
908 [ - - ]: 0 : if (p.find(*j) == p.end())
909 : : {
910 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM -- because its teq " << *j
911 : 0 : << " isn't in " << p << endl;
912 : 0 : break;
913 : : }
914 : : else
915 : : {
916 [ - - ]: 0 : Trace("ufsymm:eq") << "UFSYMM -- yep" << endl;
917 : : }
918 : : }
919 : 0 : Assert(j != teq.end())
920 : 0 : << "failed to find a difference between p and teq ?!";
921 : : }
922 : : }
923 : : }
924 : : else
925 : : {
926 [ + - ]: 644 : Trace("ufsymm") << "selectTerms: don't have data for " << *i
927 : 322 : << " so can't conclude anything" << endl;
928 : : }
929 : : }
930 [ - + ]: 231 : if (TraceIsOn("ufsymm"))
931 : : {
932 [ - - ]: 0 : for (list<Term>::iterator i = d_terms.begin(); i != d_terms.end(); ++i)
933 : : {
934 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM selectTerms() returning: " << *i << endl;
935 : : }
936 : : }
937 : 231 : }
938 : :
939 : 27723 : SymmetryBreaker::Statistics::Statistics(StatisticsRegistry& sr,
940 : 27723 : const std::string& name)
941 : 27723 : : d_clauses(sr.registerInt(name + "clauses")),
942 : 27723 : d_units(sr.registerInt(name + "units")),
943 : : d_permutationSetsConsidered(
944 : 27723 : sr.registerInt(name + "permutationSetsConsidered")),
945 : : d_permutationSetsInvariant(
946 : 27723 : sr.registerInt(name + "permutationSetsInvariant")),
947 : : d_invariantByPermutationsTimer(
948 : 27723 : sr.registerTimer(name + "timers::invariantByPermutations")),
949 : 27723 : d_selectTermsTimer(sr.registerTimer(name + "timers::selectTerms")),
950 : : d_initNormalizationTimer(
951 : 27723 : sr.registerTimer(name + "timers::initNormalization"))
952 : : {
953 : 27723 : }
954 : :
955 : 60 : SymmetryBreaker::Terms::iterator SymmetryBreaker::selectMostPromisingTerm(
956 : : Terms& terms)
957 : : {
958 : : // use d_phi
959 [ + - ]: 60 : Trace("ufsymm") << "UFSYMM selectMostPromisingTerm()" << endl;
960 : 60 : return terms.begin();
961 : : }
962 : :
963 : 92 : void SymmetryBreaker::insertUsedIn(Term term,
964 : : const Permutation& p,
965 : : set<Node>& cts)
966 : : {
967 : : // insert terms from p used in term into cts
968 : : // Trace("ufsymm") << "UFSYMM usedIn(): " << term << " , " << p << endl;
969 [ + + ]: 92 : if (p.find(term) != p.end())
970 : : {
971 : 32 : cts.insert(term);
972 : : }
973 : : else
974 : : {
975 [ + + ]: 92 : for (TNode::iterator i = term.begin(); i != term.end(); ++i)
976 : : {
977 : 32 : insertUsedIn(*i, p, cts);
978 : : }
979 : : }
980 : 92 : }
981 : :
982 : : } // namespace uf
983 : : } // namespace theory
984 : :
985 : 0 : std::ostream& operator<<(std::ostream& out,
986 : : const theory::uf::SymmetryBreaker::Permutation& p)
987 : : {
988 : 0 : out << "{";
989 : 0 : set<TNode>::const_iterator i = p.begin();
990 [ - - ]: 0 : while (i != p.end())
991 : : {
992 : 0 : out << *i;
993 [ - - ]: 0 : if (++i != p.end())
994 : : {
995 : 0 : out << ",";
996 : : }
997 : : }
998 : 0 : out << "}";
999 : 0 : return out;
1000 : : }
1001 : :
1002 : : } // namespace cvc5::internal
|
