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  **

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                        **
40  **/ 41 42 #include "theory/uf/symmetry_breaker.h" 43 #include "theory/rewriter.h" 44 #include "util/hash.h" 45 46 #include  47 #include  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::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::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::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::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 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 kids; 235 44  kids.reserve(n.getNumChildren()); 236 88  queue 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 kids; 274 13216  kids.reserve(n.getNumChildren()); 275 26432  queue work; 276 13216  work.push(n); 277 13216  Debug("ufsymm:norm") << "UFSYMM processing " << n << endl; 278 26432  TNode matchingTerm = TNode::null(); 279 26432  vector 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::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, TNodeHashFunction>& ps = t.partitions(); 403 8894  for (auto& kv : ps) 404  { 405 2168  Debug("ufsymm") << "UFSYMM partition*: " << kv.first; 406 2168  set& p = kv.second; 407 5226  for(set::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, TNodeHashFunction>& ps = d_template.partitions(); 423 21790  Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl; 424 23052  for(unordered_map, TNodeHashFunction>::iterator i = ps.begin(); 425 23052  i != ps.end(); 426  ++i) { 427 1262  Debug("ufsymm") << "UFSYMM partition: " << (*i).first; 428 1262  set& p = (*i).second; 429 1262  if(Debug.isOn("ufsymm")) { 430  for(set::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& 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::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 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::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::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 subs; 589 4416  vector 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  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 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::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::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& 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::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 */

 Generated by: GCOVR (Version 3.2)