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