1 /********************* */
2 /*! \file symmetry_breaker.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Morgan Deters, Liana Hadarean, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Implementation of algorithm suggested by Deharbe, Fontaine,
13 ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011
14 **
15 ** Implementation of algorithm suggested by Deharbe, Fontaine, Merz,
16 ** and Paleo, "Exploiting symmetry in SMT problems," CADE 2011.
17 **
18 ** From the paper:
19 **
20 ** <pre>
21 ** \f$ P := guess\_permutations(\phi) \f$
22 ** foreach \f$ {c_0, ..., c_n} \in P \f$ do
23 ** if \f$ invariant\_by\_permutations(\phi, {c_0, ..., c_n}) \f$ then
24 ** T := \f$ select\_terms(\phi, {c_0, ..., c_n}) \f$
25 ** cts := \f$ \emptyset \f$
26 ** while T != \f$ \empty \wedge |cts| <= n \f$ do
27 ** \f$ t := select\_most\_promising\_term(T, \phi) \f$
28 ** \f$ T := T \setminus {t} \f$
29 ** cts := cts \f$ \cup used\_in(t, {c_0, ..., c_n}) \f$
30 ** let \f$ c \in {c_0, ..., c_n} \setminus cts \f$
31 ** cts := cts \f$ \cup {c} \f$
32 ** if cts != \f$ {c_0, ..., c_n} \f$ then
33 ** \f$ \phi := \phi \wedge ( \vee_{c_i \in cts} t = c_i ) \f$
34 ** end
35 ** end
36 ** end
37 ** end
38 ** return \f$ \phi \f$
39 ** </pre>
40 **/
41
42 #include "theory/uf/symmetry_breaker.h"
43 #include "theory/rewriter.h"
44 #include "util/hash.h"
45
46 #include <iterator>
47 #include <queue>
48
49 using namespace std;
50
51 namespace CVC4 {
52 namespace theory {
53 namespace uf {
54
55 using namespace ::CVC4::context;
56
Template()57 SymmetryBreaker::Template::Template() :
58 d_template(),
59 d_sets(),
60 d_reps() {
61 }
62
find(TNode n)63 TNode SymmetryBreaker::Template::find(TNode n) {
64 unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
65 if(i == d_reps.end()) {
66 return n;
67 } else {
68 return d_reps[n] = find((*i).second);
69 }
70 }
71
matchRecursive(TNode t,TNode n)72 bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) {
73 IndentedScope scope(Debug("ufsymm:match"));
74
75 Debug("ufsymm:match") << "UFSYMM matching " << t << endl
76 << "UFSYMM to " << n << endl;
77
78 if(t.getKind() != n.getKind() || t.getNumChildren() != n.getNumChildren()) {
79 Debug("ufsymm:match") << "UFSYMM BAD MATCH on kind, #children" << endl;
80 return false;
81 }
82
83 if(t.getNumChildren() == 0) {
84 if(t.isConst()) {
85 Assert(n.isConst());
86 Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl;
87 return false;
88 }
89 Assert(t.isVar() &&
90 n.isVar());
91 t = find(t);
92 n = find(n);
93 Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl;
94 Debug("ufsymm:match") << "UFSYMM sets: " << t << " =>";
95 if(d_sets.find(t) != d_sets.end()) {
96 for(set<TNode>::iterator i = d_sets[t].begin(); i != d_sets[t].end(); ++i) {
97 Debug("ufsymm:match") << " " << *i;
98 }
99 }
100 Debug("ufsymm:match") << endl;
101 if(t != n) {
102 Debug("ufsymm:match") << "UFSYMM sets: " << n << " =>";
103 if(d_sets.find(n) != d_sets.end()) {
104 for(set<TNode>::iterator i = d_sets[n].begin(); i != d_sets[n].end(); ++i) {
105 Debug("ufsymm:match") << " " << *i;
106 }
107 }
108 Debug("ufsymm:match") << endl;
109
110 if(d_sets.find(t) == d_sets.end()) {
111 Debug("ufsymm:match") << "UFSYMM inserting " << t << " in with " << n << endl;
112 d_reps[t] = n;
113 d_sets[n].insert(t);
114 } else {
115 if(d_sets.find(n) != d_sets.end()) {
116 Debug("ufsymm:match") << "UFSYMM merging " << n << " and " << t << " in with " << n << endl;
117 d_sets[n].insert(d_sets[t].begin(), d_sets[t].end());
118 d_sets[n].insert(t);
119 d_reps[t] = n;
120 d_sets.erase(t);
121 } else {
122 Debug("ufsymm:match") << "UFSYMM inserting " << n << " in with " << t << endl;
123 d_sets[t].insert(n);
124 d_reps[n] = t;
125 }
126 }
127 }
128 return true;
129 }
130
131 if(t.getMetaKind() == kind::metakind::PARAMETERIZED) {
132 if(t.getOperator() != n.getOperator()) {
133 Debug("ufsymm:match") << "UFSYMM BAD MATCH on operators: " << t.getOperator() << " != " << n.getOperator() << endl;
134 return false;
135 }
136 }
137 TNode::iterator ti = t.begin();
138 TNode::iterator ni = n.begin();
139 while(ti != t.end()) {
140 if(*ti != *ni) { // nothing to do if equal
141 if(!matchRecursive(*ti, *ni)) {
142 Debug("ufsymm:match") << "UFSYMM BAD MATCH, withdrawing.." << endl;
143 return false;
144 }
145 }
146 ++ti;
147 ++ni;
148 }
149
150 return true;
151 }
152
match(TNode n)153 bool SymmetryBreaker::Template::match(TNode n) {
154 // try to "match" n and d_template
155 if(d_template.isNull()) {
156 Debug("ufsymm") << "UFSYMM setting template " << n << endl;
157 d_template = n;
158 return true;
159 } else {
160 return matchRecursive(d_template, n);
161 }
162 }
163
reset()164 void SymmetryBreaker::Template::reset() {
165 d_template = Node::null();
166 d_sets.clear();
167 d_reps.clear();
168 }
169
SymmetryBreaker(context::Context * context,std::string name)170 SymmetryBreaker::SymmetryBreaker(context::Context* context,
171 std::string name) :
172 ContextNotifyObj(context),
173 d_assertionsToRerun(context),
174 d_rerunningAssertions(false),
175 d_phi(),
176 d_phiSet(),
177 d_permutations(),
178 d_terms(),
179 d_template(),
180 d_normalizationCache(),
181 d_termEqs(),
182 d_termEqsOnly(),
183 d_name(name),
184 d_stats(d_name)
185 {
186 }
187
188 class SBGuard {
189 bool& d_ref;
190 bool d_old;
191 public:
SBGuard(bool & b)192 SBGuard(bool& b) : d_ref(b), d_old(b) {}
~SBGuard()193 ~SBGuard() { Debug("uf") << "reset to " << d_old << std::endl; d_ref = d_old; }
194 };/* class SBGuard */
195
rerunAssertionsIfNecessary()196 void SymmetryBreaker::rerunAssertionsIfNecessary() {
197 if(d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty()) {
198 return;
199 }
200
201 SBGuard g(d_rerunningAssertions);
202 d_rerunningAssertions = true;
203
204 Debug("ufsymm") << "UFSYMM: rerunning assertions..." << std::endl;
205 for(CDList<Node>::const_iterator i = d_assertionsToRerun.begin();
206 i != d_assertionsToRerun.end();
207 ++i) {
208 assertFormula(*i);
209 }
210 Debug("ufsymm") << "UFSYMM: DONE rerunning assertions..." << std::endl;
211 }
212
norm(TNode phi)213 Node SymmetryBreaker::norm(TNode phi) {
214 Node n = Rewriter::rewrite(phi);
215 return normInternal(n, 0);
216 }
217
normInternal(TNode n,size_t level)218 Node SymmetryBreaker::normInternal(TNode n, size_t level) {
219 Node& result = d_normalizationCache[n];
220 if(!result.isNull()) {
221 return result;
222 }
223
224 switch(Kind k = n.getKind()) {
225
226 case kind::DISTINCT: {
227 // commutative N-ary operator handling
228 vector<TNode> kids(n.begin(), n.end());
229 sort(kids.begin(), kids.end());
230 return result = NodeManager::currentNM()->mkNode(k, kids);
231 }
232
233 case kind::AND: {
234 // commutative+associative N-ary operator handling
235 vector<Node> kids;
236 kids.reserve(n.getNumChildren());
237 queue<TNode> work;
238 work.push(n);
239 Debug("ufsymm:norm") << "UFSYMM processing " << n << endl;
240 do {
241 TNode m = work.front();
242 work.pop();
243 for(TNode::iterator i = m.begin(); i != m.end(); ++i) {
244 if((*i).getKind() == k) {
245 work.push(*i);
246 } else {
247 if( (*i).getKind() == kind::OR ) {
248 kids.push_back(normInternal(*i, level));
249 } else if((*i).getKind() == kind::EQUAL) {
250 kids.push_back(normInternal(*i, level));
251 if((*i)[0].isVar() ||
252 (*i)[1].isVar()) {
253 d_termEqs[(*i)[0]].insert((*i)[1]);
254 d_termEqs[(*i)[1]].insert((*i)[0]);
255 if(level == 0) {
256 d_termEqsOnly[(*i)[0]].insert((*i)[1]);
257 d_termEqsOnly[(*i)[1]].insert((*i)[0]);
258 Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl;
259 }
260 }
261 } else {
262 kids.push_back(*i);
263 }
264 }
265 }
266 } while(!work.empty());
267 Debug("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl;
268 sort(kids.begin(), kids.end());
269 return result = NodeManager::currentNM()->mkNode(k, kids);
270 }
271
272 case kind::OR: {
273 // commutative+associative N-ary operator handling
274 vector<Node> kids;
275 kids.reserve(n.getNumChildren());
276 queue<TNode> work;
277 work.push(n);
278 Debug("ufsymm:norm") << "UFSYMM processing " << n << endl;
279 TNode matchingTerm = TNode::null();
280 vector<TNode> matchingTermEquals;
281 bool first = true, matchedVar = false;
282 do {
283 TNode m = work.front();
284 work.pop();
285 for(TNode::iterator i = m.begin(); i != m.end(); ++i) {
286 if((*i).getKind() == k) {
287 work.push(*i);
288 } else {
289 if( (*i).getKind() == kind::AND ) {
290 first = false;
291 matchingTerm = TNode::null();
292 kids.push_back(normInternal(*i, level + 1));
293 } else if((*i).getKind() == kind::EQUAL) {
294 kids.push_back(normInternal(*i, level + 1));
295 if((*i)[0].isVar() ||
296 (*i)[1].isVar()) {
297 d_termEqs[(*i)[0]].insert((*i)[1]);
298 d_termEqs[(*i)[1]].insert((*i)[0]);
299 if(level == 0) {
300 if(first) {
301 matchingTerm = *i;
302 } else if(!matchingTerm.isNull()) {
303 if(matchedVar) {
304 if(matchingTerm == (*i)[0]) {
305 matchingTermEquals.push_back((*i)[1]);
306 } else if(matchingTerm == (*i)[1]) {
307 matchingTermEquals.push_back((*i)[0]);
308 } else {
309 matchingTerm = TNode::null();
310 }
311 } else if((*i)[0] == matchingTerm[0]) {
312 matchingTermEquals.push_back(matchingTerm[1]);
313 matchingTermEquals.push_back((*i)[1]);
314 matchingTerm = matchingTerm[0];
315 matchedVar = true;
316 } else if((*i)[1] == matchingTerm[0]) {
317 matchingTermEquals.push_back(matchingTerm[1]);
318 matchingTermEquals.push_back((*i)[0]);
319 matchingTerm = matchingTerm[0];
320 matchedVar = true;
321 } else if((*i)[0] == matchingTerm[1]) {
322 matchingTermEquals.push_back(matchingTerm[0]);
323 matchingTermEquals.push_back((*i)[1]);
324 matchingTerm = matchingTerm[1];
325 matchedVar = true;
326 } else if((*i)[1] == matchingTerm[1]) {
327 matchingTermEquals.push_back(matchingTerm[0]);
328 matchingTermEquals.push_back((*i)[0]);
329 matchingTerm = matchingTerm[1];
330 matchedVar = true;
331 } else {
332 matchingTerm = TNode::null();
333 }
334 }
335 }
336 } else {
337 matchingTerm = TNode::null();
338 }
339 first = false;
340 } else {
341 first = false;
342 matchingTerm = TNode::null();
343 kids.push_back(*i);
344 }
345 }
346 }
347 } while(!work.empty());
348 if(!matchingTerm.isNull()) {
349 if(Debug.isOn("ufsymm:eq")) {
350 Debug("ufsymm:eq") << "UFSYMM here we can conclude that " << matchingTerm << " is one of {";
351 for(vector<TNode>::const_iterator i = matchingTermEquals.begin(); i != matchingTermEquals.end(); ++i) {
352 Debug("ufsymm:eq") << " " << *i;
353 }
354 Debug("ufsymm:eq") << " }" << endl;
355 }
356 d_termEqsOnly[matchingTerm].insert(matchingTermEquals.begin(), matchingTermEquals.end());
357 }
358 Debug("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl;
359 sort(kids.begin(), kids.end());
360 return result = NodeManager::currentNM()->mkNode(k, kids);
361 }
362
363 case kind::EQUAL:
364 if(n[0].isVar() ||
365 n[1].isVar()) {
366 d_termEqs[n[0]].insert(n[1]);
367 d_termEqs[n[1]].insert(n[0]);
368 if(level == 0) {
369 d_termEqsOnly[n[0]].insert(n[1]);
370 d_termEqsOnly[n[1]].insert(n[0]);
371 Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl;
372 }
373 }
374 /* intentional fall-through! */
375 case kind::XOR:
376 // commutative binary operator handling
377 return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n);
378
379 default:
380 // Normally T-rewriting is enough; only special cases (like
381 // Boolean-layer stuff) has to go above.
382 return n;
383 }
384 }
385
assertFormula(TNode phi)386 void SymmetryBreaker::assertFormula(TNode phi) {
387 rerunAssertionsIfNecessary();
388 if(!d_rerunningAssertions) {
389 d_assertionsToRerun.push_back(phi);
390 }
391 // use d_phi, put into d_permutations
392 Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl;
393 d_phi.push_back(phi);
394 if(phi.getKind() == kind::OR) {
395 Template t;
396 Node::iterator i = phi.begin();
397 t.match(*i++);
398 while(i != phi.end()) {
399 if(!t.match(*i++)) {
400 break;
401 }
402 }
403 unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
404 for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
405 i != ps.end();
406 ++i) {
407 Debug("ufsymm") << "UFSYMM partition*: " << (*i).first;
408 set<TNode>& p = (*i).second;
409 for(set<TNode>::iterator j = p.begin();
410 j != p.end();
411 ++j) {
412 Debug("ufsymm") << " " << *j;
413 }
414 Debug("ufsymm") << endl;
415 p.insert((*i).first);
416 Permutations::iterator pi = d_permutations.find(p);
417 if(pi == d_permutations.end()) {
418 d_permutations.insert(p);
419 }
420 }
421 }
422 if(!d_template.match(phi)) {
423 // we hit a bad match, extract the partitions and reset the template
424 unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
425 Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl;
426 for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
427 i != ps.end();
428 ++i) {
429 Debug("ufsymm") << "UFSYMM partition: " << (*i).first;
430 set<TNode>& p = (*i).second;
431 if(Debug.isOn("ufsymm")) {
432 for(set<TNode>::iterator j = p.begin();
433 j != p.end();
434 ++j) {
435 Debug("ufsymm") << " " << *j;
436 }
437 }
438 Debug("ufsymm") << endl;
439 p.insert((*i).first);
440 d_permutations.insert(p);
441 }
442 d_template.reset();
443 bool good CVC4_UNUSED = d_template.match(phi);
444 Assert(good);
445 }
446 }
447
clear()448 void SymmetryBreaker::clear() {
449 d_phi.clear();
450 d_phiSet.clear();
451 d_permutations.clear();
452 d_terms.clear();
453 d_template.reset();
454 d_normalizationCache.clear();
455 d_termEqs.clear();
456 d_termEqsOnly.clear();
457 }
458
apply(std::vector<Node> & newClauses)459 void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
460 rerunAssertionsIfNecessary();
461 guessPermutations();
462 Debug("ufsymm") << "UFSYMM =====================================================" << endl
463 << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;
464 if(!d_permutations.empty()) {
465 { TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer);
466 // normalize d_phi
467
468 for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
469 Node n = *i;
470 *i = norm(n);
471 d_phiSet.insert(*i);
472 Debug("ufsymm:norm") << "UFSYMM init-norm-rewrite " << n << endl
473 << "UFSYMM to " << *i << endl;
474 }
475 }
476
477 for(Permutations::iterator i = d_permutations.begin();
478 i != d_permutations.end();
479 ++i) {
480 ++(d_stats.d_permutationSetsConsidered);
481 const Permutation& p = *i;
482 Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl;
483 size_t n = p.size() - 1;
484 if(invariantByPermutations(p)) {
485 ++(d_stats.d_permutationSetsInvariant);
486 selectTerms(p);
487 set<Node> cts;
488 while(!d_terms.empty() && cts.size() <= n) {
489 Debug("ufsymm") << "UFSYMM ==== top of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl;
490 Terms::iterator ti = selectMostPromisingTerm(d_terms);
491 Node t = *ti;
492 Debug("ufsymm") << "UFSYMM promising term is " << t << endl;
493 d_terms.erase(ti);
494 insertUsedIn(t, p, cts);
495 if(Debug.isOn("ufsymm")) {
496 if(cts.empty()) {
497 Debug("ufsymm") << "UFSYMM cts is empty" << endl;
498 } else {
499 for(set<Node>::iterator ctsi = cts.begin(); ctsi != cts.end(); ++ctsi) {
500 Debug("ufsymm") << "UFSYMM cts: " << *ctsi << endl;
501 }
502 }
503 }
504 TNode c;
505 Debug("ufsymm") << "UFSYMM looking for c \\in " << p << " \\ cts" << endl;
506 set<TNode>::const_iterator i;
507 for(i = p.begin(); i != p.end(); ++i) {
508 if(cts.find(*i) == cts.end()) {
509 if(c.isNull()) {
510 c = *i;
511 Debug("ufsymm") << "UFSYMM found first: " << c << endl;
512 } else {
513 Debug("ufsymm") << "UFSYMM found second: " << *i << endl;
514 break;
515 }
516 }
517 }
518 if(c.isNull()) {
519 Debug("ufsymm") << "UFSYMM can't find a c, restart outer loop" << endl;
520 break;
521 }
522 Debug("ufsymm") << "UFSYMM inserting into cts: " << c << endl;
523 cts.insert(c);
524 // This tests cts != p: if "i == p.end()", we got all the way
525 // through p without seeing two elements not in cts (on the
526 // second one, we break from the above loop). We know we
527 // found at least one (and subsequently added it to cts). So
528 // now cts == p.
529 Debug("ufsymm") << "UFSYMM p == " << p << endl;
530 if(i != p.end() || p.size() != cts.size()) {
531 Debug("ufsymm") << "UFSYMM cts != p" << endl;
532 NodeBuilder<> disj(kind::OR);
533 for(set<Node>::const_iterator i = cts.begin();
534 i != cts.end();
535 ++i) {
536 if(t != *i) {
537 disj << NodeManager::currentNM()->mkNode(kind::EQUAL, t, *i);
538 }
539 }
540 Node d;
541 if(disj.getNumChildren() > 1) {
542 d = disj;
543 ++(d_stats.d_clauses);
544 } else {
545 d = disj[0];
546 disj.clear();
547 ++(d_stats.d_units);
548 }
549 if(Debug.isOn("ufsymm")) {
550 Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl;
551 } else {
552 Debug("ufsymm:clauses") << "UFSYMM symmetry-breaking clause: " << d << endl;
553 }
554 newClauses.push_back(d);
555 } else {
556 Debug("ufsymm") << "UFSYMM cts == p" << endl;
557 }
558 Debug("ufsymm") << "UFSYMM ==== end of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl;
559 }
560 }
561 }
562 }
563
564 clear();
565 }
566
guessPermutations()567 void SymmetryBreaker::guessPermutations() {
568 // use d_phi, put into d_permutations
569 Debug("ufsymm") << "UFSYMM guessPermutations()" << endl;
570 }
571
invariantByPermutations(const Permutation & p)572 bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
573 TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer);
574
575 // use d_phi
576 Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl;
577
578 Assert(p.size() > 1);
579
580 // check that the types match
581 Permutation::iterator permIt = p.begin();
582 TypeNode type = (*permIt++).getType();
583 do {
584 if(type != (*permIt++).getType()) {
585 Debug("ufsymm") << "UFSYMM types don't match, aborting.." << endl;
586 return false;
587 }
588 } while(permIt != p.end());
589
590 // check P_swap
591 vector<Node> subs;
592 vector<Node> repls;
593 Permutation::iterator i = p.begin();
594 TNode p0 = *i++;
595 TNode p1 = *i;
596 subs.push_back(p0);
597 subs.push_back(p1);
598 repls.push_back(p1);
599 repls.push_back(p0);
600 for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
601 Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
602 Node n = norm(s);
603 if(*i != n && d_phiSet.find(n) == d_phiSet.end()) {
604 Debug("ufsymm") << "UFSYMM P_swap is NOT an inv perm op for " << p << endl
605 << "UFSYMM because this node: " << *i << endl
606 << "UFSYMM rewrite-norms to : " << n << endl
607 << "UFSYMM which is not in our set of normalized assertions" << endl;
608 return false;
609 } else if(Debug.isOn("ufsymm:p")) {
610 if(*i == s) {
611 Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << *i << endl;
612 } else {
613 Debug("ufsymm:p") << "UFSYMM P_swap passes: " << *i << endl
614 << "UFSYMM rewrites: " << s << endl
615 << "UFSYMM norms: " << n << endl;
616 }
617 }
618 }
619 Debug("ufsymm") << "UFSYMM P_swap is an inv perm op for " << p << endl;
620
621 // check P_circ, unless size == 2 in which case P_circ == P_swap
622 if(p.size() > 2) {
623 subs.clear();
624 repls.clear();
625 bool first = true;
626 for(Permutation::const_iterator i = p.begin(); i != p.end(); ++i) {
627 subs.push_back(*i);
628 if(!first) {
629 repls.push_back(*i);
630 } else {
631 first = false;
632 }
633 }
634 repls.push_back(*p.begin());
635 Assert(subs.size() == repls.size());
636 for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
637 Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
638 Node n = norm(s);
639 if(*i != n && d_phiSet.find(n) == d_phiSet.end()) {
640 Debug("ufsymm") << "UFSYMM P_circ is NOT an inv perm op for " << p << endl
641 << "UFSYMM because this node: " << *i << endl
642 << "UFSYMM rewrite-norms to : " << n << endl
643 << "UFSYMM which is not in our set of normalized assertions" << endl;
644 return false;
645 } else if(Debug.isOn("ufsymm:p")) {
646 if(*i == s) {
647 Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << *i << endl;
648 } else {
649 Debug("ufsymm:p") << "UFSYMM P_circ passes: " << *i << endl
650 << "UFSYMM rewrites: " << s << endl
651 << "UFSYMM norms: " << n << endl;
652 }
653 }
654 }
655 Debug("ufsymm") << "UFSYMM P_circ is an inv perm op for " << p << endl;
656 } else {
657 Debug("ufsymm") << "UFSYMM no need to check P_circ, since P_circ == P_swap for perm sets of size 2" << endl;
658 }
659
660 return true;
661 }
662
663 // debug-assertion-only function
664 template <class T1, class T2>
isSubset(const T1 & s,const T2 & t)665 static bool isSubset(const T1& s, const T2& t) {
666 if(s.size() > t.size()) {
667 //Debug("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t "
668 // << "because size(s) > size(t)" << endl;
669 return false;
670 }
671 for(typename T1::const_iterator si = s.begin(); si != s.end(); ++si) {
672 if(t.find(*si) == t.end()) {
673 //Debug("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t "
674 // << "because s element \"" << *si << "\" not in t" << endl;
675 return false;
676 }
677 }
678
679 // At this point, didn't find any elements from s not in t, so
680 // conclude that s \subseteq t
681 return true;
682 }
683
selectTerms(const Permutation & p)684 void SymmetryBreaker::selectTerms(const Permutation& p) {
685 TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer);
686
687 // use d_phi, put into d_terms
688 Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl;
689 d_terms.clear();
690 set<Node> terms;
691 for(Permutation::iterator i = p.begin(); i != p.end(); ++i) {
692 const TermEq& teq = d_termEqs[*i];
693 for(TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j) {
694 Debug("ufsymm") << "selectTerms: insert in terms " << *j << std::endl;
695 }
696 terms.insert(teq.begin(), teq.end());
697 }
698 for(set<Node>::iterator i = terms.begin(); i != terms.end(); ++i) {
699 if(d_termEqsOnly.find(*i) != d_termEqsOnly.end()) {
700 const TermEq& teq = d_termEqsOnly[*i];
701 if(isSubset(teq, p)) {
702 Debug("ufsymm") << "selectTerms: teq = {";
703 for(TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j) {
704 Debug("ufsymm") << " " << *j << std::endl;
705 }
706 Debug("ufsymm") << " } is subset of p " << p << std::endl;
707 d_terms.insert(d_terms.end(), *i);
708 } else {
709 if(Debug.isOn("ufsymm")) {
710 Debug("ufsymm") << "UFSYMM selectTerms() threw away candidate: " << *i << endl;
711 Debug("ufsymm:eq") << "UFSYMM selectTerms() #teq == " << teq.size() << " #p == " << p.size() << endl;
712 TermEq::iterator j;
713 for(j = teq.begin(); j != teq.end(); ++j) {
714 Debug("ufsymm:eq") << "UFSYMM -- teq " << *j << " in " << p << " ?" << endl;
715 if(p.find(*j) == p.end()) {
716 Debug("ufsymm") << "UFSYMM -- because its teq " << *j
717 << " isn't in " << p << endl;
718 break;
719 } else {
720 Debug("ufsymm:eq") << "UFSYMM -- yep" << endl;
721 }
722 }
723 Assert(j != teq.end(), "failed to find a difference between p and teq ?!");
724 }
725 }
726 } else {
727 Debug("ufsymm") << "selectTerms: don't have data for " << *i << " so can't conclude anything" << endl;
728 }
729 }
730 if(Debug.isOn("ufsymm")) {
731 for(list<Term>::iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
732 Debug("ufsymm") << "UFSYMM selectTerms() returning: " << *i << endl;
733 }
734 }
735 }
736
Statistics(std::string name)737 SymmetryBreaker::Statistics::Statistics(std::string name)
738 : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0)
739 , d_units(name + "theory::uf::symmetry_breaker::units", 0)
740 , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0)
741 , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0)
742 , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations")
743 , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms")
744 , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization")
745 {
746 smtStatisticsRegistry()->registerStat(&d_clauses);
747 smtStatisticsRegistry()->registerStat(&d_units);
748 smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered);
749 smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant);
750 smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer);
751 smtStatisticsRegistry()->registerStat(&d_selectTermsTimer);
752 smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer);
753 }
754
~Statistics()755 SymmetryBreaker::Statistics::~Statistics()
756 {
757 smtStatisticsRegistry()->unregisterStat(&d_clauses);
758 smtStatisticsRegistry()->unregisterStat(&d_units);
759 smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered);
760 smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant);
761 smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer);
762 smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer);
763 smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer);
764 }
765
766 SymmetryBreaker::Terms::iterator
selectMostPromisingTerm(Terms & terms)767 SymmetryBreaker::selectMostPromisingTerm(Terms& terms) {
768 // use d_phi
769 Debug("ufsymm") << "UFSYMM selectMostPromisingTerm()" << endl;
770 return terms.begin();
771 }
772
insertUsedIn(Term term,const Permutation & p,set<Node> & cts)773 void SymmetryBreaker::insertUsedIn(Term term, const Permutation& p, set<Node>& cts) {
774 // insert terms from p used in term into cts
775 //Debug("ufsymm") << "UFSYMM usedIn(): " << term << " , " << p << endl;
776 if (p.find(term) != p.end()) {
777 cts.insert(term);
778 } else {
779 for(TNode::iterator i = term.begin(); i != term.end(); ++i) {
780 insertUsedIn(*i, p, cts);
781 }
782 }
783 }
784
785 }/* CVC4::theory::uf namespace */
786 }/* CVC4::theory namespace */
787
operator <<(std::ostream & out,const theory::uf::SymmetryBreaker::Permutation & p)788 std::ostream& operator<<(std::ostream& out, const theory::uf::SymmetryBreaker::Permutation& p) {
789 out << "{";
790 set<TNode>::const_iterator i = p.begin();
791 while(i != p.end()) {
792 out << *i;
793 if(++i != p.end()) {
794 out << ",";
795 }
796 }
797 out << "}";
798 return out;
799 }
800
801 }/* CVC4 namespace */
802