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