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