Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Morgan Deters, Tim King
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 theory of UF with cardinality.
14 : : */
15 : :
16 : : #include "theory/uf/cardinality_extension.h"
17 : :
18 : : #include <sstream>
19 : :
20 : : #include "expr/cardinality_constraint.h"
21 : : #include "expr/skolem_manager.h"
22 : : #include "options/smt_options.h"
23 : : #include "options/uf_options.h"
24 : : #include "smt/logic_exception.h"
25 : : #include "theory/decision_manager.h"
26 : : #include "theory/quantifiers/term_database.h"
27 : : #include "theory/quantifiers_engine.h"
28 : : #include "theory/theory_engine.h"
29 : : #include "theory/theory_model.h"
30 : : #include "theory/uf/equality_engine.h"
31 : : #include "theory/uf/theory_uf.h"
32 : : #include "util/rational.h"
33 : :
34 : : using namespace std;
35 : : using namespace cvc5::internal::kind;
36 : : using namespace cvc5::context;
37 : :
38 : : namespace cvc5::internal {
39 : : namespace theory {
40 : : namespace uf {
41 : :
42 : : /* These are names are unambigious are we use abbreviations. */
43 : : typedef CardinalityExtension::SortModel SortModel;
44 : : typedef SortModel::Region Region;
45 : : typedef Region::RegionNodeInfo RegionNodeInfo;
46 : : typedef RegionNodeInfo::DiseqList DiseqList;
47 : :
48 : 3858 : Region::Region(SortModel* cf, context::Context* c)
49 : : : d_cf(cf),
50 : 0 : d_testCliqueSize(c, 0),
51 : 0 : d_splitsSize(c, 0),
52 : : d_testClique(c),
53 : : d_splits(c),
54 : 0 : d_reps_size(c, 0),
55 : 0 : d_total_diseq_external(c, 0),
56 : 0 : d_total_diseq_internal(c, 0),
57 : 3858 : d_valid(c, true)
58 : : {
59 : 3858 : }
60 : :
61 : 7716 : Region::~Region() {
62 [ + + ]: 18160 : for(iterator i = begin(), iend = end(); i != iend; ++i) {
63 : 14302 : RegionNodeInfo* regionNodeInfo = (*i).second;
64 [ + - ]: 14302 : delete regionNodeInfo;
65 : : }
66 : 3858 : d_nodes.clear();
67 : 7716 : }
68 : :
69 : 7603 : void Region::addRep( Node n ) {
70 : 7603 : setRep( n, true );
71 : 7603 : }
72 : :
73 : 850 : void Region::takeNode( Region* r, Node n ){
74 [ - + ][ - + ]: 850 : Assert(!hasRep(n));
[ - - ]
75 [ - + ][ - + ]: 850 : Assert(r->hasRep(n));
[ - - ]
76 : : //add representative
77 : 850 : setRep( n, true );
78 : : //take disequalities from r
79 : 850 : RegionNodeInfo* rni = r->d_nodes[n];
80 [ + + ]: 2550 : for( int t=0; t<2; t++ ){
81 : 1700 : DiseqList* del = rni->get(t);
82 [ + + ]: 4550 : for(DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
83 [ + + ]: 2850 : if( (*it).second ){
84 : 1689 : r->setDisequal( n, (*it).first, t, false );
85 [ + + ]: 1689 : if( t==0 ){
86 [ + + ]: 687 : if( hasRep( (*it).first ) ){
87 : 573 : setDisequal( (*it).first, n, 0, false );
88 : 573 : setDisequal( (*it).first, n, 1, true );
89 : 573 : setDisequal( n, (*it).first, 1, true );
90 : : }else{
91 : 114 : setDisequal( n, (*it).first, 0, true );
92 : : }
93 : : }else{
94 : 1002 : r->setDisequal( (*it).first, n, 1, false );
95 : 1002 : r->setDisequal( (*it).first, n, 0, true );
96 : 1002 : setDisequal( n, (*it).first, 0, true );
97 : : }
98 : : }
99 : : }
100 : : }
101 : : //remove representative
102 : 850 : r->setRep( n, false );
103 : 850 : }
104 : :
105 : 56379 : void Region::combine( Region* r ){
106 : : //take all nodes from r
107 [ + + ]: 292037 : for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it) {
108 [ + + ]: 235658 : if( it->second->valid() ){
109 : 59903 : setRep( it->first, true );
110 : : }
111 : : }
112 [ + + ]: 292037 : for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it){
113 [ + + ]: 235658 : if( it->second->valid() ){
114 : : //take disequalities from r
115 : 119806 : Node n = it->first;
116 : 59903 : RegionNodeInfo* rni = it->second;
117 [ + + ]: 179709 : for( int t=0; t<2; t++ ){
118 : 119806 : RegionNodeInfo::DiseqList* del = rni->get(t);
119 : 316845 : for( RegionNodeInfo::DiseqList::iterator it2 = del->begin(),
120 [ + + ]: 513884 : it2end = del->end(); it2 != it2end; ++it2 ){
121 [ + + ]: 197039 : if( (*it2).second ){
122 [ + + ][ + + ]: 184855 : if( t==0 && hasRep( (*it2).first ) ){
[ + + ][ + + ]
[ - - ]
123 : 89687 : setDisequal( (*it2).first, n, 0, false );
124 : 89687 : setDisequal( (*it2).first, n, 1, true );
125 : 89687 : setDisequal( n, (*it2).first, 1, true );
126 : : }else{
127 : 95168 : setDisequal( n, (*it2).first, t, true );
128 : : }
129 : : }
130 : : }
131 : : }
132 : : }
133 : : }
134 : 56379 : r->d_valid = false;
135 : 56379 : }
136 : :
137 : : /** setEqual */
138 : 43654 : void Region::setEqual( Node a, Node b ){
139 : 87308 : Assert(hasRep(a) && hasRep(b));
140 : : //move disequalities of b over to a
141 [ + + ]: 130962 : for( int t=0; t<2; t++ ){
142 : 87308 : DiseqList* del = d_nodes[b]->get(t);
143 [ + + ]: 195422 : for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
144 [ + + ]: 108114 : if( (*it).second ){
145 : 72021 : Node n = (*it).first;
146 : : //get the region that contains the endpoint of the disequality b != ...
147 : 72021 : Region* nr = d_cf->d_regions[ d_cf->d_regions_map[ n ] ];
148 [ + + ]: 72021 : if( !isDisequal( a, n, t ) ){
149 : 32411 : setDisequal( a, n, t, true );
150 : 32411 : nr->setDisequal( n, a, t, true );
151 : : }
152 : 72021 : setDisequal( b, n, t, false );
153 : 72021 : nr->setDisequal( n, b, t, false );
154 : : }
155 : : }
156 : : }
157 : : //remove b from representatives
158 : 43654 : setRep( b, false );
159 : 43654 : }
160 : :
161 : 620799 : void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
162 : : //Trace("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " "
163 : : // << type << " " << valid << std::endl;
164 : : //debugPrint("uf-ss-region-debug");
165 : : //Assert( isDisequal( n1, n2, type )!=valid );
166 [ + + ]: 620799 : if( isDisequal( n1, n2, type )!=valid ){ //DO_THIS: make assertion
167 : 619583 : d_nodes[ n1 ]->get(type)->setDisequal( n2, valid );
168 [ + + ]: 619583 : if( type==0 ){
169 [ + + ]: 251783 : d_total_diseq_external = d_total_diseq_external + ( valid ? 1 : -1 );
170 : : }else{
171 [ + + ]: 367800 : d_total_diseq_internal = d_total_diseq_internal + ( valid ? 1 : -1 );
172 [ + + ]: 367800 : if( valid ){
173 : : //if they are both a part of testClique, then remove split
174 [ + - ][ + + ]: 249720 : if( d_testClique.find( n1 )!=d_testClique.end() && d_testClique[n1] &&
175 [ + + ][ + - ]: 249720 : d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){
[ + + ]
176 : 7926 : Node eq = NodeManager::currentNM()->mkNode(Kind::EQUAL, n1, n2);
177 [ + + ][ + - ]: 2642 : if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){
[ + + ]
178 [ + - ]: 2616 : Trace("uf-ss-debug") << "removing split for " << n1 << " " << n2
179 : 1308 : << std::endl;
180 : 1308 : d_splits[ eq ] = false;
181 : 1308 : d_splitsSize = d_splitsSize - 1;
182 : : }
183 : : }
184 : : }
185 : : }
186 : : }
187 : 620799 : }
188 : :
189 : 112860 : void Region::setRep( Node n, bool valid ) {
190 [ - + ][ - + ]: 112860 : Assert(hasRep(n) != valid);
[ - - ]
191 [ + + ][ + + ]: 112860 : if( valid && d_nodes.find( n )==d_nodes.end() ){
[ + + ]
192 : 14302 : d_nodes[n] = new RegionNodeInfo(d_cf->d_thss->context());
193 : : }
194 : 112860 : d_nodes[n]->setValid(valid);
195 [ + + ]: 112860 : d_reps_size = d_reps_size + ( valid ? 1 : -1 );
196 : : //removing a member of the test clique from this region
197 [ + + ][ + - ]: 112860 : if( d_testClique.find( n ) != d_testClique.end() && d_testClique[n] ){
[ + + ]
198 [ - + ][ - + ]: 2407 : Assert(!valid);
[ - - ]
199 : 2407 : d_testClique[n] = false;
200 : 2407 : d_testCliqueSize = d_testCliqueSize - 1;
201 : : //remove all splits involving n
202 [ + + ]: 25090 : for( split_iterator it = begin_splits(); it != end_splits(); ++it ){
203 [ + + ]: 22683 : if( (*it).second ){
204 : 6695 : if( (*it).first[0]==n || (*it).first[1]==n ){
205 : 6639 : d_splits[ (*it).first ] = false;
206 : 6639 : d_splitsSize = d_splitsSize - 1;
207 : : }
208 : : }
209 : : }
210 : : }
211 : 112860 : }
212 : :
213 : 769759 : bool Region::isDisequal( Node n1, Node n2, int type ) {
214 : 769759 : RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->get(type);
215 : 769759 : return del->isSet(n2) && del->getDisequalityValue(n2);
216 : : }
217 : :
218 : : struct sortInternalDegree {
219 : : Region* r;
220 : 25414 : bool operator() (Node i, Node j) {
221 : 50828 : return (r->getRegionInfo(i)->getNumInternalDisequalities() >
222 : 50828 : r->getRegionInfo(j)->getNumInternalDisequalities());
223 : : }
224 : : };
225 : :
226 : : struct sortExternalDegree {
227 : : Region* r;
228 : : bool operator() (Node i,Node j) {
229 : : return (r->getRegionInfo(i)->getNumExternalDisequalities() >
230 : : r->getRegionInfo(j)->getNumExternalDisequalities());
231 : : }
232 : : };
233 : :
234 : : int gmcCount = 0;
235 : :
236 : 139193 : bool Region::getMustCombine( int cardinality ){
237 [ + + ]: 139193 : if (d_total_diseq_external >= static_cast<unsigned>(cardinality))
238 : : {
239 : : //The number of external disequalities is greater than or equal to
240 : : //cardinality. Thus, a clique of size cardinality+1 may exist
241 : : //between nodes in d_regions[i] and other regions Check if this is
242 : : //actually the case: must have n nodes with outgoing degree
243 : : //(cardinality+1-n) for some n>0
244 : 24135 : std::vector< int > degrees;
245 [ + + ]: 236933 : for( Region::iterator it = begin(); it != end(); ++it ){
246 : 225716 : RegionNodeInfo* rni = it->second;
247 [ + + ]: 225716 : if( rni->valid() ){
248 [ + + ]: 107902 : if( rni->getNumDisequalities() >= cardinality ){
249 : 81144 : int outDeg = rni->getNumExternalDisequalities();
250 [ + + ]: 81144 : if( outDeg>=cardinality ){
251 : : //we have 1 node of degree greater than (cardinality)
252 : 12918 : return true;
253 [ + + ]: 69261 : }else if( outDeg>=1 ){
254 : 59726 : degrees.push_back( outDeg );
255 [ + + ]: 59726 : if( (int)degrees.size()>=cardinality ){
256 : : //we have (cardinality) nodes of degree 1
257 : 1035 : return true;
258 : : }
259 : : }
260 : : }
261 : : }
262 : : }
263 : 11217 : gmcCount++;
264 [ + + ]: 11217 : if( gmcCount%100==0 ){
265 [ + - ]: 180 : Trace("gmc-count") << gmcCount << " " << cardinality
266 : 90 : << " sample : " << degrees.size() << std::endl;
267 : : }
268 : : //this should happen relatively infrequently....
269 : 11217 : std::sort( degrees.begin(), degrees.end() );
270 [ + + ]: 61036 : for( int i=0; i<(int)degrees.size(); i++ ){
271 [ + + ]: 51396 : if( degrees[i]>=cardinality+1-((int)degrees.size()-i) ){
272 : 1577 : return true;
273 : : }
274 : : }
275 : : }
276 : 124698 : return false;
277 : : }
278 : :
279 : 1109700 : bool Region::check( Theory::Effort level, int cardinality,
280 : : std::vector< Node >& clique ) {
281 [ + + ]: 1109700 : if( d_reps_size>unsigned(cardinality) ){
282 [ + + ]: 102317 : if( d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){
283 [ + + ]: 64602 : if( d_reps_size>1 ){
284 : : //quick clique check, all reps form a clique
285 [ + + ]: 31030 : for( iterator it = begin(); it != end(); ++it ){
286 [ + + ]: 27067 : if( it->second->valid() ){
287 : 20095 : clique.push_back( it->first );
288 : : }
289 : : }
290 [ + - ]: 3963 : Trace("quick-clique") << "Found quick clique" << std::endl;
291 : 3963 : return true;
292 : : }else{
293 : 60639 : return false;
294 : : }
295 : : }
296 [ + + ]: 37715 : else if (level==Theory::EFFORT_FULL)
297 : : {
298 : : //build test clique, up to size cardinality+1
299 [ + + ]: 3061 : if( d_testCliqueSize<=unsigned(cardinality) ){
300 : 5884 : std::vector< Node > newClique;
301 [ + + ]: 2942 : if( d_testCliqueSize<unsigned(cardinality) ){
302 [ + + ]: 23601 : for( iterator it = begin(); it != end(); ++it ){
303 : : //if not in the test clique, add it to the set of new members
304 [ + + ][ + + ]: 34664 : if( it->second->valid() &&
305 [ + + ]: 34660 : ( d_testClique.find( it->first ) == d_testClique.end() ||
306 [ - + ]: 4 : !d_testClique[ it->first ] ) ){
307 : : //if( it->second->getNumInternalDisequalities()>cardinality ||
308 : : // level==Theory::EFFORT_FULL ){
309 : 13547 : newClique.push_back( it->first );
310 : : //}
311 : : }
312 : : }
313 : : //choose remaining nodes with the highest degrees
314 : : sortInternalDegree sidObj;
315 : 2492 : sidObj.r = this;
316 : 2492 : std::sort( newClique.begin(), newClique.end(), sidObj );
317 : 2492 : int offset = ( cardinality - d_testCliqueSize ) + 1;
318 : 2492 : newClique.erase( newClique.begin() + offset, newClique.end() );
319 : : }else{
320 : : //scan for the highest degree
321 : 450 : int maxDeg = -1;
322 : 900 : Node maxNode;
323 : 5785 : for( std::map< Node, RegionNodeInfo* >::iterator
324 [ + + ]: 12020 : it = d_nodes.begin(); it != d_nodes.end(); ++it ){
325 : : //if not in the test clique, add it to the set of new members
326 [ + + ][ + + ]: 12415 : if( it->second->valid() &&
327 [ + + ]: 9333 : ( d_testClique.find( it->first )==d_testClique.end() ||
328 [ - + ]: 3082 : !d_testClique[ it->first ] ) ){
329 [ + + ]: 466 : if( it->second->getNumInternalDisequalities()>maxDeg ){
330 : 450 : maxDeg = it->second->getNumInternalDisequalities();
331 : 450 : maxNode = it->first;
332 : : }
333 : : }
334 : : }
335 [ - + ][ - + ]: 450 : Assert(maxNode != Node::null());
[ - - ]
336 : 450 : newClique.push_back( maxNode );
337 : : }
338 : : //check splits internal to new members
339 [ + + ]: 16816 : for( int j=0; j<(int)newClique.size(); j++ ){
340 [ + - ]: 27748 : Trace("uf-ss-debug") << "Choose to add clique member "
341 : 13874 : << newClique[j] << std::endl;
342 [ + + ]: 67134 : for( int k=(j+1); k<(int)newClique.size(); k++ ){
343 [ + + ]: 53260 : if( !isDisequal( newClique[j], newClique[k], 1 ) ){
344 : 12642 : Node at_j = newClique[j];
345 : 12642 : Node at_k = newClique[k];
346 : : Node j_eq_k =
347 : 12642 : NodeManager::currentNM()->mkNode(Kind::EQUAL, at_j, at_k);
348 : 6321 : d_splits[ j_eq_k ] = true;
349 : 6321 : d_splitsSize = d_splitsSize + 1;
350 : : }
351 : : }
352 : : //check disequalities with old members
353 : 18559 : for( NodeBoolMap::iterator it = d_testClique.begin();
354 [ + + ]: 23244 : it != d_testClique.end(); ++it ){
355 [ + + ]: 4685 : if( (*it).second ){
356 [ + + ]: 3090 : if( !isDisequal( (*it).first, newClique[j], 1 ) ){
357 : 3804 : Node at_it = (*it).first;
358 : 3804 : Node at_j = newClique[j];
359 : 1902 : Node it_eq_j = at_it.eqNode(at_j);
360 : 1902 : d_splits[ it_eq_j ] = true;
361 : 1902 : d_splitsSize = d_splitsSize + 1;
362 : : }
363 : : }
364 : : }
365 : : }
366 : : //add new clique members to test clique
367 [ + + ]: 16816 : for( int j=0; j<(int)newClique.size(); j++ ){
368 : 13874 : d_testClique[ newClique[j] ] = true;
369 : 13874 : d_testCliqueSize = d_testCliqueSize + 1;
370 : : }
371 : : }
372 : : // Check if test clique has larger size than cardinality, and
373 : : // forms a clique.
374 [ + - ][ + + ]: 3061 : if( d_testCliqueSize >= unsigned(cardinality+1) && d_splitsSize==0 ){
[ + + ]
375 : : //test clique is a clique
376 : 137 : for( NodeBoolMap::iterator it = d_testClique.begin();
377 [ + + ]: 235 : it != d_testClique.end(); ++it ){
378 [ + - ]: 98 : if( (*it).second ){
379 : 98 : clique.push_back( (*it).first );
380 : : }
381 : : }
382 : 39 : return true;
383 : : }
384 : : }
385 : : }
386 : 1045050 : return false;
387 : : }
388 : :
389 : 0 : void Region::getNumExternalDisequalities(
390 : : std::map< Node, int >& num_ext_disequalities ){
391 [ - - ]: 0 : for( Region::iterator it = begin(); it != end(); ++it ){
392 : 0 : RegionNodeInfo* rni = it->second;
393 [ - - ]: 0 : if( rni->valid() ){
394 : 0 : DiseqList* del = rni->get(0);
395 [ - - ]: 0 : for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
396 [ - - ]: 0 : if( (*it2).second ){
397 : 0 : num_ext_disequalities[ (*it2).first ]++;
398 : : }
399 : : }
400 : : }
401 : : }
402 : 0 : }
403 : :
404 : 3745 : void Region::debugPrint( const char* c, bool incClique ) {
405 [ + - ]: 3745 : Trace( c ) << "Num reps: " << d_reps_size << std::endl;
406 [ + + ]: 10773 : for( Region::iterator it = begin(); it != end(); ++it ){
407 : 7028 : RegionNodeInfo* rni = it->second;
408 [ - + ]: 7028 : if( rni->valid() ){
409 : 0 : Node n = it->first;
410 [ - - ]: 0 : Trace( c ) << " " << n << std::endl;
411 [ - - ]: 0 : for( int i=0; i<2; i++ ){
412 : 0 : Trace( c ) << " " << ( i==0 ? "Ext" : "Int" ) << " disequal:";
413 : 0 : DiseqList* del = rni->get(i);
414 [ - - ]: 0 : for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
415 [ - - ]: 0 : if( (*it2).second ){
416 [ - - ]: 0 : Trace( c ) << " " << (*it2).first;
417 : : }
418 : : }
419 [ - - ]: 0 : Trace( c ) << ", total = " << del->size() << std::endl;
420 : : }
421 : : }
422 : : }
423 [ + - ]: 3745 : Trace( c ) << "Total disequal: " << d_total_diseq_external << " external,";
424 [ + - ]: 3745 : Trace( c ) << " " << d_total_diseq_internal << " internal." << std::endl;
425 : :
426 [ + - ]: 3745 : if( incClique ){
427 [ - + ]: 3745 : if( !d_testClique.empty() ){
428 [ - - ]: 0 : Trace( c ) << "Candidate clique members: " << std::endl;
429 [ - - ]: 0 : Trace( c ) << " ";
430 : 0 : for( NodeBoolMap::iterator it = d_testClique.begin();
431 [ - - ]: 0 : it != d_testClique.end(); ++ it ){
432 [ - - ]: 0 : if( (*it).second ){
433 [ - - ]: 0 : Trace( c ) << (*it).first << " ";
434 : : }
435 : : }
436 [ - - ]: 0 : Trace( c ) << ", size = " << d_testCliqueSize << std::endl;
437 : : }
438 [ - + ]: 3745 : if( !d_splits.empty() ){
439 [ - - ]: 0 : Trace( c ) << "Required splits: " << std::endl;
440 [ - - ]: 0 : Trace( c ) << " ";
441 [ - - ]: 0 : for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end();
442 : 0 : ++ it ){
443 [ - - ]: 0 : if( (*it).second ){
444 [ - - ]: 0 : Trace( c ) << (*it).first << " ";
445 : : }
446 : : }
447 [ - - ]: 0 : Trace( c ) << ", size = " << d_splitsSize << std::endl;
448 : : }
449 : : }
450 : 3745 : }
451 : :
452 : 745 : SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy(
453 : 745 : Env& env, TypeNode type, Valuation valuation)
454 : 745 : : DecisionStrategyFmf(env, valuation), d_type(type)
455 : : {
456 : 745 : }
457 : :
458 : 1765 : Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i)
459 : : {
460 : 1765 : NodeManager* nm = NodeManager::currentNM();
461 : 3530 : Node cco = nm->mkConst(CardinalityConstraint(d_type, Integer(i + 1)));
462 : 3530 : return nm->mkNode(Kind::CARDINALITY_CONSTRAINT, cco);
463 : : }
464 : :
465 : 0 : std::string SortModel::CardinalityDecisionStrategy::identify() const
466 : : {
467 : 0 : return std::string("uf_card");
468 : : }
469 : :
470 : 745 : SortModel::SortModel(Env& env,
471 : : TypeNode tn,
472 : : TheoryState& state,
473 : : TheoryInferenceManager& im,
474 : 745 : CardinalityExtension* thss)
475 : : : EnvObj(env),
476 : : d_type(tn),
477 : : d_state(state),
478 : : d_im(im),
479 : : d_thss(thss),
480 : 0 : d_regions_index(thss->context(), 0),
481 : : d_regions_map(thss->context()),
482 : : d_split_score(thss->context()),
483 : 0 : d_disequalities_index(thss->context(), 0),
484 : 0 : d_reps(thss->context(), 0),
485 : 0 : d_cardinality(thss->context(), 1),
486 : 0 : d_hasCard(thss->context(), false),
487 : 0 : d_maxNegCard(thss->context(), 0),
488 : 0 : d_initialized(thss->userContext(), false),
489 : 745 : d_c_dec_strat(nullptr)
490 : : {
491 [ + - ]: 745 : if (options().uf.ufssMode == options::UfssMode::FULL)
492 : : {
493 : : // Register the strategy with the decision manager of the theory.
494 : : // We are guaranteed that the decision manager is ready since we
495 : : // construct this module during TheoryUF::finishInit.
496 : 745 : d_c_dec_strat.reset(new CardinalityDecisionStrategy(
497 : 745 : thss->d_env, d_type, thss->getTheory()->getValuation()));
498 : : }
499 : 745 : }
500 : :
501 : 1490 : SortModel::~SortModel() {
502 : 4603 : for(std::vector<Region*>::iterator i = d_regions.begin();
503 [ + + ]: 8461 : i != d_regions.end(); ++i) {
504 : 3858 : Region* region = *i;
505 [ + - ]: 3858 : delete region;
506 : : }
507 : 745 : d_regions.clear();
508 : 1490 : }
509 : :
510 : : /** initialize */
511 : 25233 : void SortModel::initialize()
512 : : {
513 [ + - ][ + + ]: 25233 : if (d_c_dec_strat.get() != nullptr && !d_initialized)
[ + + ]
514 : : {
515 : 1203 : d_initialized = true;
516 : : // Strategy is user-context-dependent, since it is in sync with
517 : : // user-context-dependent flag d_initialized.
518 : 2406 : d_im.getDecisionManager()->registerStrategy(DecisionManager::STRAT_UF_CARD,
519 : 1203 : d_c_dec_strat.get());
520 : : }
521 : 25233 : }
522 : :
523 : : /** new node */
524 : 7603 : void SortModel::newEqClass( Node n ){
525 [ + - ]: 7603 : if (!d_state.isInConflict())
526 : : {
527 [ + - ]: 7603 : if( d_regions_map.find( n )==d_regions_map.end() ){
528 : 7603 : d_regions_map[n] = d_regions_index;
529 [ + - ]: 7603 : Trace("uf-ss") << "CardinalityExtension: New Eq Class " << n << std::endl;
530 [ + - ]: 15206 : Trace("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size()
531 : 7603 : << std::endl;
532 [ + + ]: 7603 : if (d_regions_index < d_regions.size())
533 : : {
534 : 3745 : d_regions[d_regions_index]->debugPrint("uf-ss-debug", true);
535 : 3745 : d_regions[d_regions_index]->setValid(true);
536 [ - + ][ - + ]: 3745 : Assert(d_regions[d_regions_index]->getNumReps() == 0);
[ - - ]
537 : : }else{
538 : 3858 : d_regions.push_back(new Region(this, d_thss->context()));
539 : : }
540 : 7603 : d_regions[d_regions_index]->addRep(n);
541 : 7603 : d_regions_index = d_regions_index + 1;
542 : :
543 : 7603 : d_reps = d_reps + 1;
544 : : }
545 : : }
546 : 7603 : }
547 : :
548 : : /** merge */
549 : 43654 : void SortModel::merge( Node a, Node b ){
550 [ - + ]: 43654 : if (d_state.isInConflict())
551 : : {
552 : 0 : return;
553 : : }
554 [ + - ]: 87308 : Trace("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b << "..."
555 : 43654 : << std::endl;
556 [ + - ]: 43654 : if (a != b)
557 : : {
558 [ - + ][ - + ]: 43654 : Assert(d_regions_map.find(a) != d_regions_map.end());
[ - - ]
559 [ - + ][ - + ]: 43654 : Assert(d_regions_map.find(b) != d_regions_map.end());
[ - - ]
560 : 43654 : int ai = d_regions_map[a];
561 : 43654 : int bi = d_regions_map[b];
562 [ + - ]: 43654 : Trace("uf-ss") << " regions: " << ai << " " << bi << std::endl;
563 [ + + ]: 43654 : if (ai != bi)
564 : : {
565 [ + + ]: 38550 : if (d_regions[ai]->getNumReps() == 1)
566 : : {
567 : 25929 : int ri = combineRegions(bi, ai);
568 : 25929 : d_regions[ri]->setEqual(a, b);
569 : 25929 : checkRegion(ri);
570 : : }
571 [ + + ]: 12621 : else if (d_regions[bi]->getNumReps() == 1)
572 : : {
573 : 11771 : int ri = combineRegions(ai, bi);
574 : 11771 : d_regions[ri]->setEqual(a, b);
575 : 11771 : checkRegion(ri);
576 : : }
577 : : else
578 : : {
579 : : // Either move a to d_regions[bi], or b to d_regions[ai].
580 : 850 : RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
581 : 850 : RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
582 : 850 : int aex = (a_region_info->getNumInternalDisequalities()
583 : 850 : - getNumDisequalitiesToRegion(a, bi));
584 : 850 : int bex = (b_region_info->getNumInternalDisequalities()
585 : 850 : - getNumDisequalitiesToRegion(b, ai));
586 : : // Based on which would produce the fewest number of
587 : : // external disequalities.
588 [ + + ]: 850 : if (aex < bex)
589 : : {
590 : 304 : moveNode(a, bi);
591 : 304 : d_regions[bi]->setEqual(a, b);
592 : : }else{
593 : 546 : moveNode(b, ai);
594 : 546 : d_regions[ai]->setEqual( a, b );
595 : : }
596 : 850 : checkRegion(ai);
597 : 850 : checkRegion(bi);
598 : : }
599 : : }
600 : : else
601 : : {
602 : 5104 : d_regions[ai]->setEqual(a, b);
603 : 5104 : checkRegion(ai);
604 : : }
605 : 43654 : d_regions_map[b] = -1;
606 : : }
607 : 43654 : d_reps = d_reps - 1;
608 : : }
609 : :
610 : : /** assert terms are disequal */
611 : 20589 : void SortModel::assertDisequal( Node a, Node b, Node reason ){
612 [ - + ]: 20589 : if (d_state.isInConflict())
613 : : {
614 : 0 : return;
615 : : }
616 : : // if they are not already disequal
617 : 20589 : eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine();
618 : 20589 : a = ee->getRepresentative(a);
619 : 20589 : b = ee->getRepresentative(b);
620 : 20589 : int ai = d_regions_map[a];
621 : 20589 : int bi = d_regions_map[b];
622 [ - + ]: 20589 : if (d_regions[ai]->isDisequal(a, b, ai == bi))
623 : : {
624 : : // already disequal
625 : 0 : return;
626 : : }
627 [ + - ]: 41178 : Trace("uf-ss") << "Assert disequal " << a << " != " << b << "..."
628 : 20589 : << std::endl;
629 [ + - ]: 41178 : Trace("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..."
630 : 20589 : << std::endl;
631 : : // add to list of disequalities
632 [ + + ]: 20589 : if (d_disequalities_index < d_disequalities.size())
633 : : {
634 : 14761 : d_disequalities[d_disequalities_index] = reason;
635 : : }
636 : : else
637 : : {
638 : 5828 : d_disequalities.push_back(reason);
639 : : }
640 : 20589 : d_disequalities_index = d_disequalities_index + 1;
641 : : // now, add disequalities to regions
642 [ - + ][ - + ]: 20589 : Assert(d_regions_map.find(a) != d_regions_map.end());
[ - - ]
643 [ - + ][ - + ]: 20589 : Assert(d_regions_map.find(b) != d_regions_map.end());
[ - - ]
644 [ + - ]: 20589 : Trace("uf-ss") << " regions: " << ai << " " << bi << std::endl;
645 [ + + ]: 20589 : if (ai == bi)
646 : : {
647 : : // internal disequality
648 : 750 : d_regions[ai]->setDisequal(a, b, 1, true);
649 : 750 : d_regions[ai]->setDisequal(b, a, 1, true);
650 : : // do not need to check if it needs to combine (no new ext. disequalities)
651 : 750 : checkRegion(ai, false);
652 : : }
653 : : else
654 : : {
655 : : // external disequality
656 : 19839 : d_regions[ai]->setDisequal(a, b, 0, true);
657 : 19839 : d_regions[bi]->setDisequal(b, a, 0, true);
658 : 19839 : checkRegion(ai);
659 : 19839 : checkRegion(bi);
660 : : }
661 : : }
662 : :
663 : 0 : bool SortModel::areDisequal( Node a, Node b ) {
664 : 0 : Assert(a == d_thss->getTheory()->getEqualityEngine()->getRepresentative(a));
665 : 0 : Assert(b == d_thss->getTheory()->getEqualityEngine()->getRepresentative(b));
666 : 0 : if( d_regions_map.find( a )!=d_regions_map.end() &&
667 [ - - ]: 0 : d_regions_map.find( b )!=d_regions_map.end() ){
668 : 0 : int ai = d_regions_map[a];
669 : 0 : int bi = d_regions_map[b];
670 [ - - ]: 0 : return d_regions[ai]->isDisequal(a, b, ai==bi ? 1 : 0);
671 : : }else{
672 : 0 : return false;
673 : : }
674 : : }
675 : :
676 : 338055 : void SortModel::check(Theory::Effort level)
677 : : {
678 [ - + ][ - + ]: 338055 : Assert(options().uf.ufssMode == options::UfssMode::FULL);
[ - - ]
679 [ + + ][ - + ]: 338055 : if (!d_hasCard && d_state.isInConflict())
[ - + ]
680 : : {
681 : : // not necessary to check
682 : 0 : return;
683 : : }
684 [ + - ]: 676110 : Trace("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
685 : 338055 : << std::endl;
686 [ + + ]: 338055 : if (level == Theory::EFFORT_FULL)
687 : : {
688 [ + - ]: 14232 : Trace("fmf-full-check") << std::endl;
689 [ + - ]: 28464 : Trace("fmf-full-check")
690 : 14232 : << "Full check for SortModel " << d_type << ", status : " << std::endl;
691 : 14232 : debugPrint("fmf-full-check");
692 [ + - ]: 14232 : Trace("fmf-full-check") << std::endl;
693 : : }
694 [ + + ]: 338055 : if (d_reps <= (unsigned)d_cardinality)
695 : : {
696 [ + - ]: 242126 : Trace("uf-ss-debug") << "We have " << d_reps << " representatives for type "
697 : 121063 : << d_type << ", <= " << d_cardinality << std::endl;
698 [ + + ]: 121063 : if( level==Theory::EFFORT_FULL ){
699 [ + - ]: 13974 : Trace("uf-ss-sat") << "We have " << d_reps << " representatives for type "
700 : 6987 : << d_type << ", <= " << d_cardinality << std::endl;
701 : : }
702 : 121063 : return;
703 : : }
704 : : // first check if we can generate a clique conflict
705 : : // do a check within each region
706 [ + + ]: 1856850 : for (size_t i = 0; i < d_regions_index; i++)
707 : : {
708 [ + + ]: 1641040 : if (d_regions[i]->valid())
709 : : {
710 : 969752 : std::vector<Node> clique;
711 [ + + ]: 969752 : if (d_regions[i]->check(level, d_cardinality, clique))
712 : : {
713 : : // add clique lemma
714 : 1184 : addCliqueLemma(clique);
715 : 1184 : return;
716 : : }
717 : : else
718 : : {
719 [ + - ]: 968568 : Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
720 : : }
721 : : }
722 : : }
723 : : // do splitting on demand
724 : 215808 : bool addedLemma = false;
725 [ + + ]: 215808 : if (level == Theory::EFFORT_FULL)
726 : : {
727 [ + - ]: 7206 : Trace("uf-ss-debug") << "Add splits?" << std::endl;
728 : : // see if we have any recommended splits from large regions
729 [ + + ]: 96172 : for (size_t i = 0; i < d_regions_index; i++)
730 : : {
731 [ + + ][ + + ]: 88966 : if (d_regions[i]->valid() && d_regions[i]->getNumReps() > d_cardinality)
[ + + ]
732 : : {
733 : 3022 : int sp = addSplit(d_regions[i]);
734 [ + - ]: 3022 : if (sp == 1)
735 : : {
736 : 3022 : addedLemma = true;
737 : : }
738 [ - - ]: 0 : else if (sp == -1)
739 : : {
740 : 0 : check(level);
741 : 0 : return;
742 : : }
743 : : }
744 : : }
745 : : }
746 : : // If no added lemmas, force continuation via combination of regions.
747 [ + + ][ + + ]: 215808 : if (level != Theory::EFFORT_FULL || addedLemma)
748 : : {
749 : 211624 : return;
750 : : }
751 : : // check at full effort
752 [ + - ]: 4184 : Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
753 [ + - ]: 4184 : Trace("uf-ss-si") << "Must combine region" << std::endl;
754 : 4184 : bool recheck = false;
755 : 4184 : SortInference* si = d_state.getSortInference();
756 [ + + ]: 4184 : if (si != nullptr)
757 : : {
758 : : // If sort inference is enabled, search for regions with same sort.
759 : 112 : std::map<int, int> sortsFound;
760 [ + - ]: 550 : for (size_t i = 0; i < d_regions_index; i++)
761 : : {
762 [ + + ]: 550 : if (d_regions[i]->valid())
763 : : {
764 : 112 : Node op = d_regions[i]->frontKey();
765 : 112 : int sort_id = si->getSortId(op);
766 [ + + ]: 112 : if (sortsFound.find(sort_id) != sortsFound.end())
767 : : {
768 [ + - ]: 112 : Trace("fmf-full-check") << "Combined regions " << i << " "
769 : 56 : << sortsFound[sort_id] << std::endl;
770 : 56 : combineRegions(sortsFound[sort_id], i);
771 : 56 : recheck = true;
772 : 56 : break;
773 : : }
774 : : else
775 : : {
776 : 56 : sortsFound[sort_id] = i;
777 : : }
778 : : }
779 : : }
780 : : }
781 [ + + ]: 4184 : if (!recheck)
782 : : {
783 : : // naive strategy, force region combination involving the first
784 : : // valid region
785 [ + - ]: 11935 : for (size_t i = 0; i < d_regions_index; i++)
786 : : {
787 [ + + ]: 11935 : if (d_regions[i]->valid())
788 : : {
789 : 4128 : int fcr = forceCombineRegion(i, false);
790 [ + - ]: 8256 : Trace("fmf-full-check")
791 : 4128 : << "Combined regions " << i << " " << fcr << std::endl;
792 [ + - ]: 8256 : Trace("uf-ss-debug")
793 : 4128 : << "Combined regions " << i << " " << fcr << std::endl;
794 : 4128 : recheck = true;
795 : 4128 : break;
796 : : }
797 : : }
798 : : }
799 [ + - ]: 4184 : if (recheck)
800 : : {
801 [ + - ]: 4184 : Trace("uf-ss-debug") << "Must recheck." << std::endl;
802 : 4184 : check(level);
803 : : }
804 : : }
805 : :
806 : 457 : void SortModel::presolve() {
807 : 457 : d_initialized = false;
808 : 457 : }
809 : :
810 : 1700 : int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
811 : 1700 : int ni = d_regions_map[n];
812 : 1700 : int counter = 0;
813 : 1700 : DiseqList* del = d_regions[ni]->getRegionInfo(n)->get(0);
814 [ + + ]: 4675 : for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
815 [ + + ]: 2975 : if( (*it).second ){
816 [ + + ]: 968 : if( d_regions_map[ (*it).first ]==ri ){
817 : 760 : counter++;
818 : : }
819 : : }
820 : : }
821 : 1700 : return counter;
822 : : }
823 : :
824 : 14495 : void SortModel::getDisequalitiesToRegions(int ri,
825 : : std::map< int, int >& regions_diseq)
826 : : {
827 : 14495 : Region* region = d_regions[ri];
828 [ + + ]: 176367 : for(Region::iterator it = region->begin(); it != region->end(); ++it ){
829 [ + + ]: 161872 : if( it->second->valid() ){
830 : 45245 : DiseqList* del = it->second->get(0);
831 [ + + ]: 369287 : for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
832 [ + + ]: 324042 : if( (*it2).second ){
833 [ - + ][ - + ]: 207888 : Assert(isValid(d_regions_map[(*it2).first]));
[ - - ]
834 : 207888 : regions_diseq[ d_regions_map[ (*it2).first ] ]++;
835 : : }
836 : : }
837 : : }
838 : : }
839 : 14495 : }
840 : :
841 : 0 : void SortModel::setSplitScore( Node n, int s ){
842 [ - - ]: 0 : if( d_split_score.find( n )!=d_split_score.end() ){
843 : 0 : int ss = d_split_score[ n ];
844 [ - - ]: 0 : d_split_score[ n ] = s>ss ? s : ss;
845 : : }else{
846 : 0 : d_split_score[ n ] = s;
847 : : }
848 [ - - ]: 0 : for( int i=0; i<(int)n.getNumChildren(); i++ ){
849 : 0 : setSplitScore( n[i], s+1 );
850 : : }
851 : 0 : }
852 : :
853 : 13595 : void SortModel::assertCardinality(uint32_t c, bool val)
854 : : {
855 [ + - ]: 13595 : if (!d_state.isInConflict())
856 : : {
857 [ + - ]: 27190 : Trace("uf-ss-assert")
858 : 0 : << "Assert cardinality " << d_type << " " << c << " " << val
859 : 0 : << " level = "
860 : 13595 : << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl;
861 [ - + ][ - + ]: 13595 : Assert(c > 0);
[ - - ]
862 : 13595 : Node cl = getCardinalityLiteral( c );
863 [ + + ]: 13595 : if( val ){
864 : 11215 : bool doCheckRegions = !d_hasCard;
865 : 11215 : bool prevHasCard = d_hasCard;
866 : 11215 : d_hasCard = true;
867 [ + + ][ + + ]: 11215 : if (!prevHasCard || c < d_cardinality)
[ + + ]
868 : : {
869 : 11209 : d_cardinality = c;
870 : 11209 : simpleCheckCardinality();
871 [ + + ]: 11209 : if (d_state.isInConflict())
872 : : {
873 : 256 : return;
874 : : }
875 : : }
876 : : //should check all regions now
877 [ + + ]: 10959 : if (doCheckRegions)
878 : : {
879 [ + + ]: 68972 : for (size_t i = 0; i < d_regions_index; i++)
880 : : {
881 [ + + ]: 58048 : if( d_regions[i]->valid() ){
882 : 49700 : checkRegion( i );
883 [ - + ]: 49700 : if (d_state.isInConflict())
884 : : {
885 : 0 : return;
886 : : }
887 : : }
888 : : }
889 : : }
890 : : // we assert it positively, if its beyond the bound, abort
891 : 10959 : if (options().uf.ufssAbortCardinality >= 0
892 [ - + ][ - - ]: 10959 : && c >= static_cast<uint32_t>(options().uf.ufssAbortCardinality))
[ - + ]
893 : : {
894 : 0 : std::stringstream ss;
895 : 0 : ss << "Maximum cardinality (" << options().uf.ufssAbortCardinality
896 : 0 : << ") for finite model finding exceeded." << std::endl;
897 : 0 : throw LogicException(ss.str());
898 : : }
899 : : }
900 : : else
901 : : {
902 [ + + ]: 2380 : if (c > d_maxNegCard.get())
903 : : {
904 [ + - ]: 4136 : Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for "
905 : 2068 : << d_type << " is now " << c << std::endl;
906 : 2068 : d_maxNegCard.set(c);
907 : 2068 : simpleCheckCardinality();
908 : : }
909 : : }
910 : : }
911 : : }
912 : :
913 : 149127 : void SortModel::checkRegion( int ri, bool checkCombine ){
914 [ + + ][ + + ]: 149127 : if( isValid(ri) && d_hasCard ){
[ + + ]
915 [ - + ][ - + ]: 139943 : Assert(d_cardinality > 0);
[ - - ]
916 [ + + ][ + + ]: 139943 : if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
[ + + ]
917 : 14495 : int riNew = forceCombineRegion( ri, true );
918 [ + - ]: 14495 : if( riNew>=0 ){
919 : 14495 : checkRegion( riNew, checkCombine );
920 : : }
921 : : }
922 : : //now check if region is in conflict
923 : 279886 : std::vector< Node > clique;
924 [ + + ]: 139943 : if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
925 : : //explain clique
926 : 2818 : addCliqueLemma(clique);
927 : : }
928 : : }
929 : 149127 : }
930 : :
931 : 18623 : int SortModel::forceCombineRegion( int ri, bool useDensity ){
932 [ + + ]: 18623 : if( !useDensity ){
933 [ + - ]: 34274 : for( int i=0; i<(int)d_regions_index; i++ ){
934 [ + + ][ + + ]: 34274 : if( ri!=i && d_regions[i]->valid() ){
[ + + ]
935 : 4128 : return combineRegions( ri, i );
936 : : }
937 : : }
938 : 0 : return -1;
939 : : }else{
940 : : //this region must merge with another
941 [ - + ]: 14495 : if( TraceIsOn("uf-ss-check-region") ){
942 [ - - ]: 0 : Trace("uf-ss-check-region") << "We must combine Region #" << ri << ". " << std::endl;
943 : 0 : d_regions[ri]->debugPrint("uf-ss-check-region");
944 : : }
945 : : //take region with maximum disequality density
946 : 14495 : double maxScore = 0;
947 : 14495 : int maxRegion = -1;
948 : 28990 : std::map< int, int > regions_diseq;
949 : 14495 : getDisequalitiesToRegions( ri, regions_diseq );
950 [ + + ]: 97184 : for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
951 [ + - ]: 82689 : Trace("uf-ss-check-region") << it->first << " : " << it->second << std::endl;
952 : : }
953 [ + + ]: 97184 : for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
954 [ - + ][ - + ]: 82689 : Assert(it->first != ri);
[ - - ]
955 [ - + ][ - + ]: 82689 : Assert(isValid(it->first));
[ - - ]
956 [ - + ][ - + ]: 82689 : Assert(d_regions[it->first]->getNumReps() > 0);
[ - - ]
957 : 82689 : double tempScore = double(it->second)/double(d_regions[it->first]->getNumReps() );
958 [ + + ]: 82689 : if( tempScore>maxScore ){
959 : 18025 : maxRegion = it->first;
960 : 18025 : maxScore = tempScore;
961 : : }
962 : : }
963 [ + - ]: 14495 : if( maxRegion!=-1 ){
964 [ - + ]: 14495 : if( TraceIsOn("uf-ss-check-region") ){
965 [ - - ]: 0 : Trace("uf-ss-check-region") << "Combine with region #" << maxRegion << ":" << std::endl;
966 : 0 : d_regions[maxRegion]->debugPrint("uf-ss-check-region");
967 : : }
968 : 14495 : return combineRegions( ri, maxRegion );
969 : : }
970 : 0 : return -1;
971 : : }
972 : : }
973 : :
974 : :
975 : 56379 : int SortModel::combineRegions( int ai, int bi ){
976 [ + - ]: 56379 : Trace("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl;
977 [ + - ][ + - ]: 112758 : Assert(isValid(ai) && isValid(bi));
[ - + ][ - - ]
978 : 56379 : Region* region_bi = d_regions[bi];
979 [ + + ]: 292037 : for(Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it){
980 : 235658 : Region::RegionNodeInfo* rni = it->second;
981 [ + + ]: 235658 : if( rni->valid() ){
982 : 59903 : d_regions_map[ it->first ] = ai;
983 : : }
984 : : }
985 : : //update regions disequal DO_THIS?
986 : 56379 : d_regions[ai]->combine( d_regions[bi] );
987 : 56379 : d_regions[bi]->setValid( false );
988 : 56379 : return ai;
989 : : }
990 : :
991 : 850 : void SortModel::moveNode( Node n, int ri ){
992 [ + - ]: 850 : Trace("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl;
993 [ - + ][ - + ]: 850 : Assert(isValid(d_regions_map[n]));
[ - - ]
994 [ - + ][ - + ]: 850 : Assert(isValid(ri));
[ - - ]
995 : : //move node to region ri
996 : 850 : d_regions[ri]->takeNode( d_regions[ d_regions_map[n] ], n );
997 : 850 : d_regions_map[n] = ri;
998 : 850 : }
999 : :
1000 : 3022 : int SortModel::addSplit(Region* r)
1001 : : {
1002 : 6044 : Node s;
1003 [ + - ]: 3022 : if( r->hasSplits() ){
1004 : : //take the first split you find
1005 : 17903 : for( Region::split_iterator it = r->begin_splits();
1006 [ + - ]: 32784 : it != r->end_splits(); ++it ){
1007 [ + + ]: 17903 : if( (*it).second ){
1008 : 3022 : s = (*it).first;
1009 : 3022 : break;
1010 : : }
1011 : : }
1012 [ - + ][ - + ]: 3022 : Assert(s != Node::null());
[ - - ]
1013 : : }
1014 [ + - ]: 3022 : if (!s.isNull() ){
1015 : : //add lemma to output channel
1016 [ - + ][ - + ]: 3022 : Assert(s.getKind() == Kind::EQUAL);
[ - - ]
1017 : 6044 : Node ss = rewrite(s);
1018 [ - + ]: 3022 : if (ss.getKind() != Kind::EQUAL)
1019 : : {
1020 : 0 : Node b_t = NodeManager::currentNM()->mkConst( true );
1021 : 0 : Node b_f = NodeManager::currentNM()->mkConst( false );
1022 [ - - ]: 0 : if( ss==b_f ){
1023 [ - - ]: 0 : Trace("uf-ss-lemma") << "....Assert disequal directly : "
1024 : 0 : << s[0] << " " << s[1] << std::endl;
1025 : 0 : assertDisequal( s[0], s[1], b_t );
1026 : 0 : return -1;
1027 : : }else{
1028 [ - - ]: 0 : Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl;
1029 : : }
1030 [ - - ]: 0 : if (ss == b_t)
1031 : : {
1032 : 0 : AlwaysAssert(false) << "Bad split " << s << std::endl;
1033 : : }
1034 : : }
1035 [ - + ]: 3022 : if (TraceIsOn("uf-ss-split-si"))
1036 : : {
1037 : 0 : SortInference* si = d_state.getSortInference();
1038 [ - - ]: 0 : if (si != nullptr)
1039 : : {
1040 [ - - ]: 0 : for (size_t i = 0; i < 2; i++)
1041 : : {
1042 : 0 : int sid = si->getSortId(ss[i]);
1043 [ - - ]: 0 : Trace("uf-ss-split-si") << sid << " ";
1044 : : }
1045 [ - - ]: 0 : Trace("uf-ss-split-si") << std::endl;
1046 : : }
1047 : : }
1048 : : //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
1049 : : //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
1050 : : //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
1051 : : //split on the equality s
1052 : 6044 : Node lem = NodeManager::currentNM()->mkNode(Kind::OR, ss, ss.negate());
1053 : : // send lemma, with caching
1054 [ + - ]: 3022 : if (d_im.lemma(lem, InferenceId::UF_CARD_SPLIT))
1055 : : {
1056 [ + - ]: 3022 : Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
1057 : : //tell the sat solver to explore the equals branch first
1058 : 3022 : d_im.preferPhase(ss, true);
1059 : 3022 : ++( d_thss->d_statistics.d_split_lemmas );
1060 : : }
1061 : 3022 : return 1;
1062 : : }else{
1063 : 0 : return 0;
1064 : : }
1065 : : }
1066 : :
1067 : 4002 : void SortModel::addCliqueLemma(std::vector<Node>& clique)
1068 : : {
1069 [ - + ][ - + ]: 4002 : Assert(d_hasCard);
[ - - ]
1070 [ - + ][ - + ]: 4002 : Assert(d_cardinality > 0);
[ - - ]
1071 [ + + ]: 6656 : while (clique.size() > d_cardinality + 1)
1072 : : {
1073 : 2654 : clique.pop_back();
1074 : : }
1075 : : // add as lemma
1076 : 8004 : std::vector<Node> eqs;
1077 [ + + ]: 21541 : for (unsigned i = 0, size = clique.size(); i < size; i++)
1078 : : {
1079 [ + + ]: 72669 : for (unsigned j = 0; j < i; j++)
1080 : : {
1081 : 55130 : eqs.push_back(clique[i].eqNode(clique[j]));
1082 : : }
1083 : : }
1084 : 4002 : eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
1085 : 8004 : Node lem = NodeManager::currentNM()->mkNode(Kind::OR, eqs);
1086 : : // send lemma, with caching
1087 [ + - ]: 4002 : if (d_im.lemma(lem, InferenceId::UF_CARD_CLIQUE))
1088 : : {
1089 [ + - ]: 4002 : Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
1090 : 4002 : ++(d_thss->d_statistics.d_clique_lemmas);
1091 : : }
1092 : 4002 : }
1093 : :
1094 : 13277 : void SortModel::simpleCheckCardinality() {
1095 [ + + ][ + + ]: 13277 : if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()<d_maxNegCard.get() ){
[ + + ][ + + ]
1096 : : Node lem = NodeManager::currentNM()->mkNode(
1097 : : Kind::AND,
1098 : 528 : getCardinalityLiteral(d_cardinality.get()),
1099 : 1056 : getCardinalityLiteral(d_maxNegCard.get()).negate());
1100 [ + - ]: 264 : Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
1101 : 264 : d_im.conflict(lem, InferenceId::UF_CARD_SIMPLE_CONFLICT);
1102 : : }
1103 : 13277 : }
1104 : :
1105 : 14232 : void SortModel::debugPrint( const char* c ){
1106 [ - + ]: 14232 : if( TraceIsOn( c ) ){
1107 [ - - ]: 0 : Trace( c ) << "Number of reps = " << d_reps << std::endl;
1108 [ - - ]: 0 : Trace( c ) << "Cardinality req = " << d_cardinality << std::endl;
1109 : 0 : unsigned debugReps = 0;
1110 [ - - ]: 0 : for( unsigned i=0; i<d_regions_index; i++ ){
1111 : 0 : Region* region = d_regions[i];
1112 [ - - ]: 0 : if( region->valid() ){
1113 [ - - ]: 0 : Trace( c ) << "Region #" << i << ": " << std::endl;
1114 : 0 : region->debugPrint( c, true );
1115 [ - - ]: 0 : Trace( c ) << std::endl;
1116 [ - - ]: 0 : for( Region::iterator it = region->begin(); it != region->end(); ++it ){
1117 [ - - ]: 0 : if( it->second->valid() ){
1118 [ - - ]: 0 : if( d_regions_map[ it->first ]!=(int)i ){
1119 [ - - ]: 0 : Trace( c ) << "***Bad regions map : " << it->first
1120 : 0 : << " " << d_regions_map[ it->first ].get() << std::endl;
1121 : : }
1122 : : }
1123 : : }
1124 : 0 : debugReps += region->getNumReps();
1125 : : }
1126 : : }
1127 : :
1128 [ - - ]: 0 : if( debugReps!=d_reps ){
1129 [ - - ]: 0 : Trace( c ) << "***Bad reps: " << d_reps << ", "
1130 : 0 : << "actual = " << debugReps << std::endl;
1131 : : }
1132 : : }
1133 : 14232 : }
1134 : :
1135 : 2038 : bool SortModel::checkLastCall()
1136 : : {
1137 : 2038 : NodeManager* nm = NodeManager::currentNM();
1138 : 2038 : SkolemManager* sm = nm->getSkolemManager();
1139 : 2038 : TheoryModel* m = d_state.getModel();
1140 [ - + ]: 2038 : if( TraceIsOn("uf-ss-warn") ){
1141 : 0 : std::vector< Node > eqcs;
1142 : : eq::EqClassesIterator eqcs_i =
1143 : 0 : eq::EqClassesIterator(m->getEqualityEngine());
1144 [ - - ]: 0 : while( !eqcs_i.isFinished() ){
1145 : 0 : Node eqc = (*eqcs_i);
1146 [ - - ]: 0 : if( eqc.getType()==d_type ){
1147 [ - - ]: 0 : if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
1148 : 0 : eqcs.push_back( eqc );
1149 : : //we must ensure that this equivalence class has been accounted for
1150 [ - - ]: 0 : if( d_regions_map.find( eqc )==d_regions_map.end() ){
1151 [ - - ]: 0 : Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
1152 [ - - ]: 0 : Trace("uf-ss-warn") << " type : " << d_type << std::endl;
1153 [ - - ]: 0 : Trace("uf-ss-warn") << " kind : " << eqc.getKind() << std::endl;
1154 : : }
1155 : : }
1156 : : }
1157 : 0 : ++eqcs_i;
1158 : : }
1159 : : }
1160 : 2038 : RepSet* rs = m->getRepSetPtr();
1161 : 2038 : size_t nReps = rs->getNumRepresentatives(d_type);
1162 [ + + ]: 2038 : if (nReps != d_maxNegCard + 1)
1163 : : {
1164 [ + - ]: 62 : Trace("uf-ss-warn") << "WARNING : Model does not have same # "
1165 : 0 : "representatives as cardinality for "
1166 : 31 : << d_type << "." << std::endl;
1167 [ + - ]: 62 : Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard
1168 : 31 : << std::endl;
1169 [ + - ]: 31 : Trace("uf-ss-warn") << " # Reps : " << nReps << std::endl;
1170 [ + - ]: 31 : if (d_maxNegCard >= nReps)
1171 : : {
1172 [ + + ]: 345 : while (d_fresh_aloc_reps.size() <= d_maxNegCard)
1173 : : {
1174 : 628 : std::stringstream ss;
1175 : 314 : ss << "r_" << d_type << "_";
1176 : : Node nn = sm->mkDummySkolem(
1177 : 942 : ss.str(), d_type, "enumeration to meet negative card constraint");
1178 : 314 : d_fresh_aloc_reps.push_back( nn );
1179 : : }
1180 [ + + ]: 31 : if (d_maxNegCard == 0)
1181 : : {
1182 : 4 : rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]);
1183 : : }
1184 : : else
1185 : : {
1186 : : //must add lemma
1187 : 54 : std::vector< Node > force_cl;
1188 [ + + ]: 337 : for (size_t i = 0; i <= d_maxNegCard; i++)
1189 : : {
1190 [ + + ]: 2777 : for (size_t j = (i + 1); j <= d_maxNegCard; j++)
1191 : : {
1192 : 2467 : force_cl.push_back(
1193 : 4934 : d_fresh_aloc_reps[i].eqNode(d_fresh_aloc_reps[j]).negate());
1194 : : }
1195 : : }
1196 : 54 : Node cl = getCardinalityLiteral( d_maxNegCard );
1197 : 54 : Node lem = nm->mkNode(Kind::OR, cl, nm->mkAnd(force_cl));
1198 [ + - ]: 27 : Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
1199 : 27 : d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE);
1200 : 27 : return false;
1201 : : }
1202 : : }
1203 : : }
1204 : 2011 : return true;
1205 : : }
1206 : :
1207 : 0 : int SortModel::getNumRegions(){
1208 : 0 : int count = 0;
1209 [ - - ]: 0 : for( int i=0; i<(int)d_regions_index; i++ ){
1210 [ - - ]: 0 : if( d_regions[i]->valid() ){
1211 : 0 : count++;
1212 : : }
1213 : : }
1214 : 0 : return count;
1215 : : }
1216 : :
1217 : 16690 : Node SortModel::getCardinalityLiteral(uint32_t c)
1218 : : {
1219 [ - + ][ - + ]: 16690 : Assert(c > 0);
[ - - ]
1220 : 16690 : std::map<uint32_t, Node>::iterator itcl = d_cardinality_literal.find(c);
1221 [ + + ]: 16690 : if (itcl != d_cardinality_literal.end())
1222 : : {
1223 : 15054 : return itcl->second;
1224 : : }
1225 : : // get the literal from the decision strategy
1226 : 3272 : Node lit = d_c_dec_strat->getLiteral(c - 1);
1227 : 1636 : d_cardinality_literal[c] = lit;
1228 : :
1229 : : // return the literal
1230 : 1636 : return lit;
1231 : : }
1232 : :
1233 : 721 : CardinalityExtension::CardinalityExtension(Env& env,
1234 : : TheoryState& state,
1235 : : TheoryInferenceManager& im,
1236 : 721 : TheoryUF* th)
1237 : : : EnvObj(env),
1238 : : d_statistics(statisticsRegistry()),
1239 : : d_state(state),
1240 : : d_im(im),
1241 : : d_th(th),
1242 : : d_rep_model(),
1243 : 0 : d_min_pos_com_card(context(), 0),
1244 : 0 : d_min_pos_com_card_set(context(), false),
1245 : : d_cc_dec_strat(nullptr),
1246 : 0 : d_initializedCombinedCardinality(userContext(), false),
1247 : 1442 : d_card_assertions_eqv_lemma(userContext()),
1248 : 0 : d_min_pos_tn_master_card(context(), 0),
1249 : 0 : d_min_pos_tn_master_card_set(context(), false),
1250 : 721 : d_rel_eqc(context())
1251 : : {
1252 : 721 : if (options().uf.ufssMode == options::UfssMode::FULL
1253 [ + + ][ + - ]: 721 : && options().uf.ufssFairness)
[ + + ]
1254 : : {
1255 : : // Register the strategy with the decision manager of the theory.
1256 : : // We are guaranteed that the decision manager is ready since we
1257 : : // construct this module during TheoryUF::finishInit.
1258 : 709 : d_cc_dec_strat.reset(
1259 : 709 : new CombinedCardinalityDecisionStrategy(env, th->getValuation()));
1260 : : }
1261 : 721 : }
1262 : :
1263 : 1442 : CardinalityExtension::~CardinalityExtension()
1264 : : {
1265 : 1466 : for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1266 [ + + ]: 2211 : it != d_rep_model.end(); ++it) {
1267 [ + - ]: 745 : delete it->second;
1268 : : }
1269 : 1442 : }
1270 : :
1271 : : /** ensure eqc */
1272 : 0 : void CardinalityExtension::ensureEqc(SortModel* c, Node a)
1273 : : {
1274 [ - - ]: 0 : if( !hasEqc( a ) ){
1275 : 0 : d_rel_eqc[a] = true;
1276 [ - - ]: 0 : Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
1277 : 0 : << a.getType() << std::endl;
1278 : 0 : c->newEqClass( a );
1279 [ - - ]: 0 : Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1280 : 0 : << std::endl;
1281 : : }
1282 : 0 : }
1283 : :
1284 : 0 : void CardinalityExtension::ensureEqcRec(Node n)
1285 : : {
1286 [ - - ]: 0 : if( !hasEqc( n ) ){
1287 : 0 : SortModel* c = getSortModel( n );
1288 [ - - ]: 0 : if( c ){
1289 : 0 : ensureEqc( c, n );
1290 : : }
1291 [ - - ]: 0 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
1292 : 0 : ensureEqcRec( n[i] );
1293 : : }
1294 : : }
1295 : 0 : }
1296 : :
1297 : : /** has eqc */
1298 : 0 : bool CardinalityExtension::hasEqc(Node a)
1299 : : {
1300 : 0 : NodeBoolMap::iterator it = d_rel_eqc.find( a );
1301 : 0 : return it!=d_rel_eqc.end() && (*it).second;
1302 : : }
1303 : :
1304 : : /** new node */
1305 : 53408 : void CardinalityExtension::newEqClass(Node a)
1306 : : {
1307 : 53408 : SortModel* c = getSortModel( a );
1308 [ + + ]: 53408 : if( c ){
1309 [ + - ]: 15206 : Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
1310 [ - + ][ - - ]: 7603 : << a.getType() << std::endl;
1311 : 7603 : c->newEqClass( a );
1312 [ + - ]: 15206 : Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1313 : 7603 : << std::endl;
1314 : : }
1315 : 53408 : }
1316 : :
1317 : : /** merge */
1318 : 308148 : void CardinalityExtension::merge(Node a, Node b)
1319 : : {
1320 : : //TODO: ensure they are relevant
1321 : 308148 : SortModel* c = getSortModel( a );
1322 [ + + ]: 308148 : if( c ){
1323 [ + - ]: 87308 : Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b
1324 [ - + ][ - - ]: 43654 : << " : " << a.getType() << std::endl;
1325 : 43654 : c->merge( a, b );
1326 [ + - ]: 43654 : Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
1327 : : }
1328 : 308148 : }
1329 : :
1330 : : /** assert terms are disequal */
1331 : 34052 : void CardinalityExtension::assertDisequal(Node a, Node b, Node reason)
1332 : : {
1333 : 34052 : SortModel* c = getSortModel( a );
1334 [ + + ]: 34052 : if( c ){
1335 [ + - ]: 41178 : Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a
1336 [ - + ][ - - ]: 20589 : << " " << b << " : " << a.getType() << std::endl;
1337 : 20589 : c->assertDisequal( a, b, reason );
1338 [ + - ]: 41178 : Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal."
1339 : 20589 : << std::endl;
1340 : : }
1341 : 34052 : }
1342 : :
1343 : : /** assert a node */
1344 : 225296 : void CardinalityExtension::assertNode(Node n, bool isDecision)
1345 : : {
1346 [ + - ]: 225296 : Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
1347 : 225296 : bool polarity = n.getKind() != Kind::NOT;
1348 [ + + ]: 225296 : TNode lit = polarity ? n : n[0];
1349 [ + + ]: 225296 : if (options().uf.ufssMode == options::UfssMode::FULL)
1350 : : {
1351 [ + + ]: 181875 : if (lit.getKind() == Kind::CARDINALITY_CONSTRAINT)
1352 : : {
1353 : : const CardinalityConstraint& cc =
1354 : 13595 : lit.getOperator().getConst<CardinalityConstraint>();
1355 : 27190 : TypeNode tn = cc.getType();
1356 [ - + ][ - + ]: 13595 : Assert(tn.isUninterpretedSort());
[ - - ]
1357 [ - + ][ - + ]: 13595 : Assert(d_rep_model[tn]);
[ - - ]
1358 : 13595 : uint32_t nCard = cc.getUpperBound().getUnsignedInt();
1359 [ + - ]: 27190 : Trace("uf-ss-debug") << "...check cardinality constraint : " << tn
1360 : 13595 : << std::endl;
1361 [ + + ]: 13595 : if (options().uf.ufssFairnessMonotone)
1362 : : {
1363 : 68 : SortInference* si = d_state.getSortInference();
1364 [ + - ]: 68 : Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
1365 [ + + ]: 68 : if (tn != d_tn_mono_master)
1366 : : {
1367 : 52 : std::map<TypeNode, bool>::iterator it = d_tn_mono_slave.find(tn);
1368 [ + + ]: 52 : if (it == d_tn_mono_slave.end())
1369 : : {
1370 : : bool isMonotonic;
1371 [ - + ]: 10 : if (si != nullptr)
1372 : : {
1373 : 0 : isMonotonic = si->isMonotonic(tn);
1374 : : }
1375 : : else
1376 : : {
1377 : : // if ground, everything is monotonic
1378 : 10 : isMonotonic = true;
1379 : : }
1380 [ + - ]: 10 : if (isMonotonic)
1381 : : {
1382 [ + + ]: 10 : if (d_tn_mono_master.isNull())
1383 : : {
1384 [ + - ]: 8 : Trace("uf-ss-com-card-debug")
1385 : 4 : << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
1386 : 4 : d_tn_mono_master = tn;
1387 : : }
1388 : : else
1389 : : {
1390 [ + - ]: 12 : Trace("uf-ss-com-card-debug")
1391 : 6 : << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
1392 : 6 : d_tn_mono_slave[tn] = true;
1393 : : }
1394 : : }
1395 : : else
1396 : : {
1397 [ - - ]: 0 : Trace("uf-ss-com-card-debug")
1398 : 0 : << "uf-ss-fair-monotone: Set non-monotonic : " << tn
1399 : 0 : << std::endl;
1400 : 0 : d_tn_mono_slave[tn] = false;
1401 : : }
1402 : : }
1403 : : }
1404 : : // set the minimum positive cardinality for master if necessary
1405 [ + + ][ + + ]: 68 : if (polarity && tn == d_tn_mono_master)
[ + + ]
1406 : : {
1407 [ + - ]: 40 : Trace("uf-ss-com-card-debug")
1408 : 20 : << "...set min positive cardinality" << std::endl;
1409 : 20 : if (!d_min_pos_tn_master_card_set.get()
1410 [ - + ][ - - ]: 20 : || nCard < d_min_pos_tn_master_card.get())
[ + - ]
1411 : : {
1412 : 20 : d_min_pos_tn_master_card_set.set(true);
1413 : 20 : d_min_pos_tn_master_card.set(nCard);
1414 : : }
1415 : : }
1416 : : }
1417 [ + - ]: 13595 : Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
1418 : 13595 : d_rep_model[tn]->assertCardinality(nCard, polarity);
1419 : : // check if combined cardinality is violated
1420 : 13595 : checkCombinedCardinality();
1421 : : }
1422 [ + + ]: 168280 : else if (lit.getKind() == Kind::COMBINED_CARDINALITY_CONSTRAINT)
1423 : : {
1424 [ + + ]: 6997 : if( polarity ){
1425 : : //safe to assume int here
1426 : : const CombinedCardinalityConstraint& cc =
1427 : 5504 : lit.getOperator().getConst<CombinedCardinalityConstraint>();
1428 : 5504 : uint32_t nCard = cc.getUpperBound().getUnsignedInt();
1429 [ - + ][ - - ]: 5504 : if (!d_min_pos_com_card_set.get() || nCard < d_min_pos_com_card.get())
[ + - ]
1430 : : {
1431 : 5504 : d_min_pos_com_card_set.set(true);
1432 : 5504 : d_min_pos_com_card.set( nCard );
1433 : 5504 : checkCombinedCardinality();
1434 : : }
1435 : : }
1436 : : }
1437 : : else
1438 : : {
1439 [ - + ]: 161283 : if( TraceIsOn("uf-ss-warn") ){
1440 : : ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
1441 : : //// a theory propagation is not a decision.
1442 [ - - ]: 0 : if( isDecision ){
1443 [ - - ]: 0 : for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1444 [ - - ]: 0 : if( !it->second->hasCardinalityAsserted() ){
1445 [ - - ]: 0 : Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
1446 : : }
1447 : : }
1448 : : }
1449 : : }
1450 : : }
1451 : : }
1452 : : else
1453 : : {
1454 : 43421 : if (lit.getKind() == Kind::CARDINALITY_CONSTRAINT
1455 [ + + ][ - + ]: 43421 : || lit.getKind() == Kind::COMBINED_CARDINALITY_CONSTRAINT)
[ + + ]
1456 : : {
1457 : : // cardinality constraint from user input, set incomplete
1458 [ + - ]: 2 : Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
1459 : 2 : d_im.setModelUnsound(IncompleteId::UF_CARD_MODE);
1460 : : }
1461 : : }
1462 [ + - ]: 225296 : Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
1463 : 225296 : }
1464 : :
1465 : 0 : bool CardinalityExtension::areDisequal(Node a, Node b)
1466 : : {
1467 [ - - ]: 0 : if( a==b ){
1468 : 0 : return false;
1469 : : }
1470 : 0 : eq::EqualityEngine* ee = d_th->getEqualityEngine();
1471 : 0 : a = ee->getRepresentative(a);
1472 : 0 : b = ee->getRepresentative(b);
1473 [ - - ]: 0 : if (ee->areDisequal(a, b, false))
1474 : : {
1475 : 0 : return true;
1476 : : }
1477 : 0 : SortModel* c = getSortModel(a);
1478 [ - - ]: 0 : if (c)
1479 : : {
1480 : 0 : return c->areDisequal(a, b);
1481 : : }
1482 : 0 : return false;
1483 : : }
1484 : :
1485 : : /** check */
1486 : 106872 : void CardinalityExtension::check(Theory::Effort level)
1487 : : {
1488 [ + + ]: 106872 : if (level == Theory::EFFORT_LAST_CALL)
1489 : : {
1490 : : // if last call, call last call check for each sort
1491 [ + + ]: 3507 : for (std::pair<const TypeNode, SortModel*>& r : d_rep_model)
1492 : : {
1493 [ + + ]: 2038 : if (!r.second->checkLastCall())
1494 : : {
1495 : 27 : break;
1496 : : }
1497 : : }
1498 : 1496 : return;
1499 : : }
1500 [ + - ]: 105376 : if (!d_state.isInConflict())
1501 : : {
1502 [ + + ]: 105376 : if (options().uf.ufssMode == options::UfssMode::FULL)
1503 : : {
1504 [ + - ]: 163656 : Trace("uf-ss-solver")
1505 : 81828 : << "CardinalityExtension: check " << level << std::endl;
1506 [ + + ]: 81828 : if (level == Theory::EFFORT_FULL)
1507 : : {
1508 [ - + ]: 6332 : if (TraceIsOn("uf-ss-debug"))
1509 : : {
1510 : 0 : debugPrint("uf-ss-debug");
1511 : : }
1512 [ - + ]: 6332 : if (TraceIsOn("uf-ss-state"))
1513 : : {
1514 [ - - ]: 0 : Trace("uf-ss-state")
1515 : 0 : << "CardinalityExtension::check " << level << std::endl;
1516 [ - - ]: 0 : for (std::pair<const TypeNode, SortModel*>& rm : d_rep_model)
1517 : : {
1518 [ - - ]: 0 : Trace("uf-ss-state") << " " << rm.first << " has cardinality "
1519 : 0 : << rm.second->getCardinality() << std::endl;
1520 : : }
1521 : : }
1522 : : }
1523 [ + + ]: 415699 : for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1524 : 333871 : it->second->check(level);
1525 [ - + ]: 333871 : if (d_state.isInConflict())
1526 : : {
1527 : 0 : break;
1528 : : }
1529 : : }
1530 : : }
1531 [ + - ]: 23548 : else if (options().uf.ufssMode == options::UfssMode::NO_MINIMAL)
1532 : : {
1533 [ + + ]: 23548 : if( level==Theory::EFFORT_FULL ){
1534 : : // split on an equality between two equivalence classes (at most one per type)
1535 : 1314 : std::map< TypeNode, std::vector< Node > > eqc_list;
1536 : 1314 : std::map< TypeNode, bool > type_proc;
1537 : 657 : eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine());
1538 [ + + ]: 60633 : while( !eqcs_i.isFinished() ){
1539 : 119952 : Node a = *eqcs_i;
1540 : 119952 : TypeNode tn = a.getType();
1541 [ + + ]: 59976 : if (tn.isUninterpretedSort())
1542 : : {
1543 [ + + ]: 8425 : if( type_proc.find( tn )==type_proc.end() ){
1544 : 6366 : std::map< TypeNode, std::vector< Node > >::iterator itel = eqc_list.find( tn );
1545 [ + + ]: 6366 : if( itel!=eqc_list.end() ){
1546 [ + + ]: 10494 : for( unsigned j=0; j<itel->second.size(); j++ ){
1547 : 7239 : Node b = itel->second[j];
1548 [ + + ]: 7239 : if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){
1549 : 2043 : Node eq = rewrite(a.eqNode(b));
1550 : : Node lem = NodeManager::currentNM()->mkNode(
1551 : 2043 : Kind::OR, eq, eq.negate());
1552 [ + - ]: 681 : Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
1553 : 681 : d_im.lemma(lem, InferenceId::UF_CARD_SPLIT);
1554 : 681 : d_im.preferPhase(eq, true);
1555 : 681 : type_proc[tn] = true;
1556 : 681 : break;
1557 : : }
1558 : : }
1559 : : }
1560 : 6366 : eqc_list[tn].push_back( a );
1561 : : }
1562 : : }
1563 : 59976 : ++eqcs_i;
1564 : : }
1565 : : }
1566 : : }
1567 : : else
1568 : : {
1569 : : // unhandled uf ss mode
1570 : 0 : Assert(false);
1571 : : }
1572 [ + - ]: 210752 : Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
1573 : 105376 : << std::endl;
1574 : : }
1575 : : }
1576 : :
1577 : 734 : void CardinalityExtension::presolve()
1578 : : {
1579 : 734 : d_initializedCombinedCardinality = false;
1580 [ + + ]: 1191 : for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1581 : 457 : it->second->presolve();
1582 : 457 : it->second->initialize();
1583 : : }
1584 : 734 : }
1585 : :
1586 : 709 : CardinalityExtension::CombinedCardinalityDecisionStrategy::
1587 : 709 : CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation)
1588 : 709 : : DecisionStrategyFmf(env, valuation)
1589 : : {
1590 : 709 : }
1591 : 1336 : Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
1592 : : unsigned i)
1593 : : {
1594 : 1336 : NodeManager* nm = NodeManager::currentNM();
1595 : 2672 : Node cco = nm->mkConst(CombinedCardinalityConstraint(Integer(i)));
1596 : 2672 : return nm->mkNode(Kind::COMBINED_CARDINALITY_CONSTRAINT, cco);
1597 : : }
1598 : :
1599 : : std::string
1600 : 0 : CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
1601 : : {
1602 : 0 : return std::string("uf_combined_card");
1603 : : }
1604 : :
1605 : 382601 : void CardinalityExtension::preRegisterTerm(TNode n)
1606 : : {
1607 [ + + ]: 382601 : if (options().uf.ufssMode != options::UfssMode::FULL)
1608 : : {
1609 : 357825 : return;
1610 : : }
1611 : : // initialize combined cardinality
1612 : 296164 : initializeCombinedCardinality();
1613 : :
1614 [ + - ]: 296164 : Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
1615 : : // shouldn't have to preregister this type (it may be that there are no
1616 : : // quantifiers over tn)
1617 : 296164 : TypeNode tn;
1618 [ + + ]: 296164 : if (n.getKind() == Kind::CARDINALITY_CONSTRAINT)
1619 : : {
1620 : : const CardinalityConstraint& cc =
1621 : 17471 : n.getOperator().getConst<CardinalityConstraint>();
1622 : 17471 : tn = cc.getType();
1623 : : }
1624 : : else
1625 : : {
1626 : 278693 : tn = n.getType();
1627 : : }
1628 [ + + ]: 296164 : if (!tn.isUninterpretedSort())
1629 : : {
1630 : 271388 : return;
1631 : : }
1632 : 24776 : std::map<TypeNode, SortModel*>::iterator it = d_rep_model.find(tn);
1633 [ + + ]: 24776 : if (it == d_rep_model.end())
1634 : : {
1635 : 745 : SortModel* rm = nullptr;
1636 [ + - ]: 745 : if (tn.isUninterpretedSort())
1637 : : {
1638 [ + - ]: 745 : Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
1639 : 745 : rm = new SortModel(d_env, tn, d_state, d_im, this);
1640 : : }
1641 [ + - ]: 745 : if (rm)
1642 : : {
1643 : 745 : rm->initialize();
1644 : 745 : d_rep_model[tn] = rm;
1645 : : // d_rep_model_init[tn] = true;
1646 : : }
1647 : : }
1648 : : else
1649 : : {
1650 : : // ensure sort model is initialized
1651 : 24031 : it->second->initialize();
1652 : : }
1653 : : }
1654 : :
1655 : 395608 : SortModel* CardinalityExtension::getSortModel(Node n)
1656 : : {
1657 : 791216 : TypeNode tn = n.getType();
1658 : 395608 : std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
1659 : : //pre-register the type if not done already
1660 [ + + ]: 395608 : if( it==d_rep_model.end() ){
1661 : 323762 : preRegisterTerm( n );
1662 : 323762 : it = d_rep_model.find( tn );
1663 : : }
1664 [ + + ]: 395608 : if( it!=d_rep_model.end() ){
1665 : 71846 : return it->second;
1666 : : }else{
1667 : 323762 : return NULL;
1668 : : }
1669 : : }
1670 : :
1671 : : /** get cardinality for sort */
1672 : 0 : int CardinalityExtension::getCardinality(Node n)
1673 : : {
1674 : 0 : SortModel* c = getSortModel( n );
1675 [ - - ]: 0 : if( c ){
1676 : 0 : return c->getCardinality();
1677 : : }else{
1678 : 0 : return -1;
1679 : : }
1680 : : }
1681 : :
1682 : 0 : int CardinalityExtension::getCardinality(TypeNode tn)
1683 : : {
1684 : 0 : std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
1685 [ - - ][ - - ]: 0 : if( it!=d_rep_model.end() && it->second ){
[ - - ]
1686 : 0 : return it->second->getCardinality();
1687 : : }
1688 : 0 : return -1;
1689 : : }
1690 : :
1691 : : //print debug
1692 : 0 : void CardinalityExtension::debugPrint(const char* c)
1693 : : {
1694 [ - - ]: 0 : for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1695 [ - - ]: 0 : Trace( c ) << "Conflict find structure for " << it->first << ": " << std::endl;
1696 : 0 : it->second->debugPrint( c );
1697 [ - - ]: 0 : Trace( c ) << std::endl;
1698 : : }
1699 : 0 : }
1700 : :
1701 : : /** initialize */
1702 : 296164 : void CardinalityExtension::initializeCombinedCardinality()
1703 : : {
1704 : 296164 : if (d_cc_dec_strat.get() != nullptr
1705 [ + - ][ + + ]: 296164 : && !d_initializedCombinedCardinality.get())
[ + + ]
1706 : : {
1707 : 776 : d_initializedCombinedCardinality = true;
1708 : 1552 : d_im.getDecisionManager()->registerStrategy(
1709 : 776 : DecisionManager::STRAT_UF_COMBINED_CARD, d_cc_dec_strat.get());
1710 : : }
1711 : 296164 : }
1712 : :
1713 : : /** check */
1714 : 19099 : void CardinalityExtension::checkCombinedCardinality()
1715 : : {
1716 [ - + ][ - + ]: 19099 : Assert(options().uf.ufssMode == options::UfssMode::FULL);
[ - - ]
1717 [ + - ]: 19099 : if (options().uf.ufssFairness)
1718 : : {
1719 [ + - ]: 19099 : Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
1720 : 19099 : uint32_t totalCombinedCard = 0;
1721 : 19099 : uint32_t maxMonoSlave = 0;
1722 : 19099 : TypeNode maxSlaveType;
1723 [ + + ]: 111565 : for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1724 : 92466 : uint32_t max_neg = it->second->getMaximumNegativeCardinality();
1725 [ + + ]: 92466 : if (!options().uf.ufssFairnessMonotone)
1726 : : {
1727 : 92244 : totalCombinedCard += max_neg;
1728 : : }
1729 : : else
1730 : : {
1731 : 222 : std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first );
1732 [ + + ][ - + ]: 222 : if( its==d_tn_mono_slave.end() || !its->second ){
[ + + ]
1733 : 92 : totalCombinedCard += max_neg;
1734 : : }else{
1735 [ + + ]: 130 : if( max_neg>maxMonoSlave ){
1736 : 8 : maxMonoSlave = max_neg;
1737 : 8 : maxSlaveType = it->first;
1738 : : }
1739 : : }
1740 : : }
1741 : : }
1742 [ + - ]: 19099 : Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl;
1743 [ + + ]: 19099 : if (options().uf.ufssFairnessMonotone)
1744 : : {
1745 [ + - ]: 88 : Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave << std::endl;
1746 : 88 : if (!d_min_pos_tn_master_card_set.get()
1747 [ + + ][ - + ]: 88 : && maxMonoSlave > d_min_pos_tn_master_card.get())
[ - + ]
1748 : : {
1749 : 0 : uint32_t mc = d_min_pos_tn_master_card.get();
1750 : 0 : std::vector< Node > conf;
1751 : 0 : conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) );
1752 : 0 : conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() );
1753 : 0 : Node cf = NodeManager::currentNM()->mkNode(Kind::AND, conf);
1754 [ - - ]: 0 : Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict"
1755 : 0 : << " : " << cf << std::endl;
1756 [ - - ]: 0 : Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
1757 : 0 : << " : " << cf << std::endl;
1758 : 0 : d_im.conflict(cf, InferenceId::UF_CARD_MONOTONE_COMBINED);
1759 : 0 : return;
1760 : : }
1761 : : }
1762 : 19099 : uint32_t cc = d_min_pos_com_card.get();
1763 [ + + ][ + + ]: 19099 : if (d_min_pos_com_card_set.get() && totalCombinedCard > cc)
[ + + ]
1764 : : {
1765 : : //conflict
1766 : 2280 : Node com_lit = d_cc_dec_strat->getLiteral(cc);
1767 : 2280 : std::vector< Node > conf;
1768 : 1140 : conf.push_back( com_lit );
1769 : 1140 : uint32_t totalAdded = 0;
1770 : 3516 : for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin();
1771 [ + - ]: 5892 : it != d_rep_model.end(); ++it ){
1772 : 3516 : bool doAdd = true;
1773 [ - + ]: 3516 : if (options().uf.ufssFairnessMonotone)
1774 : : {
1775 : : std::map< TypeNode, bool >::iterator its =
1776 : 0 : d_tn_mono_slave.find( it->first );
1777 [ - - ][ - - ]: 0 : if( its!=d_tn_mono_slave.end() && its->second ){
[ - - ]
1778 : 0 : doAdd = false;
1779 : : }
1780 : : }
1781 [ + - ]: 3516 : if( doAdd ){
1782 : 3516 : uint32_t c = it->second->getMaximumNegativeCardinality();
1783 [ + + ]: 3516 : if( c>0 ){
1784 : 2540 : conf.push_back( it->second->getCardinalityLiteral( c ).negate() );
1785 : 2540 : totalAdded += c;
1786 : : }
1787 [ + + ]: 3516 : if( totalAdded>cc ){
1788 : 1140 : break;
1789 : : }
1790 : : }
1791 : : }
1792 : 1140 : Node cf = NodeManager::currentNM()->mkNode(Kind::AND, conf);
1793 [ + - ]: 2280 : Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
1794 : 1140 : << std::endl;
1795 [ + - ]: 2280 : Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
1796 : 1140 : << std::endl;
1797 : 1140 : d_im.conflict(cf, InferenceId::UF_CARD_COMBINED);
1798 : : }
1799 : : }
1800 : : }
1801 : :
1802 : 721 : CardinalityExtension::Statistics::Statistics(StatisticsRegistry& sr)
1803 : : : d_clique_conflicts(
1804 : 721 : sr.registerInt("CardinalityExtension::Clique_Conflicts")),
1805 : 721 : d_clique_lemmas(sr.registerInt("CardinalityExtension::Clique_Lemmas")),
1806 : 721 : d_split_lemmas(sr.registerInt("CardinalityExtension::Split_Lemmas")),
1807 : 721 : d_max_model_size(sr.registerInt("CardinalityExtension::Max_Model_Size"))
1808 : : {
1809 : 721 : d_max_model_size.maxAssign(1);
1810 : 721 : }
1811 : :
1812 : : } // namespace uf
1813 : : } // namespace theory
1814 : : } // namespace cvc5::internal
|
