src/theory/uf/symmetry_breaker.cpp

   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-2020 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 SymmetryBreaker::Template::Template() :
  58   d_template(),
  59   d_sets(),
  60   d_reps() {
  61 }
  62
  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
  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() && n.isVar());
  90     t = find(t);
  91     n = find(n);
  92     Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl;
  93     Debug("ufsymm:match") << "UFSYMM sets: " << t << " =>";
  94     if(d_sets.find(t) != d_sets.end()) {
  95       for(set<TNode>::iterator i = d_sets[t].begin(); i != d_sets[t].end(); ++i) {
  96         Debug("ufsymm:match") << " " << *i;
  97       }
  98     }
  99     Debug("ufsymm:match") << endl;
 100     if(t != n) {
 101       Debug("ufsymm:match") << "UFSYMM sets: " << n << " =>";
 102       if(d_sets.find(n) != d_sets.end()) {
 103         for(set<TNode>::iterator i = d_sets[n].begin(); i != d_sets[n].end(); ++i) {
 104           Debug("ufsymm:match") << " " << *i;
 105         }
 106       }
 107       Debug("ufsymm:match") << endl;
 108
 109       if(d_sets.find(t) == d_sets.end()) {
 110         Debug("ufsymm:match") << "UFSYMM inserting " << t << " in with " << n << endl;
 111         d_reps[t] = n;
 112         d_sets[n].insert(t);
 113       } else {
 114         if(d_sets.find(n) != d_sets.end()) {
 115           Debug("ufsymm:match") << "UFSYMM merging " << n << " and " << t << " in with " << n << endl;
 116           d_sets[n].insert(d_sets[t].begin(), d_sets[t].end());
 117           d_sets[n].insert(t);
 118           d_reps[t] = n;
 119           d_sets.erase(t);
 120         } else {
 121           Debug("ufsymm:match") << "UFSYMM inserting " << n << " in with " << t << endl;
 122           d_sets[t].insert(n);
 123           d_reps[n] = t;
 124         }
 125       }
 126     }
 127     return true;
 128   }
 129
 130   if(t.getMetaKind() == kind::metakind::PARAMETERIZED) {
 131     if(t.getOperator() != n.getOperator()) {
 132       Debug("ufsymm:match") << "UFSYMM BAD MATCH on operators: " << t.getOperator() << " != " << n.getOperator() << endl;
 133       return false;
 134     }
 135   }
 136   TNode::iterator ti = t.begin();
 137   TNode::iterator ni = n.begin();
 138   while(ti != t.end()) {
 139     if(*ti != *ni) { // nothing to do if equal
 140       if(!matchRecursive(*ti, *ni)) {
 141         Debug("ufsymm:match") << "UFSYMM BAD MATCH, withdrawing.." << endl;
 142         return false;
 143       }
 144     }
 145     ++ti;
 146     ++ni;
 147   }
 148
 149   return true;
 150 }
 151
 152 bool SymmetryBreaker::Template::match(TNode n) {
 153   // try to "match" n and d_template
 154   if(d_template.isNull()) {
 155     Debug("ufsymm") << "UFSYMM setting template " << n << endl;
 156     d_template = n;
 157     return true;
 158   } else {
 159     return matchRecursive(d_template, n);
 160   }
 161 }
 162
 163 void SymmetryBreaker::Template::reset() {
 164   d_template = Node::null();
 165   d_sets.clear();
 166   d_reps.clear();
 167 }
 168
 169 SymmetryBreaker::SymmetryBreaker(context::Context* context,
 170                                  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   d_stats(d_name)
 184 {
 185 }
 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 void SymmetryBreaker::rerunAssertionsIfNecessary() {
 196   if(d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty()) {
 197     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 Node SymmetryBreaker::norm(TNode phi) {
 213   Node n = Rewriter::rewrite(phi);
 214   return normInternal(n, 0);
 215 }
 216
 217 Node SymmetryBreaker::normInternal(TNode n, size_t level) {
 218   Node& result = d_normalizationCache[n];
 219   if(!result.isNull()) {
 220     return result;
 221   }
 222
 223   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   case kind::AND: {
 233     // commutative+associative N-ary operator handling
 234     vector<Node> kids;
 235     kids.reserve(n.getNumChildren());
 236     queue<TNode> work;
 237     work.push(n);
 238     Debug("ufsymm:norm") << "UFSYMM processing " << n << endl;
 239     do {
 240       TNode m = work.front();
 241       work.pop();
 242       for(TNode::iterator i = m.begin(); i != m.end(); ++i) {
 243         if((*i).getKind() == k) {
 244           work.push(*i);
 245         } else {
 246           if( (*i).getKind() == kind::OR ) {
 247             kids.push_back(normInternal(*i, level));
 248           } else if((*i).getKind() == kind::EQUAL) {
 249             kids.push_back(normInternal(*i, level));
 250             if((*i)[0].isVar() ||
 251                (*i)[1].isVar()) {
 252               d_termEqs[(*i)[0]].insert((*i)[1]);
 253               d_termEqs[(*i)[1]].insert((*i)[0]);
 254               if(level == 0) {
 255                 d_termEqsOnly[(*i)[0]].insert((*i)[1]);
 256                 d_termEqsOnly[(*i)[1]].insert((*i)[0]);
 257                 Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl;
 258               }
 259             }
 260           } else {
 261             kids.push_back(*i);
 262           }
 263         }
 264       }
 265     } while(!work.empty());
 266     Debug("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl;
 267     sort(kids.begin(), kids.end());
 268     return result = NodeManager::currentNM()->mkNode(k, kids);
 269   }
 270
 271   case kind::OR: {
 272     // commutative+associative N-ary operator handling
 273     vector<Node> kids;
 274     kids.reserve(n.getNumChildren());
 275     queue<TNode> work;
 276     work.push(n);
 277     Debug("ufsymm:norm") << "UFSYMM processing " << n << endl;
 278     TNode matchingTerm = TNode::null();
 279     vector<TNode> matchingTermEquals;
 280     bool first = true, matchedVar = false;
 281     do {
 282       TNode m = work.front();
 283       work.pop();
 284       for(TNode::iterator i = m.begin(); i != m.end(); ++i) {
 285         if((*i).getKind() == k) {
 286           work.push(*i);
 287         } else {
 288           if( (*i).getKind() == kind::AND ) {
 289             first = false;
 290             matchingTerm = TNode::null();
 291             kids.push_back(normInternal(*i, level + 1));
 292           } else if((*i).getKind() == kind::EQUAL) {
 293             kids.push_back(normInternal(*i, level + 1));
 294             if((*i)[0].isVar() ||
 295                (*i)[1].isVar()) {
 296               d_termEqs[(*i)[0]].insert((*i)[1]);
 297               d_termEqs[(*i)[1]].insert((*i)[0]);
 298               if(level == 0) {
 299                 if(first) {
 300                   matchingTerm = *i;
 301                 } else if(!matchingTerm.isNull()) {
 302                   if(matchedVar) {
 303                     if(matchingTerm == (*i)[0]) {
 304                       matchingTermEquals.push_back((*i)[1]);
 305                     } else if(matchingTerm == (*i)[1]) {
 306                       matchingTermEquals.push_back((*i)[0]);
 307                     } else {
 308                       matchingTerm = TNode::null();
 309                     }
 310                   } else if((*i)[0] == matchingTerm[0]) {
 311                     matchingTermEquals.push_back(matchingTerm[1]);
 312                     matchingTermEquals.push_back((*i)[1]);
 313                     matchingTerm = matchingTerm[0];
 314                     matchedVar = true;
 315                   } 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                   } else if((*i)[0] == matchingTerm[1]) {
 321                     matchingTermEquals.push_back(matchingTerm[0]);
 322                     matchingTermEquals.push_back((*i)[1]);
 323                     matchingTerm = matchingTerm[1];
 324                     matchedVar = true;
 325                   } else if((*i)[1] == matchingTerm[1]) {
 326                     matchingTermEquals.push_back(matchingTerm[0]);
 327                     matchingTermEquals.push_back((*i)[0]);
 328                     matchingTerm = matchingTerm[1];
 329                     matchedVar = true;
 330                   } else {
 331                     matchingTerm = TNode::null();
 332                   }
 333                 }
 334               }
 335             } else {
 336               matchingTerm = TNode::null();
 337             }
 338             first = false;
 339           } else {
 340             first = false;
 341             matchingTerm = TNode::null();
 342             kids.push_back(*i);
 343           }
 344         }
 345       }
 346     } while(!work.empty());
 347     if(!matchingTerm.isNull()) {
 348       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       d_termEqsOnly[matchingTerm].insert(matchingTermEquals.begin(), matchingTermEquals.end());
 356     }
 357     Debug("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl;
 358     sort(kids.begin(), kids.end());
 359     return result = NodeManager::currentNM()->mkNode(k, kids);
 360   }
 361
 362   case kind::EQUAL:
 363     if(n[0].isVar() ||
 364        n[1].isVar()) {
 365       d_termEqs[n[0]].insert(n[1]);
 366       d_termEqs[n[1]].insert(n[0]);
 367       if(level == 0) {
 368         d_termEqsOnly[n[0]].insert(n[1]);
 369         d_termEqsOnly[n[1]].insert(n[0]);
 370         Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl;
 371       }
 372     }
 373     CVC4_FALLTHROUGH;
 374   case kind::XOR:
 375     // commutative binary operator handling
 376     return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n);
 377
 378   default:
 379     // Normally T-rewriting is enough; only special cases (like
 380     // Boolean-layer stuff) has to go above.
 381     return n;
 382   }
 383 }
 384
 385 void SymmetryBreaker::assertFormula(TNode phi) {
 386   rerunAssertionsIfNecessary();
 387   if(!d_rerunningAssertions) {
 388     d_assertionsToRerun.push_back(phi);
 389   }
 390   // use d_phi, put into d_permutations
 391   Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl;
 392   d_phi.push_back(phi);
 393   if(phi.getKind() == kind::OR) {
 394     Template t;
 395     Node::iterator i = phi.begin();
 396     t.match(*i++);
 397     while(i != phi.end()) {
 398       if(!t.match(*i++)) {
 399         break;
 400       }
 401     }
 402     unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
 403     for (auto& kv : ps)
 404     {
 405       Debug("ufsymm") << "UFSYMM partition*: " << kv.first;
 406       set<TNode>& p = kv.second;
 407       for(set<TNode>::iterator j = p.begin();
 408           j != p.end();
 409           ++j) {
 410         Debug("ufsymm") << " " << *j;
 411       }
 412       Debug("ufsymm") << endl;
 413       p.insert(kv.first);
 414       Permutations::iterator pi = d_permutations.find(p);
 415       if(pi == d_permutations.end()) {
 416         d_permutations.insert(p);
 417       }
 418     }
 419   }
 420   if(!d_template.match(phi)) {
 421     // we hit a bad match, extract the partitions and reset the template
 422     unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
 423     Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl;
 424     for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
 425         i != ps.end();
 426         ++i) {
 427       Debug("ufsymm") << "UFSYMM partition: " << (*i).first;
 428       set<TNode>& p = (*i).second;
 429       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       Debug("ufsymm") << endl;
 437       p.insert((*i).first);
 438       d_permutations.insert(p);
 439     }
 440     d_template.reset();
 441     bool good CVC4_UNUSED = d_template.match(phi);
 442     Assert(good);
 443   }
 444 }
 445
 446 void SymmetryBreaker::clear() {
 447   d_phi.clear();
 448   d_phiSet.clear();
 449   d_permutations.clear();
 450   d_terms.clear();
 451   d_template.reset();
 452   d_normalizationCache.clear();
 453   d_termEqs.clear();
 454   d_termEqsOnly.clear();
 455 }
 456
 457 void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
 458   rerunAssertionsIfNecessary();
 459   guessPermutations();
 460   Debug("ufsymm") << "UFSYMM =====================================================" << endl
 461                   << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;
 462   if(!d_permutations.empty()) {
 463     { TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer);
 464       // normalize d_phi
 465
 466       for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
 467         Node n = *i;
 468         *i = norm(n);
 469         d_phiSet.insert(*i);
 470         Debug("ufsymm:norm") << "UFSYMM init-norm-rewrite " << n << endl
 471                              << "UFSYMM                to " << *i << endl;
 472       }
 473     }
 474
 475     for (const Permutation& p : d_permutations)
 476     {
 477       ++(d_stats.d_permutationSetsConsidered);
 478       Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl;
 479       size_t n = p.size() - 1;
 480       if(invariantByPermutations(p)) {
 481         ++(d_stats.d_permutationSetsInvariant);
 482         selectTerms(p);
 483         set<Node> cts;
 484         while(!d_terms.empty() && cts.size() <= n) {
 485           Debug("ufsymm") << "UFSYMM ==== top of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl;
 486           Terms::iterator ti = selectMostPromisingTerm(d_terms);
 487           Node t = *ti;
 488           Debug("ufsymm") << "UFSYMM promising term is " << t << endl;
 489           d_terms.erase(ti);
 490           insertUsedIn(t, p, cts);
 491           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           TNode c;
 501           Debug("ufsymm") << "UFSYMM looking for c \\in " << p << " \\ cts" << endl;
 502           set<TNode>::const_iterator i;
 503           for(i = p.begin(); i != p.end(); ++i) {
 504             if(cts.find(*i) == cts.end()) {
 505               if(c.isNull()) {
 506                 c = *i;
 507                 Debug("ufsymm") << "UFSYMM found first: " << c << endl;
 508               } else {
 509                 Debug("ufsymm") << "UFSYMM found second: " << *i << endl;
 510                 break;
 511               }
 512             }
 513           }
 514           if(c.isNull()) {
 515             Debug("ufsymm") << "UFSYMM can't find a c, restart outer loop" << endl;
 516             break;
 517           }
 518           Debug("ufsymm") << "UFSYMM inserting into cts: " << c << endl;
 519           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           Debug("ufsymm") << "UFSYMM p == " << p << endl;
 526           if(i != p.end() || p.size() != cts.size()) {
 527             Debug("ufsymm") << "UFSYMM cts != p" << endl;
 528             NodeBuilder<> disj(kind::OR);
 529             NodeManager* nm = NodeManager::currentNM();
 530             for (const Node& nn : cts)
 531             {
 532               if (t != nn)
 533               {
 534                 disj << nm->mkNode(kind::EQUAL, t, nn);
 535               }
 536             }
 537             Node d;
 538             if(disj.getNumChildren() > 1) {
 539               d = disj;
 540               ++(d_stats.d_clauses);
 541             } else {
 542               d = disj[0];
 543               disj.clear();
 544               ++(d_stats.d_units);
 545             }
 546             if(Debug.isOn("ufsymm")) {
 547               Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl;
 548             } else {
 549               Debug("ufsymm:clauses") << "UFSYMM symmetry-breaking clause: " << d << endl;
 550             }
 551             newClauses.push_back(d);
 552           } else {
 553             Debug("ufsymm") << "UFSYMM cts == p" << endl;
 554           }
 555           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   clear();
 562 }
 563
 564 void SymmetryBreaker::guessPermutations() {
 565   // use d_phi, put into d_permutations
 566   Debug("ufsymm") << "UFSYMM guessPermutations()" << endl;
 567 }
 568
 569 bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
 570   TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer);
 571
 572   // use d_phi
 573   Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl;
 574
 575   Assert(p.size() > 1);
 576
 577   // check that the types match
 578   Permutation::iterator permIt = p.begin();
 579   TypeNode type = (*permIt++).getType();
 580   do {
 581     if(type != (*permIt++).getType()) {
 582       Debug("ufsymm") << "UFSYMM types don't match, aborting.." << endl;
 583       return false;
 584     }
 585   } while(permIt != p.end());
 586
 587   // check P_swap
 588   vector<Node> subs;
 589   vector<Node> repls;
 590   Permutation::iterator i = p.begin();
 591   TNode p0 = *i++;
 592   TNode p1 = *i;
 593   subs.push_back(p0);
 594   subs.push_back(p1);
 595   repls.push_back(p1);
 596   repls.push_back(p0);
 597   for (const Node& nn : d_phi)
 598   {
 599     Node s =
 600         nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
 601     Node n = norm(s);
 602     if (nn != n && d_phiSet.find(n) == d_phiSet.end())
 603     {
 604       Debug("ufsymm")
 605           << "UFSYMM P_swap is NOT an inv perm op for " << p << endl
 606           << "UFSYMM because this node: " << nn << endl
 607           << "UFSYMM rewrite-norms to : " << n << endl
 608           << "UFSYMM which is not in our set of normalized assertions" << endl;
 609       return false;
 610     }
 611     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   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   if(p.size() > 2) {
 629     subs.clear();
 630     repls.clear();
 631     bool first = true;
 632     for (TNode nn : p)
 633     {
 634       subs.push_back(nn);
 635       if(!first) {
 636         repls.push_back(nn);
 637       } else {
 638         first = false;
 639       }
 640     }
 641     repls.push_back(*p.begin());
 642     Assert(subs.size() == repls.size());
 643     for (const Node& nn : d_phi)
 644     {
 645       Node s =
 646           nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
 647       Node n = norm(s);
 648       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       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     Debug("ufsymm") << "UFSYMM P_circ is an inv perm op for " << p << endl;
 673   } else {
 674     Debug("ufsymm") << "UFSYMM no need to check P_circ, since P_circ == P_swap for perm sets of size 2" << endl;
 675   }
 676
 677   return true;
 678 }
 679
 680 // debug-assertion-only function
 681 template <class T1, class T2>
 682 static bool isSubset(const T1& s, const T2& t) {
 683   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     return false;
 687   }
 688   for(typename T1::const_iterator si = s.begin(); si != s.end(); ++si) {
 689     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   return true;
 699 }
 700
 701 void SymmetryBreaker::selectTerms(const Permutation& p) {
 702   TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer);
 703
 704   // use d_phi, put into d_terms
 705   Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl;
 706   d_terms.clear();
 707   set<Node> terms;
 708   for(Permutation::iterator i = p.begin(); i != p.end(); ++i) {
 709     const TermEq& teq = d_termEqs[*i];
 710     for(TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j) {
 711       Debug("ufsymm") << "selectTerms: insert in terms " << *j << std::endl;
 712     }
 713     terms.insert(teq.begin(), teq.end());
 714   }
 715   for(set<Node>::iterator i = terms.begin(); i != terms.end(); ++i) {
 716     if(d_termEqsOnly.find(*i) != d_termEqsOnly.end()) {
 717       const TermEq& teq = d_termEqsOnly[*i];
 718       if(isSubset(teq, p)) {
 719         Debug("ufsymm") << "selectTerms: teq = {";
 720         for(TermEq::const_iterator j = teq.begin(); j != teq.end(); ++j) {
 721           Debug("ufsymm") << " " << *j << std::endl;
 722         }
 723         Debug("ufsymm") << " } is subset of p " << p << std::endl;
 724         d_terms.insert(d_terms.end(), *i);
 725       } else {
 726         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       Debug("ufsymm") << "selectTerms: don't have data for " << *i << " so can't conclude anything" << endl;
 746     }
 747   }
 748   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 }
 754
 755 SymmetryBreaker::Statistics::Statistics(std::string name)
 756   : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0)
 757   , d_units(name + "theory::uf::symmetry_breaker::units", 0)
 758   , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0)
 759   , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0)
 760   , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations")
 761   , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms")
 762   , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization")
 763 {
 764   smtStatisticsRegistry()->registerStat(&d_clauses);
 765   smtStatisticsRegistry()->registerStat(&d_units);
 766   smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered);
 767   smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant);
 768   smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer);
 769   smtStatisticsRegistry()->registerStat(&d_selectTermsTimer);
 770   smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer);
 771 }
 772
 773 SymmetryBreaker::Statistics::~Statistics()
 774 {
 775   smtStatisticsRegistry()->unregisterStat(&d_clauses);
 776   smtStatisticsRegistry()->unregisterStat(&d_units);
 777   smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered);
 778   smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant);
 779   smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer);
 780   smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer);
 781   smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer);
 782 }
 783
 784 SymmetryBreaker::Terms::iterator
 785 SymmetryBreaker::selectMostPromisingTerm(Terms& terms) {
 786   // use d_phi
 787   Debug("ufsymm") << "UFSYMM selectMostPromisingTerm()" << endl;
 788   return terms.begin();
 789 }
 790
 791 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   if (p.find(term) != p.end()) {
 795     cts.insert(term);
 796   } else {
 797     for(TNode::iterator i = term.begin(); i != term.end(); ++i) {
 798       insertUsedIn(*i, p, cts);
 799     }
 800   }
 801 }
 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 }/* CVC4 namespace */