projects / cvc5.git / blob
? search:


eb9e5e9872c08d5d394c0a1e797d5424db5697da
[cvc5.git] / src / theory / uf / theory_uf_strong_solver.cpp
1 /********************* */
2 /*! \file theory_uf_strong_solver.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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.\endverbatim
11 **
12 ** \brief Implementation of theory uf strong solver class
13 **/
14
15 #include "theory/uf/theory_uf_strong_solver.h"
16
17 #include "options/uf_options.h"
18 #include "theory/uf/theory_uf.h"
19 #include "theory/uf/equality_engine.h"
20 #include "theory/theory_engine.h"
21 #include "theory/quantifiers_engine.h"
22 #include "theory/quantifiers/term_database.h"
23 #include "theory/theory_model.h"
24 #include "theory/quantifiers/symmetry_breaking.h"
25
26 //#define ONE_SPLIT_REGION
27 //#define DISABLE_QUICK_CLIQUE_CHECKS
28 //#define COMBINE_REGIONS_SMALL_INTO_LARGE
29 //#define LAZY_REL_EQC
30
31 using namespace std;
32 using namespace CVC4::kind;
33 using namespace CVC4::context;
34
35
36 namespace CVC4 {
37 namespace theory {
38 namespace uf {
39
40 /* These are names are unambigious are we use abbreviations. */
41 typedef StrongSolverTheoryUF::SortModel SortModel;
42 typedef SortModel::Region Region;
43 typedef Region::RegionNodeInfo RegionNodeInfo;
44 typedef RegionNodeInfo::DiseqList DiseqList;
45
46 Region::Region(SortModel* cf, context::Context* c)
47 : d_cf( cf )
48 , d_testCliqueSize( c, 0 )
49 , d_splitsSize( c, 0 )
50 , d_testClique( c )
51 , d_splits( c )
52 , d_reps_size( c, 0 )
53 , d_total_diseq_external( c, 0 )
54 , d_total_diseq_internal( c, 0 )
55 , d_valid( c, true ) {}
56
57 Region::~Region() {
58 for(iterator i = begin(), iend = end(); i != iend; ++i) {
59 RegionNodeInfo* regionNodeInfo = (*i).second;
60 delete regionNodeInfo;
61 }
62 d_nodes.clear();
63 }
64
65 void Region::addRep( Node n ) {
66 setRep( n, true );
67 }
68
69 void Region::takeNode( Region* r, Node n ){
70 Assert( !hasRep( n ) );
71 Assert( r->hasRep( n ) );
72 //add representative
73 setRep( n, true );
74 //take disequalities from r
75 RegionNodeInfo* rni = r->d_nodes[n];
76 for( int t=0; t<2; t++ ){
77 DiseqList* del = rni->get(t);
78 for(DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
79 if( (*it).second ){
80 r->setDisequal( n, (*it).first, t, false );
81 if( t==0 ){
82 if( hasRep( (*it).first ) ){
83 setDisequal( (*it).first, n, 0, false );
84 setDisequal( (*it).first, n, 1, true );
85 setDisequal( n, (*it).first, 1, true );
86 }else{
87 setDisequal( n, (*it).first, 0, true );
88 }
89 }else{
90 r->setDisequal( (*it).first, n, 1, false );
91 r->setDisequal( (*it).first, n, 0, true );
92 setDisequal( n, (*it).first, 0, true );
93 }
94 }
95 }
96 }
97 //remove representative
98 r->setRep( n, false );
99 }
100
101 void Region::combine( Region* r ){
102 //take all nodes from r
103 for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it) {
104 if( it->second->valid() ){
105 setRep( it->first, true );
106 }
107 }
108 for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it){
109 if( it->second->valid() ){
110 //take disequalities from r
111 Node n = it->first;
112 RegionNodeInfo* rni = it->second;
113 for( int t=0; t<2; t++ ){
114 RegionNodeInfo::DiseqList* del = rni->get(t);
115 for( RegionNodeInfo::DiseqList::iterator it2 = del->begin(),
116 it2end = del->end(); it2 != it2end; ++it2 ){
117 if( (*it2).second ){
118 if( t==0 && hasRep( (*it2).first ) ){
119 setDisequal( (*it2).first, n, 0, false );
120 setDisequal( (*it2).first, n, 1, true );
121 setDisequal( n, (*it2).first, 1, true );
122 }else{
123 setDisequal( n, (*it2).first, t, true );
124 }
125 }
126 }
127 }
128 }
129 }
130 r->d_valid = false;
131 }
132
133 /** setEqual */
134 void Region::setEqual( Node a, Node b ){
135 Assert( hasRep( a ) && hasRep( b ) );
136 //move disequalities of b over to a
137 for( int t=0; t<2; t++ ){
138 DiseqList* del = d_nodes[b]->get(t);
139 for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
140 if( (*it).second ){
141 Node n = (*it).first;
142 //get the region that contains the endpoint of the disequality b != ...
143 Region* nr = d_cf->d_regions[ d_cf->d_regions_map[ n ] ];
144 if( !isDisequal( a, n, t ) ){
145 setDisequal( a, n, t, true );
146 nr->setDisequal( n, a, t, true );
147 //notify the disequality propagator
148 if( options::ufssDiseqPropagation() ){
149 d_cf->d_thss->getDisequalityPropagator()->assertDisequal(a, n, Node::null());
150 }
151 if( options::ufssSymBreak() ){
152 d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n );
153 }
154 }
155 setDisequal( b, n, t, false );
156 nr->setDisequal( n, b, t, false );
157 }
158 }
159 }
160 //remove b from representatives
161 setRep( b, false );
162 }
163
164 void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
165 //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " "
166 // << type << " " << valid << std::endl;
167 //debugPrint("uf-ss-region-debug");
168 //Assert( isDisequal( n1, n2, type )!=valid );
169 if( isDisequal( n1, n2, type )!=valid ){ //DO_THIS: make assertion
170 d_nodes[ n1 ]->get(type)->setDisequal( n2, valid );
171 if( type==0 ){
172 d_total_diseq_external = d_total_diseq_external + ( valid ? 1 : -1 );
173 }else{
174 d_total_diseq_internal = d_total_diseq_internal + ( valid ? 1 : -1 );
175 if( valid ){
176 //if they are both a part of testClique, then remove split
177 if( d_testClique.find( n1 )!=d_testClique.end() && d_testClique[n1] &&
178 d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){
179 Node eq = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
180 if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){
181 Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2
182 << std::endl;
183 d_splits[ eq ] = false;
184 d_splitsSize = d_splitsSize - 1;
185 }
186 }
187 }
188 }
189 }
190 }
191
192 void Region::setRep( Node n, bool valid ) {
193 Assert( hasRep( n )!=valid );
194 if( valid && d_nodes.find( n )==d_nodes.end() ){
195 d_nodes[n] = new RegionNodeInfo( d_cf->d_thss->getSatContext() );
196 }
197 d_nodes[n]->setValid(valid);
198 d_reps_size = d_reps_size + ( valid ? 1 : -1 );
199 //removing a member of the test clique from this region
200 if( d_testClique.find( n ) != d_testClique.end() && d_testClique[n] ){
201 Assert( !valid );
202 d_testClique[n] = false;
203 d_testCliqueSize = d_testCliqueSize - 1;
204 //remove all splits involving n
205 for( split_iterator it = begin_splits(); it != end_splits(); ++it ){
206 if( (*it).second ){
207 if( (*it).first[0]==n || (*it).first[1]==n ){
208 d_splits[ (*it).first ] = false;
209 d_splitsSize = d_splitsSize - 1;
210 }
211 }
212 }
213 }
214 }
215
216 bool Region::isDisequal( Node n1, Node n2, int type ) {
217 RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->get(type);
218 return del->isSet(n2) && del->getDisequalityValue(n2);
219 }
220
221 struct sortInternalDegree {
222 Region* r;
223 bool operator() (Node i, Node j) {
224 return (r->getRegionInfo(i)->getNumInternalDisequalities() >
225 r->getRegionInfo(j)->getNumInternalDisequalities());
226 }
227 };
228
229 struct sortExternalDegree {
230 Region* r;
231 bool operator() (Node i,Node j) {
232 return (r->getRegionInfo(i)->getNumExternalDisequalities() >
233 r->getRegionInfo(j)->getNumExternalDisequalities());
234 }
235 };
236
237 int gmcCount = 0;
238
239 bool Region::getMustCombine( int cardinality ){
240 if( options::ufssRegions() && d_total_diseq_external>=unsigned(cardinality) ){
241 //The number of external disequalities is greater than or equal to
242 //cardinality. Thus, a clique of size cardinality+1 may exist
243 //between nodes in d_regions[i] and other regions Check if this is
244 //actually the case: must have n nodes with outgoing degree
245 //(cardinality+1-n) for some n>0
246 std::vector< int > degrees;
247 for( Region::iterator it = begin(); it != end(); ++it ){
248 RegionNodeInfo* rni = it->second;
249 if( rni->valid() ){
250 if( rni->getNumDisequalities() >= cardinality ){
251 int outDeg = rni->getNumExternalDisequalities();
252 if( outDeg>=cardinality ){
253 //we have 1 node of degree greater than (cardinality)
254 return true;
255 }else if( outDeg>=1 ){
256 degrees.push_back( outDeg );
257 if( (int)degrees.size()>=cardinality ){
258 //we have (cardinality) nodes of degree 1
259 return true;
260 }
261 }
262 }
263 }
264 }
265 gmcCount++;
266 if( gmcCount%100==0 ){
267 Trace("gmc-count") << gmcCount << " " << cardinality
268 << " sample : " << degrees.size() << std::endl;
269 }
270 //this should happen relatively infrequently....
271 std::sort( degrees.begin(), degrees.end() );
272 for( int i=0; i<(int)degrees.size(); i++ ){
273 if( degrees[i]>=cardinality+1-((int)degrees.size()-i) ){
274 return true;
275 }
276 }
277 }
278 return false;
279 }
280
281 bool Region::check( Theory::Effort level, int cardinality,
282 std::vector< Node >& clique ) {
283 if( d_reps_size>unsigned(cardinality) ){
284 if( d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){
285 if( d_reps_size>1 ){
286 //quick clique check, all reps form a clique
287 for( iterator it = begin(); it != end(); ++it ){
288 if( it->second->valid() ){
289 clique.push_back( it->first );
290 }
291 }
292 Trace("quick-clique") << "Found quick clique" << std::endl;
293 return true;
294 }else{
295 return false;
296 }
297 }else if( options::ufssRegions() || options::ufssEagerSplits() ||
298 level==Theory::EFFORT_FULL ) {
299 //build test clique, up to size cardinality+1
300 if( d_testCliqueSize<=unsigned(cardinality) ){
301 std::vector< Node > newClique;
302 if( d_testCliqueSize<unsigned(cardinality) ){
303 for( iterator it = begin(); it != end(); ++it ){
304 //if not in the test clique, add it to the set of new members
305 if( it->second->valid() &&
306 ( d_testClique.find( it->first ) == d_testClique.end() ||
307 !d_testClique[ it->first ] ) ){
308 //if( it->second->getNumInternalDisequalities()>cardinality ||
309 // level==Theory::EFFORT_FULL ){
310 newClique.push_back( it->first );
311 //}
312 }
313 }
314 //choose remaining nodes with the highest degrees
315 sortInternalDegree sidObj;
316 sidObj.r = this;
317 std::sort( newClique.begin(), newClique.end(), sidObj );
318 int offset = ( cardinality - d_testCliqueSize ) + 1;
319 newClique.erase( newClique.begin() + offset, newClique.end() );
320 }else{
321 //scan for the highest degree
322 int maxDeg = -1;
323 Node maxNode;
324 for( std::map< Node, RegionNodeInfo* >::iterator
325 it = d_nodes.begin(); it != d_nodes.end(); ++it ){
326 //if not in the test clique, add it to the set of new members
327 if( it->second->valid() &&
328 ( d_testClique.find( it->first )==d_testClique.end() ||
329 !d_testClique[ it->first ] ) ){
330 if( it->second->getNumInternalDisequalities()>maxDeg ){
331 maxDeg = it->second->getNumInternalDisequalities();
332 maxNode = it->first;
333 }
334 }
335 }
336 Assert( maxNode!=Node::null() );
337 newClique.push_back( maxNode );
338 }
339 //check splits internal to new members
340 for( int j=0; j<(int)newClique.size(); j++ ){
341 Debug("uf-ss-debug") << "Choose to add clique member "
342 << newClique[j] << std::endl;
343 for( int k=(j+1); k<(int)newClique.size(); k++ ){
344 if( !isDisequal( newClique[j], newClique[k], 1 ) ){
345 Node at_j = newClique[j];
346 Node at_k = newClique[k];
347 Node j_eq_k =
348 NodeManager::currentNM()->mkNode( EQUAL, at_j, at_k );
349 d_splits[ j_eq_k ] = true;
350 d_splitsSize = d_splitsSize + 1;
351 }
352 }
353 //check disequalities with old members
354 for( NodeBoolMap::iterator it = d_testClique.begin();
355 it != d_testClique.end(); ++it ){
356 if( (*it).second ){
357 if( !isDisequal( (*it).first, newClique[j], 1 ) ){
358 Node at_it = (*it).first;
359 Node at_j = newClique[j];
360 Node it_eq_j = at_it.eqNode(at_j);
361 d_splits[ it_eq_j ] = true;
362 d_splitsSize = d_splitsSize + 1;
363 }
364 }
365 }
366 }
367 //add new clique members to test clique
368 for( int j=0; j<(int)newClique.size(); j++ ){
369 d_testClique[ newClique[j] ] = true;
370 d_testCliqueSize = d_testCliqueSize + 1;
371 }
372 }
373 // Check if test clique has larger size than cardinality, and
374 // forms a clique.
375 if( d_testCliqueSize >= unsigned(cardinality+1) && d_splitsSize==0 ){
376 //test clique is a clique
377 for( NodeBoolMap::iterator it = d_testClique.begin();
378 it != d_testClique.end(); ++it ){
379 if( (*it).second ){
380 clique.push_back( (*it).first );
381 }
382 }
383 return true;
384 }
385 }
386 }
387 return false;
388 }
389
390 bool Region::getCandidateClique( int cardinality, std::vector< Node >& clique )
391 {
392 if( d_testCliqueSize>=unsigned(cardinality+1) ){
393 //test clique is a clique
394 for( NodeBoolMap::iterator it = d_testClique.begin();
395 it != d_testClique.end(); ++it ){
396 if( (*it).second ){
397 clique.push_back( (*it).first );
398 }
399 }
400 return true;
401 }
402 return false;
403 }
404
405 void Region::getNumExternalDisequalities(
406 std::map< Node, int >& num_ext_disequalities ){
407 for( Region::iterator it = begin(); it != end(); ++it ){
408 RegionNodeInfo* rni = it->second;
409 if( rni->valid() ){
410 DiseqList* del = rni->get(0);
411 for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
412 if( (*it2).second ){
413 num_ext_disequalities[ (*it2).first ]++;
414 }
415 }
416 }
417 }
418 }
419
420 void Region::debugPrint( const char* c, bool incClique ) {
421 Debug( c ) << "Num reps: " << d_reps_size << std::endl;
422 for( Region::iterator it = begin(); it != end(); ++it ){
423 RegionNodeInfo* rni = it->second;
424 if( rni->valid() ){
425 Node n = it->first;
426 Debug( c ) << " " << n << std::endl;
427 for( int i=0; i<2; i++ ){
428 Debug( c ) << " " << ( i==0 ? "Ext" : "Int" ) << " disequal:";
429 DiseqList* del = rni->get(i);
430 for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
431 if( (*it2).second ){
432 Debug( c ) << " " << (*it2).first;
433 }
434 }
435 Debug( c ) << ", total = " << del->size() << std::endl;
436 }
437 }
438 }
439 Debug( c ) << "Total disequal: " << d_total_diseq_external << " external,";
440 Debug( c ) << " " << d_total_diseq_internal << " internal." << std::endl;
441
442 if( incClique ){
443 if( !d_testClique.empty() ){
444 Debug( c ) << "Candidate clique members: " << std::endl;
445 Debug( c ) << " ";
446 for( NodeBoolMap::iterator it = d_testClique.begin();
447 it != d_testClique.end(); ++ it ){
448 if( (*it).second ){
449 Debug( c ) << (*it).first << " ";
450 }
451 }
452 Debug( c ) << ", size = " << d_testCliqueSize << std::endl;
453 }
454 if( !d_splits.empty() ){
455 Debug( c ) << "Required splits: " << std::endl;
456 Debug( c ) << " ";
457 for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end();
458 ++ it ){
459 if( (*it).second ){
460 Debug( c ) << (*it).first << " ";
461 }
462 }
463 Debug( c ) << ", size = " << d_splitsSize << std::endl;
464 }
465 }
466 }
467
468 SortModel::SortModel( Node n,
469 context::Context* c,
470 context::UserContext* u,
471 StrongSolverTheoryUF* thss )
472 : d_type( n.getType() )
473 , d_thss( thss )
474 , d_regions_index( c, 0 )
475 , d_regions_map( c )
476 , d_split_score( c )
477 , d_disequalities_index( c, 0 )
478 , d_reps( c, 0 )
479 , d_conflict( c, false )
480 , d_cardinality( c, 1 )
481 , d_aloc_cardinality( u, 0 )
482 , d_hasCard( c, false )
483 , d_maxNegCard( c, 0 )
484 , d_initialized( u, false )
485 , d_lemma_cache( u )
486 {
487 d_cardinality_term = n;
488 //if( d_type.isSort() ){
489 // TypeEnumerator te(tn);
490 // d_cardinality_term = *te;
491 //}else{
492 // d_cardinality_term = tn.mkGroundTerm();
493 //}
494 }
495
496 SortModel::~SortModel() {
497 for(std::vector<Region*>::iterator i = d_regions.begin();
498 i != d_regions.end(); ++i) {
499 Region* region = *i;
500 delete region;
501 }
502 d_regions.clear();
503 }
504
505 /** initialize */
506 void SortModel::initialize( OutputChannel* out ){
507 if( !d_initialized ){
508 d_initialized = true;
509 allocateCardinality( out );
510 }
511 }
512
513 /** new node */
514 void SortModel::newEqClass( Node n ){
515 if( !d_conflict ){
516 if( d_regions_map.find( n )==d_regions_map.end() ){
517 // Must generate totality axioms for every cardinality we have
518 // allocated thus far.
519 for( std::map< int, Node >::iterator it = d_cardinality_literal.begin();
520 it != d_cardinality_literal.end(); ++it ){
521 if( applyTotality( it->first ) ){
522 addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() );
523 }
524 }
525 if( options::ufssTotality() ){
526 // Regions map will store whether we need to equate this term
527 // with a constant equivalence class.
528 if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
529 d_regions_map[n] = 0;
530 }else{
531 d_regions_map[n] = -1;
532 }
533 }else{
534 if( !options::ufssRegions() ){
535 // If not using regions, always add new equivalence classes
536 // to region index = 0.
537 d_regions_index = 0;
538 }
539 d_regions_map[n] = d_regions_index;
540 Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n
541 << std::endl;
542 Debug("uf-ss-debug") << d_regions_index << " "
543 << (int)d_regions.size() << std::endl;
544 if( d_regions_index<d_regions.size() ){
545 d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
546 d_regions[ d_regions_index ]->setValid(true);
547 Assert( !options::ufssRegions() ||
548 d_regions[ d_regions_index ]->getNumReps()==0 );
549 }else{
550 d_regions.push_back( new Region( this, d_thss->getSatContext() ) );
551 }
552 d_regions[ d_regions_index ]->addRep( n );
553 d_regions_index = d_regions_index + 1;
554 }
555 d_reps = d_reps + 1;
556 }
557 }
558 }
559
560 /** merge */
561 void SortModel::merge( Node a, Node b ){
562 if( !d_conflict ){
563 if( options::ufssTotality() ){
564 if( d_regions_map[b]==-1 ){
565 d_regions_map[a] = -1;
566 }
567 d_regions_map[b] = -1;
568 }else{
569 //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) );
570 //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) );
571 Debug("uf-ss") << "StrongSolverTheoryUF: Merging "
572 << a << " = " << b << "..." << std::endl;
573 if( a!=b ){
574 Assert( d_regions_map.find( a )!=d_regions_map.end() );
575 Assert( d_regions_map.find( b )!=d_regions_map.end() );
576 int ai = d_regions_map[a];
577 int bi = d_regions_map[b];
578 Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
579 if( ai!=bi ){
580 if( d_regions[ai]->getNumReps()==1 ){
581 int ri = combineRegions( bi, ai );
582 d_regions[ri]->setEqual( a, b );
583 checkRegion( ri );
584 }else if( d_regions[bi]->getNumReps()==1 ){
585 int ri = combineRegions( ai, bi );
586 d_regions[ri]->setEqual( a, b );
587 checkRegion( ri );
588 }else{
589 // Either move a to d_regions[bi], or b to d_regions[ai].
590 RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
591 RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
592 int aex = ( a_region_info->getNumInternalDisequalities() -
593 getNumDisequalitiesToRegion( a, bi ) );
594 int bex = ( b_region_info->getNumInternalDisequalities() -
595 getNumDisequalitiesToRegion( b, ai ) );
596 // Based on which would produce the fewest number of
597 // external disequalities.
598 if( aex<bex ){
599 moveNode( a, bi );
600 d_regions[bi]->setEqual( a, b );
601 }else{
602 moveNode( b, ai );
603 d_regions[ai]->setEqual( a, b );
604 }
605 checkRegion( ai );
606 checkRegion( bi );
607 }
608 }else{
609 d_regions[ai]->setEqual( a, b );
610 checkRegion( ai );
611 }
612 d_regions_map[b] = -1;
613 }
614 d_reps = d_reps - 1;
615
616 if( !d_conflict ){
617 if( options::ufssDiseqPropagation() ){
618 //notify the disequality propagator
619 d_thss->getDisequalityPropagator()->merge(a, b);
620 }
621 if( options::ufssSymBreak() ){
622 d_thss->getSymmetryBreaker()->merge(a, b);
623 }
624 }
625 }
626 }
627 }
628
629 /** assert terms are disequal */
630 void SortModel::assertDisequal( Node a, Node b, Node reason ){
631 if( !d_conflict ){
632 if( options::ufssTotality() ){
633 //do nothing
634 }else{
635 //if they are not already disequal
636 a = d_thss->getTheory()->d_equalityEngine.getRepresentative( a );
637 b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b );
638 int ai = d_regions_map[a];
639 int bi = d_regions_map[b];
640 if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){
641 Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
642 //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL ||
643 // a!=reason[0][0] || b!=reason[0][1] ){
644 // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
645 //}
646 Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." << std::endl;
647 //add to list of disequalities
648 if( d_disequalities_index<d_disequalities.size() ){
649 d_disequalities[d_disequalities_index] = reason;
650 }else{
651 d_disequalities.push_back( reason );
652 }
653 d_disequalities_index = d_disequalities_index + 1;
654 //now, add disequalities to regions
655 Assert( d_regions_map.find( a )!=d_regions_map.end() );
656 Assert( d_regions_map.find( b )!=d_regions_map.end() );
657 Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
658 if( ai==bi ){
659 //internal disequality
660 d_regions[ai]->setDisequal( a, b, 1, true );
661 d_regions[ai]->setDisequal( b, a, 1, true );
662 checkRegion( ai, false ); //do not need to check if it needs to combine (no new ext. disequalities)
663 }else{
664 //external disequality
665 d_regions[ai]->setDisequal( a, b, 0, true );
666 d_regions[bi]->setDisequal( b, a, 0, true );
667 checkRegion( ai );
668 checkRegion( bi );
669 }
670
671 if( !d_conflict ){
672 if( options::ufssDiseqPropagation() ){
673 //notify the disequality propagator
674 d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null());
675 }
676 if( options::ufssSymBreak() ){
677 d_thss->getSymmetryBreaker()->assertDisequal(a, b);
678 }
679 }
680 }
681 }
682 }
683 }
684
685 bool SortModel::areDisequal( Node a, Node b ) {
686 Assert( a == d_thss->getTheory()->d_equalityEngine.getRepresentative( a ) );
687 Assert( b == d_thss->getTheory()->d_equalityEngine.getRepresentative( b ) );
688 if( d_regions_map.find( a )!=d_regions_map.end() &&
689 d_regions_map.find( b )!=d_regions_map.end() ){
690 int ai = d_regions_map[a];
691 int bi = d_regions_map[b];
692 return d_regions[ai]->isDisequal(a, b, ai==bi ? 1 : 0);
693 }else{
694 return false;
695 }
696 }
697
698 /** check */
699 void SortModel::check( Theory::Effort level, OutputChannel* out ){
700 Assert( options::ufssMode()==UF_SS_FULL );
701 if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
702 Debug("uf-ss") << "StrongSolverTheoryUF: Check " << level << " " << d_type << std::endl;
703 if( level==Theory::EFFORT_FULL ){
704 Debug("fmf-full-check") << std::endl;
705 Debug("fmf-full-check") << "Full check for SortModel " << d_type << ", status : " << std::endl;
706 debugPrint("fmf-full-check");
707 Debug("fmf-full-check") << std::endl;
708 }
709 //Notice() << "StrongSolverTheoryUF: Check " << level << std::endl;
710 if( d_reps<=(unsigned)d_cardinality ){
711 Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
712 if( level==Theory::EFFORT_FULL ){
713 Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
714 //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl;
715 //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl;
716 //Notice() << cardinality << " ";
717 }
718 return;
719 }else{
720 //first check if we can generate a clique conflict
721 if( !options::ufssTotality() ){
722 //do a check within each region
723 for( int i=0; i<(int)d_regions_index; i++ ){
724 if( d_regions[i]->valid() ){
725 std::vector< Node > clique;
726 if( d_regions[i]->check( level, d_cardinality, clique ) ){
727 //add clique lemma
728 addCliqueLemma( clique, out );
729 return;
730 }else{
731 Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
732 }
733 }
734 }
735 }
736 if( !applyTotality( d_cardinality ) ){
737 //do splitting on demand
738 bool addedLemma = false;
739 if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
740 Trace("uf-ss-debug") << "Add splits?" << std::endl;
741 //see if we have any recommended splits from large regions
742 for( int i=0; i<(int)d_regions_index; i++ ){
743 if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){
744 //just add the clique lemma
745 if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){
746 std::vector< Node > clique;
747 if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){
748 //add clique lemma
749 addCliqueLemma( clique, out );
750 return;
751 }
752 }else{
753 int sp = addSplit( d_regions[i], out );
754 if( sp==1 ){
755 addedLemma = true;
756 #ifdef ONE_SPLIT_REGION
757 break;
758 #endif
759 }else if( sp==-1 ){
760 check( level, out );
761 return;
762 }
763 }
764 }
765 }
766 }
767 //If no added lemmas, force continuation via combination of regions.
768 if( level==Theory::EFFORT_FULL ){
769 if( !addedLemma ){
770 Trace("uf-ss-debug") << "No splits added. " << d_cardinality
771 << std::endl;
772 Trace("uf-ss-si") << "Must combine region" << std::endl;
773 bool recheck = false;
774 if( options::sortInference()){
775 //If sort inference is enabled, search for regions with same sort.
776 std::map< int, int > sortsFound;
777 for( int i=0; i<(int)d_regions_index; i++ ){
778 if( d_regions[i]->valid() ){
779 Node op = d_regions[i]->frontKey();
780 int sort_id = d_thss->getSortInference()->getSortId(op);
781 if( sortsFound.find( sort_id )!=sortsFound.end() ){
782 Debug("fmf-full-check") << "Combined regions " << i << " " << sortsFound[sort_id] << std::endl;
783 combineRegions( sortsFound[sort_id], i );
784 recheck = true;
785 break;
786 }else{
787 sortsFound[sort_id] = i;
788 }
789 }
790 }
791 }
792 if( !recheck ) {
793 //naive strategy, force region combination involving the first valid region
794 for( int i=0; i<(int)d_regions_index; i++ ){
795 if( d_regions[i]->valid() ){
796 int fcr = forceCombineRegion( i, false );
797 Debug("fmf-full-check") << "Combined regions " << i << " " << fcr << std::endl;
798 Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
799 recheck = true;
800 break;
801 }
802 }
803 }
804 if( recheck ){
805 Trace("uf-ss-debug") << "Must recheck." << std::endl;
806 check( level, out );
807 }
808 }
809 }
810 }
811 }
812 }
813 }
814
815 void SortModel::presolve() {
816 d_initialized = false;
817 d_aloc_cardinality = 0;
818 }
819
820 void SortModel::propagate( Theory::Effort level, OutputChannel* out ){
821
822 }
823
824 Node SortModel::getNextDecisionRequest(){
825 //request the current cardinality as a decision literal, if not already asserted
826 for( int i=1; i<=d_aloc_cardinality; i++ ){
827 if( !d_hasCard || i<d_cardinality ){
828 Node cn = d_cardinality_literal[ i ];
829 Assert( !cn.isNull() );
830 bool value;
831 if( !d_thss->getTheory()->d_valuation.hasSatValue( cn, value ) ){
832 Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl;
833 return cn;
834 }else{
835 Trace("uf-ss-dec-debug") << " dec : " << cn << " already asserted " << value << std::endl;
836 Assert( !value );
837 }
838 }
839 }
840 Trace("uf-ss-dec") << "UFSS : no decisions for " << d_type << "." << std::endl;
841 Trace("uf-ss-dec-debug") << " aloc_cardinality = " << d_aloc_cardinality << ", cardinality = " << d_cardinality << ", hasCard = " << d_hasCard << std::endl;
842 Assert( d_hasCard );
843 return Node::null();
844 }
845
846 bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){
847 if( options::ufssTotality() ){
848 //do nothing
849 }else{
850 if( m ){
851 #if 0
852 // ensure that the constructed model is minimal
853 // if the model has terms that the strong solver does not know about
854 if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){
855 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() );
856 while( !eqcs_i.isFinished() ){
857 Node eqc = (*eqcs_i);
858 if( eqc.getType()==d_type ){
859 //we must ensure that this equivalence class has been accounted for
860 if( d_regions_map.find( eqc )==d_regions_map.end() ){
861 //split on unaccounted for term and cardinality lemma term (as default)
862 Node splitEq = eqc.eqNode( d_cardinality_term );
863 splitEq = Rewriter::rewrite( splitEq );
864 Trace("uf-ss-minimize") << "Last chance minimize : " << splitEq << std::endl;
865 out->split( splitEq );
866 //tell the sat solver to explore the equals branch first
867 out->requirePhase( splitEq, true );
868 ++( d_thss->d_statistics.d_split_lemmas );
869 return false;
870 }
871 }
872 ++eqcs_i;
873 }
874 Assert( false );
875 }
876 #endif
877 }else{
878 Trace("uf-ss-debug") << "Minimize the UF model..." << std::endl;
879 //internal minimize, ensure that model forms a clique:
880 // if two equivalence classes are neither equal nor disequal, add a split
881 int validRegionIndex = -1;
882 for( int i=0; i<(int)d_regions_index; i++ ){
883 if( d_regions[i]->valid() ){
884 if( validRegionIndex!=-1 ){
885 combineRegions( validRegionIndex, i );
886 if( addSplit( d_regions[validRegionIndex], out )!=0 ){
887 Trace("uf-ss-debug") << "Minimize model : combined regions, found split. " << std::endl;
888 return false;
889 }
890 }else{
891 validRegionIndex = i;
892 }
893 }
894 }
895 Assert( validRegionIndex!=-1 );
896 if( addSplit( d_regions[validRegionIndex], out )!=0 ){
897 Trace("uf-ss-debug") << "Minimize model : found split. " << std::endl;
898 return false;
899 }
900 Trace("uf-ss-debug") << "Minimize success. " << std::endl;
901 }
902 }
903 return true;
904 }
905
906
907 int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
908 int ni = d_regions_map[n];
909 int counter = 0;
910 DiseqList* del = d_regions[ni]->getRegionInfo(n)->get(0);
911 for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
912 if( (*it).second ){
913 if( d_regions_map[ (*it).first ]==ri ){
914 counter++;
915 }
916 }
917 }
918 return counter;
919 }
920
921 void SortModel::getDisequalitiesToRegions(int ri,
922 std::map< int, int >& regions_diseq)
923 {
924 Region* region = d_regions[ri];
925 for(Region::iterator it = region->begin(); it != region->end(); ++it ){
926 if( it->second->valid() ){
927 DiseqList* del = it->second->get(0);
928 for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
929 if( (*it2).second ){
930 Assert( isValid( d_regions_map[ (*it2).first ] ) );
931 //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
932 regions_diseq[ d_regions_map[ (*it2).first ] ]++;
933 }
934 }
935 }
936 }
937 }
938
939 void SortModel::setSplitScore( Node n, int s ){
940 if( d_split_score.find( n )!=d_split_score.end() ){
941 int ss = d_split_score[ n ];
942 d_split_score[ n ] = s>ss ? s : ss;
943 }else{
944 d_split_score[ n ] = s;
945 }
946 for( int i=0; i<(int)n.getNumChildren(); i++ ){
947 setSplitScore( n[i], s+1 );
948 }
949 }
950
951 void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
952 if( !d_conflict ){
953 Trace("uf-ss-assert")
954 << "Assert cardinality "<< d_type << " " << c << " " << val << " level = "
955 << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl;
956 Assert( c>0 );
957 Node cl = getCardinalityLiteral( c );
958 if( val ){
959 bool doCheckRegions = !d_hasCard;
960 bool prevHasCard = d_hasCard;
961 d_hasCard = true;
962 if( !prevHasCard || c<d_cardinality ){
963 d_cardinality = c;
964 simpleCheckCardinality();
965 if( d_thss->d_conflict.get() ){
966 return;
967 }
968 }
969 //should check all regions now
970 if( doCheckRegions ){
971 for( int i=0; i<(int)d_regions_index; i++ ){
972 if( d_regions[i]->valid() ){
973 checkRegion( i );
974 if( d_conflict ){
975 return;
976 }
977 }
978 }
979 }
980 }else{
981 /*
982 if( options::ufssModelInference() ){
983 //check if we are at decision level 0
984 if( d_th->d_valuation.getAssertionLevel()==0 ){
985 Trace("uf-ss-mi") << "We have proved that no models of size " << c << " for type " << d_type << " exist." << std::endl;
986 Trace("uf-ss-mi") << " # Clique lemmas : " << d_cliques[c].size() << std::endl;
987 if( d_cliques[c].size()==1 ){
988 if( d_totality_terms[c+1].empty() ){
989 Trace("uf-ss-mi") << "*** Establish model" << std::endl;
990 //d_totality_terms[c+1].insert( d_totality_terms[c].begin(), d_cliques[c][0].begin(), d_cliques[c][0].end() );
991 }
992 }
993 }
994 }
995 */
996 //see if we need to request a new cardinality
997 if( !d_hasCard ){
998 bool needsCard = true;
999 for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){
1000 if( it->first<=d_aloc_cardinality.get() ){
1001 bool value;
1002 if( !d_thss->getTheory()->d_valuation.hasSatValue( it->second, value ) ){
1003 Debug("fmf-card-debug") << "..does not need allocate because we are waiting for " << it->second << std::endl;
1004 needsCard = false;
1005 break;
1006 }
1007 }
1008 }
1009 if( needsCard ){
1010 allocateCardinality( out );
1011 }
1012 }else{
1013 Debug("fmf-card-debug") << "..already has card = " << d_cardinality << std::endl;
1014 }
1015 if( c>d_maxNegCard.get() ){
1016 Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for " << d_type << " is now " << c << std::endl;
1017 d_maxNegCard.set( c );
1018 simpleCheckCardinality();
1019 }
1020 }
1021 }
1022 }
1023
1024 void SortModel::checkRegion( int ri, bool checkCombine ){
1025 if( isValid(ri) && d_hasCard ){
1026 Assert( d_cardinality>0 );
1027 if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
1028 ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
1029 //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
1030 // if( it->second ){
1031 // int inDeg = d_regions[i]->d_disequalities_size[1][ it-> first ];
1032 // int outDeg = d_regions[i]->d_disequalities_size[0][ it-> first ];
1033 // if( inDeg<outDeg ){
1034 // }
1035 // }
1036 //}
1037 int riNew = forceCombineRegion( ri, true );
1038 if( riNew>=0 ){
1039 checkRegion( riNew, checkCombine );
1040 }
1041 }
1042 //now check if region is in conflict
1043 std::vector< Node > clique;
1044 if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
1045 //explain clique
1046 addCliqueLemma( clique, &d_thss->getOutputChannel() );
1047 }
1048 }
1049 }
1050
1051 int SortModel::forceCombineRegion( int ri, bool useDensity ){
1052 if( !useDensity ){
1053 for( int i=0; i<(int)d_regions_index; i++ ){
1054 if( ri!=i && d_regions[i]->valid() ){
1055 return combineRegions( ri, i );
1056 }
1057 }
1058 return -1;
1059 }else{
1060 //this region must merge with another
1061 if( Debug.isOn("uf-ss-check-region") ){
1062 Debug("uf-ss-check-region") << "We must combine Region #" << ri << ". " << std::endl;
1063 d_regions[ri]->debugPrint("uf-ss-check-region");
1064 }
1065 //take region with maximum disequality density
1066 double maxScore = 0;
1067 int maxRegion = -1;
1068 std::map< int, int > regions_diseq;
1069 getDisequalitiesToRegions( ri, regions_diseq );
1070 for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
1071 Debug("uf-ss-check-region") << it->first << " : " << it->second << std::endl;
1072 }
1073 for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
1074 Assert( it->first!=ri );
1075 Assert( isValid( it->first ) );
1076 Assert( d_regions[ it->first ]->getNumReps()>0 );
1077 double tempScore = double(it->second)/double(d_regions[it->first]->getNumReps() );
1078 if( tempScore>maxScore ){
1079 maxRegion = it->first;
1080 maxScore = tempScore;
1081 }
1082 }
1083 if( maxRegion!=-1 ){
1084 if( Debug.isOn("uf-ss-check-region") ){
1085 Debug("uf-ss-check-region") << "Combine with region #" << maxRegion << ":" << std::endl;
1086 d_regions[maxRegion]->debugPrint("uf-ss-check-region");
1087 }
1088 return combineRegions( ri, maxRegion );
1089 }
1090 return -1;
1091 }
1092 }
1093
1094
1095 int SortModel::combineRegions( int ai, int bi ){
1096 #ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
1097 if( d_regions[ai]->getNumReps()<d_regions[bi]->getNumReps() ){
1098 return combineRegions( bi, ai );
1099 }
1100 #endif
1101 Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl;
1102 Assert( isValid( ai ) && isValid( bi ) );
1103 Region* region_bi = d_regions[bi];
1104 for(Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it){
1105 Region::RegionNodeInfo* rni = it->second;
1106 if( rni->valid() ){
1107 d_regions_map[ it->first ] = ai;
1108 }
1109 }
1110 //update regions disequal DO_THIS?
1111 d_regions[ai]->combine( d_regions[bi] );
1112 d_regions[bi]->setValid( false );
1113 return ai;
1114 }
1115
1116 void SortModel::moveNode( Node n, int ri ){
1117 Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl;
1118 Assert( isValid( d_regions_map[ n ] ) );
1119 Assert( isValid( ri ) );
1120 //move node to region ri
1121 d_regions[ri]->takeNode( d_regions[ d_regions_map[n] ], n );
1122 d_regions_map[n] = ri;
1123 }
1124
1125 void SortModel::allocateCardinality( OutputChannel* out ){
1126 if( d_aloc_cardinality>0 ){
1127 Trace("uf-ss-fmf") << "No model of size " << d_aloc_cardinality << " exists for type " << d_type << " in this branch" << std::endl;
1128 }
1129 Trace("uf-ss-debug") << "Allocate cardinality " << d_aloc_cardinality << " for type " << d_type << std::endl;
1130 if( Trace.isOn("uf-ss-cliques") ){
1131 Trace("uf-ss-cliques") << "Cliques of size " << (d_aloc_cardinality+1) << " for " << d_type << " : " << std::endl;
1132 for( size_t i=0; i<d_cliques[ d_aloc_cardinality ].size(); i++ ){
1133 Trace("uf-ss-cliques") << " ";
1134 for( size_t j=0; j<d_cliques[ d_aloc_cardinality ][i].size(); j++ ){
1135 Trace("uf-ss-cliques") << d_cliques[ d_aloc_cardinality ][i][j] << " ";
1136 }
1137 Trace("uf-ss-cliques") << std::endl;
1138 }
1139 }
1140
1141 //allocate the lowest such that it is not asserted
1142 Node cl;
1143 bool increment;
1144 do {
1145 increment = false;
1146 d_aloc_cardinality = d_aloc_cardinality + 1;
1147 cl = getCardinalityLiteral( d_aloc_cardinality );
1148 bool value;
1149 if( d_thss->getTheory()->d_valuation.hasSatValue( cl, value ) ){
1150 if( value ){
1151 //if one is already asserted postively, abort
1152 return;
1153 }else{
1154 increment = true;
1155 }
1156 }
1157 }while( increment );
1158
1159 //check for abort case
1160 if (options::ufssAbortCardinality() != -1 &&
1161 d_aloc_cardinality >= options::ufssAbortCardinality()) {
1162 Message() << "Maximum cardinality (" << options::ufssAbortCardinality()
1163 << ") for finite model finding exceeded." << std::endl;
1164 exit( 1 );
1165 }else{
1166 if( applyTotality( d_aloc_cardinality ) ){
1167 //must generate new cardinality lemma term
1168 Node var;
1169 if( d_aloc_cardinality==1 && !options::ufssTotalitySymBreak() ){
1170 //get arbitrary ground term
1171 var = d_cardinality_term;
1172 }else{
1173 std::stringstream ss;
1174 ss << "_c_" << d_aloc_cardinality;
1175 var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
1176 }
1177 if( d_aloc_cardinality-1<(int)d_totality_terms[0].size() ){
1178 d_totality_terms[0][d_aloc_cardinality-1] = var;
1179 }else{
1180 d_totality_terms[0].push_back( var );
1181 }
1182 Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl;
1183 //must be distinct from all other cardinality terms
1184 for( int i=0; i<(int)(d_totality_terms[0].size()-1); i++ ){
1185 Node lem = NodeManager::currentNM()->mkNode( NOT, var.eqNode( d_totality_terms[0][i] ) );
1186 Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem << std::endl;
1187 d_thss->getOutputChannel().lemma( lem );
1188 }
1189 }
1190
1191 //add splitting lemma for cardinality constraint
1192 Assert( !d_cardinality_term.isNull() );
1193 Node lem = getCardinalityLiteral( d_aloc_cardinality );
1194 lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
1195 d_cardinality_lemma[ d_aloc_cardinality ] = lem;
1196 //add as lemma to output channel
1197 if( doSendLemma( lem ) ){
1198 Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
1199 }
1200 //require phase
1201 out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true );
1202 //add the appropriate lemma, propagate as decision
1203 //Trace("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << " " << d_type << std::endl;
1204 //out->propagateAsDecision( lem[0] );
1205 d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality );
1206
1207 if( applyTotality( d_aloc_cardinality ) ){
1208 //must send totality axioms for each existing term
1209 for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
1210 addTotalityAxiom( (*it).first, d_aloc_cardinality, &d_thss->getOutputChannel() );
1211 }
1212 }
1213 }
1214 }
1215
1216 int SortModel::addSplit( Region* r, OutputChannel* out ){
1217 Node s;
1218 if( r->hasSplits() ){
1219 //take the first split you find
1220 for( Region::split_iterator it = r->begin_splits();
1221 it != r->end_splits(); ++it ){
1222 if( (*it).second ){
1223 s = (*it).first;
1224 break;
1225 }
1226 }
1227 Assert( s!=Node::null() );
1228 }
1229 if (!s.isNull() ){
1230 //add lemma to output channel
1231 Assert( s.getKind()==EQUAL );
1232 Node ss = Rewriter::rewrite( s );
1233 if( ss.getKind()!=EQUAL ){
1234 Node b_t = NodeManager::currentNM()->mkConst( true );
1235 Node b_f = NodeManager::currentNM()->mkConst( false );
1236 if( ss==b_f ){
1237 Trace("uf-ss-lemma") << "....Assert disequal directly : "
1238 << s[0] << " " << s[1] << std::endl;
1239 assertDisequal( s[0], s[1], b_t );
1240 return -1;
1241 }else{
1242 Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl;
1243 }
1244 if( ss==b_t ){
1245 Message() << "Bad split " << s << std::endl;
1246 exit( 16 );
1247 }
1248 }
1249 if( options::sortInference()) {
1250 for( int i=0; i<2; i++ ){
1251 int si = d_thss->getSortInference()->getSortId( ss[i] );
1252 Trace("uf-ss-split-si") << si << " ";
1253 }
1254 Trace("uf-ss-split-si") << std::endl;
1255 }
1256 //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
1257 //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
1258 //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
1259 //Notice() << "*** Split on " << s << std::endl;
1260 //split on the equality s
1261 Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
1262 if( doSendLemma( lem ) ){
1263 Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
1264 //tell the sat solver to explore the equals branch first
1265 out->requirePhase( ss, true );
1266 ++( d_thss->d_statistics.d_split_lemmas );
1267 }
1268 return 1;
1269 }else{
1270 return 0;
1271 }
1272 }
1273
1274
1275 void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
1276 Assert( d_hasCard );
1277 Assert( d_cardinality>0 );
1278 while( clique.size()>size_t(d_cardinality+1) ){
1279 clique.pop_back();
1280 }
1281 //debugging information
1282 if( Trace.isOn("uf-ss-cliques") ){
1283 std::vector< Node > clique_vec;
1284 clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
1285 addClique( d_cardinality, clique_vec );
1286 }
1287 if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){
1288 //add as lemma
1289 std::vector< Node > eqs;
1290 for( int i=0; i<(int)clique.size(); i++ ){
1291 for( int j=0; j<i; j++ ){
1292 Node r1 = d_thss->getTheory()->d_equalityEngine.getRepresentative(clique[i]);
1293 Node r2 = d_thss->getTheory()->d_equalityEngine.getRepresentative(clique[j]);
1294 eqs.push_back( clique[i].eqNode( clique[j] ) );
1295 }
1296 }
1297 eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
1298 Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
1299 if( doSendLemma( lem ) ){
1300 Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
1301 ++( d_thss->d_statistics.d_clique_lemmas );
1302 }
1303 }else{
1304 //found a clique
1305 Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
1306 Debug("uf-ss-cliques") << " ";
1307 for( int i=0; i<(int)clique.size(); i++ ){
1308 Debug("uf-ss-cliques") << clique[i] << " ";
1309 }
1310 Debug("uf-ss-cliques") << std::endl;
1311 Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl;
1312
1313 //we will scan through each of the disequaltities
1314 bool isSatConflict = true;
1315 std::vector< Node > conflict;
1316 //collect disequalities, and nodes that must be equal within representatives
1317 std::map< Node, std::map< Node, bool > > explained;
1318 std::map< Node, std::map< Node, bool > > nodesWithinRep;
1319 //map from the reprorted clique members to those reported in the lemma
1320 std::map< Node, Node > cliqueRepMap;
1321 for( int i=0; i<(int)d_disequalities_index; i++ ){
1322 //if both sides of disequality exist in clique
1323 Node r1 = d_thss->getTheory()->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
1324 Node r2 = d_thss->getTheory()->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
1325 if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
1326 std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
1327 std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
1328 explained[r1][r2] = true;
1329 explained[r2][r1] = true;
1330 if( options::ufssExplainedCliques() ){
1331 conflict.push_back( d_disequalities[i] );
1332 Debug("uf-ss-cliques") << " -> disequality : " << d_disequalities[i] << std::endl;
1333 nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
1334 nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
1335 }else{
1336 //get the terms we report in the lemma
1337 Node ru1 = r1;
1338 if( cliqueRepMap.find( r1 )==cliqueRepMap.end() ){
1339 ru1 = d_disequalities[i][0][0];
1340 cliqueRepMap[r1] = ru1;
1341 }else{
1342 ru1 = cliqueRepMap[r1];
1343 }
1344 Node ru2 = r2;
1345 if( cliqueRepMap.find( r2 )==cliqueRepMap.end() ){
1346 ru2 = d_disequalities[i][0][1];
1347 cliqueRepMap[r2] = ru2;
1348 }else{
1349 ru2 = cliqueRepMap[r2];
1350 }
1351 if( ru1!=d_disequalities[i][0][0] || ru2!=d_disequalities[i][0][1] ){
1352 //disequalities have endpoints that are not connected within an equivalence class
1353 // we will be producing a lemma, introducing a new literal ru1 != ru2
1354 conflict.push_back( ru1.eqNode( ru2 ).notNode() );
1355 isSatConflict = false;
1356 }else{
1357 conflict.push_back( d_disequalities[i] );
1358 }
1359 }
1360 if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
1361 break;
1362 }
1363 }
1364 }
1365 if( options::ufssExplainedCliques() ){
1366 //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl;
1367 Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
1368 //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
1369 Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl;
1370 //now, we must explain equalities within each equivalence class
1371 for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
1372 if( it->second.size()>1 ){
1373 Node prev;
1374 //add explanation of t1 = t2 = ... = tn
1375 Debug("uf-ss-cliques") << "Explain ";
1376 for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
1377 if( prev!=Node::null() ){
1378 Debug("uf-ss-cliques") << " = ";
1379 //explain it2->first and prev
1380 std::vector< TNode > expl;
1381 d_thss->getTheory()->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
1382 for( int i=0; i<(int)expl.size(); i++ ){
1383 if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
1384 conflict.push_back( expl[i] );
1385 }
1386 }
1387 }
1388 prev = it2->first;
1389 Debug("uf-ss-cliques") << prev;
1390 }
1391 Debug("uf-ss-cliques") << std::endl;
1392 }
1393 }
1394 Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
1395 for( int i=0; i<(int)conflict.size(); i++ ){
1396 Debug("uf-ss-cliques") << conflict[i] << " ";
1397 }
1398 Debug("uf-ss-cliques") << std::endl;
1399 }
1400 //now, make the conflict
1401 if( isSatConflict ){
1402 conflict.push_back( d_cardinality_literal[ d_cardinality ] );
1403 Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict );
1404 Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
1405 //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
1406 out->conflict( conflictNode );
1407 d_conflict = true;
1408 ++( d_thss->d_statistics.d_clique_conflicts );
1409 }else{
1410 Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
1411 //add cardinality constraint
1412 Node cardNode = d_cardinality_literal[ d_cardinality ];
1413 //bool value;
1414 //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value );
1415 //Assert( hasValue );
1416 //Assert( value );
1417 conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
1418 if( doSendLemma( conflictNode ) ){
1419 Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
1420 ++( d_thss->d_statistics.d_clique_lemmas );
1421 }
1422 }
1423
1424 //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique.
1425 }
1426 }
1427
1428 void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
1429 if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
1430 if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){
1431 d_totality_lems[n].push_back( cardinality );
1432 Node cardLit = d_cardinality_literal[ cardinality ];
1433 int sort_id = 0;
1434 if( options::sortInference() ){
1435 sort_id = d_thss->getSortInference()->getSortId(n);
1436 }
1437 Trace("uf-ss-totality") << "Add totality lemma for " << n << " " << cardinality << ", sort id is " << sort_id << std::endl;
1438 int use_cardinality = cardinality;
1439 if( options::ufssTotalitySymBreak() ){
1440 if( d_sym_break_index.find(n)!=d_sym_break_index.end() ){
1441 use_cardinality = d_sym_break_index[n];
1442 }else if( (int)d_sym_break_terms[n.getType()][sort_id].size()<cardinality-1 ){
1443 use_cardinality = d_sym_break_terms[n.getType()][sort_id].size() + 1;
1444 d_sym_break_terms[n.getType()][sort_id].push_back( n );
1445 d_sym_break_index[n] = use_cardinality;
1446 Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n << ", index = " << use_cardinality << std::endl;
1447 if( d_sym_break_terms[n.getType()][sort_id].size()>1 ){
1448 //enforce canonicity
1449 for( int i=2; i<use_cardinality; i++ ){
1450 //can only be assigned to domain constant d if someone has been assigned domain constant d-1
1451 Node eq = n.eqNode( getTotalityLemmaTerm( cardinality, i ) );
1452 std::vector< Node > eqs;
1453 for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){
1454 eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) );
1455 }
1456 Node ax = eqs.size()==1 ? eqs[0] : NodeManager::currentNM()->mkNode( OR, eqs );
1457 Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax );
1458 Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl;
1459 d_thss->getOutputChannel().lemma( lem );
1460 }
1461 }
1462 }
1463 }
1464
1465 std::vector< Node > eqs;
1466 for( int i=0; i<use_cardinality; i++ ){
1467 eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) );
1468 }
1469 Node ax = NodeManager::currentNM()->mkNode( OR, eqs );
1470 Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax );
1471 Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl;
1472 //send as lemma to the output channel
1473 d_thss->getOutputChannel().lemma( lem );
1474 ++( d_thss->d_statistics.d_totality_lemmas );
1475 }
1476 }
1477 }
1478
1479 void SortModel::addClique( int c, std::vector< Node >& clique ) {
1480 //if( d_clique_trie[c].add( clique ) ){
1481 // d_cliques[ c ].push_back( clique );
1482 //}
1483 }
1484
1485
1486 /** apply totality */
1487 bool SortModel::applyTotality( int cardinality ){
1488 return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
1489 // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
1490 }
1491
1492 /** get totality lemma terms */
1493 Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){
1494 return d_totality_terms[0][i];
1495 //}else{
1496 // return d_totality_terms[cardinality][i];
1497 //}
1498 }
1499
1500 void SortModel::simpleCheckCardinality() {
1501 if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()<d_maxNegCard.get() ){
1502 Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
1503 getCardinalityLiteral( d_maxNegCard.get() ).negate() );
1504 Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
1505 d_thss->getOutputChannel().conflict( lem );
1506 d_thss->d_conflict.set( true );
1507 }
1508 }
1509
1510 bool SortModel::doSendLemma( Node lem ) {
1511 if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){
1512 d_lemma_cache[lem] = true;
1513 d_thss->getOutputChannel().lemma( lem );
1514 return true;
1515 }else{
1516 return false;
1517 }
1518 }
1519
1520 void SortModel::debugPrint( const char* c ){
1521 if( Debug.isOn( c ) ){
1522 Debug( c ) << "Number of reps = " << d_reps << std::endl;
1523 Debug( c ) << "Cardinality req = " << d_cardinality << std::endl;
1524 unsigned debugReps = 0;
1525 for( unsigned i=0; i<d_regions_index; i++ ){
1526 Region* region = d_regions[i];
1527 if( region->valid() ){
1528 Debug( c ) << "Region #" << i << ": " << std::endl;
1529 region->debugPrint( c, true );
1530 Debug( c ) << std::endl;
1531 for( Region::iterator it = region->begin(); it != region->end(); ++it ){
1532 if( it->second->valid() ){
1533 if( d_regions_map[ it->first ]!=(int)i ){
1534 Debug( c ) << "***Bad regions map : " << it->first
1535 << " " << d_regions_map[ it->first ].get() << std::endl;
1536 }
1537 }
1538 }
1539 debugReps += region->getNumReps();
1540 }
1541 }
1542
1543 if( debugReps!=d_reps ){
1544 Debug( c ) << "***Bad reps: " << d_reps << ", "
1545 << "actual = " << debugReps << std::endl;
1546 }
1547 }
1548 }
1549
1550 bool SortModel::debugModel( TheoryModel* m ){
1551 if( Trace.isOn("uf-ss-warn") ){
1552 std::vector< Node > eqcs;
1553 eq::EqClassesIterator eqcs_i =
1554 eq::EqClassesIterator(m->getEqualityEngine());
1555 while( !eqcs_i.isFinished() ){
1556 Node eqc = (*eqcs_i);
1557 if( eqc.getType()==d_type ){
1558 if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
1559 eqcs.push_back( eqc );
1560 //we must ensure that this equivalence class has been accounted for
1561 if( d_regions_map.find( eqc )==d_regions_map.end() ){
1562 Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
1563 Trace("uf-ss-warn") << " type : " << d_type << std::endl;
1564 Trace("uf-ss-warn") << " kind : " << eqc.getKind() << std::endl;
1565 }
1566 }
1567 }
1568 ++eqcs_i;
1569 }
1570 }
1571 RepSet* rs = m->getRepSetPtr();
1572 int nReps = (int)rs->getNumRepresentatives(d_type);
1573 if( nReps!=(d_maxNegCard+1) ){
1574 Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
1575 Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard << std::endl;
1576 Trace("uf-ss-warn") << " # Reps : " << nReps << std::endl;
1577 if( d_maxNegCard>=nReps ){
1578 /*
1579 for( unsigned i=0; i<d_fresh_aloc_reps.size(); i++ ){
1580 if( add>0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){
1581 rs->d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] );
1582 add--;
1583 }
1584 }
1585 for( int i=0; i<add; i++ ){
1586 std::stringstream ss;
1587 ss << "r_" << d_type << "_";
1588 Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type,
1589 "enumeration to meet negative card constraint" );
1590 d_fresh_aloc_reps.push_back( nn );
1591 rs->d_type_reps[d_type].push_back( nn );
1592 }
1593 */
1594 while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){
1595 std::stringstream ss;
1596 ss << "r_" << d_type << "_";
1597 Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
1598 d_fresh_aloc_reps.push_back( nn );
1599 }
1600 if( d_maxNegCard==0 ){
1601 rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]);
1602 }else{
1603 //must add lemma
1604 std::vector< Node > force_cl;
1605 for( int i=0; i<=d_maxNegCard; i++ ){
1606 for( int j=(i+1); j<=d_maxNegCard; j++ ){
1607 force_cl.push_back( d_fresh_aloc_reps[i].eqNode( d_fresh_aloc_reps[j] ).negate() );
1608 }
1609 }
1610 Node cl = getCardinalityLiteral( d_maxNegCard );
1611 Node lem = NodeManager::currentNM()->mkNode( OR, cl, NodeManager::currentNM()->mkNode( AND, force_cl ) );
1612 Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
1613 d_thss->getOutputChannel().lemma( lem );
1614 return false;
1615 }
1616 }
1617 }
1618 return true;
1619 }
1620
1621 int SortModel::getNumRegions(){
1622 int count = 0;
1623 for( int i=0; i<(int)d_regions_index; i++ ){
1624 if( d_regions[i]->valid() ){
1625 count++;
1626 }
1627 }
1628 return count;
1629 }
1630
1631 Node SortModel::getCardinalityLiteral( int c ) {
1632 if( d_cardinality_literal.find(c) == d_cardinality_literal.end() ){
1633 Node c_as_rational = NodeManager::currentNM()->mkConst(Rational(c));
1634 d_cardinality_literal[c] =
1635 NodeManager::currentNM()->mkNode(CARDINALITY_CONSTRAINT,
1636 d_cardinality_term,
1637 c_as_rational);
1638
1639 }
1640 return d_cardinality_literal[c];
1641 }
1642
1643 StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
1644 context::UserContext* u,
1645 OutputChannel& out, TheoryUF* th)
1646 : d_out(&out),
1647 d_th(th),
1648 d_conflict(c, false),
1649 d_rep_model(),
1650 d_aloc_com_card(u, 0),
1651 d_com_card_assertions(c),
1652 d_min_pos_com_card(c, -1),
1653 d_card_assertions_eqv_lemma(u),
1654 d_min_pos_tn_master_card(c, -1),
1655 d_rel_eqc(c),
1656 d_deq_prop(NULL),
1657 d_sym_break(NULL) {
1658 if (options::ufssDiseqPropagation()) {
1659 d_deq_prop = new DisequalityPropagator(th->getQuantifiersEngine(), this);
1660 }
1661 if (options::ufssSymBreak()) {
1662 d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c);
1663 }
1664 }
1665
1666 StrongSolverTheoryUF::~StrongSolverTheoryUF() {
1667 for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1668 it != d_rep_model.end(); ++it) {
1669 delete it->second;
1670 }
1671 if (d_sym_break) {
1672 delete d_sym_break;
1673 }
1674 if (d_deq_prop) {
1675 delete d_deq_prop;
1676 }
1677 }
1678
1679 SortInference* StrongSolverTheoryUF::getSortInference() {
1680 return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference();
1681 }
1682
1683 /** get default sat context */
1684 context::Context* StrongSolverTheoryUF::getSatContext() {
1685 return d_th->getSatContext();
1686 }
1687
1688 /** get default output channel */
1689 OutputChannel& StrongSolverTheoryUF::getOutputChannel() {
1690 return d_th->getOutputChannel();
1691 }
1692
1693 /** ensure eqc */
1694 void StrongSolverTheoryUF::ensureEqc( SortModel* c, Node a ) {
1695 if( !hasEqc( a ) ){
1696 d_rel_eqc[a] = true;
1697 Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
1698 c->newEqClass( a );
1699 if( options::ufssSymBreak() ){
1700 d_sym_break->newEqClass( a );
1701 }
1702 Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
1703 }
1704 }
1705
1706 void StrongSolverTheoryUF::ensureEqcRec( Node n ) {
1707 if( !hasEqc( n ) ){
1708 SortModel* c = getSortModel( n );
1709 if( c ){
1710 ensureEqc( c, n );
1711 }
1712 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1713 ensureEqcRec( n[i] );
1714 }
1715 }
1716 }
1717
1718 /** has eqc */
1719 bool StrongSolverTheoryUF::hasEqc( Node a ) {
1720 NodeBoolMap::iterator it = d_rel_eqc.find( a );
1721 return it!=d_rel_eqc.end() && (*it).second;
1722 }
1723
1724 /** new node */
1725 void StrongSolverTheoryUF::newEqClass( Node a ){
1726 SortModel* c = getSortModel( a );
1727 if( c ){
1728 #ifdef LAZY_REL_EQC
1729 //do nothing
1730 #else
1731 Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
1732 c->newEqClass( a );
1733 if( options::ufssSymBreak() ){
1734 d_sym_break->newEqClass( a );
1735 }
1736 Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
1737 #endif
1738 }
1739 }
1740
1741 /** merge */
1742 void StrongSolverTheoryUF::merge( Node a, Node b ){
1743 //TODO: ensure they are relevant
1744 SortModel* c = getSortModel( a );
1745 if( c ){
1746 #ifdef LAZY_REL_EQC
1747 ensureEqc( c, a );
1748 if( hasEqc( b ) ){
1749 Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
1750 c->merge( a, b );
1751 Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
1752 }else{
1753 //c->assignEqClass( b, a );
1754 d_rel_eqc[b] = true;
1755 }
1756 #else
1757 Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
1758 c->merge( a, b );
1759 Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
1760 #endif
1761 }else{
1762 if( options::ufssDiseqPropagation() ){
1763 d_deq_prop->merge(a, b);
1764 }
1765 }
1766 }
1767
1768 /** assert terms are disequal */
1769 void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
1770 SortModel* c = getSortModel( a );
1771 if( c ){
1772 #ifdef LAZY_REL_EQC
1773 ensureEqc( c, a );
1774 ensureEqc( c, b );
1775 #endif
1776 Trace("uf-ss-solver") << "StrongSolverTheoryUF: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl;
1777 //Assert( d_th->d_equalityEngine.getRepresentative( a )==a );
1778 //Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
1779 c->assertDisequal( a, b, reason );
1780 Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Assert disequal." << std::endl;
1781 }else{
1782 if( options::ufssDiseqPropagation() ){
1783 d_deq_prop->assertDisequal(a, b, reason);
1784 }
1785 }
1786 }
1787
1788 /** assert a node */
1789 void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
1790 Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
1791 #ifdef LAZY_REL_EQC
1792 ensureEqcRec( n );
1793 #endif
1794 bool polarity = n.getKind() != kind::NOT;
1795 TNode lit = polarity ? n : n[0];
1796 if( options::ufssMode()==UF_SS_FULL ){
1797 if( lit.getKind()==CARDINALITY_CONSTRAINT ){
1798 TypeNode tn = lit[0].getType();
1799 Assert( tn.isSort() );
1800 Assert( d_rep_model[tn] );
1801 int nCard = lit[1].getConst<Rational>().getNumerator().getSignedInt();
1802 Node ct = d_rep_model[tn]->getCardinalityTerm();
1803 Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
1804 if( lit[0]==ct ){
1805 if( options::ufssFairnessMonotone() ){
1806 Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
1807 if( tn!=d_tn_mono_master ){
1808 std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
1809 if( it==d_tn_mono_slave.end() ){
1810 bool isMonotonic;
1811 if( d_th->getQuantifiersEngine() ){
1812 isMonotonic = getSortInference()->isMonotonic( tn );
1813 }else{
1814 //if ground, everything is monotonic
1815 isMonotonic = true;
1816 }
1817 if( isMonotonic ){
1818 if( d_tn_mono_master.isNull() ){
1819 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
1820 d_tn_mono_master = tn;
1821 }else{
1822 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
1823 d_tn_mono_slave[tn] = true;
1824 }
1825 }else{
1826 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl;
1827 d_tn_mono_slave[tn] = false;
1828 }
1829 }
1830 }
1831 //set the minimum positive cardinality for master if necessary
1832 if( polarity && tn==d_tn_mono_master ){
1833 Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl;
1834 if( d_min_pos_tn_master_card.get()==-1 || nCard<d_min_pos_tn_master_card.get() ){
1835 d_min_pos_tn_master_card.set( nCard );
1836 }
1837 }
1838 }
1839 Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
1840 d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
1841 //check if combined cardinality is violated
1842 checkCombinedCardinality();
1843 }else{
1844 //otherwise, make equal via lemma
1845 if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
1846 Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
1847 eqv_lit = lit.eqNode( eqv_lit );
1848 Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
1849 getOutputChannel().lemma( eqv_lit );
1850 d_card_assertions_eqv_lemma[lit] = true;
1851 }
1852 }
1853 }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
1854 d_com_card_assertions[lit] = polarity;
1855 if( polarity ){
1856 //safe to assume int here
1857 int nCard = lit[0].getConst<Rational>().getNumerator().getSignedInt();
1858 if( d_min_pos_com_card.get()==-1 || nCard<d_min_pos_com_card.get() ){
1859 d_min_pos_com_card.set( nCard );
1860 checkCombinedCardinality();
1861 }
1862 }else{
1863 bool needsCard = true;
1864 if( d_min_pos_com_card.get()==-1 ){
1865 //check if all current combined cardinality constraints are asserted negatively
1866 for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){
1867 if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() ){
1868 Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : non-assertion : " << it->first << std::endl;
1869 needsCard = false;
1870 break;
1871 }else{
1872 Assert( !d_com_card_assertions[it->second] );
1873 }
1874 }
1875 }else{
1876 Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : positive assertion : " << d_min_pos_com_card.get() << std::endl;
1877 needsCard = false;
1878 }
1879 if( needsCard ){
1880 allocateCombinedCardinality();
1881 }
1882 }
1883 }else{
1884 if( Trace.isOn("uf-ss-warn") ){
1885 ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
1886 //// a theory propagation is not a decision.
1887 if( isDecision ){
1888 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1889 if( !it->second->hasCardinalityAsserted() ){
1890 Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
1891 //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
1892 //Unimplemented();
1893 }
1894 }
1895 }
1896 }
1897 if( lit.getKind()!=EQUAL ){
1898 //it is a predicate
1899 if( options::ufssDiseqPropagation() ){
1900 d_deq_prop->assertPredicate(lit, polarity);
1901 }
1902 }
1903 }
1904 }else{
1905 if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
1906 // cardinality constraint from user input, set incomplete
1907 Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
1908 d_out->setIncomplete();
1909 }
1910 }
1911 Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
1912 }
1913
1914 bool StrongSolverTheoryUF::areDisequal( Node a, Node b ) {
1915 if( a==b ){
1916 return false;
1917 }else{
1918 a = d_th->d_equalityEngine.getRepresentative( a );
1919 b = d_th->d_equalityEngine.getRepresentative( b );
1920 if( d_th->d_equalityEngine.areDisequal( a, b, false ) ){
1921 return true;
1922 }else{
1923 SortModel* c = getSortModel( a );
1924 if( c ){
1925 return c->areDisequal( a, b );
1926 }else{
1927 return false;
1928 }
1929 }
1930 }
1931 }
1932
1933 /** check */
1934 void StrongSolverTheoryUF::check( Theory::Effort level ){
1935 if( !d_conflict ){
1936 if( options::ufssMode()==UF_SS_FULL ){
1937 Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl;
1938 if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){
1939 debugPrint( "uf-ss-debug" );
1940 }
1941 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1942 it->second->check( level, d_out );
1943 if( it->second->isConflict() ){
1944 d_conflict = true;
1945 break;
1946 }
1947 }
1948 //check symmetry breaker
1949 if( !d_conflict && options::ufssSymBreak() ){
1950 d_sym_break->check( level );
1951 }
1952 }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){
1953 if( level==Theory::EFFORT_FULL ){
1954 // split on an equality between two equivalence classes (at most one per type)
1955 std::map< TypeNode, std::vector< Node > > eqc_list;
1956 std::map< TypeNode, bool > type_proc;
1957 eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine());
1958 while( !eqcs_i.isFinished() ){
1959 Node a = *eqcs_i;
1960 TypeNode tn = a.getType();
1961 if( tn.isSort() ){
1962 if( type_proc.find( tn )==type_proc.end() ){
1963 std::map< TypeNode, std::vector< Node > >::iterator itel = eqc_list.find( tn );
1964 if( itel!=eqc_list.end() ){
1965 for( unsigned j=0; j<itel->second.size(); j++ ){
1966 Node b = itel->second[j];
1967 if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){
1968 Node eq = Rewriter::rewrite( a.eqNode( b ) );
1969 Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
1970 Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
1971 d_out->lemma( lem );
1972 d_out->requirePhase( eq, true );
1973 type_proc[tn] = true;
1974 break;
1975 }
1976 }
1977 }
1978 eqc_list[tn].push_back( a );
1979 }
1980 }
1981 ++eqcs_i;
1982 }
1983 }
1984 }else{
1985 // unhandled uf ss mode
1986 Assert( false );
1987 }
1988 Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl;
1989 }
1990 }
1991
1992 void StrongSolverTheoryUF::presolve() {
1993 d_aloc_com_card.set( 0 );
1994 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1995 it->second->presolve();
1996 it->second->initialize( d_out );
1997 }
1998 }
1999
2000 /** get next decision request */
2001 Node StrongSolverTheoryUF::getNextDecisionRequest( unsigned& priority ){
2002 //request the combined cardinality as a decision literal, if not already asserted
2003 if( options::ufssMode()==UF_SS_FULL ){
2004 if( options::ufssFairness() ){
2005 int comCard = 0;
2006 Node com_lit;
2007 do {
2008 if( comCard<d_aloc_com_card.get() ){
2009 com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null();
2010 if( !com_lit.isNull() && d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){
2011 Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl;
2012 priority = 1;
2013 return com_lit;
2014 }
2015 comCard++;
2016 }else{
2017 com_lit = Node::null();
2018 }
2019 }while( !com_lit.isNull() );
2020 }
2021 //otherwise, check each individual sort
2022 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
2023 Node n = it->second->getNextDecisionRequest();
2024 if( !n.isNull() ){
2025 priority = 1;
2026 return n;
2027 }
2028 }
2029 }
2030 Trace("uf-ss-dec") << "...no UF SS decisions." << std::endl;
2031 return Node::null();
2032 }
2033
2034 void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
2035 if( options::ufssMode()==UF_SS_FULL ){
2036 //initialize combined cardinality
2037 initializeCombinedCardinality();
2038
2039 Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
2040 //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
2041 TypeNode tn = n.getType();
2042 std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
2043 if( it==d_rep_model.end() ){
2044 SortModel* rm = NULL;
2045 if( tn.isSort() ){
2046 Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
2047 rm = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
2048 //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
2049 }else{
2050 /*
2051 if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
2052 Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
2053 Debug("uf-ss-na") << " (" << f << ")";
2054 Debug("uf-ss-na") << std::endl;
2055 Unimplemented("Cannot perform finite model finding on arithmetic quantifier");
2056 }else if( tn.isDatatype() ){
2057 Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
2058 Debug("uf-ss-na") << " (" << f << ")";
2059 Debug("uf-ss-na") << std::endl;
2060 Unimplemented("Cannot perform finite model finding on datatype quantifier");
2061 }
2062 */
2063 }
2064 if( rm ){
2065 rm->initialize( d_out );
2066 d_rep_model[tn] = rm;
2067 //d_rep_model_init[tn] = true;
2068 }
2069 }else{
2070 //ensure sort model is initialized
2071 it->second->initialize( d_out );
2072 }
2073 }
2074 }
2075
2076 //void StrongSolverTheoryUF::registerQuantifier( Node f ){
2077 // Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
2078 //must ensure the quantifier does not quantify over arithmetic
2079 //for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
2080 // TypeNode tn = f[0][i].getType();
2081 // preRegisterType( tn, true );
2082 //}
2083 //}
2084
2085
2086 SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
2087 TypeNode tn = n.getType();
2088 std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
2089 //pre-register the type if not done already
2090 if( it==d_rep_model.end() ){
2091 preRegisterTerm( n );
2092 it = d_rep_model.find( tn );
2093 }
2094 if( it!=d_rep_model.end() ){
2095 return it->second;
2096 }else{
2097 return NULL;
2098 }
2099 }
2100
2101 void StrongSolverTheoryUF::notifyRestart(){}
2102
2103 /** get cardinality for sort */
2104 int StrongSolverTheoryUF::getCardinality( Node n ) {
2105 SortModel* c = getSortModel( n );
2106 if( c ){
2107 return c->getCardinality();
2108 }else{
2109 return -1;
2110 }
2111 }
2112
2113 int StrongSolverTheoryUF::getCardinality( TypeNode tn ) {
2114 std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
2115 if( it!=d_rep_model.end() && it->second ){
2116 return it->second->getCardinality();
2117 }
2118 return -1;
2119 }
2120
2121 bool StrongSolverTheoryUF::minimize( TheoryModel* m ){
2122 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
2123 if( !it->second->minimize( d_out, m ) ){
2124 return false;
2125 }
2126 }
2127 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
2128 Trace("uf-ss-minimize") << "Cardinality( " << it->first << " ) : " << it->second->getCardinality() << std::endl;
2129 }
2130 return true;
2131 }
2132
2133 //print debug
2134 void StrongSolverTheoryUF::debugPrint( const char* c ){
2135 //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine );
2136 //while( !eqc_iter.isFinished() ){
2137 // Debug( c ) << "Eq class [[" << (*eqc_iter) << "]]" << std::endl;
2138 // EqClassIterator< TheoryUF::NotifyClass > eqc_iter2( *eqc_iter, &((TheoryUF*)d_th)->d_equalityEngine );
2139 // Debug( c ) << " ";
2140 // while( !eqc_iter2.isFinished() ){
2141 // Debug( c ) << "[" << (*eqc_iter2) << "] ";
2142 // eqc_iter2++;
2143 // }
2144 // Debug( c ) << std::endl;
2145 // eqc_iter++;
2146 //}
2147
2148 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
2149 Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl;
2150 it->second->debugPrint( c );
2151 Debug( c ) << std::endl;
2152 }
2153 }
2154
2155 bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){
2156 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
2157 if( !it->second->debugModel( m ) ){
2158 return false;
2159 }
2160 }
2161 return true;
2162 }
2163
2164 /** initialize */
2165 void StrongSolverTheoryUF::initializeCombinedCardinality() {
2166 Assert( options::ufssMode()==UF_SS_FULL );
2167 if( options::ufssFairness() ){
2168 if( d_aloc_com_card.get()==0 ){
2169 Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl;
2170 allocateCombinedCardinality();
2171 }
2172 }
2173 }
2174
2175 /** check */
2176 void StrongSolverTheoryUF::checkCombinedCardinality() {
2177 Assert( options::ufssMode()==UF_SS_FULL );
2178 if( options::ufssFairness() ){
2179 Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
2180 int totalCombinedCard = 0;
2181 int maxMonoSlave = 0;
2182 TypeNode maxSlaveType;
2183 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
2184 int max_neg = it->second->getMaximumNegativeCardinality();
2185 if( !options::ufssFairnessMonotone() ){
2186 totalCombinedCard += max_neg;
2187 }else{
2188 std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first );
2189 if( its==d_tn_mono_slave.end() || !its->second ){
2190 totalCombinedCard += max_neg;
2191 }else{
2192 if( max_neg>maxMonoSlave ){
2193 maxMonoSlave = max_neg;
2194 maxSlaveType = it->first;
2195 }
2196 }
2197 }
2198 }
2199 Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl;
2200 if( options::ufssFairnessMonotone() ){
2201 Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave << std::endl;
2202 if( d_min_pos_tn_master_card.get()!=-1 && maxMonoSlave>d_min_pos_tn_master_card.get() ){
2203 int mc = d_min_pos_tn_master_card.get();
2204 std::vector< Node > conf;
2205 conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) );
2206 conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() );
2207 Node cf = NodeManager::currentNM()->mkNode( AND, conf );
2208 Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict"
2209 << " : " << cf << std::endl;
2210 Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
2211 << " : " << cf << std::endl;
2212 getOutputChannel().conflict( cf );
2213 d_conflict.set( true );
2214 return;
2215 }
2216 }
2217 int cc = d_min_pos_com_card.get();
2218 if( cc !=-1 && totalCombinedCard > cc ){
2219 //conflict
2220 Assert( d_com_card_literal.find( cc ) != d_com_card_literal.end() );
2221 Node com_lit = d_com_card_literal[cc];
2222 Assert(d_com_card_assertions.find(com_lit)!=d_com_card_assertions.end());
2223 Assert( d_com_card_assertions[com_lit] );
2224 std::vector< Node > conf;
2225 conf.push_back( com_lit );
2226 int totalAdded = 0;
2227 for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin();
2228 it != d_rep_model.end(); ++it ){
2229 bool doAdd = true;
2230 if( options::ufssFairnessMonotone() ){
2231 std::map< TypeNode, bool >::iterator its =
2232 d_tn_mono_slave.find( it->first );
2233 if( its!=d_tn_mono_slave.end() && its->second ){
2234 doAdd = false;
2235 }
2236 }
2237 if( doAdd ){
2238 int c = it->second->getMaximumNegativeCardinality();
2239 if( c>0 ){
2240 conf.push_back( it->second->getCardinalityLiteral( c ).negate() );
2241 totalAdded += c;
2242 }
2243 if( totalAdded>cc ){
2244 break;
2245 }
2246 }
2247 }
2248 Node cf = NodeManager::currentNM()->mkNode( AND, conf );
2249 Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
2250 << std::endl;
2251 Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
2252 << std::endl;
2253 getOutputChannel().conflict( cf );
2254 d_conflict.set( true );
2255 }
2256 }
2257 }
2258
2259 void StrongSolverTheoryUF::allocateCombinedCardinality() {
2260 Assert( options::ufssMode()==UF_SS_FULL );
2261 Trace("uf-ss-com-card") << "Allocate combined cardinality (" << d_aloc_com_card.get() << ")" << std::endl;
2262 //make node
2263 Node lem = NodeManager::currentNM()->mkNode( COMBINED_CARDINALITY_CONSTRAINT,
2264 NodeManager::currentNM()->mkConst( Rational( d_aloc_com_card.get() ) ) );
2265 Trace("uf-ss-com-card") << "Split on " << lem << std::endl;
2266 lem = Rewriter::rewrite(lem);
2267 d_com_card_literal[ d_aloc_com_card.get() ] = lem;
2268 lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
2269 //add as lemma to output channel
2270 Trace("uf-ss-lemma") << "*** Combined cardinality split : " << lem << std::endl;
2271 getOutputChannel().lemma( lem );
2272 //require phase
2273 getOutputChannel().requirePhase( d_com_card_literal[ d_aloc_com_card.get() ], true );
2274 //increment cardinality
2275 d_aloc_com_card.set( d_aloc_com_card.get() + 1 );
2276 }
2277
2278 StrongSolverTheoryUF::Statistics::Statistics():
2279 d_clique_conflicts("StrongSolverTheoryUF::Clique_Conflicts", 0),
2280 d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0),
2281 d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0),
2282 d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0),
2283 d_sym_break_lemmas("StrongSolverTheoryUF::Symmetry_Breaking_Lemmas", 0),
2284 d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0),
2285 d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1)
2286 {
2287 smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
2288 smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
2289 smtStatisticsRegistry()->registerStat(&d_split_lemmas);
2290 smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas);
2291 smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas);
2292 smtStatisticsRegistry()->registerStat(&d_totality_lemmas);
2293 smtStatisticsRegistry()->registerStat(&d_max_model_size);
2294 }
2295
2296 StrongSolverTheoryUF::Statistics::~Statistics(){
2297 smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
2298 smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
2299 smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
2300 smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas);
2301 smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas);
2302 smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas);
2303 smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
2304 }
2305
2306
2307 DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe,
2308 StrongSolverTheoryUF* ufss)
2309 : d_qe(qe), d_ufss(ufss)
2310 {
2311 d_true = NodeManager::currentNM()->mkConst( true );
2312 d_false = NodeManager::currentNM()->mkConst( false );
2313 }
2314
2315 void DisequalityPropagator::checkEquivalenceClass( Node t, Node eqc ) {
2316 if( t.getKind()==APPLY_UF ){
2317 Node op = t.getOperator();
2318 eqc = d_ufss->getTheory()->getEqualityEngine()->getRepresentative( eqc );
2319 eq::EqClassIterator eqc_i(eqc, d_ufss->getTheory()->getEqualityEngine());
2320 while( !eqc_i.isFinished() ){
2321 Node s = *eqc_i;
2322 if( s.getKind()==APPLY_UF && s.getOperator()==op ){
2323 int unkIndex = -1;
2324 for( size_t i=0; i<t.getNumChildren(); i++ ){
2325 //should consult strong solver since it knows more disequalities
2326 if( d_ufss->areDisequal( t[i], s[i] ) ){
2327 //if( d_qe->getEqualityQuery()->areDisequal( t[i], s[i] ) ){
2328 unkIndex = -1;
2329 break;
2330 }else if( !d_qe->getEqualityQuery()->areEqual( t[i], s[i] ) ){
2331 if( unkIndex==-1 ){
2332 unkIndex = i;
2333 }else{
2334 unkIndex = -1;
2335 break;
2336 }
2337 }
2338 }
2339 if( unkIndex!=-1 ){
2340 Trace("deq-prop") << "propagate disequality " << t[unkIndex] << " " << s[unkIndex] << std::endl;
2341 d_ufss->assertDisequal(t[unkIndex], s[unkIndex], Node::null());
2342 ++( d_statistics.d_propagations );
2343 if( d_ufss->isConflict() ){
2344 return;
2345 }
2346 }
2347 }
2348 ++eqc_i;
2349 }
2350 }
2351 }
2352
2353 /** merge */
2354 void DisequalityPropagator::merge( Node a, Node b ){
2355
2356 }
2357
2358 /** assert terms are disequal */
2359 void DisequalityPropagator::assertDisequal( Node a, Node b, Node reason ){
2360 Trace("deq-prop") << "Notify disequal : " << a << " " << b << std::endl;
2361 }
2362
2363
2364 void DisequalityPropagator::assertPredicate( Node p, bool polarity ) {
2365 Trace("deq-prop") << "Assert predicate : " << p << " " << polarity << std::endl;
2366 checkEquivalenceClass( p, polarity ? d_false : d_true );
2367 }
2368
2369 DisequalityPropagator::Statistics::Statistics():
2370 d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0)
2371 {
2372 smtStatisticsRegistry()->registerStat(& d_propagations);
2373 }
2374
2375 DisequalityPropagator::Statistics::~Statistics(){
2376 smtStatisticsRegistry()->unregisterStat(& d_propagations);
2377 }
2378
2379 }/* CVC4::theory namespace::uf */
2380 }/* CVC4::theory namespace */
2381 }/* CVC4 namespace */