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