GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/symmetry_breaker.cpp Lines: 414 498 83.1 %
Date: 2021-03-23 Branches: 978 2248 43.5 %

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