Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of theory of UF with cardinality.
11 : : */
12 : :
13 : : #include "theory/uf/cardinality_extension.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "expr/cardinality_constraint.h"
18 : : #include "expr/skolem_manager.h"
19 : : #include "options/smt_options.h"
20 : : #include "options/uf_options.h"
21 : : #include "smt/logic_exception.h"
22 : : #include "theory/decision_manager.h"
23 : : #include "theory/quantifiers/term_database.h"
24 : : #include "theory/quantifiers_engine.h"
25 : : #include "theory/theory_engine.h"
26 : : #include "theory/theory_model.h"
27 : : #include "theory/uf/equality_engine.h"
28 : : #include "theory/uf/theory_uf.h"
29 : : #include "util/rational.h"
30 : :
31 : : using namespace std;
32 : : using namespace cvc5::internal::kind;
33 : : using namespace cvc5::context;
34 : :
35 : : namespace cvc5::internal {
36 : : namespace theory {
37 : : namespace uf {
38 : :
39 : : /* These are names are unambigious are we use abbreviations. */
40 : : typedef CardinalityExtension::SortModel SortModel;
41 : : typedef SortModel::Region Region;
42 : : typedef Region::RegionNodeInfo RegionNodeInfo;
43 : : typedef RegionNodeInfo::DiseqList DiseqList;
44 : :
45 : 3842 : Region::Region(SortModel* cf, context::Context* c)
46 : 3842 : : d_cf(cf),
47 : 0 : d_testCliqueSize(c, 0),
48 : 3842 : d_splitsSize(c, 0),
49 : 3842 : d_testClique(c),
50 : 3842 : d_splits(c),
51 : 3842 : d_reps_size(c, 0),
52 : 3842 : d_total_diseq_external(c, 0),
53 : 3842 : d_total_diseq_internal(c, 0),
54 : 7684 : d_valid(c, true)
55 : : {
56 : 3842 : }
57 : :
58 : 7676 : Region::~Region()
59 : : {
60 [ + + ]: 18587 : for (iterator i = begin(), iend = end(); i != iend; ++i)
61 : : {
62 : 14749 : RegionNodeInfo* regionNodeInfo = (*i).second;
63 [ + - ]: 14749 : delete regionNodeInfo;
64 : : }
65 : 3838 : d_nodes.clear();
66 : 7676 : }
67 : :
68 : 7678 : void Region::addRep(Node n) { setRep(n, true); }
69 : :
70 : 983 : void Region::takeNode(Region* r, Node n)
71 : : {
72 [ - + ][ - + ]: 983 : Assert(!hasRep(n));
[ - - ]
73 [ - + ][ - + ]: 983 : Assert(r->hasRep(n));
[ - - ]
74 : : // add representative
75 : 983 : setRep(n, true);
76 : : // take disequalities from r
77 : 983 : RegionNodeInfo* rni = r->d_nodes[n];
78 [ + + ]: 2949 : for (int t = 0; t < 2; t++)
79 : : {
80 : 1966 : DiseqList* del = rni->get(t);
81 [ + + ]: 5166 : for (DiseqList::iterator it = del->begin(); it != del->end(); ++it)
82 : : {
83 [ + + ]: 3200 : if ((*it).second)
84 : : {
85 : 2003 : r->setDisequal(n, (*it).first, t, false);
86 [ + + ]: 2003 : if (t == 0)
87 : : {
88 [ + + ]: 846 : if (hasRep((*it).first))
89 : : {
90 : 725 : setDisequal((*it).first, n, 0, false);
91 : 725 : setDisequal((*it).first, n, 1, true);
92 : 725 : setDisequal(n, (*it).first, 1, true);
93 : : }
94 : : else
95 : : {
96 : 121 : setDisequal(n, (*it).first, 0, true);
97 : : }
98 : : }
99 : : else
100 : : {
101 : 1157 : r->setDisequal((*it).first, n, 1, false);
102 : 1157 : r->setDisequal((*it).first, n, 0, true);
103 : 1157 : setDisequal(n, (*it).first, 0, true);
104 : : }
105 : : }
106 : : }
107 : : }
108 : : // remove representative
109 : 983 : r->setRep(n, false);
110 : 983 : }
111 : :
112 : 61417 : void Region::combine(Region* r)
113 : : {
114 : : // take all nodes from r
115 [ + + ]: 341008 : for (Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it)
116 : : {
117 [ + + ]: 279591 : if (it->second->valid())
118 : : {
119 : 65240 : setRep(it->first, true);
120 : : }
121 : : }
122 [ + + ]: 341008 : for (Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it)
123 : : {
124 [ + + ]: 279591 : if (it->second->valid())
125 : : {
126 : : // take disequalities from r
127 : 65240 : Node n = it->first;
128 : 65240 : RegionNodeInfo* rni = it->second;
129 [ + + ]: 195720 : for (int t = 0; t < 2; t++)
130 : : {
131 : 130480 : RegionNodeInfo::DiseqList* del = rni->get(t);
132 : 260960 : for (RegionNodeInfo::DiseqList::iterator it2 = del->begin(),
133 : 130480 : it2end = del->end();
134 [ + + ]: 320647 : it2 != it2end;
135 : 190167 : ++it2)
136 : : {
137 [ + + ]: 190167 : if ((*it2).second)
138 : : {
139 [ + + ][ + + ]: 176190 : if (t == 0 && hasRep((*it2).first))
[ + + ][ + + ]
[ - - ]
140 : : {
141 : 84479 : setDisequal((*it2).first, n, 0, false);
142 : 84479 : setDisequal((*it2).first, n, 1, true);
143 : 84479 : setDisequal(n, (*it2).first, 1, true);
144 : : }
145 : : else
146 : : {
147 : 91711 : setDisequal(n, (*it2).first, t, true);
148 : : }
149 : : }
150 : : }
151 : : }
152 : 65240 : }
153 : : }
154 : 61417 : r->d_valid = false;
155 : 61417 : }
156 : :
157 : : /** setEqual */
158 : 48920 : void Region::setEqual(Node a, Node b)
159 : : {
160 : 48920 : Assert(hasRep(a) && hasRep(b));
161 : : // move disequalities of b over to a
162 [ + + ]: 146760 : for (int t = 0; t < 2; t++)
163 : : {
164 : 97840 : DiseqList* del = d_nodes[b]->get(t);
165 [ + + ]: 200433 : for (DiseqList::iterator it = del->begin(); it != del->end(); ++it)
166 : : {
167 [ + + ]: 102593 : if ((*it).second)
168 : : {
169 : 69335 : Node n = (*it).first;
170 : : // get the region that contains the endpoint of the disequality b != ...
171 : 69335 : Region* nr = d_cf->d_regions[d_cf->d_regions_map[n]];
172 [ + + ]: 69335 : if (!isDisequal(a, n, t))
173 : : {
174 : 31640 : setDisequal(a, n, t, true);
175 : 31640 : nr->setDisequal(n, a, t, true);
176 : : }
177 : 69335 : setDisequal(b, n, t, false);
178 : 69335 : nr->setDisequal(n, b, t, false);
179 : 69335 : }
180 : : }
181 : : }
182 : : // remove b from representatives
183 : 48920 : setRep(b, false);
184 : 48920 : }
185 : :
186 : 597840 : void Region::setDisequal(Node n1, Node n2, int type, bool valid)
187 : : {
188 : : // Trace("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " "
189 : : // << type << " " << valid << std::endl;
190 : : // debugPrint("uf-ss-region-debug");
191 : : // Assert( isDisequal( n1, n2, type )!=valid );
192 [ + + ]: 597840 : if (isDisequal(n1, n2, type) != valid)
193 : : { // DO_THIS: make assertion
194 : 596313 : d_nodes[n1]->get(type)->setDisequal(n2, valid);
195 [ + + ]: 596313 : if (type == 0)
196 : : {
197 [ + + ]: 249742 : d_total_diseq_external = d_total_diseq_external + (valid ? 1 : -1);
198 : : }
199 : : else
200 : : {
201 [ + + ]: 346571 : d_total_diseq_internal = d_total_diseq_internal + (valid ? 1 : -1);
202 [ + + ]: 346571 : if (valid)
203 : : {
204 : : // if they are both a part of testClique, then remove split
205 [ + - ]: 231989 : if (d_testClique.find(n1) != d_testClique.end() && d_testClique[n1]
206 [ + + ][ + + ]: 231989 : && d_testClique.find(n2) != d_testClique.end() && d_testClique[n2])
[ + - ][ + + ]
207 : : {
208 : 4802 : Node eq = NodeManager::mkNode(Kind::EQUAL, n1, n2);
209 [ + + ][ + - ]: 2401 : if (d_splits.find(eq) != d_splits.end() && d_splits[eq])
[ + + ]
210 : : {
211 [ + - ]: 2370 : Trace("uf-ss-debug")
212 : 1185 : << "removing split for " << n1 << " " << n2 << std::endl;
213 : 1185 : d_splits[eq] = false;
214 : 1185 : d_splitsSize = d_splitsSize - 1;
215 : : }
216 : 2401 : }
217 : : }
218 : : }
219 : : }
220 : 597840 : }
221 : :
222 : 123804 : void Region::setRep(Node n, bool valid)
223 : : {
224 [ - + ][ - + ]: 123804 : Assert(hasRep(n) != valid);
[ - - ]
225 [ + + ][ + + ]: 123804 : if (valid && d_nodes.find(n) == d_nodes.end())
[ + + ]
226 : : {
227 : 14755 : d_nodes[n] = new RegionNodeInfo(d_cf->d_thss->context());
228 : : }
229 : 123804 : d_nodes[n]->setValid(valid);
230 [ + + ]: 123804 : d_reps_size = d_reps_size + (valid ? 1 : -1);
231 : : // removing a member of the test clique from this region
232 [ + + ][ + - ]: 123804 : if (d_testClique.find(n) != d_testClique.end() && d_testClique[n])
[ + + ]
233 : : {
234 [ - + ][ - + ]: 2358 : Assert(!valid);
[ - - ]
235 : 2358 : d_testClique[n] = false;
236 : 2358 : d_testCliqueSize = d_testCliqueSize - 1;
237 : : // remove all splits involving n
238 [ + + ]: 22547 : for (split_iterator it = begin_splits(); it != end_splits(); ++it)
239 : : {
240 [ + + ]: 20189 : if ((*it).second)
241 : : {
242 : 6284 : if ((*it).first[0] == n || (*it).first[1] == n)
243 : : {
244 : 6230 : d_splits[(*it).first] = false;
245 : 6230 : d_splitsSize = d_splitsSize - 1;
246 : : }
247 : : }
248 : : }
249 : : }
250 : 123804 : }
251 : :
252 : 740042 : bool Region::isDisequal(Node n1, Node n2, int type)
253 : : {
254 : 740042 : RegionNodeInfo::DiseqList* del = d_nodes[n1]->get(type);
255 : 740042 : return del->isSet(n2) && del->getDisequalityValue(n2);
256 : : }
257 : :
258 : : struct sortInternalDegree
259 : : {
260 : : Region* r;
261 : 23748 : bool operator()(Node i, Node j)
262 : : {
263 : 47496 : return (r->getRegionInfo(i)->getNumInternalDisequalities()
264 : 47496 : > r->getRegionInfo(j)->getNumInternalDisequalities());
265 : : }
266 : : };
267 : :
268 : : struct sortExternalDegree
269 : : {
270 : : Region* r;
271 : : bool operator()(Node i, Node j)
272 : : {
273 : : return (r->getRegionInfo(i)->getNumExternalDisequalities()
274 : : > r->getRegionInfo(j)->getNumExternalDisequalities());
275 : : }
276 : : };
277 : :
278 : : int gmcCount = 0;
279 : :
280 : 147306 : bool Region::getMustCombine(int cardinality)
281 : : {
282 [ + + ]: 147306 : if (d_total_diseq_external >= static_cast<unsigned>(cardinality))
283 : : {
284 : : // The number of external disequalities is greater than or equal to
285 : : // cardinality. Thus, a clique of size cardinality+1 may exist
286 : : // between nodes in d_regions[i] and other regions Check if this is
287 : : // actually the case: must have n nodes with outgoing degree
288 : : //(cardinality+1-n) for some n>0
289 : 24833 : std::vector<int> degrees;
290 [ + + ]: 226831 : for (Region::iterator it = begin(); it != end(); ++it)
291 : : {
292 : 216293 : RegionNodeInfo* rni = it->second;
293 [ + + ]: 216293 : if (rni->valid())
294 : : {
295 [ + + ]: 100506 : if (rni->getNumDisequalities() >= cardinality)
296 : : {
297 : 75241 : int outDeg = rni->getNumExternalDisequalities();
298 [ + + ]: 75241 : if (outDeg >= cardinality)
299 : : {
300 : : // we have 1 node of degree greater than (cardinality)
301 : 14295 : return true;
302 : : }
303 [ + + ]: 62314 : else if (outDeg >= 1)
304 : : {
305 : 53956 : degrees.push_back(outDeg);
306 [ + + ]: 53956 : if ((int)degrees.size() >= cardinality)
307 : : {
308 : : // we have (cardinality) nodes of degree 1
309 : 1368 : return true;
310 : : }
311 : : }
312 : : }
313 : : }
314 : : }
315 : 10538 : gmcCount++;
316 [ + + ]: 10538 : if (gmcCount % 100 == 0)
317 : : {
318 [ + - ]: 166 : Trace("gmc-count") << gmcCount << " " << cardinality
319 : 83 : << " sample : " << degrees.size() << std::endl;
320 : : }
321 : : // this should happen relatively infrequently....
322 : 10538 : std::sort(degrees.begin(), degrees.end());
323 [ + + ]: 54505 : for (int i = 0; i < (int)degrees.size(); i++)
324 : : {
325 [ + + ]: 45408 : if (degrees[i] >= cardinality + 1 - ((int)degrees.size() - i))
326 : : {
327 : 1441 : return true;
328 : : }
329 : : }
330 [ + + ]: 24833 : }
331 : 131570 : return false;
332 : : }
333 : :
334 : 1144478 : bool Region::check(Theory::Effort level,
335 : : int cardinality,
336 : : std::vector<Node>& clique)
337 : : {
338 [ + + ]: 1144478 : if (d_reps_size > unsigned(cardinality))
339 : : {
340 [ + + ]: 116033 : if (d_total_diseq_internal == d_reps_size * (d_reps_size - 1))
341 : : {
342 [ + + ]: 68176 : if (d_reps_size > 1)
343 : : {
344 : : // quick clique check, all reps form a clique
345 [ + + ]: 37128 : for (iterator it = begin(); it != end(); ++it)
346 : : {
347 [ + + ]: 32622 : if (it->second->valid())
348 : : {
349 : 22061 : clique.push_back(it->first);
350 : : }
351 : : }
352 [ + - ]: 4506 : Trace("quick-clique") << "Found quick clique" << std::endl;
353 : 4506 : return true;
354 : : }
355 : : else
356 : : {
357 : 63670 : return false;
358 : : }
359 : : }
360 [ + + ]: 47857 : else if (level == Theory::EFFORT_FULL)
361 : : {
362 : : // build test clique, up to size cardinality+1
363 [ + + ]: 2985 : if (d_testCliqueSize <= unsigned(cardinality))
364 : : {
365 : 2865 : std::vector<Node> newClique;
366 [ + + ]: 2865 : if (d_testCliqueSize < unsigned(cardinality))
367 : : {
368 [ + + ]: 22595 : for (iterator it = begin(); it != end(); ++it)
369 : : {
370 : : // if not in the test clique, add it to the set of new members
371 : 20186 : if (it->second->valid()
372 [ + + ][ + + ]: 20188 : && (d_testClique.find(it->first) == d_testClique.end()
[ + + ]
373 [ - + ]: 2 : || !d_testClique[it->first]))
374 : : {
375 : : // if( it->second->getNumInternalDisequalities()>cardinality ||
376 : : // level==Theory::EFFORT_FULL ){
377 : 12770 : newClique.push_back(it->first);
378 : : //}
379 : : }
380 : : }
381 : : // choose remaining nodes with the highest degrees
382 : : sortInternalDegree sidObj;
383 : 2409 : sidObj.r = this;
384 : 2409 : std::sort(newClique.begin(), newClique.end(), sidObj);
385 : 2409 : int offset = (cardinality - d_testCliqueSize) + 1;
386 : 2409 : newClique.erase(newClique.begin() + offset, newClique.end());
387 : : }
388 : : else
389 : : {
390 : : // scan for the highest degree
391 : 456 : int maxDeg = -1;
392 : 456 : Node maxNode;
393 : 456 : for (std::map<Node, RegionNodeInfo*>::iterator it = d_nodes.begin();
394 [ + + ]: 5945 : it != d_nodes.end();
395 : 5489 : ++it)
396 : : {
397 : : // if not in the test clique, add it to the set of new members
398 : 5489 : if (it->second->valid()
399 [ + + ][ + + ]: 8278 : && (d_testClique.find(it->first) == d_testClique.end()
[ + + ]
400 [ - + ]: 2789 : || !d_testClique[it->first]))
401 : : {
402 [ + + ]: 471 : if (it->second->getNumInternalDisequalities() > maxDeg)
403 : : {
404 : 456 : maxDeg = it->second->getNumInternalDisequalities();
405 : 456 : maxNode = it->first;
406 : : }
407 : : }
408 : : }
409 [ - + ][ - + ]: 456 : Assert(maxNode != Node::null());
[ - - ]
410 : 456 : newClique.push_back(maxNode);
411 : 456 : }
412 : : // check splits internal to new members
413 [ + + ]: 15958 : for (int j = 0; j < (int)newClique.size(); j++)
414 : : {
415 [ + - ]: 26186 : Trace("uf-ss-debug")
416 : 13093 : << "Choose to add clique member " << newClique[j] << std::endl;
417 [ + + ]: 61681 : for (int k = (j + 1); k < (int)newClique.size(); k++)
418 : : {
419 [ + + ]: 48588 : if (!isDisequal(newClique[j], newClique[k], 1))
420 : : {
421 : 5921 : Node at_j = newClique[j];
422 : 5921 : Node at_k = newClique[k];
423 : 11842 : Node j_eq_k = NodeManager::mkNode(Kind::EQUAL, at_j, at_k);
424 : 5921 : d_splits[j_eq_k] = true;
425 : 5921 : d_splitsSize = d_splitsSize + 1;
426 : 5921 : }
427 : : }
428 : : // check disequalities with old members
429 : 13093 : for (NodeBoolMap::iterator it = d_testClique.begin();
430 [ + + ]: 17321 : it != d_testClique.end();
431 : 4228 : ++it)
432 : : {
433 [ + + ]: 4228 : if ((*it).second)
434 : : {
435 [ + + ]: 2793 : if (!isDisequal((*it).first, newClique[j], 1))
436 : : {
437 : 1737 : Node at_it = (*it).first;
438 : 1737 : Node at_j = newClique[j];
439 : 1737 : Node it_eq_j = at_it.eqNode(at_j);
440 : 1737 : d_splits[it_eq_j] = true;
441 : 1737 : d_splitsSize = d_splitsSize + 1;
442 : 1737 : }
443 : : }
444 : : }
445 : : }
446 : : // add new clique members to test clique
447 [ + + ]: 15958 : for (int j = 0; j < (int)newClique.size(); j++)
448 : : {
449 : 13093 : d_testClique[newClique[j]] = true;
450 : 13093 : d_testCliqueSize = d_testCliqueSize + 1;
451 : : }
452 : 2865 : }
453 : : // Check if test clique has larger size than cardinality, and
454 : : // forms a clique.
455 [ + - ][ + + ]: 2985 : if (d_testCliqueSize >= unsigned(cardinality + 1) && d_splitsSize == 0)
[ + + ]
456 : : {
457 : : // test clique is a clique
458 : 35 : for (NodeBoolMap::iterator it = d_testClique.begin();
459 [ + + ]: 123 : it != d_testClique.end();
460 : 88 : ++it)
461 : : {
462 [ + - ]: 88 : if ((*it).second)
463 : : {
464 : 88 : clique.push_back((*it).first);
465 : : }
466 : : }
467 : 35 : return true;
468 : : }
469 : : }
470 : : }
471 : 1076267 : return false;
472 : : }
473 : :
474 : 0 : void Region::getNumExternalDisequalities(
475 : : std::map<Node, int>& num_ext_disequalities)
476 : : {
477 [ - - ]: 0 : for (Region::iterator it = begin(); it != end(); ++it)
478 : : {
479 : 0 : RegionNodeInfo* rni = it->second;
480 [ - - ]: 0 : if (rni->valid())
481 : : {
482 : 0 : DiseqList* del = rni->get(0);
483 [ - - ]: 0 : for (DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2)
484 : : {
485 [ - - ]: 0 : if ((*it2).second)
486 : : {
487 : 0 : num_ext_disequalities[(*it2).first]++;
488 : : }
489 : : }
490 : : }
491 : : }
492 : 0 : }
493 : :
494 : 3836 : void Region::debugPrint(CVC5_UNUSED const char* c, bool incClique)
495 : : {
496 [ + - ]: 3836 : Trace(c) << "Num reps: " << d_reps_size << std::endl;
497 [ + + ]: 10991 : for (Region::iterator it = begin(); it != end(); ++it)
498 : : {
499 : 7155 : RegionNodeInfo* rni = it->second;
500 [ - + ]: 7155 : if (rni->valid())
501 : : {
502 : 0 : Node n = it->first;
503 [ - - ]: 0 : Trace(c) << " " << n << std::endl;
504 [ - - ]: 0 : for (int i = 0; i < 2; i++)
505 : : {
506 : 0 : Trace(c) << " " << (i == 0 ? "Ext" : "Int") << " disequal:";
507 : 0 : DiseqList* del = rni->get(i);
508 [ - - ]: 0 : for (DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2)
509 : : {
510 [ - - ]: 0 : if ((*it2).second)
511 : : {
512 [ - - ]: 0 : Trace(c) << " " << (*it2).first;
513 : : }
514 : : }
515 [ - - ]: 0 : Trace(c) << ", total = " << del->size() << std::endl;
516 : : }
517 : 0 : }
518 : : }
519 [ + - ]: 3836 : Trace(c) << "Total disequal: " << d_total_diseq_external << " external,";
520 [ + - ]: 3836 : Trace(c) << " " << d_total_diseq_internal << " internal." << std::endl;
521 : :
522 [ + - ]: 3836 : if (incClique)
523 : : {
524 [ - + ]: 3836 : if (!d_testClique.empty())
525 : : {
526 [ - - ]: 0 : Trace(c) << "Candidate clique members: " << std::endl;
527 [ - - ]: 0 : Trace(c) << " ";
528 : 0 : for (NodeBoolMap::iterator it = d_testClique.begin();
529 [ - - ]: 0 : it != d_testClique.end();
530 : 0 : ++it)
531 : : {
532 [ - - ]: 0 : if ((*it).second)
533 : : {
534 [ - - ]: 0 : Trace(c) << (*it).first << " ";
535 : : }
536 : : }
537 [ - - ]: 0 : Trace(c) << ", size = " << d_testCliqueSize << std::endl;
538 : : }
539 [ - + ]: 3836 : if (!d_splits.empty())
540 : : {
541 [ - - ]: 0 : Trace(c) << "Required splits: " << std::endl;
542 [ - - ]: 0 : Trace(c) << " ";
543 [ - - ]: 0 : for (NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end();
544 : 0 : ++it)
545 : : {
546 [ - - ]: 0 : if ((*it).second)
547 : : {
548 [ - - ]: 0 : Trace(c) << (*it).first << " ";
549 : : }
550 : : }
551 [ - - ]: 0 : Trace(c) << ", size = " << d_splitsSize << std::endl;
552 : : }
553 : : }
554 : 3836 : }
555 : :
556 : 722 : SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy(
557 : 722 : Env& env, TypeNode type, Valuation valuation)
558 : 722 : : DecisionStrategyFmf(env, valuation), d_type(type)
559 : : {
560 : 722 : }
561 : :
562 : 1688 : Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i)
563 : : {
564 : 1688 : NodeManager* nm = nodeManager();
565 : 3376 : Node cco = nm->mkConst(CardinalityConstraint(d_type, Integer(i + 1)));
566 : 3376 : return nm->mkNode(Kind::CARDINALITY_CONSTRAINT, cco);
567 : 1688 : }
568 : :
569 : 0 : std::string SortModel::CardinalityDecisionStrategy::identify() const
570 : : {
571 : 0 : return std::string("uf_card");
572 : : }
573 : :
574 : 722 : SortModel::SortModel(Env& env,
575 : : TypeNode tn,
576 : : TheoryState& state,
577 : : TheoryInferenceManager& im,
578 : 722 : CardinalityExtension* thss)
579 : : : EnvObj(env),
580 : 722 : d_type(tn),
581 : 722 : d_state(state),
582 : 722 : d_im(im),
583 : 722 : d_thss(thss),
584 : 722 : d_regions_index(thss->context(), 0),
585 : 722 : d_regions_map(thss->context()),
586 : 722 : d_split_score(thss->context()),
587 : 722 : d_disequalities_index(thss->context(), 0),
588 : 722 : d_reps(thss->context(), 0),
589 : 722 : d_cardinality(thss->context(), 1),
590 : 722 : d_hasCard(thss->context(), false),
591 : 722 : d_maxNegCard(thss->context(), 0),
592 : 722 : d_initialized(thss->userContext(), false),
593 : 5054 : d_c_dec_strat(nullptr)
594 : : {
595 [ + - ]: 722 : if (options().uf.ufssMode == options::UfssMode::FULL)
596 : : {
597 : : // Register the strategy with the decision manager of the theory.
598 : : // We are guaranteed that the decision manager is ready since we
599 : : // construct this module during TheoryUF::finishInit.
600 : 722 : d_c_dec_strat.reset(new CardinalityDecisionStrategy(
601 : 722 : thss->d_env, d_type, thss->getTheory()->getValuation()));
602 : : }
603 : 722 : }
604 : :
605 : 1440 : SortModel::~SortModel()
606 : : {
607 : 720 : for (std::vector<Region*>::iterator i = d_regions.begin();
608 [ + + ]: 4558 : i != d_regions.end();
609 : 3838 : ++i)
610 : : {
611 : 3838 : Region* region = *i;
612 [ + - ]: 3838 : delete region;
613 : : }
614 : 720 : d_regions.clear();
615 : 1440 : }
616 : :
617 : : /** initialize */
618 : 24535 : void SortModel::initialize()
619 : : {
620 [ + - ][ + + ]: 24535 : if (d_c_dec_strat.get() != nullptr && !d_initialized)
[ + + ]
621 : : {
622 : 1160 : d_initialized = true;
623 : : // Strategy is user-context-dependent, since it is in sync with
624 : : // user-context-dependent flag d_initialized.
625 : 2320 : d_im.getDecisionManager()->registerStrategy(DecisionManager::STRAT_UF_CARD,
626 : 1160 : d_c_dec_strat.get());
627 : : }
628 : 24535 : }
629 : :
630 : : /** new node */
631 : 7678 : void SortModel::newEqClass(Node n)
632 : : {
633 [ + - ]: 7678 : if (!d_state.isInConflict())
634 : : {
635 [ + - ]: 7678 : if (d_regions_map.find(n) == d_regions_map.end())
636 : : {
637 : 7678 : d_regions_map[n] = d_regions_index;
638 [ + - ]: 7678 : Trace("uf-ss") << "CardinalityExtension: New Eq Class " << n << std::endl;
639 [ + - ]: 15356 : Trace("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size()
640 : 7678 : << std::endl;
641 [ + + ]: 7678 : if (d_regions_index < d_regions.size())
642 : : {
643 : 3836 : d_regions[d_regions_index]->debugPrint("uf-ss-debug", true);
644 : 3836 : d_regions[d_regions_index]->setValid(true);
645 [ - + ][ - + ]: 3836 : Assert(d_regions[d_regions_index]->getNumReps() == 0);
[ - - ]
646 : : }
647 : : else
648 : : {
649 : 3842 : d_regions.push_back(new Region(this, d_thss->context()));
650 : : }
651 : 7678 : d_regions[d_regions_index]->addRep(n);
652 : 7678 : d_regions_index = d_regions_index + 1;
653 : :
654 : 7678 : d_reps = d_reps + 1;
655 : : }
656 : : }
657 : 7678 : }
658 : :
659 : : /** merge */
660 : 48920 : void SortModel::merge(Node a, Node b)
661 : : {
662 [ - + ]: 48920 : if (d_state.isInConflict())
663 : : {
664 : 0 : return;
665 : : }
666 [ + - ]: 97840 : Trace("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b << "..."
667 : 48920 : << std::endl;
668 [ + - ]: 48920 : if (a != b)
669 : : {
670 [ - + ][ - + ]: 48920 : Assert(d_regions_map.find(a) != d_regions_map.end());
[ - - ]
671 [ - + ][ - + ]: 48920 : Assert(d_regions_map.find(b) != d_regions_map.end());
[ - - ]
672 : 48920 : int ai = d_regions_map[a];
673 : 48920 : int bi = d_regions_map[b];
674 [ + - ]: 48920 : Trace("uf-ss") << " regions: " << ai << " " << bi << std::endl;
675 [ + + ]: 48920 : if (ai != bi)
676 : : {
677 [ + + ]: 42570 : if (d_regions[ai]->getNumReps() == 1)
678 : : {
679 : 28374 : int ri = combineRegions(bi, ai);
680 : 28374 : d_regions[ri]->setEqual(a, b);
681 : 28374 : checkRegion(ri);
682 : : }
683 [ + + ]: 14196 : else if (d_regions[bi]->getNumReps() == 1)
684 : : {
685 : 13213 : int ri = combineRegions(ai, bi);
686 : 13213 : d_regions[ri]->setEqual(a, b);
687 : 13213 : checkRegion(ri);
688 : : }
689 : : else
690 : : {
691 : : // Either move a to d_regions[bi], or b to d_regions[ai].
692 : 983 : RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
693 : 983 : RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
694 : 983 : int aex = (a_region_info->getNumInternalDisequalities()
695 : 983 : - getNumDisequalitiesToRegion(a, bi));
696 : 983 : int bex = (b_region_info->getNumInternalDisequalities()
697 : 983 : - getNumDisequalitiesToRegion(b, ai));
698 : : // Based on which would produce the fewest number of
699 : : // external disequalities.
700 [ + + ]: 983 : if (aex < bex)
701 : : {
702 : 356 : moveNode(a, bi);
703 : 356 : d_regions[bi]->setEqual(a, b);
704 : : }
705 : : else
706 : : {
707 : 627 : moveNode(b, ai);
708 : 627 : d_regions[ai]->setEqual(a, b);
709 : : }
710 : 983 : checkRegion(ai);
711 : 983 : checkRegion(bi);
712 : : }
713 : : }
714 : : else
715 : : {
716 : 6350 : d_regions[ai]->setEqual(a, b);
717 : 6350 : checkRegion(ai);
718 : : }
719 : 48920 : d_regions_map[b] = -1;
720 : : }
721 : 48920 : d_reps = d_reps - 1;
722 : : }
723 : :
724 : : /** assert terms are disequal */
725 : 21486 : void SortModel::assertDisequal(Node a, Node b, Node reason)
726 : : {
727 [ - + ]: 21486 : if (d_state.isInConflict())
728 : : {
729 : 0 : return;
730 : : }
731 : : // if they are not already disequal
732 : 21486 : eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine();
733 : 21486 : a = ee->getRepresentative(a);
734 : 21486 : b = ee->getRepresentative(b);
735 : 21486 : int ai = d_regions_map[a];
736 : 21486 : int bi = d_regions_map[b];
737 [ - + ]: 21486 : if (d_regions[ai]->isDisequal(a, b, ai == bi))
738 : : {
739 : : // already disequal
740 : 0 : return;
741 : : }
742 [ + - ]: 42972 : Trace("uf-ss") << "Assert disequal " << a << " != " << b << "..."
743 : 21486 : << std::endl;
744 [ + - ]: 42972 : Trace("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..."
745 : 21486 : << std::endl;
746 : : // add to list of disequalities
747 [ + + ]: 21486 : if (d_disequalities_index < d_disequalities.size())
748 : : {
749 : 16174 : d_disequalities[d_disequalities_index] = reason;
750 : : }
751 : : else
752 : : {
753 : 5312 : d_disequalities.push_back(reason);
754 : : }
755 : 21486 : d_disequalities_index = d_disequalities_index + 1;
756 : : // now, add disequalities to regions
757 [ - + ][ - + ]: 21486 : Assert(d_regions_map.find(a) != d_regions_map.end());
[ - - ]
758 [ - + ][ - + ]: 21486 : Assert(d_regions_map.find(b) != d_regions_map.end());
[ - - ]
759 [ + - ]: 21486 : Trace("uf-ss") << " regions: " << ai << " " << bi << std::endl;
760 [ + + ]: 21486 : if (ai == bi)
761 : : {
762 : : // internal disequality
763 : 761 : d_regions[ai]->setDisequal(a, b, 1, true);
764 : 761 : d_regions[ai]->setDisequal(b, a, 1, true);
765 : : // do not need to check if it needs to combine (no new ext. disequalities)
766 : 761 : checkRegion(ai, false);
767 : : }
768 : : else
769 : : {
770 : : // external disequality
771 : 20725 : d_regions[ai]->setDisequal(a, b, 0, true);
772 : 20725 : d_regions[bi]->setDisequal(b, a, 0, true);
773 : 20725 : checkRegion(ai);
774 : 20725 : checkRegion(bi);
775 : : }
776 : : }
777 : :
778 : 0 : bool SortModel::areDisequal(Node a, Node b)
779 : : {
780 : 0 : Assert(a == d_thss->getTheory()->getEqualityEngine()->getRepresentative(a));
781 : 0 : Assert(b == d_thss->getTheory()->getEqualityEngine()->getRepresentative(b));
782 : 0 : if (d_regions_map.find(a) != d_regions_map.end()
783 : 0 : && d_regions_map.find(b) != d_regions_map.end())
784 : : {
785 : 0 : int ai = d_regions_map[a];
786 : 0 : int bi = d_regions_map[b];
787 [ - - ]: 0 : return d_regions[ai]->isDisequal(a, b, ai == bi ? 1 : 0);
788 : : }
789 : : else
790 : : {
791 : 0 : return false;
792 : : }
793 : : }
794 : :
795 : 336065 : void SortModel::check(Theory::Effort level)
796 : : {
797 [ - + ][ - + ]: 336065 : Assert(options().uf.ufssMode == options::UfssMode::FULL);
[ - - ]
798 [ + + ][ - + ]: 336065 : if (!d_hasCard && d_state.isInConflict())
[ - + ]
799 : : {
800 : : // not necessary to check
801 : 0 : return;
802 : : }
803 [ + - ]: 672130 : Trace("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
804 : 336065 : << std::endl;
805 [ + + ]: 336065 : if (level == Theory::EFFORT_FULL)
806 : : {
807 [ + - ]: 14140 : Trace("fmf-full-check") << std::endl;
808 [ + - ]: 28280 : Trace("fmf-full-check")
809 : 14140 : << "Full check for SortModel " << d_type << ", status : " << std::endl;
810 : 14140 : debugPrint("fmf-full-check");
811 [ + - ]: 14140 : Trace("fmf-full-check") << std::endl;
812 : : }
813 [ + + ]: 336065 : if (d_reps <= (unsigned)d_cardinality)
814 : : {
815 [ + - ]: 241904 : Trace("uf-ss-debug") << "We have " << d_reps << " representatives for type "
816 : 120952 : << d_type << ", <= " << d_cardinality << std::endl;
817 [ + + ]: 120952 : if (level == Theory::EFFORT_FULL)
818 : : {
819 [ + - ]: 14106 : Trace("uf-ss-sat") << "We have " << d_reps << " representatives for type "
820 : 7053 : << d_type << ", <= " << d_cardinality << std::endl;
821 : : }
822 : 120952 : return;
823 : : }
824 : : // first check if we can generate a clique conflict
825 : : // do a check within each region
826 [ + + ]: 1999312 : for (size_t i = 0; i < d_regions_index; i++)
827 : : {
828 [ + + ]: 1785814 : if (d_regions[i]->valid())
829 : : {
830 : 996411 : std::vector<Node> clique;
831 [ + + ]: 996411 : if (d_regions[i]->check(level, d_cardinality, clique))
832 : : {
833 : : // add clique lemma
834 : 1615 : addCliqueLemma(clique);
835 : 1615 : return;
836 : : }
837 : : else
838 : : {
839 [ + - ]: 994796 : Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
840 : : }
841 [ + + ]: 996411 : }
842 : : }
843 : : // do splitting on demand
844 : 213498 : bool addedLemma = false;
845 [ + + ]: 213498 : if (level == Theory::EFFORT_FULL)
846 : : {
847 [ + - ]: 7044 : Trace("uf-ss-debug") << "Add splits?" << std::endl;
848 : : // see if we have any recommended splits from large regions
849 [ + + ]: 93029 : for (size_t i = 0; i < d_regions_index; i++)
850 : : {
851 [ + + ][ + + ]: 85985 : if (d_regions[i]->valid() && d_regions[i]->getNumReps() > d_cardinality)
[ + + ]
852 : : {
853 : 2950 : int sp = addSplit(d_regions[i]);
854 [ + - ]: 2950 : if (sp == 1)
855 : : {
856 : 2950 : addedLemma = true;
857 : : }
858 [ - - ]: 0 : else if (sp == -1)
859 : : {
860 : 0 : check(level);
861 : 0 : return;
862 : : }
863 : : }
864 : : }
865 : : }
866 : : // If no added lemmas, force continuation via combination of regions.
867 [ + + ][ + + ]: 213498 : if (level != Theory::EFFORT_FULL || addedLemma)
868 : : {
869 : 209404 : return;
870 : : }
871 : : // check at full effort
872 [ + - ]: 4094 : Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
873 [ + - ]: 4094 : Trace("uf-ss-si") << "Must combine region" << std::endl;
874 : 4094 : bool recheck = false;
875 : 4094 : SortInference* si = d_state.getSortInference();
876 [ + + ]: 4094 : if (si != nullptr)
877 : : {
878 : : // If sort inference is enabled, search for regions with same sort.
879 : 217 : std::map<int, int> sortsFound;
880 [ + - ]: 1628 : for (size_t i = 0; i < d_regions_index; i++)
881 : : {
882 [ + + ]: 1628 : if (d_regions[i]->valid())
883 : : {
884 : 434 : Node op = d_regions[i]->frontKey();
885 : 434 : int sort_id = si->getSortId(op);
886 [ + + ]: 434 : if (sortsFound.find(sort_id) != sortsFound.end())
887 : : {
888 [ + - ]: 434 : Trace("fmf-full-check") << "Combined regions " << i << " "
889 : 217 : << sortsFound[sort_id] << std::endl;
890 : 217 : combineRegions(sortsFound[sort_id], i);
891 : 217 : recheck = true;
892 : 217 : break;
893 : : }
894 : : else
895 : : {
896 : 217 : sortsFound[sort_id] = i;
897 : : }
898 [ + + ]: 434 : }
899 : : }
900 : 217 : }
901 [ + + ]: 4094 : if (!recheck)
902 : : {
903 : : // naive strategy, force region combination involving the first
904 : : // valid region
905 [ + - ]: 12234 : for (size_t i = 0; i < d_regions_index; i++)
906 : : {
907 [ + + ]: 12234 : if (d_regions[i]->valid())
908 : : {
909 : 3877 : int fcr = forceCombineRegion(i, false);
910 [ + - ]: 7754 : Trace("fmf-full-check")
911 : 3877 : << "Combined regions " << i << " " << fcr << std::endl;
912 [ + - ]: 7754 : Trace("uf-ss-debug")
913 : 3877 : << "Combined regions " << i << " " << fcr << std::endl;
914 : 3877 : recheck = true;
915 : 3877 : break;
916 : : }
917 : : }
918 : : }
919 [ + - ]: 4094 : if (recheck)
920 : : {
921 [ + - ]: 4094 : Trace("uf-ss-debug") << "Must recheck." << std::endl;
922 : 4094 : check(level);
923 : : }
924 : : }
925 : :
926 : 437 : void SortModel::presolve() { d_initialized = false; }
927 : :
928 : 1966 : int SortModel::getNumDisequalitiesToRegion(Node n, int ri)
929 : : {
930 : 1966 : int ni = d_regions_map[n];
931 : 1966 : int counter = 0;
932 : 1966 : DiseqList* del = d_regions[ni]->getRegionInfo(n)->get(0);
933 [ + + ]: 5409 : for (DiseqList::iterator it = del->begin(); it != del->end(); ++it)
934 : : {
935 [ + + ]: 3443 : if ((*it).second)
936 : : {
937 [ + + ]: 1227 : if (d_regions_map[(*it).first] == ri)
938 : : {
939 : 974 : counter++;
940 : : }
941 : : }
942 : : }
943 : 1966 : return counter;
944 : : }
945 : :
946 : 15736 : void SortModel::getDisequalitiesToRegions(int ri,
947 : : std::map<int, int>& regions_diseq)
948 : : {
949 : 15736 : Region* region = d_regions[ri];
950 [ + + ]: 202400 : for (Region::iterator it = region->begin(); it != region->end(); ++it)
951 : : {
952 [ + + ]: 186664 : if (it->second->valid())
953 : : {
954 : 46106 : DiseqList* del = it->second->get(0);
955 [ + + ]: 344267 : for (DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2)
956 : : {
957 [ + + ]: 298161 : if ((*it2).second)
958 : : {
959 [ - + ][ - + ]: 190773 : Assert(isValid(d_regions_map[(*it2).first]));
[ - - ]
960 : 190773 : regions_diseq[d_regions_map[(*it2).first]]++;
961 : : }
962 : : }
963 : : }
964 : : }
965 : 15736 : }
966 : :
967 : 0 : void SortModel::setSplitScore(Node n, int s)
968 : : {
969 [ - - ]: 0 : if (d_split_score.find(n) != d_split_score.end())
970 : : {
971 : 0 : int ss = d_split_score[n];
972 [ - - ]: 0 : d_split_score[n] = s > ss ? s : ss;
973 : : }
974 : : else
975 : : {
976 : 0 : d_split_score[n] = s;
977 : : }
978 [ - - ]: 0 : for (int i = 0; i < (int)n.getNumChildren(); i++)
979 : : {
980 : 0 : setSplitScore(n[i], s + 1);
981 : : }
982 : 0 : }
983 : :
984 : 12950 : void SortModel::assertCardinality(uint32_t c, bool val)
985 : : {
986 [ + - ]: 12950 : if (!d_state.isInConflict())
987 : : {
988 [ + - ]: 25900 : Trace("uf-ss-assert")
989 : 0 : << "Assert cardinality " << d_type << " " << c << " " << val
990 : 0 : << " level = "
991 : 12950 : << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl;
992 [ - + ][ - + ]: 12950 : Assert(c > 0);
[ - - ]
993 : 12950 : Node cl = getCardinalityLiteral(c);
994 [ + + ]: 12950 : if (val)
995 : : {
996 : 10695 : bool doCheckRegions = !d_hasCard;
997 : 10695 : bool prevHasCard = d_hasCard;
998 : 10695 : d_hasCard = true;
999 [ + + ][ + + ]: 10695 : if (!prevHasCard || c < d_cardinality)
[ + + ]
1000 : : {
1001 : 10687 : d_cardinality = c;
1002 : 10687 : simpleCheckCardinality();
1003 [ + + ]: 10687 : if (d_state.isInConflict())
1004 : : {
1005 : 222 : return;
1006 : : }
1007 : : }
1008 : : // should check all regions now
1009 [ + + ]: 10473 : if (doCheckRegions)
1010 : : {
1011 [ + + ]: 68973 : for (size_t i = 0; i < d_regions_index; i++)
1012 : : {
1013 [ + + ]: 58552 : if (d_regions[i]->valid())
1014 : : {
1015 : 50144 : checkRegion(i);
1016 [ - + ]: 50144 : if (d_state.isInConflict())
1017 : : {
1018 : 0 : return;
1019 : : }
1020 : : }
1021 : : }
1022 : : }
1023 : : // we assert it positively, if its beyond the bound, abort
1024 : 10473 : if (options().uf.ufssAbortCardinality >= 0
1025 [ - + ][ - - ]: 10473 : && c >= static_cast<uint32_t>(options().uf.ufssAbortCardinality))
[ - + ]
1026 : : {
1027 : 0 : std::stringstream ss;
1028 : 0 : ss << "Maximum cardinality (" << options().uf.ufssAbortCardinality
1029 : 0 : << ") for finite model finding exceeded." << std::endl;
1030 : 0 : throw LogicException(ss.str());
1031 : 0 : }
1032 : : }
1033 : : else
1034 : : {
1035 [ + + ]: 2255 : if (c > d_maxNegCard.get())
1036 : : {
1037 [ + - ]: 3982 : Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for "
1038 : 1991 : << d_type << " is now " << c << std::endl;
1039 : 1991 : d_maxNegCard.set(c);
1040 : 1991 : simpleCheckCardinality();
1041 : : }
1042 : : }
1043 [ + + ]: 12950 : }
1044 : : }
1045 : :
1046 : 157994 : void SortModel::checkRegion(int ri, bool checkCombine)
1047 : : {
1048 [ + + ][ + + ]: 157994 : if (isValid(ri) && d_hasCard)
[ + + ]
1049 : : {
1050 [ - + ][ - + ]: 148067 : Assert(d_cardinality > 0);
[ - - ]
1051 [ + + ][ + + ]: 148067 : if (checkCombine && d_regions[ri]->getMustCombine(d_cardinality))
[ + + ]
1052 : : {
1053 : 15736 : int riNew = forceCombineRegion(ri, true);
1054 [ + - ]: 15736 : if (riNew >= 0)
1055 : : {
1056 : 15736 : checkRegion(riNew, checkCombine);
1057 : : }
1058 : : }
1059 : : // now check if region is in conflict
1060 : 148067 : std::vector<Node> clique;
1061 [ + + ]: 148067 : if (d_regions[ri]->check(Theory::EFFORT_STANDARD, d_cardinality, clique))
1062 : : {
1063 : : // explain clique
1064 : 2926 : addCliqueLemma(clique);
1065 : : }
1066 : 148067 : }
1067 : 157994 : }
1068 : :
1069 : 19613 : int SortModel::forceCombineRegion(int ri, bool useDensity)
1070 : : {
1071 [ + + ]: 19613 : if (!useDensity)
1072 : : {
1073 [ + - ]: 32190 : for (int i = 0; i < (int)d_regions_index; i++)
1074 : : {
1075 [ + + ][ + + ]: 32190 : if (ri != i && d_regions[i]->valid())
[ + + ]
1076 : : {
1077 : 3877 : return combineRegions(ri, i);
1078 : : }
1079 : : }
1080 : 0 : return -1;
1081 : : }
1082 : : else
1083 : : {
1084 : : // this region must merge with another
1085 [ - + ]: 15736 : if (TraceIsOn("uf-ss-check-region"))
1086 : : {
1087 [ - - ]: 0 : Trace("uf-ss-check-region")
1088 : 0 : << "We must combine Region #" << ri << ". " << std::endl;
1089 : 0 : d_regions[ri]->debugPrint("uf-ss-check-region");
1090 : : }
1091 : : // take region with maximum disequality density
1092 : 15736 : double maxScore = 0;
1093 : 15736 : int maxRegion = -1;
1094 : 15736 : std::map<int, int> regions_diseq;
1095 : 15736 : getDisequalitiesToRegions(ri, regions_diseq);
1096 : 15736 : for (std::map<int, int>::iterator it = regions_diseq.begin();
1097 [ + + ]: 95364 : it != regions_diseq.end();
1098 : 79628 : ++it)
1099 : : {
1100 [ + - ]: 159256 : Trace("uf-ss-check-region")
1101 : 79628 : << it->first << " : " << it->second << std::endl;
1102 : : }
1103 : 15736 : for (std::map<int, int>::iterator it = regions_diseq.begin();
1104 [ + + ]: 95364 : it != regions_diseq.end();
1105 : 79628 : ++it)
1106 : : {
1107 [ - + ][ - + ]: 79628 : Assert(it->first != ri);
[ - - ]
1108 [ - + ][ - + ]: 79628 : Assert(isValid(it->first));
[ - - ]
1109 [ - + ][ - + ]: 79628 : Assert(d_regions[it->first]->getNumReps() > 0);
[ - - ]
1110 : : double tempScore =
1111 : 79628 : double(it->second) / double(d_regions[it->first]->getNumReps());
1112 [ + + ]: 79628 : if (tempScore > maxScore)
1113 : : {
1114 : 19077 : maxRegion = it->first;
1115 : 19077 : maxScore = tempScore;
1116 : : }
1117 : : }
1118 [ + - ]: 15736 : if (maxRegion != -1)
1119 : : {
1120 [ - + ]: 15736 : if (TraceIsOn("uf-ss-check-region"))
1121 : : {
1122 [ - - ]: 0 : Trace("uf-ss-check-region")
1123 : 0 : << "Combine with region #" << maxRegion << ":" << std::endl;
1124 : 0 : d_regions[maxRegion]->debugPrint("uf-ss-check-region");
1125 : : }
1126 : 15736 : return combineRegions(ri, maxRegion);
1127 : : }
1128 : 0 : return -1;
1129 : 15736 : }
1130 : : }
1131 : :
1132 : 61417 : int SortModel::combineRegions(int ai, int bi)
1133 : : {
1134 [ + - ]: 122834 : Trace("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #"
1135 : 61417 : << ai << std::endl;
1136 [ + - ][ + - ]: 61417 : Assert(isValid(ai) && isValid(bi));
[ - + ][ - + ]
[ - - ]
1137 : 61417 : Region* region_bi = d_regions[bi];
1138 [ + + ]: 341008 : for (Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it)
1139 : : {
1140 : 279591 : Region::RegionNodeInfo* rni = it->second;
1141 [ + + ]: 279591 : if (rni->valid())
1142 : : {
1143 : 65240 : d_regions_map[it->first] = ai;
1144 : : }
1145 : : }
1146 : : // update regions disequal DO_THIS?
1147 : 61417 : d_regions[ai]->combine(d_regions[bi]);
1148 : 61417 : d_regions[bi]->setValid(false);
1149 : 61417 : return ai;
1150 : : }
1151 : :
1152 : 983 : void SortModel::moveNode(Node n, int ri)
1153 : : {
1154 [ + - ]: 1966 : Trace("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri
1155 : 983 : << std::endl;
1156 [ - + ][ - + ]: 983 : Assert(isValid(d_regions_map[n]));
[ - - ]
1157 [ - + ][ - + ]: 983 : Assert(isValid(ri));
[ - - ]
1158 : : // move node to region ri
1159 : 983 : d_regions[ri]->takeNode(d_regions[d_regions_map[n]], n);
1160 : 983 : d_regions_map[n] = ri;
1161 : 983 : }
1162 : :
1163 : 2950 : int SortModel::addSplit(Region* r)
1164 : : {
1165 : 2950 : Node s;
1166 [ + - ]: 2950 : if (r->hasSplits())
1167 : : {
1168 : : // take the first split you find
1169 [ + - ]: 15877 : for (Region::split_iterator it = r->begin_splits(); it != r->end_splits();
1170 : 12927 : ++it)
1171 : : {
1172 [ + + ]: 15877 : if ((*it).second)
1173 : : {
1174 : 2950 : s = (*it).first;
1175 : 2950 : break;
1176 : : }
1177 : : }
1178 [ - + ][ - + ]: 2950 : Assert(s != Node::null());
[ - - ]
1179 : : }
1180 [ + - ]: 2950 : if (!s.isNull())
1181 : : {
1182 : : // add lemma to output channel
1183 [ - + ][ - + ]: 2950 : Assert(s.getKind() == Kind::EQUAL);
[ - - ]
1184 : 2950 : Node ss = rewrite(s);
1185 [ - + ]: 2950 : if (ss.getKind() != Kind::EQUAL)
1186 : : {
1187 : 0 : Node b_t = nodeManager()->mkConst(true);
1188 : 0 : Node b_f = nodeManager()->mkConst(false);
1189 [ - - ]: 0 : if (ss == b_f)
1190 : : {
1191 : 0 : Trace("uf-ss-lemma") << "....Assert disequal directly : " << s[0] << " "
1192 : 0 : << s[1] << std::endl;
1193 : 0 : assertDisequal(s[0], s[1], b_t);
1194 : 0 : return -1;
1195 : : }
1196 : : else
1197 : : {
1198 [ - - ]: 0 : Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl;
1199 : : }
1200 [ - - ]: 0 : if (ss == b_t)
1201 : : {
1202 : 0 : AlwaysAssert(false) << "Bad split " << s << std::endl;
1203 : : }
1204 [ - - ][ - - ]: 0 : }
1205 [ - + ]: 2950 : if (TraceIsOn("uf-ss-split-si"))
1206 : : {
1207 : 0 : SortInference* si = d_state.getSortInference();
1208 [ - - ]: 0 : if (si != nullptr)
1209 : : {
1210 [ - - ]: 0 : for (size_t i = 0; i < 2; i++)
1211 : : {
1212 : 0 : int sid = si->getSortId(ss[i]);
1213 [ - - ]: 0 : Trace("uf-ss-split-si") << sid << " ";
1214 : : }
1215 [ - - ]: 0 : Trace("uf-ss-split-si") << std::endl;
1216 : : }
1217 : : }
1218 : : // Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] )
1219 : : // << " "; Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal(
1220 : : // s[0], s[1] ) << std::endl; Trace("uf-ss-lemma") << s[0].getType() << " "
1221 : : // << s[1].getType() << std::endl; split on the equality s
1222 : 5900 : Node lem = NodeManager::mkNode(Kind::OR, ss, ss.negate());
1223 : : // send lemma, with caching
1224 [ + - ]: 2950 : if (d_im.lemma(lem, InferenceId::UF_CARD_SPLIT))
1225 : : {
1226 [ + - ]: 2950 : Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
1227 : : // tell the sat solver to explore the equals branch first
1228 : 2950 : d_im.preferPhase(ss, true);
1229 : 2950 : ++(d_thss->d_statistics.d_split_lemmas);
1230 : : }
1231 : 2950 : return 1;
1232 : 2950 : }
1233 : : else
1234 : : {
1235 : 0 : return 0;
1236 : : }
1237 : 2950 : }
1238 : :
1239 : 4541 : void SortModel::addCliqueLemma(std::vector<Node>& clique)
1240 : : {
1241 [ - + ][ - + ]: 4541 : Assert(d_hasCard);
[ - - ]
1242 [ - + ][ - + ]: 4541 : Assert(d_cardinality > 0);
[ - - ]
1243 [ + + ]: 7191 : while (clique.size() > d_cardinality + 1)
1244 : : {
1245 : 2650 : clique.pop_back();
1246 : : }
1247 : : // add as lemma
1248 : 4541 : std::vector<Node> eqs;
1249 [ + + ]: 24040 : for (unsigned i = 0, size = clique.size(); i < size; i++)
1250 : : {
1251 [ + + ]: 76622 : for (unsigned j = 0; j < i; j++)
1252 : : {
1253 : 57123 : eqs.push_back(clique[i].eqNode(clique[j]));
1254 : : }
1255 : : }
1256 : 4541 : eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
1257 : 4541 : Node lem = nodeManager()->mkNode(Kind::OR, eqs);
1258 : : // send lemma, with caching
1259 [ + - ]: 4541 : if (d_im.lemma(lem, InferenceId::UF_CARD_CLIQUE))
1260 : : {
1261 [ + - ]: 4541 : Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
1262 : 4541 : ++(d_thss->d_statistics.d_clique_lemmas);
1263 : : }
1264 : 4541 : }
1265 : :
1266 : 12678 : void SortModel::simpleCheckCardinality()
1267 : : {
1268 [ + + ]: 20185 : if (d_maxNegCard.get() != 0 && d_hasCard.get()
1269 [ + + ][ + + ]: 20185 : && d_cardinality.get() < d_maxNegCard.get())
[ + + ]
1270 : : {
1271 : 687 : Node lem = NodeManager::mkNode(
1272 : : Kind::AND,
1273 : 229 : {getCardinalityLiteral(d_cardinality.get()),
1274 : 458 : getCardinalityLiteral(d_maxNegCard.get()).negate()});
1275 [ + - ]: 458 : Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem
1276 : 229 : << std::endl;
1277 : 229 : d_im.conflict(lem, InferenceId::UF_CARD_SIMPLE_CONFLICT);
1278 : 229 : }
1279 : 12678 : }
1280 : :
1281 : 14140 : void SortModel::debugPrint(const char* c)
1282 : : {
1283 [ - + ]: 14140 : if (TraceIsOn(c))
1284 : : {
1285 [ - - ]: 0 : Trace(c) << "Number of reps = " << d_reps << std::endl;
1286 [ - - ]: 0 : Trace(c) << "Cardinality req = " << d_cardinality << std::endl;
1287 : 0 : unsigned debugReps = 0;
1288 [ - - ]: 0 : for (unsigned i = 0; i < d_regions_index; i++)
1289 : : {
1290 : 0 : Region* region = d_regions[i];
1291 [ - - ]: 0 : if (region->valid())
1292 : : {
1293 [ - - ]: 0 : Trace(c) << "Region #" << i << ": " << std::endl;
1294 : 0 : region->debugPrint(c, true);
1295 [ - - ]: 0 : Trace(c) << std::endl;
1296 [ - - ]: 0 : for (Region::iterator it = region->begin(); it != region->end(); ++it)
1297 : : {
1298 [ - - ]: 0 : if (it->second->valid())
1299 : : {
1300 [ - - ]: 0 : if (d_regions_map[it->first] != (int)i)
1301 : : {
1302 [ - - ]: 0 : Trace(c) << "***Bad regions map : " << it->first << " "
1303 : 0 : << d_regions_map[it->first].get() << std::endl;
1304 : : }
1305 : : }
1306 : : }
1307 : 0 : debugReps += region->getNumReps();
1308 : : }
1309 : : }
1310 : :
1311 [ - - ]: 0 : if (debugReps != d_reps)
1312 : : {
1313 [ - - ]: 0 : Trace(c) << "***Bad reps: " << d_reps << ", "
1314 : 0 : << "actual = " << debugReps << std::endl;
1315 : : }
1316 : : }
1317 : 14140 : }
1318 : :
1319 : 2040 : bool SortModel::checkLastCall()
1320 : : {
1321 : 2040 : TheoryModel* m = d_state.getModel();
1322 [ - + ]: 2040 : if (TraceIsOn("uf-ss-warn"))
1323 : : {
1324 : 0 : std::vector<Node> eqcs;
1325 : : eq::EqClassesIterator eqcs_i =
1326 : 0 : eq::EqClassesIterator(m->getEqualityEngine());
1327 [ - - ]: 0 : while (!eqcs_i.isFinished())
1328 : : {
1329 : 0 : Node eqc = (*eqcs_i);
1330 [ - - ]: 0 : if (eqc.getType() == d_type)
1331 : : {
1332 [ - - ]: 0 : if (std::find(eqcs.begin(), eqcs.end(), eqc) == eqcs.end())
1333 : : {
1334 : 0 : eqcs.push_back(eqc);
1335 : : // we must ensure that this equivalence class has been accounted for
1336 [ - - ]: 0 : if (d_regions_map.find(eqc) == d_regions_map.end())
1337 : : {
1338 [ - - ]: 0 : Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc
1339 : 0 : << " unaccounted for." << std::endl;
1340 [ - - ]: 0 : Trace("uf-ss-warn") << " type : " << d_type << std::endl;
1341 [ - - ]: 0 : Trace("uf-ss-warn") << " kind : " << eqc.getKind() << std::endl;
1342 : : }
1343 : : }
1344 : : }
1345 : 0 : ++eqcs_i;
1346 : 0 : }
1347 : 0 : }
1348 : 2040 : RepSet* rs = m->getRepSetPtr();
1349 : 2040 : size_t nReps = rs->getNumRepresentatives(d_type);
1350 [ + + ]: 2040 : if (nReps != d_maxNegCard + 1)
1351 : : {
1352 [ + - ]: 72 : Trace("uf-ss-warn") << "WARNING : Model does not have same # "
1353 : 0 : "representatives as cardinality for "
1354 : 36 : << d_type << "." << std::endl;
1355 [ + - ]: 72 : Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard
1356 : 36 : << std::endl;
1357 [ + - ]: 36 : Trace("uf-ss-warn") << " # Reps : " << nReps << std::endl;
1358 [ + - ]: 36 : if (d_maxNegCard >= nReps)
1359 : : {
1360 [ + + ]: 324 : while (d_fresh_aloc_reps.size() <= d_maxNegCard)
1361 : : {
1362 : 288 : std::stringstream ss;
1363 : 288 : ss << "r_" << d_type;
1364 : 288 : Node nn = NodeManager::mkDummySkolem(ss.str(), d_type);
1365 : 288 : d_fresh_aloc_reps.push_back(nn);
1366 : 288 : }
1367 [ + + ]: 36 : if (d_maxNegCard == 0)
1368 : : {
1369 : 6 : rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]);
1370 : : }
1371 : : else
1372 : : {
1373 : : // must add lemma
1374 : 30 : std::vector<Node> force_cl;
1375 [ + + ]: 312 : for (size_t i = 0; i <= d_maxNegCard; i++)
1376 : : {
1377 [ + + ]: 2428 : for (size_t j = (i + 1); j <= d_maxNegCard; j++)
1378 : : {
1379 : 2146 : force_cl.push_back(
1380 : 4292 : d_fresh_aloc_reps[i].eqNode(d_fresh_aloc_reps[j]).negate());
1381 : : }
1382 : : }
1383 : 30 : Node cl = getCardinalityLiteral(d_maxNegCard);
1384 : : Node lem =
1385 : 60 : NodeManager::mkNode(Kind::OR, cl, nodeManager()->mkAnd(force_cl));
1386 [ + - ]: 60 : Trace("uf-ss-lemma")
1387 : 0 : << "*** Enforce negative cardinality constraint lemma : " << lem
1388 : 30 : << std::endl;
1389 : 30 : d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE);
1390 : 30 : return false;
1391 : 30 : }
1392 : : }
1393 : : }
1394 : 2010 : return true;
1395 : : }
1396 : :
1397 : 0 : int SortModel::getNumRegions()
1398 : : {
1399 : 0 : int count = 0;
1400 [ - - ]: 0 : for (int i = 0; i < (int)d_regions_index; i++)
1401 : : {
1402 [ - - ]: 0 : if (d_regions[i]->valid())
1403 : : {
1404 : 0 : count++;
1405 : : }
1406 : : }
1407 : 0 : return count;
1408 : : }
1409 : :
1410 : 15747 : Node SortModel::getCardinalityLiteral(uint32_t c)
1411 : : {
1412 [ - + ][ - + ]: 15747 : Assert(c > 0);
[ - - ]
1413 : 15747 : std::map<uint32_t, Node>::iterator itcl = d_cardinality_literal.find(c);
1414 [ + + ]: 15747 : if (itcl != d_cardinality_literal.end())
1415 : : {
1416 : 14179 : return itcl->second;
1417 : : }
1418 : : // get the literal from the decision strategy
1419 : 1568 : Node lit = d_c_dec_strat->getLiteral(c - 1);
1420 : 1568 : d_cardinality_literal[c] = lit;
1421 : :
1422 : : // return the literal
1423 : 1568 : return lit;
1424 : 1568 : }
1425 : :
1426 : 741 : CardinalityExtension::CardinalityExtension(Env& env,
1427 : : TheoryState& state,
1428 : : TheoryInferenceManager& im,
1429 : 741 : TheoryUF* th)
1430 : : : EnvObj(env),
1431 : 741 : d_statistics(statisticsRegistry()),
1432 : 741 : d_state(state),
1433 : 741 : d_im(im),
1434 : 741 : d_th(th),
1435 : 741 : d_rep_model(),
1436 : 741 : d_min_pos_com_card(context(), 0),
1437 : 741 : d_min_pos_com_card_set(context(), false),
1438 : 741 : d_cc_dec_strat(nullptr),
1439 : 741 : d_initializedCombinedCardinality(userContext(), false),
1440 : 741 : d_card_assertions_eqv_lemma(userContext()),
1441 : 741 : d_min_pos_tn_master_card(context(), 0),
1442 : 741 : d_min_pos_tn_master_card_set(context(), false),
1443 : 1482 : d_rel_eqc(context())
1444 : : {
1445 : 741 : if (options().uf.ufssMode == options::UfssMode::FULL
1446 [ + + ][ + - ]: 741 : && options().uf.ufssFairness)
[ + + ]
1447 : : {
1448 : : // Register the strategy with the decision manager of the theory.
1449 : : // We are guaranteed that the decision manager is ready since we
1450 : : // construct this module during TheoryUF::finishInit.
1451 : 727 : d_cc_dec_strat.reset(
1452 : 727 : new CombinedCardinalityDecisionStrategy(env, th->getValuation()));
1453 : : }
1454 : 741 : }
1455 : :
1456 : 1478 : CardinalityExtension::~CardinalityExtension()
1457 : : {
1458 : 739 : for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1459 [ + + ]: 1459 : it != d_rep_model.end();
1460 : 720 : ++it)
1461 : : {
1462 [ + - ]: 720 : delete it->second;
1463 : : }
1464 : 1478 : }
1465 : :
1466 : : /** ensure eqc */
1467 : 0 : void CardinalityExtension::ensureEqc(SortModel* c, Node a)
1468 : : {
1469 [ - - ]: 0 : if (!hasEqc(a))
1470 : : {
1471 : 0 : d_rel_eqc[a] = true;
1472 [ - - ]: 0 : Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
1473 : 0 : << a.getType() << std::endl;
1474 : 0 : c->newEqClass(a);
1475 [ - - ]: 0 : Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1476 : 0 : << std::endl;
1477 : : }
1478 : 0 : }
1479 : :
1480 : 0 : void CardinalityExtension::ensureEqcRec(Node n)
1481 : : {
1482 [ - - ]: 0 : if (!hasEqc(n))
1483 : : {
1484 : 0 : SortModel* c = getSortModel(n);
1485 [ - - ]: 0 : if (c)
1486 : : {
1487 : 0 : ensureEqc(c, n);
1488 : : }
1489 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
1490 : : {
1491 : 0 : ensureEqcRec(n[i]);
1492 : : }
1493 : : }
1494 : 0 : }
1495 : :
1496 : : /** has eqc */
1497 : 0 : bool CardinalityExtension::hasEqc(Node a)
1498 : : {
1499 : 0 : NodeBoolMap::iterator it = d_rel_eqc.find(a);
1500 : 0 : return it != d_rel_eqc.end() && (*it).second;
1501 : : }
1502 : :
1503 : : /** new node */
1504 : 54045 : void CardinalityExtension::newEqClass(Node a)
1505 : : {
1506 : 54045 : SortModel* c = getSortModel(a);
1507 [ + + ]: 54045 : if (c)
1508 : : {
1509 [ + - ]: 15356 : Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
1510 [ - + ][ - - ]: 7678 : << a.getType() << std::endl;
1511 : 7678 : c->newEqClass(a);
1512 [ + - ]: 15356 : Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1513 : 7678 : << std::endl;
1514 : : }
1515 : 54045 : }
1516 : :
1517 : : /** merge */
1518 : 354431 : void CardinalityExtension::merge(Node a, Node b)
1519 : : {
1520 : : // TODO: ensure they are relevant
1521 : 354431 : SortModel* c = getSortModel(a);
1522 [ + + ]: 354431 : if (c)
1523 : : {
1524 [ + - ]: 97840 : Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b
1525 [ - + ][ - - ]: 48920 : << " : " << a.getType() << std::endl;
1526 : 48920 : c->merge(a, b);
1527 [ + - ]: 48920 : Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
1528 : : }
1529 : 354431 : }
1530 : :
1531 : : /** assert terms are disequal */
1532 : 40556 : void CardinalityExtension::assertDisequal(Node a, Node b, Node reason)
1533 : : {
1534 : 40556 : SortModel* c = getSortModel(a);
1535 [ + + ]: 40556 : if (c)
1536 : : {
1537 [ + - ]: 42972 : Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a
1538 [ - + ][ - - ]: 21486 : << " " << b << " : " << a.getType() << std::endl;
1539 : 21486 : c->assertDisequal(a, b, reason);
1540 [ + - ]: 42972 : Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal."
1541 : 21486 : << std::endl;
1542 : : }
1543 : 40556 : }
1544 : :
1545 : : /** assert a node */
1546 : 254447 : void CardinalityExtension::assertNode(Node n, bool isDecision)
1547 : : {
1548 [ + - ]: 254447 : Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
1549 : 254447 : bool polarity = n.getKind() != Kind::NOT;
1550 [ + + ]: 254447 : TNode lit = polarity ? n : n[0];
1551 [ + + ]: 254447 : if (options().uf.ufssMode == options::UfssMode::FULL)
1552 : : {
1553 [ + + ]: 187632 : if (lit.getKind() == Kind::CARDINALITY_CONSTRAINT)
1554 : : {
1555 : : const CardinalityConstraint& cc =
1556 : 12950 : lit.getOperator().getConst<CardinalityConstraint>();
1557 : 12950 : TypeNode tn = cc.getType();
1558 [ - + ][ - + ]: 12950 : Assert(tn.isUninterpretedSort());
[ - - ]
1559 [ - + ][ - + ]: 12950 : Assert(d_rep_model[tn]);
[ - - ]
1560 : 12950 : uint32_t nCard = cc.getUpperBound().getUnsignedInt();
1561 [ + - ]: 25900 : Trace("uf-ss-debug") << "...check cardinality constraint : " << tn
1562 : 12950 : << std::endl;
1563 [ + - ]: 12950 : Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
1564 : 12950 : d_rep_model[tn]->assertCardinality(nCard, polarity);
1565 : : // check if combined cardinality is violated
1566 : 12950 : checkCombinedCardinality();
1567 : 12950 : }
1568 [ + + ]: 174682 : else if (lit.getKind() == Kind::COMBINED_CARDINALITY_CONSTRAINT)
1569 : : {
1570 [ + + ]: 7204 : if (polarity)
1571 : : {
1572 : : // safe to assume int here
1573 : : const CombinedCardinalityConstraint& cc =
1574 : 5755 : lit.getOperator().getConst<CombinedCardinalityConstraint>();
1575 : 5755 : uint32_t nCard = cc.getUpperBound().getUnsignedInt();
1576 [ - + ][ - - ]: 5755 : if (!d_min_pos_com_card_set.get() || nCard < d_min_pos_com_card.get())
[ + - ]
1577 : : {
1578 : 5755 : d_min_pos_com_card_set.set(true);
1579 : 5755 : d_min_pos_com_card.set(nCard);
1580 : 5755 : checkCombinedCardinality();
1581 : : }
1582 : : }
1583 : : }
1584 : : else
1585 : : {
1586 [ - + ]: 167478 : if (TraceIsOn("uf-ss-warn"))
1587 : : {
1588 : : ////FIXME: this is too strict: theory propagations are showing up as
1589 : : /// isDecision=true, but / a theory propagation is not a decision.
1590 [ - - ]: 0 : if (isDecision)
1591 : : {
1592 : 0 : for (std::map<TypeNode, SortModel*>::iterator it =
1593 : 0 : d_rep_model.begin();
1594 [ - - ]: 0 : it != d_rep_model.end();
1595 : 0 : ++it)
1596 : : {
1597 [ - - ]: 0 : if (!it->second->hasCardinalityAsserted())
1598 : : {
1599 [ - - ]: 0 : Trace("uf-ss-warn") << "WARNING: Assert " << n
1600 : 0 : << " as a decision before cardinality for "
1601 : 0 : << it->first << "." << std::endl;
1602 : : }
1603 : : }
1604 : : }
1605 : : }
1606 : : }
1607 : : }
1608 : : else
1609 : : {
1610 : 66815 : if (lit.getKind() == Kind::CARDINALITY_CONSTRAINT
1611 [ + + ][ - + ]: 66815 : || lit.getKind() == Kind::COMBINED_CARDINALITY_CONSTRAINT)
[ + + ]
1612 : : {
1613 : : // cardinality constraint from user input, set incomplete
1614 [ + - ]: 4 : Trace("uf-ss")
1615 : 0 : << "Literal " << lit
1616 : 0 : << " not handled when uf ss mode is not FULL, set incomplete."
1617 : 2 : << std::endl;
1618 : 2 : d_im.setModelUnsound(IncompleteId::UF_CARD_MODE);
1619 : : }
1620 : : }
1621 [ + - ]: 254447 : Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
1622 : 254447 : }
1623 : :
1624 : 0 : bool CardinalityExtension::areDisequal(Node a, Node b)
1625 : : {
1626 [ - - ]: 0 : if (a == b)
1627 : : {
1628 : 0 : return false;
1629 : : }
1630 : 0 : eq::EqualityEngine* ee = d_th->getEqualityEngine();
1631 : 0 : a = ee->getRepresentative(a);
1632 : 0 : b = ee->getRepresentative(b);
1633 [ - - ]: 0 : if (ee->areDisequal(a, b, false))
1634 : : {
1635 : 0 : return true;
1636 : : }
1637 : 0 : SortModel* c = getSortModel(a);
1638 [ - - ]: 0 : if (c)
1639 : : {
1640 : 0 : return c->areDisequal(a, b);
1641 : : }
1642 : 0 : return false;
1643 : : }
1644 : :
1645 : : /** check */
1646 : 120648 : void CardinalityExtension::check(Theory::Effort level)
1647 : : {
1648 [ + + ]: 120648 : if (level == Theory::EFFORT_LAST_CALL)
1649 : : {
1650 : : // if last call, call last call check for each sort
1651 [ + + ]: 3641 : for (std::pair<const TypeNode, SortModel*>& r : d_rep_model)
1652 : : {
1653 [ + + ]: 2040 : if (!r.second->checkLastCall())
1654 : : {
1655 : 30 : break;
1656 : : }
1657 : : }
1658 : 1631 : return;
1659 : : }
1660 [ + - ]: 119017 : if (!d_state.isInConflict())
1661 : : {
1662 [ + + ]: 119017 : if (options().uf.ufssMode == options::UfssMode::FULL)
1663 : : {
1664 [ + - ]: 168746 : Trace("uf-ss-solver")
1665 : 84373 : << "CardinalityExtension: check " << level << std::endl;
1666 [ + + ]: 84373 : if (level == Theory::EFFORT_FULL)
1667 : : {
1668 [ - + ]: 6916 : if (TraceIsOn("uf-ss-debug"))
1669 : : {
1670 : 0 : debugPrint("uf-ss-debug");
1671 : : }
1672 [ - + ]: 6916 : if (TraceIsOn("uf-ss-state"))
1673 : : {
1674 [ - - ]: 0 : Trace("uf-ss-state")
1675 : 0 : << "CardinalityExtension::check " << level << std::endl;
1676 [ - - ]: 0 : for (std::pair<const TypeNode, SortModel*>& rm : d_rep_model)
1677 : : {
1678 [ - - ]: 0 : Trace("uf-ss-state") << " " << rm.first << " has cardinality "
1679 : 0 : << rm.second->getCardinality() << std::endl;
1680 : : }
1681 : : }
1682 : : }
1683 : 84373 : for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1684 [ + + ]: 416344 : it != d_rep_model.end();
1685 : 331971 : ++it)
1686 : : {
1687 : 331971 : it->second->check(level);
1688 [ - + ]: 331971 : if (d_state.isInConflict())
1689 : : {
1690 : 0 : break;
1691 : : }
1692 : : }
1693 : : }
1694 [ + - ]: 34644 : else if (options().uf.ufssMode == options::UfssMode::NO_MINIMAL)
1695 : : {
1696 [ + + ]: 34644 : if (level == Theory::EFFORT_FULL)
1697 : : {
1698 : : // split on an equality between two equivalence classes (at most one per
1699 : : // type)
1700 : 918 : std::map<TypeNode, std::vector<Node> > eqc_list;
1701 : 918 : std::map<TypeNode, bool> type_proc;
1702 : 918 : eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine());
1703 [ + + ]: 78838 : while (!eqcs_i.isFinished())
1704 : : {
1705 : 77920 : Node a = *eqcs_i;
1706 : 77920 : TypeNode tn = a.getType();
1707 [ + + ]: 77920 : if (tn.isUninterpretedSort())
1708 : : {
1709 [ + + ]: 12032 : if (type_proc.find(tn) == type_proc.end())
1710 : : {
1711 : : std::map<TypeNode, std::vector<Node> >::iterator itel =
1712 : 9898 : eqc_list.find(tn);
1713 [ + + ]: 9898 : if (itel != eqc_list.end())
1714 : : {
1715 [ + + ]: 16873 : for (unsigned j = 0; j < itel->second.size(); j++)
1716 : : {
1717 : 11547 : Node b = itel->second[j];
1718 [ + + ]: 11547 : if (!d_th->getEqualityEngine()->areDisequal(a, b, false))
1719 : : {
1720 : 1862 : Node eq = rewrite(a.eqNode(b));
1721 : 1862 : Node lem = NodeManager::mkNode(Kind::OR, eq, eq.negate());
1722 [ + - ]: 1862 : Trace("uf-ss-lemma")
1723 : 931 : << "*** Split (no-minimal) : " << lem << std::endl;
1724 : 931 : d_im.lemma(lem, InferenceId::UF_CARD_SPLIT);
1725 : 931 : d_im.preferPhase(eq, true);
1726 : 931 : type_proc[tn] = true;
1727 : 931 : break;
1728 : 931 : }
1729 [ + + ]: 11547 : }
1730 : : }
1731 : 9898 : eqc_list[tn].push_back(a);
1732 : : }
1733 : : }
1734 : 77920 : ++eqcs_i;
1735 : 77920 : }
1736 : 918 : }
1737 : : }
1738 : : else
1739 : : {
1740 : : // unhandled uf ss mode
1741 : 0 : DebugUnhandled();
1742 : : }
1743 [ + - ]: 238034 : Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
1744 : 119017 : << std::endl;
1745 : : }
1746 : : }
1747 : :
1748 : 740 : void CardinalityExtension::presolve()
1749 : : {
1750 : 740 : d_initializedCombinedCardinality = false;
1751 : 740 : for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1752 [ + + ]: 1177 : it != d_rep_model.end();
1753 : 437 : ++it)
1754 : : {
1755 : 437 : it->second->presolve();
1756 : 437 : it->second->initialize();
1757 : : }
1758 : 740 : }
1759 : :
1760 : 727 : CardinalityExtension::CombinedCardinalityDecisionStrategy::
1761 : 727 : CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation)
1762 : 727 : : DecisionStrategyFmf(env, valuation)
1763 : : {
1764 : 727 : }
1765 : 1273 : Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
1766 : : unsigned i)
1767 : : {
1768 : 1273 : NodeManager* nm = nodeManager();
1769 : 2546 : Node cco = nm->mkConst(CombinedCardinalityConstraint(Integer(i)));
1770 : 2546 : return nm->mkNode(Kind::COMBINED_CARDINALITY_CONSTRAINT, cco);
1771 : 1273 : }
1772 : :
1773 : : std::string
1774 : 0 : CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
1775 : : {
1776 : 0 : return std::string("uf_combined_card");
1777 : : }
1778 : :
1779 : 431161 : void CardinalityExtension::preRegisterTerm(TNode n)
1780 : : {
1781 [ + + ]: 431161 : if (options().uf.ufssMode != options::UfssMode::FULL)
1782 : : {
1783 : 407063 : return;
1784 : : }
1785 : : // initialize combined cardinality
1786 : 302367 : initializeCombinedCardinality();
1787 : :
1788 [ + - ]: 302367 : Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
1789 : : // shouldn't have to preregister this type (it may be that there are no
1790 : : // quantifiers over tn)
1791 : 302367 : TypeNode tn;
1792 [ + + ]: 302367 : if (n.getKind() == Kind::CARDINALITY_CONSTRAINT)
1793 : : {
1794 : : const CardinalityConstraint& cc =
1795 : 16680 : n.getOperator().getConst<CardinalityConstraint>();
1796 : 16680 : tn = cc.getType();
1797 : : }
1798 : : else
1799 : : {
1800 : 285687 : tn = n.getType();
1801 : : }
1802 [ + + ]: 302367 : if (!tn.isUninterpretedSort())
1803 : : {
1804 : 278269 : return;
1805 : : }
1806 : 24098 : std::map<TypeNode, SortModel*>::iterator it = d_rep_model.find(tn);
1807 [ + + ]: 24098 : if (it == d_rep_model.end())
1808 : : {
1809 : 722 : SortModel* rm = nullptr;
1810 [ + - ]: 722 : if (tn.isUninterpretedSort())
1811 : : {
1812 [ + - ]: 722 : Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
1813 : 722 : rm = new SortModel(d_env, tn, d_state, d_im, this);
1814 : : }
1815 [ + - ]: 722 : if (rm)
1816 : : {
1817 : 722 : rm->initialize();
1818 : 722 : d_rep_model[tn] = rm;
1819 : : // d_rep_model_init[tn] = true;
1820 : : }
1821 : : }
1822 : : else
1823 : : {
1824 : : // ensure sort model is initialized
1825 : 23376 : it->second->initialize();
1826 : : }
1827 [ + + ]: 302367 : }
1828 : :
1829 : 449032 : SortModel* CardinalityExtension::getSortModel(Node n)
1830 : : {
1831 : 449032 : TypeNode tn = n.getType();
1832 : 449032 : std::map<TypeNode, SortModel*>::iterator it = d_rep_model.find(tn);
1833 : : // pre-register the type if not done already
1834 [ + + ]: 449032 : if (it == d_rep_model.end())
1835 : : {
1836 : 370948 : preRegisterTerm(n);
1837 : 370948 : it = d_rep_model.find(tn);
1838 : : }
1839 [ + + ]: 449032 : if (it != d_rep_model.end())
1840 : : {
1841 : 78084 : return it->second;
1842 : : }
1843 : : else
1844 : : {
1845 : 370948 : return nullptr;
1846 : : }
1847 : 449032 : }
1848 : :
1849 : : /** get cardinality for sort */
1850 : 0 : int CardinalityExtension::getCardinality(Node n)
1851 : : {
1852 : 0 : SortModel* c = getSortModel(n);
1853 [ - - ]: 0 : if (c)
1854 : : {
1855 : 0 : return c->getCardinality();
1856 : : }
1857 : : else
1858 : : {
1859 : 0 : return -1;
1860 : : }
1861 : : }
1862 : :
1863 : 0 : int CardinalityExtension::getCardinality(TypeNode tn)
1864 : : {
1865 : 0 : std::map<TypeNode, SortModel*>::iterator it = d_rep_model.find(tn);
1866 [ - - ][ - - ]: 0 : if (it != d_rep_model.end() && it->second)
[ - - ]
1867 : : {
1868 : 0 : return it->second->getCardinality();
1869 : : }
1870 : 0 : return -1;
1871 : : }
1872 : :
1873 : : // print debug
1874 : 0 : void CardinalityExtension::debugPrint(const char* c)
1875 : : {
1876 : 0 : for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1877 [ - - ]: 0 : it != d_rep_model.end();
1878 : 0 : ++it)
1879 : : {
1880 [ - - ]: 0 : Trace(c) << "Conflict find structure for " << it->first << ": "
1881 : 0 : << std::endl;
1882 : 0 : it->second->debugPrint(c);
1883 [ - - ]: 0 : Trace(c) << std::endl;
1884 : : }
1885 : 0 : }
1886 : :
1887 : : /** initialize */
1888 : 302367 : void CardinalityExtension::initializeCombinedCardinality()
1889 : : {
1890 : 302367 : if (d_cc_dec_strat.get() != nullptr
1891 [ + - ][ + + ]: 302367 : && !d_initializedCombinedCardinality.get())
[ + + ]
1892 : : {
1893 : 745 : d_initializedCombinedCardinality = true;
1894 : 1490 : d_im.getDecisionManager()->registerStrategy(
1895 : 745 : DecisionManager::STRAT_UF_COMBINED_CARD, d_cc_dec_strat.get());
1896 : : }
1897 : 302367 : }
1898 : :
1899 : : /** check */
1900 : 18705 : void CardinalityExtension::checkCombinedCardinality()
1901 : : {
1902 [ - + ][ - + ]: 18705 : Assert(options().uf.ufssMode == options::UfssMode::FULL);
[ - - ]
1903 [ + - ]: 18705 : if (options().uf.ufssFairness)
1904 : : {
1905 [ + - ]: 37410 : Trace("uf-ss-com-card-debug")
1906 : 0 : << "Check combined cardinality, get maximum negative cardinalities..."
1907 : 18705 : << std::endl;
1908 : 18705 : uint32_t totalCombinedCard = 0;
1909 : 18705 : TypeNode maxSlaveType;
1910 : 18705 : for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1911 [ + + ]: 105571 : it != d_rep_model.end();
1912 : 86866 : ++it)
1913 : : {
1914 : 86866 : uint32_t max_neg = it->second->getMaximumNegativeCardinality();
1915 : 86866 : totalCombinedCard += max_neg;
1916 : : }
1917 [ + - ]: 37410 : Trace("uf-ss-com-card-debug")
1918 : 0 : << "Check combined cardinality, total combined card : "
1919 : 18705 : << totalCombinedCard << std::endl;
1920 : 18705 : uint32_t cc = d_min_pos_com_card.get();
1921 [ + + ][ + + ]: 18705 : if (d_min_pos_com_card_set.get() && totalCombinedCard > cc)
[ + + ]
1922 : : {
1923 : : // conflict
1924 : 1060 : Node com_lit = d_cc_dec_strat->getLiteral(cc);
1925 : 1060 : std::vector<Node> conf;
1926 : 1060 : conf.push_back(com_lit);
1927 : 1060 : uint32_t totalAdded = 0;
1928 : 1060 : for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1929 [ + - ]: 3185 : it != d_rep_model.end();
1930 : 2125 : ++it)
1931 : : {
1932 : 3185 : uint32_t c = it->second->getMaximumNegativeCardinality();
1933 [ + + ]: 3185 : if (c > 0)
1934 : : {
1935 : 2309 : conf.push_back(it->second->getCardinalityLiteral(c).negate());
1936 : 2309 : totalAdded += c;
1937 : : }
1938 [ + + ]: 3185 : if (totalAdded > cc)
1939 : : {
1940 : 1060 : break;
1941 : : }
1942 : : }
1943 : 1060 : Node cf = nodeManager()->mkNode(Kind::AND, conf);
1944 [ + - ]: 2120 : Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
1945 : 1060 : << std::endl;
1946 [ + - ]: 2120 : Trace("uf-ss-com-card")
1947 : 1060 : << "*** Combined cardinality conflict : " << cf << std::endl;
1948 : 1060 : d_im.conflict(cf, InferenceId::UF_CARD_COMBINED);
1949 : 1060 : }
1950 : 18705 : }
1951 : 18705 : }
1952 : :
1953 : 741 : CardinalityExtension::Statistics::Statistics(StatisticsRegistry& sr)
1954 : : : d_clique_conflicts(
1955 : 741 : sr.registerInt("CardinalityExtension::Clique_Conflicts")),
1956 : 741 : d_clique_lemmas(sr.registerInt("CardinalityExtension::Clique_Lemmas")),
1957 : 741 : d_split_lemmas(sr.registerInt("CardinalityExtension::Split_Lemmas")),
1958 : 741 : d_max_model_size(sr.registerInt("CardinalityExtension::Max_Model_Size"))
1959 : : {
1960 : 741 : d_max_model_size.maxAssign(1);
1961 : 741 : }
1962 : :
1963 : : } // namespace uf
1964 : : } // namespace theory
1965 : : } // namespace cvc5::internal
|
