1 /********************* */
2 /*! \file cardinality_extension.cpp
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
12 ** \brief Implementation of theory of UF with cardinality.
15 #include "theory/uf/cardinality_extension.h"
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"
25 //#define ONE_SPLIT_REGION
26 //#define COMBINE_REGIONS_SMALL_INTO_LARGE
27 //#define LAZY_REL_EQC
30 using namespace CVC4::kind
;
31 using namespace CVC4::context
;
38 /* These are names are unambigious are we use abbreviations. */
39 typedef CardinalityExtension::SortModel SortModel
;
40 typedef SortModel::Region Region
;
41 typedef Region::RegionNodeInfo RegionNodeInfo
;
42 typedef RegionNodeInfo::DiseqList DiseqList
;
44 Region::Region(SortModel
* cf
, context::Context
* c
)
46 , d_testCliqueSize( c
, 0 )
47 , d_splitsSize( c
, 0 )
51 , d_total_diseq_external( c
, 0 )
52 , d_total_diseq_internal( c
, 0 )
53 , d_valid( c
, true ) {}
56 for(iterator i
= begin(), iend
= end(); i
!= iend
; ++i
) {
57 RegionNodeInfo
* regionNodeInfo
= (*i
).second
;
58 delete regionNodeInfo
;
63 void Region::addRep( Node n
) {
67 void Region::takeNode( Region
* r
, Node n
){
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
){
78 r
->setDisequal( n
, (*it
).first
, t
, false );
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 );
85 setDisequal( n
, (*it
).first
, 0, true );
88 r
->setDisequal( (*it
).first
, n
, 1, false );
89 r
->setDisequal( (*it
).first
, n
, 0, true );
90 setDisequal( n
, (*it
).first
, 0, true );
95 //remove representative
96 r
->setRep( n
, false );
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 );
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
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
){
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 );
121 setDisequal( n
, (*it2
).first
, t
, true );
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
){
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 );
146 setDisequal( b
, n
, t
, false );
147 nr
->setDisequal( n
, b
, t
, false );
151 //remove b from representatives
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
);
163 d_total_diseq_external
= d_total_diseq_external
+ ( valid
? 1 : -1 );
165 d_total_diseq_internal
= d_total_diseq_internal
+ ( valid
? 1 : -1 );
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
174 d_splits
[ eq
] = false;
175 d_splitsSize
= d_splitsSize
- 1;
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() );
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
] ){
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
){
198 if( (*it
).first
[0]==n
|| (*it
).first
[1]==n
){
199 d_splits
[ (*it
).first
] = false;
200 d_splitsSize
= d_splitsSize
- 1;
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
);
212 struct sortInternalDegree
{
214 bool operator() (Node i
, Node j
) {
215 return (r
->getRegionInfo(i
)->getNumInternalDisequalities() >
216 r
->getRegionInfo(j
)->getNumInternalDisequalities());
220 struct sortExternalDegree
{
222 bool operator() (Node i
,Node j
) {
223 return (r
->getRegionInfo(i
)->getNumExternalDisequalities() >
224 r
->getRegionInfo(j
)->getNumExternalDisequalities());
230 bool Region::getMustCombine( int cardinality
){
231 if (d_total_diseq_external
>= static_cast<unsigned>(cardinality
))
233 //The number of external disequalities is greater than or equal to
234 //cardinality. Thus, a clique of size cardinality+1 may exist
235 //between nodes in d_regions[i] and other regions Check if this is
236 //actually the case: must have n nodes with outgoing degree
237 //(cardinality+1-n) for some n>0
238 std::vector
< int > degrees
;
239 for( Region::iterator it
= begin(); it
!= end(); ++it
){
240 RegionNodeInfo
* rni
= it
->second
;
242 if( rni
->getNumDisequalities() >= cardinality
){
243 int outDeg
= rni
->getNumExternalDisequalities();
244 if( outDeg
>=cardinality
){
245 //we have 1 node of degree greater than (cardinality)
247 }else if( outDeg
>=1 ){
248 degrees
.push_back( outDeg
);
249 if( (int)degrees
.size()>=cardinality
){
250 //we have (cardinality) nodes of degree 1
258 if( gmcCount
%100==0 ){
259 Trace("gmc-count") << gmcCount
<< " " << cardinality
260 << " sample : " << degrees
.size() << std::endl
;
262 //this should happen relatively infrequently....
263 std::sort( degrees
.begin(), degrees
.end() );
264 for( int i
=0; i
<(int)degrees
.size(); i
++ ){
265 if( degrees
[i
]>=cardinality
+1-((int)degrees
.size()-i
) ){
273 bool Region::check( Theory::Effort level
, int cardinality
,
274 std::vector
< Node
>& clique
) {
275 if( d_reps_size
>unsigned(cardinality
) ){
276 if( d_total_diseq_internal
==d_reps_size
*( d_reps_size
- 1 ) ){
278 //quick clique check, all reps form a clique
279 for( iterator it
= begin(); it
!= end(); ++it
){
280 if( it
->second
->valid() ){
281 clique
.push_back( it
->first
);
284 Trace("quick-clique") << "Found quick clique" << std::endl
;
290 else if (level
==Theory::EFFORT_FULL
)
292 //build test clique, up to size cardinality+1
293 if( d_testCliqueSize
<=unsigned(cardinality
) ){
294 std::vector
< Node
> newClique
;
295 if( d_testCliqueSize
<unsigned(cardinality
) ){
296 for( iterator it
= begin(); it
!= end(); ++it
){
297 //if not in the test clique, add it to the set of new members
298 if( it
->second
->valid() &&
299 ( d_testClique
.find( it
->first
) == d_testClique
.end() ||
300 !d_testClique
[ it
->first
] ) ){
301 //if( it->second->getNumInternalDisequalities()>cardinality ||
302 // level==Theory::EFFORT_FULL ){
303 newClique
.push_back( it
->first
);
307 //choose remaining nodes with the highest degrees
308 sortInternalDegree sidObj
;
310 std::sort( newClique
.begin(), newClique
.end(), sidObj
);
311 int offset
= ( cardinality
- d_testCliqueSize
) + 1;
312 newClique
.erase( newClique
.begin() + offset
, newClique
.end() );
314 //scan for the highest degree
317 for( std::map
< Node
, RegionNodeInfo
* >::iterator
318 it
= d_nodes
.begin(); it
!= d_nodes
.end(); ++it
){
319 //if not in the test clique, add it to the set of new members
320 if( it
->second
->valid() &&
321 ( d_testClique
.find( it
->first
)==d_testClique
.end() ||
322 !d_testClique
[ it
->first
] ) ){
323 if( it
->second
->getNumInternalDisequalities()>maxDeg
){
324 maxDeg
= it
->second
->getNumInternalDisequalities();
329 Assert(maxNode
!= Node::null());
330 newClique
.push_back( maxNode
);
332 //check splits internal to new members
333 for( int j
=0; j
<(int)newClique
.size(); j
++ ){
334 Debug("uf-ss-debug") << "Choose to add clique member "
335 << newClique
[j
] << std::endl
;
336 for( int k
=(j
+1); k
<(int)newClique
.size(); k
++ ){
337 if( !isDisequal( newClique
[j
], newClique
[k
], 1 ) ){
338 Node at_j
= newClique
[j
];
339 Node at_k
= newClique
[k
];
341 NodeManager::currentNM()->mkNode( EQUAL
, at_j
, at_k
);
342 d_splits
[ j_eq_k
] = true;
343 d_splitsSize
= d_splitsSize
+ 1;
346 //check disequalities with old members
347 for( NodeBoolMap::iterator it
= d_testClique
.begin();
348 it
!= d_testClique
.end(); ++it
){
350 if( !isDisequal( (*it
).first
, newClique
[j
], 1 ) ){
351 Node at_it
= (*it
).first
;
352 Node at_j
= newClique
[j
];
353 Node it_eq_j
= at_it
.eqNode(at_j
);
354 d_splits
[ it_eq_j
] = true;
355 d_splitsSize
= d_splitsSize
+ 1;
360 //add new clique members to test clique
361 for( int j
=0; j
<(int)newClique
.size(); j
++ ){
362 d_testClique
[ newClique
[j
] ] = true;
363 d_testCliqueSize
= d_testCliqueSize
+ 1;
366 // Check if test clique has larger size than cardinality, and
368 if( d_testCliqueSize
>= unsigned(cardinality
+1) && d_splitsSize
==0 ){
369 //test clique is a clique
370 for( NodeBoolMap::iterator it
= d_testClique
.begin();
371 it
!= d_testClique
.end(); ++it
){
373 clique
.push_back( (*it
).first
);
383 void Region::getNumExternalDisequalities(
384 std::map
< Node
, int >& num_ext_disequalities
){
385 for( Region::iterator it
= begin(); it
!= end(); ++it
){
386 RegionNodeInfo
* rni
= it
->second
;
388 DiseqList
* del
= rni
->get(0);
389 for( DiseqList::iterator it2
= del
->begin(); it2
!= del
->end(); ++it2
){
391 num_ext_disequalities
[ (*it2
).first
]++;
398 void Region::debugPrint( const char* c
, bool incClique
) {
399 Debug( c
) << "Num reps: " << d_reps_size
<< std::endl
;
400 for( Region::iterator it
= begin(); it
!= end(); ++it
){
401 RegionNodeInfo
* rni
= it
->second
;
404 Debug( c
) << " " << n
<< std::endl
;
405 for( int i
=0; i
<2; i
++ ){
406 Debug( c
) << " " << ( i
==0 ? "Ext" : "Int" ) << " disequal:";
407 DiseqList
* del
= rni
->get(i
);
408 for( DiseqList::iterator it2
= del
->begin(); it2
!= del
->end(); ++it2
){
410 Debug( c
) << " " << (*it2
).first
;
413 Debug( c
) << ", total = " << del
->size() << std::endl
;
417 Debug( c
) << "Total disequal: " << d_total_diseq_external
<< " external,";
418 Debug( c
) << " " << d_total_diseq_internal
<< " internal." << std::endl
;
421 if( !d_testClique
.empty() ){
422 Debug( c
) << "Candidate clique members: " << std::endl
;
424 for( NodeBoolMap::iterator it
= d_testClique
.begin();
425 it
!= d_testClique
.end(); ++ it
){
427 Debug( c
) << (*it
).first
<< " ";
430 Debug( c
) << ", size = " << d_testCliqueSize
<< std::endl
;
432 if( !d_splits
.empty() ){
433 Debug( c
) << "Required splits: " << std::endl
;
435 for( NodeBoolMap::iterator it
= d_splits
.begin(); it
!= d_splits
.end();
438 Debug( c
) << (*it
).first
<< " ";
441 Debug( c
) << ", size = " << d_splitsSize
<< std::endl
;
446 SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy(
447 Node t
, context::Context
* satContext
, Valuation valuation
)
448 : DecisionStrategyFmf(satContext
, valuation
), d_cardinality_term(t
)
451 Node
SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i
)
453 NodeManager
* nm
= NodeManager::currentNM();
455 CARDINALITY_CONSTRAINT
, d_cardinality_term
, nm
->mkConst(Rational(i
+ 1)));
457 std::string
SortModel::CardinalityDecisionStrategy::identify() const
459 return std::string("uf_card");
462 SortModel::SortModel(Node n
,
464 context::UserContext
* u
,
465 CardinalityExtension
* thss
)
466 : d_type(n
.getType()),
468 d_regions_index(c
, 0),
471 d_disequalities_index(c
, 0),
473 d_conflict(c
, false),
477 d_initialized(u
, false),
479 d_c_dec_strat(nullptr)
481 d_cardinality_term
= n
;
483 if (options::ufssMode() == options::UfssMode::FULL
)
485 // Register the strategy with the decision manager of the theory.
486 // We are guaranteed that the decision manager is ready since we
487 // construct this module during TheoryUF::finishInit.
488 d_c_dec_strat
.reset(new CardinalityDecisionStrategy(
489 n
, c
, thss
->getTheory()->getValuation()));
493 SortModel::~SortModel() {
494 for(std::vector
<Region
*>::iterator i
= d_regions
.begin();
495 i
!= d_regions
.end(); ++i
) {
503 void SortModel::initialize( OutputChannel
* out
){
504 if (d_c_dec_strat
.get() != nullptr && !d_initialized
)
506 d_initialized
= true;
507 // Strategy is user-context-dependent, since it is in sync with
508 // user-context-dependent flag d_initialized.
509 d_thss
->getTheory()->getDecisionManager()->registerStrategy(
510 DecisionManager::STRAT_UF_CARD
, d_c_dec_strat
.get());
515 void SortModel::newEqClass( Node n
){
517 if( d_regions_map
.find( n
)==d_regions_map
.end() ){
518 // Must generate totality axioms for every cardinality we have
519 // allocated thus far.
520 for( std::map
< int, Node
>::iterator it
= d_cardinality_literal
.begin();
521 it
!= d_cardinality_literal
.end(); ++it
){
522 if( applyTotality( it
->first
) ){
523 addTotalityAxiom( n
, it
->first
, &d_thss
->getOutputChannel() );
526 if( options::ufssTotality() ){
527 // Regions map will store whether we need to equate this term
528 // with a constant equivalence class.
529 if( std::find( d_totality_terms
[0].begin(), d_totality_terms
[0].end(), n
)==d_totality_terms
[0].end() ){
530 d_regions_map
[n
] = 0;
532 d_regions_map
[n
] = -1;
535 d_regions_map
[n
] = d_regions_index
;
536 Debug("uf-ss") << "CardinalityExtension: New Eq Class " << n
538 Debug("uf-ss-debug") << d_regions_index
<< " "
539 << (int)d_regions
.size() << std::endl
;
540 if( d_regions_index
<d_regions
.size() ){
541 d_regions
[ d_regions_index
]->debugPrint("uf-ss-debug",true);
542 d_regions
[ d_regions_index
]->setValid(true);
543 Assert(d_regions
[d_regions_index
]->getNumReps() == 0);
545 d_regions
.push_back( new Region( this, d_thss
->getSatContext() ) );
547 d_regions
[ d_regions_index
]->addRep( n
);
548 d_regions_index
= d_regions_index
+ 1;
556 void SortModel::merge( Node a
, Node b
){
558 if( options::ufssTotality() ){
559 if( d_regions_map
[b
]==-1 ){
560 d_regions_map
[a
] = -1;
562 d_regions_map
[b
] = -1;
564 Debug("uf-ss") << "CardinalityExtension: Merging " << a
<< " = " << b
565 << "..." << std::endl
;
567 Assert(d_regions_map
.find(a
) != d_regions_map
.end());
568 Assert(d_regions_map
.find(b
) != d_regions_map
.end());
569 int ai
= d_regions_map
[a
];
570 int bi
= d_regions_map
[b
];
571 Debug("uf-ss") << " regions: " << ai
<< " " << bi
<< std::endl
;
573 if( d_regions
[ai
]->getNumReps()==1 ){
574 int ri
= combineRegions( bi
, ai
);
575 d_regions
[ri
]->setEqual( a
, b
);
577 }else if( d_regions
[bi
]->getNumReps()==1 ){
578 int ri
= combineRegions( ai
, bi
);
579 d_regions
[ri
]->setEqual( a
, b
);
582 // Either move a to d_regions[bi], or b to d_regions[ai].
583 RegionNodeInfo
* a_region_info
= d_regions
[ai
]->getRegionInfo(a
);
584 RegionNodeInfo
* b_region_info
= d_regions
[bi
]->getRegionInfo(b
);
585 int aex
= ( a_region_info
->getNumInternalDisequalities() -
586 getNumDisequalitiesToRegion( a
, bi
) );
587 int bex
= ( b_region_info
->getNumInternalDisequalities() -
588 getNumDisequalitiesToRegion( b
, ai
) );
589 // Based on which would produce the fewest number of
590 // external disequalities.
593 d_regions
[bi
]->setEqual( a
, b
);
596 d_regions
[ai
]->setEqual( a
, b
);
602 d_regions
[ai
]->setEqual( a
, b
);
605 d_regions_map
[b
] = -1;
612 /** assert terms are disequal */
613 void SortModel::assertDisequal( Node a
, Node b
, Node reason
){
615 if( options::ufssTotality() ){
618 //if they are not already disequal
619 eq::EqualityEngine
* ee
= d_thss
->getTheory()->getEqualityEngine();
620 a
= ee
->getRepresentative(a
);
621 b
= ee
->getRepresentative(b
);
622 int ai
= d_regions_map
[a
];
623 int bi
= d_regions_map
[b
];
624 if( !d_regions
[ai
]->isDisequal( a
, b
, ai
==bi
) ){
625 Debug("uf-ss") << "Assert disequal " << a
<< " != " << b
<< "..." << std::endl
;
626 //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL ||
627 // a!=reason[0][0] || b!=reason[0][1] ){
628 // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
630 Debug("uf-ss-disequal") << "Assert disequal " << a
<< " != " << b
<< "..." << std::endl
;
631 //add to list of disequalities
632 if( d_disequalities_index
<d_disequalities
.size() ){
633 d_disequalities
[d_disequalities_index
] = reason
;
635 d_disequalities
.push_back( reason
);
637 d_disequalities_index
= d_disequalities_index
+ 1;
638 //now, add disequalities to regions
639 Assert(d_regions_map
.find(a
) != d_regions_map
.end());
640 Assert(d_regions_map
.find(b
) != d_regions_map
.end());
641 Debug("uf-ss") << " regions: " << ai
<< " " << bi
<< std::endl
;
643 //internal disequality
644 d_regions
[ai
]->setDisequal( a
, b
, 1, true );
645 d_regions
[ai
]->setDisequal( b
, a
, 1, true );
646 checkRegion( ai
, false ); //do not need to check if it needs to combine (no new ext. disequalities)
648 //external disequality
649 d_regions
[ai
]->setDisequal( a
, b
, 0, true );
650 d_regions
[bi
]->setDisequal( b
, a
, 0, true );
659 bool SortModel::areDisequal( Node a
, Node b
) {
660 Assert(a
== d_thss
->getTheory()->getEqualityEngine()->getRepresentative(a
));
661 Assert(b
== d_thss
->getTheory()->getEqualityEngine()->getRepresentative(b
));
662 if( d_regions_map
.find( a
)!=d_regions_map
.end() &&
663 d_regions_map
.find( b
)!=d_regions_map
.end() ){
664 int ai
= d_regions_map
[a
];
665 int bi
= d_regions_map
[b
];
666 return d_regions
[ai
]->isDisequal(a
, b
, ai
==bi
? 1 : 0);
673 void SortModel::check( Theory::Effort level
, OutputChannel
* out
){
674 Assert(options::ufssMode() == options::UfssMode::FULL
);
675 if( level
>=Theory::EFFORT_STANDARD
&& d_hasCard
&& !d_conflict
){
676 Debug("uf-ss") << "CardinalityExtension: Check " << level
<< " " << d_type
678 if( level
==Theory::EFFORT_FULL
){
679 Debug("fmf-full-check") << std::endl
;
680 Debug("fmf-full-check") << "Full check for SortModel " << d_type
<< ", status : " << std::endl
;
681 debugPrint("fmf-full-check");
682 Debug("fmf-full-check") << std::endl
;
684 if( d_reps
<=(unsigned)d_cardinality
){
685 Debug("uf-ss-debug") << "We have " << d_reps
<< " representatives for type " << d_type
<< ", <= " << d_cardinality
<< std::endl
;
686 if( level
==Theory::EFFORT_FULL
){
687 Debug("uf-ss-sat") << "We have " << d_reps
<< " representatives for type " << d_type
<< ", <= " << d_cardinality
<< std::endl
;
688 //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl;
689 //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl;
690 //Notice() << cardinality << " ";
694 //first check if we can generate a clique conflict
695 if( !options::ufssTotality() ){
696 //do a check within each region
697 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
698 if( d_regions
[i
]->valid() ){
699 std::vector
< Node
> clique
;
700 if( d_regions
[i
]->check( level
, d_cardinality
, clique
) ){
702 addCliqueLemma( clique
, out
);
705 Trace("uf-ss-debug") << "No clique in Region #" << i
<< std::endl
;
710 if( !applyTotality( d_cardinality
) ){
711 //do splitting on demand
712 bool addedLemma
= false;
713 if (level
==Theory::EFFORT_FULL
)
715 Trace("uf-ss-debug") << "Add splits?" << std::endl
;
716 //see if we have any recommended splits from large regions
717 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
718 if( d_regions
[i
]->valid() && d_regions
[i
]->getNumReps()>d_cardinality
){
720 int sp
= addSplit( d_regions
[i
], out
);
723 #ifdef ONE_SPLIT_REGION
733 //If no added lemmas, force continuation via combination of regions.
734 if( level
==Theory::EFFORT_FULL
){
736 Trace("uf-ss-debug") << "No splits added. " << d_cardinality
738 Trace("uf-ss-si") << "Must combine region" << std::endl
;
739 bool recheck
= false;
740 SortInference
* si
= d_thss
->getSortInference();
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
= si
->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
);
755 sortsFound
[sort_id
] = i
;
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
;
773 Trace("uf-ss-debug") << "Must recheck." << std::endl
;
783 void SortModel::presolve() {
784 d_initialized
= false;
787 void SortModel::propagate( Theory::Effort level
, OutputChannel
* out
){
791 int SortModel::getNumDisequalitiesToRegion( Node n
, int ri
){
792 int ni
= d_regions_map
[n
];
794 DiseqList
* del
= d_regions
[ni
]->getRegionInfo(n
)->get(0);
795 for( DiseqList::iterator it
= del
->begin(); it
!= del
->end(); ++it
){
797 if( d_regions_map
[ (*it
).first
]==ri
){
805 void SortModel::getDisequalitiesToRegions(int ri
,
806 std::map
< int, int >& regions_diseq
)
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
){
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
] ]++;
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
;
828 d_split_score
[ n
] = s
;
830 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
831 setSplitScore( n
[i
], s
+1 );
835 void SortModel::assertCardinality( OutputChannel
* out
, int c
, bool val
){
837 Trace("uf-ss-assert")
838 << "Assert cardinality " << d_type
<< " " << c
<< " " << val
840 << d_thss
->getTheory()->getValuation().getAssertionLevel() << std::endl
;
842 Node cl
= getCardinalityLiteral( c
);
844 bool doCheckRegions
= !d_hasCard
;
845 bool prevHasCard
= d_hasCard
;
847 if( !prevHasCard
|| c
<d_cardinality
){
849 simpleCheckCardinality();
850 if( d_thss
->d_conflict
.get() ){
854 //should check all regions now
855 if( doCheckRegions
){
856 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
857 if( d_regions
[i
]->valid() ){
865 // we assert it positively, if its beyond the bound, abort
866 if (options::ufssAbortCardinality() != -1
867 && c
>= options::ufssAbortCardinality())
869 std::stringstream ss
;
870 ss
<< "Maximum cardinality (" << options::ufssAbortCardinality()
871 << ") for finite model finding exceeded." << std::endl
;
872 throw LogicException(ss
.str());
877 if( c
>d_maxNegCard
.get() ){
878 Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for " << d_type
<< " is now " << c
<< std::endl
;
879 d_maxNegCard
.set( c
);
880 simpleCheckCardinality();
886 void SortModel::checkRegion( int ri
, bool checkCombine
){
887 if( isValid(ri
) && d_hasCard
){
888 Assert(d_cardinality
> 0);
889 if( checkCombine
&& d_regions
[ri
]->getMustCombine( d_cardinality
) ){
890 ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
891 //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
893 // int inDeg = d_regions[i]->d_disequalities_size[1][ it-> first ];
894 // int outDeg = d_regions[i]->d_disequalities_size[0][ it-> first ];
895 // if( inDeg<outDeg ){
899 int riNew
= forceCombineRegion( ri
, true );
901 checkRegion( riNew
, checkCombine
);
904 //now check if region is in conflict
905 std::vector
< Node
> clique
;
906 if( d_regions
[ri
]->check( Theory::EFFORT_STANDARD
, d_cardinality
, clique
) ){
908 addCliqueLemma( clique
, &d_thss
->getOutputChannel() );
913 int SortModel::forceCombineRegion( int ri
, bool useDensity
){
915 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
916 if( ri
!=i
&& d_regions
[i
]->valid() ){
917 return combineRegions( ri
, i
);
922 //this region must merge with another
923 if( Debug
.isOn("uf-ss-check-region") ){
924 Debug("uf-ss-check-region") << "We must combine Region #" << ri
<< ". " << std::endl
;
925 d_regions
[ri
]->debugPrint("uf-ss-check-region");
927 //take region with maximum disequality density
930 std::map
< int, int > regions_diseq
;
931 getDisequalitiesToRegions( ri
, regions_diseq
);
932 for( std::map
< int, int >::iterator it
= regions_diseq
.begin(); it
!= regions_diseq
.end(); ++it
){
933 Debug("uf-ss-check-region") << it
->first
<< " : " << it
->second
<< std::endl
;
935 for( std::map
< int, int >::iterator it
= regions_diseq
.begin(); it
!= regions_diseq
.end(); ++it
){
936 Assert(it
->first
!= ri
);
937 Assert(isValid(it
->first
));
938 Assert(d_regions
[it
->first
]->getNumReps() > 0);
939 double tempScore
= double(it
->second
)/double(d_regions
[it
->first
]->getNumReps() );
940 if( tempScore
>maxScore
){
941 maxRegion
= it
->first
;
942 maxScore
= tempScore
;
946 if( Debug
.isOn("uf-ss-check-region") ){
947 Debug("uf-ss-check-region") << "Combine with region #" << maxRegion
<< ":" << std::endl
;
948 d_regions
[maxRegion
]->debugPrint("uf-ss-check-region");
950 return combineRegions( ri
, maxRegion
);
957 int SortModel::combineRegions( int ai
, int bi
){
958 #ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
959 if( d_regions
[ai
]->getNumReps()<d_regions
[bi
]->getNumReps() ){
960 return combineRegions( bi
, ai
);
963 Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi
<< " with Region #" << ai
<< std::endl
;
964 Assert(isValid(ai
) && isValid(bi
));
965 Region
* region_bi
= d_regions
[bi
];
966 for(Region::iterator it
= region_bi
->begin(); it
!= region_bi
->end(); ++it
){
967 Region::RegionNodeInfo
* rni
= it
->second
;
969 d_regions_map
[ it
->first
] = ai
;
972 //update regions disequal DO_THIS?
973 d_regions
[ai
]->combine( d_regions
[bi
] );
974 d_regions
[bi
]->setValid( false );
978 void SortModel::moveNode( Node n
, int ri
){
979 Debug("uf-ss-region") << "uf-ss: Move node " << n
<< " to Region #" << ri
<< std::endl
;
980 Assert(isValid(d_regions_map
[n
]));
982 //move node to region ri
983 d_regions
[ri
]->takeNode( d_regions
[ d_regions_map
[n
] ], n
);
984 d_regions_map
[n
] = ri
;
987 int SortModel::addSplit( Region
* r
, OutputChannel
* out
){
989 if( r
->hasSplits() ){
990 //take the first split you find
991 for( Region::split_iterator it
= r
->begin_splits();
992 it
!= r
->end_splits(); ++it
){
998 Assert(s
!= Node::null());
1001 //add lemma to output channel
1002 Assert(s
.getKind() == EQUAL
);
1003 Node ss
= Rewriter::rewrite( s
);
1004 if( ss
.getKind()!=EQUAL
){
1005 Node b_t
= NodeManager::currentNM()->mkConst( true );
1006 Node b_f
= NodeManager::currentNM()->mkConst( false );
1008 Trace("uf-ss-lemma") << "....Assert disequal directly : "
1009 << s
[0] << " " << s
[1] << std::endl
;
1010 assertDisequal( s
[0], s
[1], b_t
);
1013 Trace("uf-ss-warn") << "Split on unknown literal : " << ss
<< std::endl
;
1016 Message() << "Bad split " << s
<< std::endl
;
1017 AlwaysAssert(false);
1020 SortInference
* si
= d_thss
->getSortInference();
1023 for( int i
=0; i
<2; i
++ ){
1024 int sid
= si
->getSortId(ss
[i
]);
1025 Trace("uf-ss-split-si") << sid
<< " ";
1027 Trace("uf-ss-split-si") << std::endl
;
1029 //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
1030 //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
1031 //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
1032 //Notice() << "*** Split on " << s << std::endl;
1033 //split on the equality s
1034 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, ss
, ss
.negate() );
1035 if( doSendLemma( lem
) ){
1036 Trace("uf-ss-lemma") << "*** Split on " << s
<< std::endl
;
1037 //tell the sat solver to explore the equals branch first
1038 out
->requirePhase( ss
, true );
1039 ++( d_thss
->d_statistics
.d_split_lemmas
);
1048 void SortModel::addCliqueLemma( std::vector
< Node
>& clique
, OutputChannel
* out
){
1050 Assert(d_cardinality
> 0);
1051 while( clique
.size()>size_t(d_cardinality
+1) ){
1055 std::vector
<Node
> eqs
;
1056 for (unsigned i
= 0, size
= clique
.size(); i
< size
; i
++)
1058 for (unsigned j
= 0; j
< i
; j
++)
1060 eqs
.push_back(clique
[i
].eqNode(clique
[j
]));
1063 eqs
.push_back(d_cardinality_literal
[d_cardinality
].notNode());
1064 Node lem
= NodeManager::currentNM()->mkNode(OR
, eqs
);
1065 if (doSendLemma(lem
))
1067 Trace("uf-ss-lemma") << "*** Add clique lemma " << lem
<< std::endl
;
1068 ++(d_thss
->d_statistics
.d_clique_lemmas
);
1072 void SortModel::addTotalityAxiom( Node n
, int cardinality
, OutputChannel
* out
){
1073 if( std::find( d_totality_terms
[0].begin(), d_totality_terms
[0].end(), n
)==d_totality_terms
[0].end() ){
1074 if( std::find( d_totality_lems
[n
].begin(), d_totality_lems
[n
].end(), cardinality
) == d_totality_lems
[n
].end() ){
1075 NodeManager
* nm
= NodeManager::currentNM();
1076 d_totality_lems
[n
].push_back( cardinality
);
1077 Node cardLit
= d_cardinality_literal
[ cardinality
];
1079 SortInference
* si
= d_thss
->getSortInference();
1082 sort_id
= si
->getSortId(n
);
1084 Trace("uf-ss-totality") << "Add totality lemma for " << n
<< " " << cardinality
<< ", sort id is " << sort_id
<< std::endl
;
1085 int use_cardinality
= cardinality
;
1086 if( options::ufssTotalitySymBreak() ){
1087 if( d_sym_break_index
.find(n
)!=d_sym_break_index
.end() ){
1088 use_cardinality
= d_sym_break_index
[n
];
1089 }else if( (int)d_sym_break_terms
[n
.getType()][sort_id
].size()<cardinality
-1 ){
1090 use_cardinality
= d_sym_break_terms
[n
.getType()][sort_id
].size() + 1;
1091 d_sym_break_terms
[n
.getType()][sort_id
].push_back( n
);
1092 d_sym_break_index
[n
] = use_cardinality
;
1093 Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n
<< ", index = " << use_cardinality
<< std::endl
;
1094 if( d_sym_break_terms
[n
.getType()][sort_id
].size()>1 ){
1095 //enforce canonicity
1096 for( int i
=2; i
<use_cardinality
; i
++ ){
1097 //can only be assigned to domain constant d if someone has been assigned domain constant d-1
1098 Node eq
= n
.eqNode( getTotalityLemmaTerm( cardinality
, i
) );
1099 std::vector
< Node
> eqs
;
1100 for( unsigned j
=0; j
<(d_sym_break_terms
[n
.getType()][sort_id
].size()-1); j
++ ){
1101 eqs
.push_back( d_sym_break_terms
[n
.getType()][sort_id
][j
].eqNode( getTotalityLemmaTerm( cardinality
, i
-1 ) ) );
1103 Node ax
= eqs
.size()==1 ? eqs
[0] : NodeManager::currentNM()->mkNode( OR
, eqs
);
1104 Node lem
= NodeManager::currentNM()->mkNode( IMPLIES
, eq
, ax
);
1105 Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem
<< std::endl
;
1106 d_thss
->getOutputChannel().lemma( lem
);
1112 std::vector
< Node
> eqs
;
1113 for( int i
=0; i
<use_cardinality
; i
++ ){
1114 eqs
.push_back( n
.eqNode( getTotalityLemmaTerm( cardinality
, i
) ) );
1116 Node ax
= eqs
.size() == 1 ? eqs
[0] : nm
->mkNode(OR
, eqs
);
1117 Node lem
= NodeManager::currentNM()->mkNode( IMPLIES
, cardLit
, ax
);
1118 Trace("uf-ss-lemma") << "*** Add totality axiom " << lem
<< std::endl
;
1119 //send as lemma to the output channel
1120 d_thss
->getOutputChannel().lemma( lem
);
1121 ++( d_thss
->d_statistics
.d_totality_lemmas
);
1126 /** apply totality */
1127 bool SortModel::applyTotality( int cardinality
){
1128 return options::ufssTotality() || cardinality
<=options::ufssTotalityLimited();
1131 /** get totality lemma terms */
1132 Node
SortModel::getTotalityLemmaTerm( int cardinality
, int i
){
1133 return d_totality_terms
[0][i
];
1136 void SortModel::simpleCheckCardinality() {
1137 if( d_maxNegCard
.get()!=0 && d_hasCard
.get() && d_cardinality
.get()<d_maxNegCard
.get() ){
1138 Node lem
= NodeManager::currentNM()->mkNode( AND
, getCardinalityLiteral( d_cardinality
.get() ),
1139 getCardinalityLiteral( d_maxNegCard
.get() ).negate() );
1140 Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem
<< std::endl
;
1141 d_thss
->getOutputChannel().conflict( lem
);
1142 d_thss
->d_conflict
.set( true );
1146 bool SortModel::doSendLemma( Node lem
) {
1147 if( d_lemma_cache
.find( lem
)==d_lemma_cache
.end() ){
1148 d_lemma_cache
[lem
] = true;
1149 d_thss
->getOutputChannel().lemma( lem
);
1156 void SortModel::debugPrint( const char* c
){
1157 if( Debug
.isOn( c
) ){
1158 Debug( c
) << "Number of reps = " << d_reps
<< std::endl
;
1159 Debug( c
) << "Cardinality req = " << d_cardinality
<< std::endl
;
1160 unsigned debugReps
= 0;
1161 for( unsigned i
=0; i
<d_regions_index
; i
++ ){
1162 Region
* region
= d_regions
[i
];
1163 if( region
->valid() ){
1164 Debug( c
) << "Region #" << i
<< ": " << std::endl
;
1165 region
->debugPrint( c
, true );
1166 Debug( c
) << std::endl
;
1167 for( Region::iterator it
= region
->begin(); it
!= region
->end(); ++it
){
1168 if( it
->second
->valid() ){
1169 if( d_regions_map
[ it
->first
]!=(int)i
){
1170 Debug( c
) << "***Bad regions map : " << it
->first
1171 << " " << d_regions_map
[ it
->first
].get() << std::endl
;
1175 debugReps
+= region
->getNumReps();
1179 if( debugReps
!=d_reps
){
1180 Debug( c
) << "***Bad reps: " << d_reps
<< ", "
1181 << "actual = " << debugReps
<< std::endl
;
1186 bool SortModel::debugModel( TheoryModel
* m
){
1187 if( Trace
.isOn("uf-ss-warn") ){
1188 std::vector
< Node
> eqcs
;
1189 eq::EqClassesIterator eqcs_i
=
1190 eq::EqClassesIterator(m
->getEqualityEngine());
1191 while( !eqcs_i
.isFinished() ){
1192 Node eqc
= (*eqcs_i
);
1193 if( eqc
.getType()==d_type
){
1194 if( std::find( eqcs
.begin(), eqcs
.end(), eqc
)==eqcs
.end() ){
1195 eqcs
.push_back( eqc
);
1196 //we must ensure that this equivalence class has been accounted for
1197 if( d_regions_map
.find( eqc
)==d_regions_map
.end() ){
1198 Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc
<< " unaccounted for." << std::endl
;
1199 Trace("uf-ss-warn") << " type : " << d_type
<< std::endl
;
1200 Trace("uf-ss-warn") << " kind : " << eqc
.getKind() << std::endl
;
1207 RepSet
* rs
= m
->getRepSetPtr();
1208 int nReps
= (int)rs
->getNumRepresentatives(d_type
);
1209 if( nReps
!=(d_maxNegCard
+1) ){
1210 Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type
<< "." << std::endl
;
1211 Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard
<< std::endl
;
1212 Trace("uf-ss-warn") << " # Reps : " << nReps
<< std::endl
;
1213 if( d_maxNegCard
>=nReps
){
1214 while( (int)d_fresh_aloc_reps
.size()<=d_maxNegCard
){
1215 std::stringstream ss
;
1216 ss
<< "r_" << d_type
<< "_";
1217 Node nn
= NodeManager::currentNM()->mkSkolem( ss
.str(), d_type
, "enumeration to meet negative card constraint" );
1218 d_fresh_aloc_reps
.push_back( nn
);
1220 if( d_maxNegCard
==0 ){
1221 rs
->d_type_reps
[d_type
].push_back(d_fresh_aloc_reps
[0]);
1224 std::vector
< Node
> force_cl
;
1225 for( int i
=0; i
<=d_maxNegCard
; i
++ ){
1226 for( int j
=(i
+1); j
<=d_maxNegCard
; j
++ ){
1227 force_cl
.push_back( d_fresh_aloc_reps
[i
].eqNode( d_fresh_aloc_reps
[j
] ).negate() );
1230 Node cl
= getCardinalityLiteral( d_maxNegCard
);
1231 Node lem
= NodeManager::currentNM()->mkNode( OR
, cl
, NodeManager::currentNM()->mkNode( AND
, force_cl
) );
1232 Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem
<< std::endl
;
1233 d_thss
->getOutputChannel().lemma( lem
);
1241 int SortModel::getNumRegions(){
1243 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
1244 if( d_regions
[i
]->valid() ){
1251 Node
SortModel::getCardinalityLiteral(unsigned c
)
1254 std::map
<int, Node
>::iterator itcl
= d_cardinality_literal
.find(c
);
1255 if (itcl
!= d_cardinality_literal
.end())
1257 return itcl
->second
;
1259 // get the literal from the decision strategy
1260 Node lit
= d_c_dec_strat
->getLiteral(c
- 1);
1261 d_cardinality_literal
[c
] = lit
;
1263 // Since we are reasoning about cardinality c, we invoke a totality axiom
1264 if (!applyTotality(c
))
1266 // return if we are not using totality axioms
1270 NodeManager
* nm
= NodeManager::currentNM();
1272 if (c
== 1 && !options::ufssTotalitySymBreak())
1274 // get arbitrary ground term
1275 var
= d_cardinality_term
;
1279 std::stringstream ss
;
1281 var
= nm
->mkSkolem(ss
.str(), d_type
, "is a cardinality lemma term");
1283 if ((c
- 1) < d_totality_terms
[0].size())
1285 d_totality_terms
[0][c
- 1] = var
;
1289 d_totality_terms
[0].push_back(var
);
1291 // must be distinct from all other cardinality terms
1292 for (unsigned i
= 1, size
= d_totality_terms
[0].size(); i
< size
; i
++)
1294 Node lem
= var
.eqNode(d_totality_terms
[0][i
- 1]).notNode();
1295 Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem
1297 d_thss
->getOutputChannel().lemma(lem
);
1299 // must send totality axioms for each existing term
1300 for (NodeIntMap::iterator it
= d_regions_map
.begin();
1301 it
!= d_regions_map
.end();
1304 addTotalityAxiom((*it
).first
, c
, &d_thss
->getOutputChannel());
1309 CardinalityExtension::CardinalityExtension(context::Context
* c
,
1310 context::UserContext
* u
,
1315 d_conflict(c
, false),
1317 d_min_pos_com_card(c
, -1),
1318 d_cc_dec_strat(nullptr),
1319 d_initializedCombinedCardinality(u
, false),
1320 d_card_assertions_eqv_lemma(u
),
1321 d_min_pos_tn_master_card(c
, -1),
1324 if (options::ufssMode() == options::UfssMode::FULL
&& options::ufssFairness())
1326 // Register the strategy with the decision manager of the theory.
1327 // We are guaranteed that the decision manager is ready since we
1328 // construct this module during TheoryUF::finishInit.
1329 d_cc_dec_strat
.reset(
1330 new CombinedCardinalityDecisionStrategy(c
, th
->getValuation()));
1334 CardinalityExtension::~CardinalityExtension()
1336 for (std::map
<TypeNode
, SortModel
*>::iterator it
= d_rep_model
.begin();
1337 it
!= d_rep_model
.end(); ++it
) {
1342 SortInference
* CardinalityExtension::getSortInference()
1344 if (!options::sortInference())
1348 QuantifiersEngine
* qe
= d_th
->getQuantifiersEngine();
1351 return qe
->getTheoryEngine()->getSortInference();
1356 /** get default sat context */
1357 context::Context
* CardinalityExtension::getSatContext()
1359 return d_th
->getSatContext();
1362 /** get default output channel */
1363 OutputChannel
& CardinalityExtension::getOutputChannel()
1365 return d_th
->getOutputChannel();
1369 void CardinalityExtension::ensureEqc(SortModel
* c
, Node a
)
1372 d_rel_eqc
[a
] = true;
1373 Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a
<< " : "
1374 << a
.getType() << std::endl
;
1376 Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1381 void CardinalityExtension::ensureEqcRec(Node n
)
1384 SortModel
* c
= getSortModel( n
);
1388 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1389 ensureEqcRec( n
[i
] );
1395 bool CardinalityExtension::hasEqc(Node a
)
1397 NodeBoolMap::iterator it
= d_rel_eqc
.find( a
);
1398 return it
!=d_rel_eqc
.end() && (*it
).second
;
1402 void CardinalityExtension::newEqClass(Node a
)
1404 SortModel
* c
= getSortModel( a
);
1409 Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a
<< " : "
1410 << a
.getType() << std::endl
;
1412 Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1419 void CardinalityExtension::merge(Node a
, Node b
)
1421 //TODO: ensure they are relevant
1422 SortModel
* c
= getSortModel( a
);
1427 Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a
<< " " << b
1428 << " : " << a
.getType() << std::endl
;
1430 Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl
;
1432 //c->assignEqClass( b, a );
1433 d_rel_eqc
[b
] = true;
1436 Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a
<< " " << b
1437 << " : " << a
.getType() << std::endl
;
1439 Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl
;
1444 /** assert terms are disequal */
1445 void CardinalityExtension::assertDisequal(Node a
, Node b
, Node reason
)
1447 SortModel
* c
= getSortModel( a
);
1453 Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a
1454 << " " << b
<< " : " << a
.getType() << std::endl
;
1455 c
->assertDisequal( a
, b
, reason
);
1456 Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal."
1461 /** assert a node */
1462 void CardinalityExtension::assertNode(Node n
, bool isDecision
)
1464 Trace("uf-ss") << "Assert " << n
<< " " << isDecision
<< std::endl
;
1468 bool polarity
= n
.getKind() != kind::NOT
;
1469 TNode lit
= polarity
? n
: n
[0];
1470 if (options::ufssMode() == options::UfssMode::FULL
)
1472 if( lit
.getKind()==CARDINALITY_CONSTRAINT
){
1473 TypeNode tn
= lit
[0].getType();
1474 Assert(tn
.isSort());
1475 Assert(d_rep_model
[tn
]);
1476 int nCard
= lit
[1].getConst
<Rational
>().getNumerator().getSignedInt();
1477 Node ct
= d_rep_model
[tn
]->getCardinalityTerm();
1478 Trace("uf-ss-debug") << "...check cardinality terms : " << lit
[0] << " " << ct
<< std::endl
;
1480 if( options::ufssFairnessMonotone() ){
1481 Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl
;
1482 if( tn
!=d_tn_mono_master
){
1483 std::map
< TypeNode
, bool >::iterator it
= d_tn_mono_slave
.find( tn
);
1484 if( it
==d_tn_mono_slave
.end() ){
1486 SortInference
* si
= getSortInference();
1489 isMonotonic
= si
->isMonotonic(tn
);
1491 //if ground, everything is monotonic
1495 if( d_tn_mono_master
.isNull() ){
1496 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn
<< std::endl
;
1497 d_tn_mono_master
= tn
;
1499 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn
<< std::endl
;
1500 d_tn_mono_slave
[tn
] = true;
1503 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn
<< std::endl
;
1504 d_tn_mono_slave
[tn
] = false;
1508 //set the minimum positive cardinality for master if necessary
1509 if( polarity
&& tn
==d_tn_mono_master
){
1510 Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl
;
1511 if( d_min_pos_tn_master_card
.get()==-1 || nCard
<d_min_pos_tn_master_card
.get() ){
1512 d_min_pos_tn_master_card
.set( nCard
);
1516 Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl
;
1517 d_rep_model
[tn
]->assertCardinality( d_out
, nCard
, polarity
);
1518 //check if combined cardinality is violated
1519 checkCombinedCardinality();
1521 //otherwise, make equal via lemma
1522 if( d_card_assertions_eqv_lemma
.find( lit
)==d_card_assertions_eqv_lemma
.end() ){
1523 Node eqv_lit
= NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT
, ct
, lit
[1] );
1524 eqv_lit
= lit
.eqNode( eqv_lit
);
1525 Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit
<< std::endl
;
1526 getOutputChannel().lemma( eqv_lit
);
1527 d_card_assertions_eqv_lemma
[lit
] = true;
1530 }else if( lit
.getKind()==COMBINED_CARDINALITY_CONSTRAINT
){
1532 //safe to assume int here
1533 int nCard
= lit
[0].getConst
<Rational
>().getNumerator().getSignedInt();
1534 if( d_min_pos_com_card
.get()==-1 || nCard
<d_min_pos_com_card
.get() ){
1535 d_min_pos_com_card
.set( nCard
);
1536 checkCombinedCardinality();
1540 if( Trace
.isOn("uf-ss-warn") ){
1541 ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
1542 //// a theory propagation is not a decision.
1544 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1545 if( !it
->second
->hasCardinalityAsserted() ){
1546 Trace("uf-ss-warn") << "WARNING: Assert " << n
<< " as a decision before cardinality for " << it
->first
<< "." << std::endl
;
1547 //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
1557 if( lit
.getKind()==CARDINALITY_CONSTRAINT
|| lit
.getKind()==COMBINED_CARDINALITY_CONSTRAINT
){
1558 // cardinality constraint from user input, set incomplete
1559 Trace("uf-ss") << "Literal " << lit
<< " not handled when uf ss mode is not FULL, set incomplete." << std::endl
;
1560 d_out
->setIncomplete();
1563 Trace("uf-ss") << "Assert: done " << n
<< " " << isDecision
<< std::endl
;
1566 bool CardinalityExtension::areDisequal(Node a
, Node b
)
1571 eq::EqualityEngine
* ee
= d_th
->getEqualityEngine();
1572 a
= ee
->getRepresentative(a
);
1573 b
= ee
->getRepresentative(b
);
1574 if (ee
->areDisequal(a
, b
, false))
1578 SortModel
* c
= getSortModel(a
);
1581 return c
->areDisequal(a
, b
);
1587 void CardinalityExtension::check(Theory::Effort level
)
1590 if (options::ufssMode() == options::UfssMode::FULL
)
1592 Trace("uf-ss-solver")
1593 << "CardinalityExtension: check " << level
<< std::endl
;
1594 if (level
== Theory::EFFORT_FULL
)
1596 if (Debug
.isOn("uf-ss-debug"))
1598 debugPrint("uf-ss-debug");
1600 if (Trace
.isOn("uf-ss-state"))
1602 Trace("uf-ss-state")
1603 << "CardinalityExtension::check " << level
<< std::endl
;
1604 for (std::pair
<const TypeNode
, SortModel
*>& rm
: d_rep_model
)
1606 Trace("uf-ss-state") << " " << rm
.first
<< " has cardinality "
1607 << rm
.second
->getCardinality() << std::endl
;
1611 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1612 it
->second
->check( level
, d_out
);
1613 if( it
->second
->isConflict() ){
1619 else if (options::ufssMode() == options::UfssMode::NO_MINIMAL
)
1621 if( level
==Theory::EFFORT_FULL
){
1622 // split on an equality between two equivalence classes (at most one per type)
1623 std::map
< TypeNode
, std::vector
< Node
> > eqc_list
;
1624 std::map
< TypeNode
, bool > type_proc
;
1625 eq::EqClassesIterator
eqcs_i(d_th
->getEqualityEngine());
1626 while( !eqcs_i
.isFinished() ){
1628 TypeNode tn
= a
.getType();
1630 if( type_proc
.find( tn
)==type_proc
.end() ){
1631 std::map
< TypeNode
, std::vector
< Node
> >::iterator itel
= eqc_list
.find( tn
);
1632 if( itel
!=eqc_list
.end() ){
1633 for( unsigned j
=0; j
<itel
->second
.size(); j
++ ){
1634 Node b
= itel
->second
[j
];
1635 if( !d_th
->getEqualityEngine()->areDisequal( a
, b
, false ) ){
1636 Node eq
= Rewriter::rewrite( a
.eqNode( b
) );
1637 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, eq
.negate() );
1638 Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem
<< std::endl
;
1639 d_out
->lemma( lem
);
1640 d_out
->requirePhase( eq
, true );
1641 type_proc
[tn
] = true;
1646 eqc_list
[tn
].push_back( a
);
1655 // unhandled uf ss mode
1658 Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
1663 void CardinalityExtension::presolve()
1665 d_initializedCombinedCardinality
= false;
1666 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1667 it
->second
->presolve();
1668 it
->second
->initialize( d_out
);
1672 CardinalityExtension::CombinedCardinalityDecisionStrategy::
1673 CombinedCardinalityDecisionStrategy(context::Context
* satContext
,
1674 Valuation valuation
)
1675 : DecisionStrategyFmf(satContext
, valuation
)
1678 Node
CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
1681 NodeManager
* nm
= NodeManager::currentNM();
1682 return nm
->mkNode(COMBINED_CARDINALITY_CONSTRAINT
, nm
->mkConst(Rational(i
)));
1686 CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
1688 return std::string("uf_combined_card");
1691 void CardinalityExtension::preRegisterTerm(TNode n
)
1693 if (options::ufssMode() == options::UfssMode::FULL
)
1695 //initialize combined cardinality
1696 initializeCombinedCardinality();
1698 Trace("uf-ss-register") << "Preregister " << n
<< "." << std::endl
;
1699 //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
1700 TypeNode tn
= n
.getType();
1701 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1702 if( it
==d_rep_model
.end() ){
1703 SortModel
* rm
= NULL
;
1705 Trace("uf-ss-register") << "Create sort model " << tn
<< "." << std::endl
;
1706 rm
= new SortModel( n
, d_th
->getSatContext(), d_th
->getUserContext(), this );
1707 //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
1710 if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
1711 Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
1712 Debug("uf-ss-na") << " (" << f << ")";
1713 Debug("uf-ss-na") << std::endl;
1714 Unimplemented() << "Cannot perform finite model finding on arithmetic quantifier";
1715 }else if( tn.isDatatype() ){
1716 Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
1717 Debug("uf-ss-na") << " (" << f << ")";
1718 Debug("uf-ss-na") << std::endl;
1719 Unimplemented() << "Cannot perform finite model finding on datatype quantifier";
1724 rm
->initialize( d_out
);
1725 d_rep_model
[tn
] = rm
;
1726 //d_rep_model_init[tn] = true;
1729 //ensure sort model is initialized
1730 it
->second
->initialize( d_out
);
1735 SortModel
* CardinalityExtension::getSortModel(Node n
)
1737 TypeNode tn
= n
.getType();
1738 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1739 //pre-register the type if not done already
1740 if( it
==d_rep_model
.end() ){
1741 preRegisterTerm( n
);
1742 it
= d_rep_model
.find( tn
);
1744 if( it
!=d_rep_model
.end() ){
1751 /** get cardinality for sort */
1752 int CardinalityExtension::getCardinality(Node n
)
1754 SortModel
* c
= getSortModel( n
);
1756 return c
->getCardinality();
1762 int CardinalityExtension::getCardinality(TypeNode tn
)
1764 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1765 if( it
!=d_rep_model
.end() && it
->second
){
1766 return it
->second
->getCardinality();
1772 void CardinalityExtension::debugPrint(const char* c
)
1774 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1775 Debug( c
) << "Conflict find structure for " << it
->first
<< ": " << std::endl
;
1776 it
->second
->debugPrint( c
);
1777 Debug( c
) << std::endl
;
1781 bool CardinalityExtension::debugModel(TheoryModel
* m
)
1783 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1784 if( !it
->second
->debugModel( m
) ){
1792 void CardinalityExtension::initializeCombinedCardinality()
1794 if (d_cc_dec_strat
.get() != nullptr
1795 && !d_initializedCombinedCardinality
.get())
1797 d_initializedCombinedCardinality
= true;
1798 d_th
->getDecisionManager()->registerStrategy(
1799 DecisionManager::STRAT_UF_COMBINED_CARD
, d_cc_dec_strat
.get());
1804 void CardinalityExtension::checkCombinedCardinality()
1806 Assert(options::ufssMode() == options::UfssMode::FULL
);
1807 if( options::ufssFairness() ){
1808 Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl
;
1809 int totalCombinedCard
= 0;
1810 int maxMonoSlave
= 0;
1811 TypeNode maxSlaveType
;
1812 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1813 int max_neg
= it
->second
->getMaximumNegativeCardinality();
1814 if( !options::ufssFairnessMonotone() ){
1815 totalCombinedCard
+= max_neg
;
1817 std::map
< TypeNode
, bool >::iterator its
= d_tn_mono_slave
.find( it
->first
);
1818 if( its
==d_tn_mono_slave
.end() || !its
->second
){
1819 totalCombinedCard
+= max_neg
;
1821 if( max_neg
>maxMonoSlave
){
1822 maxMonoSlave
= max_neg
;
1823 maxSlaveType
= it
->first
;
1828 Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard
<< std::endl
;
1829 if( options::ufssFairnessMonotone() ){
1830 Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave
<< std::endl
;
1831 if( d_min_pos_tn_master_card
.get()!=-1 && maxMonoSlave
>d_min_pos_tn_master_card
.get() ){
1832 int mc
= d_min_pos_tn_master_card
.get();
1833 std::vector
< Node
> conf
;
1834 conf
.push_back( d_rep_model
[d_tn_mono_master
]->getCardinalityLiteral( mc
) );
1835 conf
.push_back( d_rep_model
[maxSlaveType
]->getCardinalityLiteral( maxMonoSlave
).negate() );
1836 Node cf
= NodeManager::currentNM()->mkNode( AND
, conf
);
1837 Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict"
1838 << " : " << cf
<< std::endl
;
1839 Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
1840 << " : " << cf
<< std::endl
;
1841 getOutputChannel().conflict( cf
);
1842 d_conflict
.set( true );
1846 int cc
= d_min_pos_com_card
.get();
1847 if( cc
!=-1 && totalCombinedCard
> cc
){
1849 Node com_lit
= d_cc_dec_strat
->getLiteral(cc
);
1850 std::vector
< Node
> conf
;
1851 conf
.push_back( com_lit
);
1853 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin();
1854 it
!= d_rep_model
.end(); ++it
){
1856 if( options::ufssFairnessMonotone() ){
1857 std::map
< TypeNode
, bool >::iterator its
=
1858 d_tn_mono_slave
.find( it
->first
);
1859 if( its
!=d_tn_mono_slave
.end() && its
->second
){
1864 int c
= it
->second
->getMaximumNegativeCardinality();
1866 conf
.push_back( it
->second
->getCardinalityLiteral( c
).negate() );
1869 if( totalAdded
>cc
){
1874 Node cf
= NodeManager::currentNM()->mkNode( AND
, conf
);
1875 Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
1877 Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
1879 getOutputChannel().conflict( cf
);
1880 d_conflict
.set( true );
1885 CardinalityExtension::Statistics::Statistics()
1886 : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
1887 d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
1888 d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
1889 d_disamb_term_lemmas("CardinalityExtension::Disambiguate_Term_Lemmas", 0),
1890 d_totality_lemmas("CardinalityExtension::Totality_Lemmas", 0),
1891 d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
1893 smtStatisticsRegistry()->registerStat(&d_clique_conflicts
);
1894 smtStatisticsRegistry()->registerStat(&d_clique_lemmas
);
1895 smtStatisticsRegistry()->registerStat(&d_split_lemmas
);
1896 smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas
);
1897 smtStatisticsRegistry()->registerStat(&d_totality_lemmas
);
1898 smtStatisticsRegistry()->registerStat(&d_max_model_size
);
1901 CardinalityExtension::Statistics::~Statistics()
1903 smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts
);
1904 smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas
);
1905 smtStatisticsRegistry()->unregisterStat(&d_split_lemmas
);
1906 smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas
);
1907 smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas
);
1908 smtStatisticsRegistry()->unregisterStat(&d_max_model_size
);
1911 }/* CVC4::theory namespace::uf */
1912 }/* CVC4::theory namespace */
1913 }/* CVC4 namespace */