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 : 100298 : SymmetryBreaker::Template::Template(NodeManager* nm)
55 : 100298 : : d_template(), d_assertions(nm), d_sets(), d_reps()
56 : : {
57 : 100298 : }
58 : :
59 : 184583 : TNode SymmetryBreaker::Template::find(TNode n) {
60 : 184583 : unordered_map<TNode, TNode>::iterator i = d_reps.find(n);
61 [ + + ]: 184583 : if(i == d_reps.end()) {
62 : 141712 : return n;
63 : : } else {
64 : 85742 : return d_reps[n] = find((*i).second);
65 : : }
66 : : }
67 : :
68 : 235944 : bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) {
69 [ + - ]: 471888 : IndentedScope scope(Trace("ufsymm:match"));
70 : :
71 [ + - ]: 471888 : Trace("ufsymm:match") << "UFSYMM matching " << t << endl
72 : 235944 : << "UFSYMM to " << n << endl;
73 : :
74 [ + + ][ + + ]: 235944 : if(t.getKind() != n.getKind() || t.getNumChildren() != n.getNumChildren()) {
[ + + ]
75 [ + - ]: 74647 : Trace("ufsymm:match") << "UFSYMM BAD MATCH on kind, #children" << endl;
76 : 74647 : return false;
77 : : }
78 : :
79 [ + + ]: 161297 : if(t.getNumChildren() == 0) {
80 [ + + ]: 70863 : if (!t.isVar())
81 : : {
82 [ + - ]: 7 : Trace("ufsymm:match") << "UFSYMM non-variables, failing match" << endl;
83 : 7 : return false;
84 : : }
85 : 70856 : t = find(t);
86 : 70856 : n = find(n);
87 [ + - ]: 70856 : Trace("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl;
88 [ + - ]: 70856 : Trace("ufsymm:match") << "UFSYMM sets: " << t << " =>";
89 [ + + ]: 70856 : if(d_sets.find(t) != d_sets.end()) {
90 [ + + ]: 134869 : for(set<TNode>::iterator i = d_sets[t].begin(); i != d_sets[t].end(); ++i) {
91 [ + - ]: 103352 : Trace("ufsymm:match") << " " << *i;
92 : : }
93 : : }
94 [ + - ]: 70856 : Trace("ufsymm:match") << endl;
95 [ + + ]: 70856 : if(t != n) {
96 [ + - ]: 53075 : Trace("ufsymm:match") << "UFSYMM sets: " << n << " =>";
97 [ + + ]: 53075 : if(d_sets.find(n) != d_sets.end()) {
98 [ + + ]: 217 : for(set<TNode>::iterator i = d_sets[n].begin(); i != d_sets[n].end(); ++i) {
99 [ + - ]: 133 : Trace("ufsymm:match") << " " << *i;
100 : : }
101 : : }
102 [ + - ]: 53075 : Trace("ufsymm:match") << endl;
103 : :
104 [ + + ]: 53075 : if(d_sets.find(t) == d_sets.end()) {
105 [ + - ]: 39339 : Trace("ufsymm:match") << "UFSYMM inserting " << t << " in with " << n << endl;
106 : 39339 : d_reps[t] = n;
107 : 39339 : d_sets[n].insert(t);
108 : : } else {
109 [ + + ]: 13736 : if(d_sets.find(n) != d_sets.end()) {
110 [ + - ]: 33 : Trace("ufsymm:match") << "UFSYMM merging " << n << " and " << t << " in with " << n << endl;
111 : 33 : d_sets[n].insert(d_sets[t].begin(), d_sets[t].end());
112 : 33 : d_sets[n].insert(t);
113 : 33 : d_reps[t] = n;
114 : 33 : d_sets.erase(t);
115 : : } else {
116 [ + - ]: 13703 : Trace("ufsymm:match") << "UFSYMM inserting " << n << " in with " << t << endl;
117 : 13703 : d_sets[t].insert(n);
118 : 13703 : d_reps[n] = t;
119 : : }
120 : : }
121 : : }
122 : 70856 : return true;
123 : : }
124 : :
125 [ + + ]: 90434 : if(t.getMetaKind() == kind::metakind::PARAMETERIZED) {
126 [ + + ]: 14231 : if(t.getOperator() != n.getOperator()) {
127 : 137 : Trace("ufsymm:match") << "UFSYMM BAD MATCH on operators: " << t.getOperator() << " != " << n.getOperator() << endl;
128 : 137 : return false;
129 : : }
130 : : }
131 : 90297 : TNode::iterator ti = t.begin();
132 : 90297 : TNode::iterator ni = n.begin();
133 [ + + ]: 195191 : while(ti != t.end()) {
134 [ + + ]: 135038 : if(*ti != *ni) { // nothing to do if equal
135 [ + + ]: 118471 : if(!matchRecursive(*ti, *ni)) {
136 [ + - ]: 30144 : Trace("ufsymm:match") << "UFSYMM BAD MATCH, withdrawing.." << endl;
137 : 30144 : return false;
138 : : }
139 : : }
140 : 104894 : ++ti;
141 : 104894 : ++ni;
142 : : }
143 : :
144 : 60153 : return true;
145 : 235944 : }
146 : :
147 : 208936 : bool SymmetryBreaker::Template::match(TNode n) {
148 : : // try to "match" n and d_template
149 [ + + ]: 208936 : if(d_template.isNull()) {
150 [ + - ]: 91463 : Trace("ufsymm") << "UFSYMM setting template " << n << endl;
151 : 91463 : d_template = n;
152 : 91463 : return true;
153 : : } else {
154 : 117473 : return matchRecursive(d_template, n);
155 : : }
156 : : }
157 : :
158 : 99758 : void SymmetryBreaker::Template::reset() {
159 : 99758 : d_template = Node::null();
160 : 99758 : d_sets.clear();
161 : 99758 : d_reps.clear();
162 : 99758 : }
163 : :
164 : 49982 : SymmetryBreaker::SymmetryBreaker(Env& env, std::string name)
165 : : : EnvObj(env),
166 : 99964 : ContextNotifyObj(userContext()),
167 : 49982 : d_assertionsToRerun(userContext()),
168 : 49982 : d_rerunningAssertions(false),
169 : 49982 : d_phi(),
170 : 49982 : d_phiSet(),
171 : 49982 : d_permutations(),
172 : 49982 : d_terms(),
173 : 49982 : d_template(nodeManager()),
174 : 49982 : d_normalizationCache(),
175 : 49982 : d_termEqs(),
176 : 49982 : d_termEqsOnly(),
177 : 49982 : d_name(name),
178 : 99964 : d_stats(statisticsRegistry(), d_name + "theory::uf::symmetry_breaker::")
179 : : {
180 : 49982 : }
181 : :
182 : : class SBGuard {
183 : : bool& d_ref;
184 : : bool d_old;
185 : : public:
186 : 0 : SBGuard(bool& b) : d_ref(b), d_old(b) {}
187 [ - - ]: 0 : ~SBGuard() { Trace("uf") << "reset to " << d_old << std::endl; d_ref = d_old; }
188 : : };/* class SBGuard */
189 : :
190 : 54051 : void SymmetryBreaker::rerunAssertionsIfNecessary() {
191 [ + - ][ + + ]: 54051 : if(d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty()) {
[ + - ][ + - ]
192 : 54051 : return;
193 : : }
194 : :
195 : 0 : SBGuard g(d_rerunningAssertions);
196 : 0 : d_rerunningAssertions = true;
197 : :
198 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM: rerunning assertions..." << std::endl;
199 : 0 : for(CDList<Node>::const_iterator i = d_assertionsToRerun.begin();
200 [ - - ]: 0 : i != d_assertionsToRerun.end();
201 : 0 : ++i) {
202 : 0 : assertFormula(*i);
203 : : }
204 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM: DONE rerunning assertions..." << std::endl;
205 : 0 : }
206 : :
207 : 18007320 : Node SymmetryBreaker::norm(TNode phi) {
208 : 18007320 : Node n = rewrite(phi);
209 : 36014640 : return normInternal(n, 0);
210 : 18007320 : }
211 : :
212 : 18024845 : Node SymmetryBreaker::normInternal(TNode n, size_t level) {
213 : 18024845 : Node& result = d_normalizationCache[n];
214 [ + + ]: 18024845 : if(!result.isNull()) {
215 : 17874836 : return result;
216 : : }
217 : :
218 [ - + ][ + + ]: 150009 : switch(Kind k = n.getKind()) {
[ - + ]
219 : 0 : case Kind::DISTINCT:
220 : : {
221 : : // commutative N-ary operator handling
222 : 0 : vector<TNode> kids(n.begin(), n.end());
223 : 0 : sort(kids.begin(), kids.end());
224 : 0 : return result = nodeManager()->mkNode(k, kids);
225 : 0 : }
226 : :
227 : 540 : case Kind::AND:
228 : : {
229 : : // commutative+associative N-ary operator handling
230 : 540 : vector<Node> kids;
231 : 540 : kids.reserve(n.getNumChildren());
232 : 540 : queue<TNode> work;
233 : 540 : work.push(n);
234 [ + - ]: 540 : Trace("ufsymm:norm") << "UFSYMM processing " << n << endl;
235 : : do
236 : : {
237 : 540 : TNode m = work.front();
238 : 540 : work.pop();
239 [ + + ]: 1620 : for (TNode::iterator i = m.begin(); i != m.end(); ++i)
240 : : {
241 [ - + ]: 1080 : if ((*i).getKind() == k)
242 : : {
243 : 0 : work.push(*i);
244 : : }
245 : : else
246 : : {
247 [ + + ]: 1080 : if ((*i).getKind() == Kind::OR)
248 : : {
249 : 1 : kids.push_back(normInternal(*i, level));
250 : : }
251 [ + + ]: 1079 : else if ((*i).getKind() == Kind::EQUAL)
252 : : {
253 : 1071 : kids.push_back(normInternal(*i, level));
254 : 1071 : if ((*i)[0].isVar() || (*i)[1].isVar())
255 : : {
256 : 1071 : d_termEqs[(*i)[0]].insert((*i)[1]);
257 : 1071 : d_termEqs[(*i)[1]].insert((*i)[0]);
258 [ - + ]: 1071 : if (level == 0)
259 : : {
260 : 0 : d_termEqsOnly[(*i)[0]].insert((*i)[1]);
261 : 0 : d_termEqsOnly[(*i)[1]].insert((*i)[0]);
262 [ - - ]: 0 : Trace("ufsymm:eq")
263 : 0 : << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl;
264 : : }
265 : : }
266 : : }
267 : : else
268 : : {
269 : 8 : kids.push_back(*i);
270 : : }
271 : : }
272 : : }
273 [ - + ]: 540 : } while (!work.empty());
274 [ + - ]: 1080 : Trace("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the "
275 : 540 : << k << "-kinded Node" << endl;
276 : 540 : sort(kids.begin(), kids.end());
277 : 1080 : return result = nodeManager()->mkNode(k, kids);
278 : 540 : }
279 : :
280 : 111969 : case Kind::OR:
281 : : {
282 : : // commutative+associative N-ary operator handling
283 : 111969 : vector<Node> kids;
284 : 111969 : kids.reserve(n.getNumChildren());
285 : 111969 : queue<TNode> work;
286 : 111969 : work.push(n);
287 [ + - ]: 111969 : Trace("ufsymm:norm") << "UFSYMM processing " << n << endl;
288 : 111969 : TNode matchingTerm = TNode::null();
289 : 111969 : vector<TNode> matchingTermEquals;
290 : 111969 : bool first = true, matchedVar = false;
291 : : do
292 : : {
293 : 111969 : TNode m = work.front();
294 : 111969 : work.pop();
295 [ + + ]: 423689 : for (TNode::iterator i = m.begin(); i != m.end(); ++i)
296 : : {
297 [ - + ]: 311720 : if ((*i).getKind() == k)
298 : : {
299 : 0 : work.push(*i);
300 : : }
301 : : else
302 : : {
303 [ + + ]: 311720 : if ((*i).getKind() == Kind::AND)
304 : : {
305 : 945 : first = false;
306 : 945 : matchingTerm = TNode::null();
307 : 945 : kids.push_back(normInternal(*i, level + 1));
308 : : }
309 [ + + ]: 310775 : else if ((*i).getKind() == Kind::EQUAL)
310 : : {
311 : 15508 : kids.push_back(normInternal(*i, level + 1));
312 : 15508 : if ((*i)[0].isVar() || (*i)[1].isVar())
313 : : {
314 : 15380 : d_termEqs[(*i)[0]].insert((*i)[1]);
315 : 15380 : d_termEqs[(*i)[1]].insert((*i)[0]);
316 [ + - ]: 15380 : if (level == 0)
317 : : {
318 [ + + ]: 15380 : if (first)
319 : : {
320 : 3257 : matchingTerm = *i;
321 : : }
322 [ + + ]: 12123 : else if (!matchingTerm.isNull())
323 : : {
324 [ + + ]: 11951 : if (matchedVar)
325 : : {
326 [ + + ]: 8708 : if (matchingTerm == (*i)[0])
327 : : {
328 : 2588 : matchingTermEquals.push_back((*i)[1]);
329 : : }
330 [ + + ]: 6120 : else if (matchingTerm == (*i)[1])
331 : : {
332 : 6115 : matchingTermEquals.push_back((*i)[0]);
333 : : }
334 : : else
335 : : {
336 : 5 : matchingTerm = TNode::null();
337 : : }
338 : : }
339 [ + + ]: 3243 : else if ((*i)[0] == matchingTerm[0])
340 : : {
341 : 859 : matchingTermEquals.push_back(matchingTerm[1]);
342 : 859 : matchingTermEquals.push_back((*i)[1]);
343 : 859 : matchingTerm = matchingTerm[0];
344 : 859 : matchedVar = true;
345 : : }
346 [ - + ]: 2384 : else if ((*i)[1] == matchingTerm[0])
347 : : {
348 : 0 : matchingTermEquals.push_back(matchingTerm[1]);
349 : 0 : matchingTermEquals.push_back((*i)[0]);
350 : 0 : matchingTerm = matchingTerm[0];
351 : 0 : matchedVar = true;
352 : : }
353 [ + + ]: 2384 : else if ((*i)[0] == matchingTerm[1])
354 : : {
355 : 5 : matchingTermEquals.push_back(matchingTerm[0]);
356 : 5 : matchingTermEquals.push_back((*i)[1]);
357 : 5 : matchingTerm = matchingTerm[1];
358 : 5 : matchedVar = true;
359 : : }
360 [ + + ]: 2379 : else if ((*i)[1] == matchingTerm[1])
361 : : {
362 : 2301 : matchingTermEquals.push_back(matchingTerm[0]);
363 : 2301 : matchingTermEquals.push_back((*i)[0]);
364 : 2301 : matchingTerm = matchingTerm[1];
365 : 2301 : matchedVar = true;
366 : : }
367 : : else
368 : : {
369 : 78 : matchingTerm = TNode::null();
370 : : }
371 : : }
372 : : }
373 : : }
374 : : else
375 : : {
376 : 128 : matchingTerm = TNode::null();
377 : : }
378 : 15508 : first = false;
379 : : }
380 : : else
381 : : {
382 : 295267 : first = false;
383 : 295267 : matchingTerm = TNode::null();
384 : 295267 : kids.push_back(*i);
385 : : }
386 : : }
387 : : }
388 [ - + ]: 111969 : } while (!work.empty());
389 [ + + ]: 111969 : if(!matchingTerm.isNull()) {
390 [ - + ]: 3156 : if(TraceIsOn("ufsymm:eq")) {
391 [ - - ]: 0 : Trace("ufsymm:eq") << "UFSYMM here we can conclude that " << matchingTerm << " is one of {";
392 [ - - ]: 0 : for(vector<TNode>::const_iterator i = matchingTermEquals.begin(); i != matchingTermEquals.end(); ++i) {
393 [ - - ]: 0 : Trace("ufsymm:eq") << " " << *i;
394 : : }
395 [ - - ]: 0 : Trace("ufsymm:eq") << " }" << endl;
396 : : }
397 : 3156 : d_termEqsOnly[matchingTerm].insert(matchingTermEquals.begin(), matchingTermEquals.end());
398 : : }
399 [ + - ]: 111969 : Trace("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl;
400 : 111969 : sort(kids.begin(), kids.end());
401 : 223938 : return result = nodeManager()->mkNode(k, kids);
402 : 111969 : }
403 : :
404 : 26806 : case Kind::EQUAL:
405 : 26806 : if (n[0].isVar() || n[1].isVar())
406 : : {
407 : 18151 : d_termEqs[n[0]].insert(n[1]);
408 : 18151 : d_termEqs[n[1]].insert(n[0]);
409 [ + + ]: 18151 : if (level == 0)
410 : : {
411 : 1700 : d_termEqsOnly[n[0]].insert(n[1]);
412 : 1700 : d_termEqsOnly[n[1]].insert(n[0]);
413 : 1700 : Trace("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl;
414 : : }
415 : : }
416 : : CVC5_FALLTHROUGH;
417 : : case Kind::XOR:
418 : : // commutative binary operator handling
419 : 26806 : return n[1] < n[0] ? nodeManager()->mkNode(k, n[1], n[0]) : Node(n);
420 : :
421 : 10694 : default:
422 : : // Normally T-rewriting is enough; only special cases (like
423 : : // Boolean-layer stuff) has to go above.
424 : 10694 : return n;
425 : : }
426 : : }
427 : :
428 : 53741 : void SymmetryBreaker::assertFormula(TNode phi) {
429 : 53741 : rerunAssertionsIfNecessary();
430 [ + - ]: 53741 : if(!d_rerunningAssertions) {
431 : 53741 : d_assertionsToRerun.push_back(phi);
432 : : }
433 : : // use d_phi, put into d_permutations
434 [ + - ]: 53741 : Trace("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl;
435 : 53741 : d_phi.push_back(phi);
436 [ + + ]: 53741 : if (phi.getKind() == Kind::OR)
437 : : {
438 : 50316 : Template t(nodeManager());
439 : 50316 : Node::iterator i = phi.begin();
440 : 50316 : t.match(*i++);
441 [ + + ]: 80404 : while(i != phi.end()) {
442 [ + + ]: 63954 : if(!t.match(*i++)) {
443 : 33866 : break;
444 : : }
445 : : }
446 : 50316 : unordered_map<TNode, set<TNode>>& ps = t.partitions();
447 [ + + ]: 72944 : for (auto& kv : ps)
448 : : {
449 [ + - ]: 22628 : Trace("ufsymm") << "UFSYMM partition*: " << kv.first;
450 : 22628 : set<TNode>& p = kv.second;
451 : 22628 : for(set<TNode>::iterator j = p.begin();
452 [ + + ]: 52619 : j != p.end();
453 : 29991 : ++j) {
454 [ + - ]: 29991 : Trace("ufsymm") << " " << *j;
455 : : }
456 [ + - ]: 22628 : Trace("ufsymm") << endl;
457 : 22628 : p.insert(kv.first);
458 : 22628 : Permutations::iterator pi = d_permutations.find(p);
459 [ + + ]: 22628 : if(pi == d_permutations.end()) {
460 : 19868 : d_permutations.insert(p);
461 : : }
462 : : }
463 : 50316 : }
464 [ + + ]: 53741 : if(!d_template.match(phi)) {
465 : : // we hit a bad match, extract the partitions and reset the template
466 : 40925 : unordered_map<TNode, set<TNode>>& ps = d_template.partitions();
467 [ + - ]: 40925 : Trace("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl;
468 : 40925 : for (unordered_map<TNode, set<TNode>>::iterator i = ps.begin();
469 [ + + ]: 57544 : i != ps.end();
470 : 16619 : ++i)
471 : : {
472 [ + - ]: 16619 : Trace("ufsymm") << "UFSYMM partition: " << (*i).first;
473 : 16619 : set<TNode>& p = (*i).second;
474 [ - + ]: 16619 : if(TraceIsOn("ufsymm")) {
475 : 0 : for(set<TNode>::iterator j = p.begin();
476 [ - - ]: 0 : j != p.end();
477 : 0 : ++j) {
478 [ - - ]: 0 : Trace("ufsymm") << " " << *j;
479 : : }
480 : : }
481 [ + - ]: 16619 : Trace("ufsymm") << endl;
482 : 16619 : p.insert((*i).first);
483 : 16619 : d_permutations.insert(p);
484 : : }
485 : 40925 : d_template.reset();
486 : 40925 : bool good CVC5_UNUSED = d_template.match(phi);
487 [ - + ][ - + ]: 40925 : Assert(good);
[ - - ]
488 : : }
489 : 53741 : }
490 : :
491 : 58833 : void SymmetryBreaker::clear() {
492 : 58833 : d_phi.clear();
493 : 58833 : d_phiSet.clear();
494 : 58833 : d_permutations.clear();
495 : 58833 : d_terms.clear();
496 : 58833 : d_template.reset();
497 : 58833 : d_normalizationCache.clear();
498 : 58833 : d_termEqs.clear();
499 : 58833 : d_termEqsOnly.clear();
500 : 58833 : }
501 : :
502 : 310 : void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
503 : 310 : rerunAssertionsIfNecessary();
504 : 310 : guessPermutations();
505 [ + - ]: 620 : Trace("ufsymm") << "UFSYMM =====================================================" << endl
506 : 310 : << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;
507 [ + + ]: 310 : if(!d_permutations.empty()) {
508 : 123 : { TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer);
509 : : // normalize d_phi
510 : :
511 [ + + ]: 52217 : for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
512 : 52094 : Node n = *i;
513 : 52094 : *i = norm(n);
514 : 52094 : d_phiSet.insert(*i);
515 [ + - ]: 104188 : Trace("ufsymm:norm") << "UFSYMM init-norm-rewrite " << n << endl
516 : 52094 : << "UFSYMM to " << *i << endl;
517 : 52094 : }
518 : 123 : }
519 : :
520 [ + + ]: 34711 : for (const Permutation& p : d_permutations)
521 : : {
522 : 34588 : ++(d_stats.d_permutationSetsConsidered);
523 [ + - ]: 34588 : Trace("ufsymm") << "UFSYMM looking at permutation: " << p << endl;
524 : 34588 : size_t n = p.size() - 1;
525 [ + + ]: 34588 : if(invariantByPermutations(p)) {
526 : 282 : ++(d_stats.d_permutationSetsInvariant);
527 : 282 : selectTerms(p);
528 : 282 : set<Node> cts;
529 [ + + ][ + + ]: 357 : while(!d_terms.empty() && cts.size() <= n) {
[ + + ]
530 [ + - ]: 75 : Trace("ufsymm") << "UFSYMM ==== top of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl;
531 : 75 : Terms::iterator ti = selectMostPromisingTerm(d_terms);
532 : 75 : Node t = *ti;
533 [ + - ]: 75 : Trace("ufsymm") << "UFSYMM promising term is " << t << endl;
534 : 75 : d_terms.erase(ti);
535 : 75 : insertUsedIn(t, p, cts);
536 [ - + ]: 75 : if(TraceIsOn("ufsymm")) {
537 [ - - ]: 0 : if(cts.empty()) {
538 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM cts is empty" << endl;
539 : : } else {
540 [ - - ]: 0 : for(set<Node>::iterator ctsi = cts.begin(); ctsi != cts.end(); ++ctsi) {
541 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM cts: " << *ctsi << endl;
542 : : }
543 : : }
544 : : }
545 : 75 : TNode c;
546 [ + - ]: 75 : Trace("ufsymm") << "UFSYMM looking for c \\in " << p << " \\ cts" << endl;
547 : 75 : set<TNode>::const_iterator i;
548 [ + + ]: 255 : for(i = p.begin(); i != p.end(); ++i) {
549 [ + + ]: 230 : if(cts.find(*i) == cts.end()) {
550 [ + + ]: 125 : if(c.isNull()) {
551 : 75 : c = *i;
552 [ + - ]: 75 : Trace("ufsymm") << "UFSYMM found first: " << c << endl;
553 : : } else {
554 [ + - ]: 50 : Trace("ufsymm") << "UFSYMM found second: " << *i << endl;
555 : 50 : break;
556 : : }
557 : : }
558 : : }
559 [ - + ]: 75 : if(c.isNull()) {
560 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM can't find a c, restart outer loop" << endl;
561 : 0 : break;
562 : : }
563 [ + - ]: 75 : Trace("ufsymm") << "UFSYMM inserting into cts: " << c << endl;
564 : 75 : cts.insert(c);
565 : : // This tests cts != p: if "i == p.end()", we got all the way
566 : : // through p without seeing two elements not in cts (on the
567 : : // second one, we break from the above loop). We know we
568 : : // found at least one (and subsequently added it to cts). So
569 : : // now cts == p.
570 [ + - ]: 75 : Trace("ufsymm") << "UFSYMM p == " << p << endl;
571 [ + + ][ - + ]: 75 : if(i != p.end() || p.size() != cts.size()) {
[ + + ]
572 [ + - ]: 50 : Trace("ufsymm") << "UFSYMM cts != p" << endl;
573 : 50 : NodeManager* nm = nodeManager();
574 : 50 : NodeBuilder disj(nm, Kind::OR);
575 [ + + ]: 150 : for (const Node& nn : cts)
576 : : {
577 [ + - ]: 100 : if (t != nn)
578 : : {
579 : 100 : disj << nm->mkNode(Kind::EQUAL, t, nn);
580 : : }
581 : : }
582 : 50 : Node d;
583 [ + + ]: 50 : if(disj.getNumChildren() > 1) {
584 : 30 : d = disj;
585 : 30 : ++(d_stats.d_clauses);
586 : : } else {
587 : 20 : d = disj[0];
588 : 20 : disj.clear();
589 : 20 : ++(d_stats.d_units);
590 : : }
591 [ - + ]: 50 : if(TraceIsOn("ufsymm")) {
592 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl;
593 : : } else {
594 [ + - ]: 50 : Trace("ufsymm:clauses") << "UFSYMM symmetry-breaking clause: " << d << endl;
595 : : }
596 : 50 : newClauses.push_back(d);
597 : 50 : } else {
598 [ + - ]: 25 : Trace("ufsymm") << "UFSYMM cts == p" << endl;
599 : : }
600 [ + - ]: 75 : Trace("ufsymm") << "UFSYMM ==== end of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl;
601 [ + - ][ + - ]: 75 : }
602 : 282 : }
603 : : }
604 : : }
605 : :
606 : 310 : clear();
607 : 310 : }
608 : :
609 : 310 : void SymmetryBreaker::guessPermutations() {
610 : : // use d_phi, put into d_permutations
611 [ + - ]: 310 : Trace("ufsymm") << "UFSYMM guessPermutations()" << endl;
612 : 310 : }
613 : :
614 : 34588 : bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
615 : 34588 : TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer);
616 : :
617 : : // use d_phi
618 [ + - ]: 34588 : Trace("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl;
619 : :
620 [ - + ][ - + ]: 34588 : Assert(p.size() > 1);
[ - - ]
621 : :
622 : : // check that the types match
623 : 34588 : Permutation::iterator permIt = p.begin();
624 : 34588 : TypeNode type = (*permIt++).getType();
625 : : do {
626 [ - + ]: 44895 : if(type != (*permIt++).getType()) {
627 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM types don't match, aborting.." << endl;
628 : 0 : return false;
629 : : }
630 [ + + ]: 44895 : } while(permIt != p.end());
631 : :
632 : : // check P_swap
633 : 34588 : vector<Node> subs;
634 : 34588 : vector<Node> repls;
635 : 34588 : Permutation::iterator i = p.begin();
636 : 34588 : TNode p0 = *i++;
637 : 34588 : TNode p1 = *i;
638 : 34588 : subs.push_back(p0);
639 : 34588 : subs.push_back(p1);
640 : 34588 : repls.push_back(p1);
641 : 34588 : repls.push_back(p0);
642 [ + + ]: 17952835 : for (const Node& nn : d_phi)
643 : : {
644 : : Node s =
645 : 17952545 : nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
646 : 17952545 : Node n = norm(s);
647 [ + + ][ + + ]: 17952545 : if (nn != n && d_phiSet.find(n) == d_phiSet.end())
[ + + ][ + + ]
[ - - ]
648 : : {
649 [ + - ]: 68596 : Trace("ufsymm")
650 : 0 : << "UFSYMM P_swap is NOT an inv perm op for " << p << endl
651 : 0 : << "UFSYMM because this node: " << nn << endl
652 : 0 : << "UFSYMM rewrite-norms to : " << n << endl
653 : 34298 : << "UFSYMM which is not in our set of normalized assertions" << endl;
654 : 34298 : return false;
655 : : }
656 [ - + ]: 17918247 : else if (TraceIsOn("ufsymm:p"))
657 : : {
658 [ - - ]: 0 : if (nn == s)
659 : : {
660 [ - - ]: 0 : Trace("ufsymm:p") << "UFSYMM P_swap passes trivially: " << nn << endl;
661 : : }
662 : : else
663 : : {
664 [ - - ]: 0 : Trace("ufsymm:p") << "UFSYMM P_swap passes: " << nn << endl
665 : 0 : << "UFSYMM rewrites: " << s << endl
666 : 0 : << "UFSYMM norms: " << n << endl;
667 : : }
668 : : }
669 [ + + ][ + + ]: 17986843 : }
670 [ + - ]: 290 : Trace("ufsymm") << "UFSYMM P_swap is an inv perm op for " << p << endl;
671 : :
672 : : // check P_circ, unless size == 2 in which case P_circ == P_swap
673 [ + + ]: 290 : if(p.size() > 2) {
674 : 32 : subs.clear();
675 : 32 : repls.clear();
676 : 32 : bool first = true;
677 [ + + ]: 179 : for (TNode nn : p)
678 : : {
679 : 147 : subs.push_back(nn);
680 [ + + ]: 147 : if(!first) {
681 : 115 : repls.push_back(nn);
682 : : } else {
683 : 32 : first = false;
684 : : }
685 : 147 : }
686 : 32 : repls.push_back(*p.begin());
687 [ - + ][ - + ]: 32 : Assert(subs.size() == repls.size());
[ - - ]
688 [ + + ]: 2705 : for (const Node& nn : d_phi)
689 : : {
690 : : Node s =
691 : 2681 : nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
692 : 2681 : Node n = norm(s);
693 [ + + ][ + + ]: 2681 : if (nn != n && d_phiSet.find(n) == d_phiSet.end())
[ + + ][ + + ]
[ - - ]
694 : : {
695 [ + - ]: 16 : Trace("ufsymm")
696 : 0 : << "UFSYMM P_circ is NOT an inv perm op for " << p << endl
697 : 0 : << "UFSYMM because this node: " << nn << endl
698 : 0 : << "UFSYMM rewrite-norms to : " << n << endl
699 : 0 : << "UFSYMM which is not in our set of normalized assertions"
700 : 8 : << endl;
701 : 8 : return false;
702 : : }
703 [ - + ]: 2673 : else if (TraceIsOn("ufsymm:p"))
704 : : {
705 [ - - ]: 0 : if (nn == s)
706 : : {
707 [ - - ]: 0 : Trace("ufsymm:p") << "UFSYMM P_circ passes trivially: " << nn << endl;
708 : : }
709 : : else
710 : : {
711 [ - - ]: 0 : Trace("ufsymm:p") << "UFSYMM P_circ passes: " << nn << endl
712 : 0 : << "UFSYMM rewrites: " << s << endl
713 : 0 : << "UFSYMM norms: " << n << endl;
714 : : }
715 : : }
716 [ + + ][ + + ]: 2689 : }
717 [ + - ]: 24 : Trace("ufsymm") << "UFSYMM P_circ is an inv perm op for " << p << endl;
718 : : } else {
719 [ + - ]: 258 : Trace("ufsymm") << "UFSYMM no need to check P_circ, since P_circ == P_swap for perm sets of size 2" << endl;
720 : : }
721 : :
722 : 282 : return true;
723 : 34588 : }
724 : :
725 : : // debug-assertion-only function
726 : : template <class T1, class T2>
727 : 2130 : static bool isSubset(const T1& s, const T2& t) {
728 [ + + ]: 2130 : if(s.size() > t.size()) {
729 : : //Trace("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t "
730 : : // << "because size(s) > size(t)" << endl;
731 : 1400 : return false;
732 : : }
733 [ + + ]: 2625 : for(typename T1::const_iterator si = s.begin(); si != s.end(); ++si) {
734 [ - + ]: 1895 : if(t.find(*si) == t.end()) {
735 : : //Trace("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t "
736 : : // << "because s element \"" << *si << "\" not in t" << endl;
737 : 0 : return false;
738 : : }
739 : : }
740 : :
741 : : // At this point, didn't find any elements from s not in t, so
742 : : // conclude that s \subseteq t
743 : 730 : return true;
744 : : }
745 : :
746 : 282 : void SymmetryBreaker::selectTerms(const Permutation& p) {
747 : 282 : TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer);
748 : :
749 : : // use d_phi, put into d_terms
750 [ + - ]: 282 : Trace("ufsymm") << "UFSYMM selectTerms(): " << p << endl;
751 : 282 : d_terms.clear();
752 : 282 : set<Node> terms;
753 [ + + ]: 885 : for(Permutation::iterator i = p.begin(); i != p.end(); ++i) {
754 : 603 : const TermEq& teq = d_termEqs[*i];
755 [ + + ]: 6104 : for(TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j) {
756 [ + - ]: 5501 : Trace("ufsymm") << "selectTerms: insert in terms " << *j << std::endl;
757 : : }
758 : 603 : terms.insert(teq.begin(), teq.end());
759 : : }
760 [ + + ]: 2813 : for(set<Node>::iterator i = terms.begin(); i != terms.end(); ++i) {
761 [ + + ]: 2531 : if(d_termEqsOnly.find(*i) != d_termEqsOnly.end()) {
762 : 2130 : const TermEq& teq = d_termEqsOnly[*i];
763 [ + + ]: 2130 : if(isSubset(teq, p)) {
764 [ + - ]: 730 : Trace("ufsymm") << "selectTerms: teq = {";
765 [ + + ]: 2625 : for(TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j) {
766 [ + - ]: 1895 : Trace("ufsymm") << " " << *j << std::endl;
767 : : }
768 [ + - ]: 730 : Trace("ufsymm") << " } is subset of p " << p << std::endl;
769 : 730 : d_terms.insert(d_terms.end(), *i);
770 : : } else {
771 [ - + ]: 1400 : if(TraceIsOn("ufsymm")) {
772 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM selectTerms() threw away candidate: " << *i << endl;
773 [ - - ]: 0 : Trace("ufsymm:eq") << "UFSYMM selectTerms() #teq == " << teq.size() << " #p == " << p.size() << endl;
774 : 0 : TermEq::iterator j;
775 [ - - ]: 0 : for(j = teq.begin(); j != teq.end(); ++j) {
776 [ - - ]: 0 : Trace("ufsymm:eq") << "UFSYMM -- teq " << *j << " in " << p << " ?" << endl;
777 [ - - ]: 0 : if(p.find(*j) == p.end()) {
778 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM -- because its teq " << *j
779 : 0 : << " isn't in " << p << endl;
780 : 0 : break;
781 : : } else {
782 [ - - ]: 0 : Trace("ufsymm:eq") << "UFSYMM -- yep" << endl;
783 : : }
784 : : }
785 : 0 : Assert(j != teq.end())
786 : 0 : << "failed to find a difference between p and teq ?!";
787 : : }
788 : : }
789 : : } else {
790 [ + - ]: 401 : Trace("ufsymm") << "selectTerms: don't have data for " << *i << " so can't conclude anything" << endl;
791 : : }
792 : : }
793 [ - + ]: 282 : if(TraceIsOn("ufsymm")) {
794 [ - - ]: 0 : for(list<Term>::iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
795 [ - - ]: 0 : Trace("ufsymm") << "UFSYMM selectTerms() returning: " << *i << endl;
796 : : }
797 : : }
798 : 282 : }
799 : :
800 : 49982 : SymmetryBreaker::Statistics::Statistics(StatisticsRegistry& sr,
801 : 49982 : const std::string& name)
802 : 49982 : : d_clauses(sr.registerInt(name + "clauses")),
803 : 49982 : d_units(sr.registerInt(name + "units")),
804 : : d_permutationSetsConsidered(
805 : 49982 : sr.registerInt(name + "permutationSetsConsidered")),
806 : : d_permutationSetsInvariant(
807 : 49982 : sr.registerInt(name + "permutationSetsInvariant")),
808 : : d_invariantByPermutationsTimer(
809 : 49982 : sr.registerTimer(name + "timers::invariantByPermutations")),
810 : 49982 : d_selectTermsTimer(sr.registerTimer(name + "timers::selectTerms")),
811 : : d_initNormalizationTimer(
812 : 49982 : sr.registerTimer(name + "timers::initNormalization"))
813 : : {
814 : 49982 : }
815 : :
816 : : SymmetryBreaker::Terms::iterator
817 : 75 : SymmetryBreaker::selectMostPromisingTerm(Terms& terms) {
818 : : // use d_phi
819 [ + - ]: 75 : Trace("ufsymm") << "UFSYMM selectMostPromisingTerm()" << endl;
820 : 75 : return terms.begin();
821 : : }
822 : :
823 : 115 : void SymmetryBreaker::insertUsedIn(Term term, const Permutation& p, set<Node>& cts) {
824 : : // insert terms from p used in term into cts
825 : : //Trace("ufsymm") << "UFSYMM usedIn(): " << term << " , " << p << endl;
826 [ + + ]: 115 : if (p.find(term) != p.end()) {
827 : 40 : cts.insert(term);
828 : : } else {
829 [ + + ]: 115 : for(TNode::iterator i = term.begin(); i != term.end(); ++i) {
830 : 40 : insertUsedIn(*i, p, cts);
831 : : }
832 : : }
833 : 115 : }
834 : :
835 : : } // namespace uf
836 : : } // namespace theory
837 : :
838 : 0 : std::ostream& operator<<(std::ostream& out, const theory::uf::SymmetryBreaker::Permutation& p) {
839 : 0 : out << "{";
840 : 0 : set<TNode>::const_iterator i = p.begin();
841 [ - - ]: 0 : while(i != p.end()) {
842 : 0 : out << *i;
843 [ - - ]: 0 : if(++i != p.end()) {
844 : 0 : out << ",";
845 : : }
846 : : }
847 : 0 : out << "}";
848 : 0 : return out;
849 : : }
850 : :
851 : : } // namespace cvc5::internal
|
