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() == UF_SS_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() == UF_SS_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 if( options::sortInference()){
741 //If sort inference is enabled, search for regions with same sort.
742 std::map
< int, int > sortsFound
;
743 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
744 if( d_regions
[i
]->valid() ){
745 Node op
= d_regions
[i
]->frontKey();
746 int sort_id
= d_thss
->getSortInference()->getSortId(op
);
747 if( sortsFound
.find( sort_id
)!=sortsFound
.end() ){
748 Debug("fmf-full-check") << "Combined regions " << i
<< " " << sortsFound
[sort_id
] << std::endl
;
749 combineRegions( sortsFound
[sort_id
], i
);
753 sortsFound
[sort_id
] = i
;
759 //naive strategy, force region combination involving the first valid region
760 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
761 if( d_regions
[i
]->valid() ){
762 int fcr
= forceCombineRegion( i
, false );
763 Debug("fmf-full-check") << "Combined regions " << i
<< " " << fcr
<< std::endl
;
764 Trace("uf-ss-debug") << "Combined regions " << i
<< " " << fcr
<< std::endl
;
771 Trace("uf-ss-debug") << "Must recheck." << std::endl
;
781 void SortModel::presolve() {
782 d_initialized
= false;
785 void SortModel::propagate( Theory::Effort level
, OutputChannel
* out
){
789 int SortModel::getNumDisequalitiesToRegion( Node n
, int ri
){
790 int ni
= d_regions_map
[n
];
792 DiseqList
* del
= d_regions
[ni
]->getRegionInfo(n
)->get(0);
793 for( DiseqList::iterator it
= del
->begin(); it
!= del
->end(); ++it
){
795 if( d_regions_map
[ (*it
).first
]==ri
){
803 void SortModel::getDisequalitiesToRegions(int ri
,
804 std::map
< int, int >& regions_diseq
)
806 Region
* region
= d_regions
[ri
];
807 for(Region::iterator it
= region
->begin(); it
!= region
->end(); ++it
){
808 if( it
->second
->valid() ){
809 DiseqList
* del
= it
->second
->get(0);
810 for( DiseqList::iterator it2
= del
->begin(); it2
!= del
->end(); ++it2
){
812 Assert(isValid(d_regions_map
[(*it2
).first
]));
813 //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
814 regions_diseq
[ d_regions_map
[ (*it2
).first
] ]++;
821 void SortModel::setSplitScore( Node n
, int s
){
822 if( d_split_score
.find( n
)!=d_split_score
.end() ){
823 int ss
= d_split_score
[ n
];
824 d_split_score
[ n
] = s
>ss
? s
: ss
;
826 d_split_score
[ n
] = s
;
828 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
829 setSplitScore( n
[i
], s
+1 );
833 void SortModel::assertCardinality( OutputChannel
* out
, int c
, bool val
){
835 Trace("uf-ss-assert")
836 << "Assert cardinality " << d_type
<< " " << c
<< " " << val
838 << d_thss
->getTheory()->getValuation().getAssertionLevel() << std::endl
;
840 Node cl
= getCardinalityLiteral( c
);
842 bool doCheckRegions
= !d_hasCard
;
843 bool prevHasCard
= d_hasCard
;
845 if( !prevHasCard
|| c
<d_cardinality
){
847 simpleCheckCardinality();
848 if( d_thss
->d_conflict
.get() ){
852 //should check all regions now
853 if( doCheckRegions
){
854 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
855 if( d_regions
[i
]->valid() ){
863 // we assert it positively, if its beyond the bound, abort
864 if (options::ufssAbortCardinality() != -1
865 && c
>= options::ufssAbortCardinality())
867 std::stringstream ss
;
868 ss
<< "Maximum cardinality (" << options::ufssAbortCardinality()
869 << ") for finite model finding exceeded." << std::endl
;
870 throw LogicException(ss
.str());
875 if( c
>d_maxNegCard
.get() ){
876 Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for " << d_type
<< " is now " << c
<< std::endl
;
877 d_maxNegCard
.set( c
);
878 simpleCheckCardinality();
884 void SortModel::checkRegion( int ri
, bool checkCombine
){
885 if( isValid(ri
) && d_hasCard
){
886 Assert(d_cardinality
> 0);
887 if( checkCombine
&& d_regions
[ri
]->getMustCombine( d_cardinality
) ){
888 ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
889 //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
891 // int inDeg = d_regions[i]->d_disequalities_size[1][ it-> first ];
892 // int outDeg = d_regions[i]->d_disequalities_size[0][ it-> first ];
893 // if( inDeg<outDeg ){
897 int riNew
= forceCombineRegion( ri
, true );
899 checkRegion( riNew
, checkCombine
);
902 //now check if region is in conflict
903 std::vector
< Node
> clique
;
904 if( d_regions
[ri
]->check( Theory::EFFORT_STANDARD
, d_cardinality
, clique
) ){
906 addCliqueLemma( clique
, &d_thss
->getOutputChannel() );
911 int SortModel::forceCombineRegion( int ri
, bool useDensity
){
913 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
914 if( ri
!=i
&& d_regions
[i
]->valid() ){
915 return combineRegions( ri
, i
);
920 //this region must merge with another
921 if( Debug
.isOn("uf-ss-check-region") ){
922 Debug("uf-ss-check-region") << "We must combine Region #" << ri
<< ". " << std::endl
;
923 d_regions
[ri
]->debugPrint("uf-ss-check-region");
925 //take region with maximum disequality density
928 std::map
< int, int > regions_diseq
;
929 getDisequalitiesToRegions( ri
, regions_diseq
);
930 for( std::map
< int, int >::iterator it
= regions_diseq
.begin(); it
!= regions_diseq
.end(); ++it
){
931 Debug("uf-ss-check-region") << it
->first
<< " : " << it
->second
<< std::endl
;
933 for( std::map
< int, int >::iterator it
= regions_diseq
.begin(); it
!= regions_diseq
.end(); ++it
){
934 Assert(it
->first
!= ri
);
935 Assert(isValid(it
->first
));
936 Assert(d_regions
[it
->first
]->getNumReps() > 0);
937 double tempScore
= double(it
->second
)/double(d_regions
[it
->first
]->getNumReps() );
938 if( tempScore
>maxScore
){
939 maxRegion
= it
->first
;
940 maxScore
= tempScore
;
944 if( Debug
.isOn("uf-ss-check-region") ){
945 Debug("uf-ss-check-region") << "Combine with region #" << maxRegion
<< ":" << std::endl
;
946 d_regions
[maxRegion
]->debugPrint("uf-ss-check-region");
948 return combineRegions( ri
, maxRegion
);
955 int SortModel::combineRegions( int ai
, int bi
){
956 #ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
957 if( d_regions
[ai
]->getNumReps()<d_regions
[bi
]->getNumReps() ){
958 return combineRegions( bi
, ai
);
961 Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi
<< " with Region #" << ai
<< std::endl
;
962 Assert(isValid(ai
) && isValid(bi
));
963 Region
* region_bi
= d_regions
[bi
];
964 for(Region::iterator it
= region_bi
->begin(); it
!= region_bi
->end(); ++it
){
965 Region::RegionNodeInfo
* rni
= it
->second
;
967 d_regions_map
[ it
->first
] = ai
;
970 //update regions disequal DO_THIS?
971 d_regions
[ai
]->combine( d_regions
[bi
] );
972 d_regions
[bi
]->setValid( false );
976 void SortModel::moveNode( Node n
, int ri
){
977 Debug("uf-ss-region") << "uf-ss: Move node " << n
<< " to Region #" << ri
<< std::endl
;
978 Assert(isValid(d_regions_map
[n
]));
980 //move node to region ri
981 d_regions
[ri
]->takeNode( d_regions
[ d_regions_map
[n
] ], n
);
982 d_regions_map
[n
] = ri
;
985 int SortModel::addSplit( Region
* r
, OutputChannel
* out
){
987 if( r
->hasSplits() ){
988 //take the first split you find
989 for( Region::split_iterator it
= r
->begin_splits();
990 it
!= r
->end_splits(); ++it
){
996 Assert(s
!= Node::null());
999 //add lemma to output channel
1000 Assert(s
.getKind() == EQUAL
);
1001 Node ss
= Rewriter::rewrite( s
);
1002 if( ss
.getKind()!=EQUAL
){
1003 Node b_t
= NodeManager::currentNM()->mkConst( true );
1004 Node b_f
= NodeManager::currentNM()->mkConst( false );
1006 Trace("uf-ss-lemma") << "....Assert disequal directly : "
1007 << s
[0] << " " << s
[1] << std::endl
;
1008 assertDisequal( s
[0], s
[1], b_t
);
1011 Trace("uf-ss-warn") << "Split on unknown literal : " << ss
<< std::endl
;
1014 Message() << "Bad split " << s
<< std::endl
;
1015 AlwaysAssert(false);
1018 if( options::sortInference()) {
1019 for( int i
=0; i
<2; i
++ ){
1020 int si
= d_thss
->getSortInference()->getSortId( ss
[i
] );
1021 Trace("uf-ss-split-si") << si
<< " ";
1023 Trace("uf-ss-split-si") << std::endl
;
1025 //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
1026 //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
1027 //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
1028 //Notice() << "*** Split on " << s << std::endl;
1029 //split on the equality s
1030 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, ss
, ss
.negate() );
1031 if( doSendLemma( lem
) ){
1032 Trace("uf-ss-lemma") << "*** Split on " << s
<< std::endl
;
1033 //tell the sat solver to explore the equals branch first
1034 out
->requirePhase( ss
, true );
1035 ++( d_thss
->d_statistics
.d_split_lemmas
);
1044 void SortModel::addCliqueLemma( std::vector
< Node
>& clique
, OutputChannel
* out
){
1046 Assert(d_cardinality
> 0);
1047 while( clique
.size()>size_t(d_cardinality
+1) ){
1051 std::vector
<Node
> eqs
;
1052 for (unsigned i
= 0, size
= clique
.size(); i
< size
; i
++)
1054 for (unsigned j
= 0; j
< i
; j
++)
1056 eqs
.push_back(clique
[i
].eqNode(clique
[j
]));
1059 eqs
.push_back(d_cardinality_literal
[d_cardinality
].notNode());
1060 Node lem
= NodeManager::currentNM()->mkNode(OR
, eqs
);
1061 if (doSendLemma(lem
))
1063 Trace("uf-ss-lemma") << "*** Add clique lemma " << lem
<< std::endl
;
1064 ++(d_thss
->d_statistics
.d_clique_lemmas
);
1068 void SortModel::addTotalityAxiom( Node n
, int cardinality
, OutputChannel
* out
){
1069 if( std::find( d_totality_terms
[0].begin(), d_totality_terms
[0].end(), n
)==d_totality_terms
[0].end() ){
1070 if( std::find( d_totality_lems
[n
].begin(), d_totality_lems
[n
].end(), cardinality
) == d_totality_lems
[n
].end() ){
1071 d_totality_lems
[n
].push_back( cardinality
);
1072 Node cardLit
= d_cardinality_literal
[ cardinality
];
1074 if( options::sortInference() ){
1075 sort_id
= d_thss
->getSortInference()->getSortId(n
);
1077 Trace("uf-ss-totality") << "Add totality lemma for " << n
<< " " << cardinality
<< ", sort id is " << sort_id
<< std::endl
;
1078 int use_cardinality
= cardinality
;
1079 if( options::ufssTotalitySymBreak() ){
1080 if( d_sym_break_index
.find(n
)!=d_sym_break_index
.end() ){
1081 use_cardinality
= d_sym_break_index
[n
];
1082 }else if( (int)d_sym_break_terms
[n
.getType()][sort_id
].size()<cardinality
-1 ){
1083 use_cardinality
= d_sym_break_terms
[n
.getType()][sort_id
].size() + 1;
1084 d_sym_break_terms
[n
.getType()][sort_id
].push_back( n
);
1085 d_sym_break_index
[n
] = use_cardinality
;
1086 Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n
<< ", index = " << use_cardinality
<< std::endl
;
1087 if( d_sym_break_terms
[n
.getType()][sort_id
].size()>1 ){
1088 //enforce canonicity
1089 for( int i
=2; i
<use_cardinality
; i
++ ){
1090 //can only be assigned to domain constant d if someone has been assigned domain constant d-1
1091 Node eq
= n
.eqNode( getTotalityLemmaTerm( cardinality
, i
) );
1092 std::vector
< Node
> eqs
;
1093 for( unsigned j
=0; j
<(d_sym_break_terms
[n
.getType()][sort_id
].size()-1); j
++ ){
1094 eqs
.push_back( d_sym_break_terms
[n
.getType()][sort_id
][j
].eqNode( getTotalityLemmaTerm( cardinality
, i
-1 ) ) );
1096 Node ax
= eqs
.size()==1 ? eqs
[0] : NodeManager::currentNM()->mkNode( OR
, eqs
);
1097 Node lem
= NodeManager::currentNM()->mkNode( IMPLIES
, eq
, ax
);
1098 Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem
<< std::endl
;
1099 d_thss
->getOutputChannel().lemma( lem
);
1105 std::vector
< Node
> eqs
;
1106 for( int i
=0; i
<use_cardinality
; i
++ ){
1107 eqs
.push_back( n
.eqNode( getTotalityLemmaTerm( cardinality
, i
) ) );
1109 Node ax
= NodeManager::currentNM()->mkNode( OR
, eqs
);
1110 Node lem
= NodeManager::currentNM()->mkNode( IMPLIES
, cardLit
, ax
);
1111 Trace("uf-ss-lemma") << "*** Add totality axiom " << lem
<< std::endl
;
1112 //send as lemma to the output channel
1113 d_thss
->getOutputChannel().lemma( lem
);
1114 ++( d_thss
->d_statistics
.d_totality_lemmas
);
1119 /** apply totality */
1120 bool SortModel::applyTotality( int cardinality
){
1121 return options::ufssTotality() || cardinality
<=options::ufssTotalityLimited();
1124 /** get totality lemma terms */
1125 Node
SortModel::getTotalityLemmaTerm( int cardinality
, int i
){
1126 return d_totality_terms
[0][i
];
1129 void SortModel::simpleCheckCardinality() {
1130 if( d_maxNegCard
.get()!=0 && d_hasCard
.get() && d_cardinality
.get()<d_maxNegCard
.get() ){
1131 Node lem
= NodeManager::currentNM()->mkNode( AND
, getCardinalityLiteral( d_cardinality
.get() ),
1132 getCardinalityLiteral( d_maxNegCard
.get() ).negate() );
1133 Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem
<< std::endl
;
1134 d_thss
->getOutputChannel().conflict( lem
);
1135 d_thss
->d_conflict
.set( true );
1139 bool SortModel::doSendLemma( Node lem
) {
1140 if( d_lemma_cache
.find( lem
)==d_lemma_cache
.end() ){
1141 d_lemma_cache
[lem
] = true;
1142 d_thss
->getOutputChannel().lemma( lem
);
1149 void SortModel::debugPrint( const char* c
){
1150 if( Debug
.isOn( c
) ){
1151 Debug( c
) << "Number of reps = " << d_reps
<< std::endl
;
1152 Debug( c
) << "Cardinality req = " << d_cardinality
<< std::endl
;
1153 unsigned debugReps
= 0;
1154 for( unsigned i
=0; i
<d_regions_index
; i
++ ){
1155 Region
* region
= d_regions
[i
];
1156 if( region
->valid() ){
1157 Debug( c
) << "Region #" << i
<< ": " << std::endl
;
1158 region
->debugPrint( c
, true );
1159 Debug( c
) << std::endl
;
1160 for( Region::iterator it
= region
->begin(); it
!= region
->end(); ++it
){
1161 if( it
->second
->valid() ){
1162 if( d_regions_map
[ it
->first
]!=(int)i
){
1163 Debug( c
) << "***Bad regions map : " << it
->first
1164 << " " << d_regions_map
[ it
->first
].get() << std::endl
;
1168 debugReps
+= region
->getNumReps();
1172 if( debugReps
!=d_reps
){
1173 Debug( c
) << "***Bad reps: " << d_reps
<< ", "
1174 << "actual = " << debugReps
<< std::endl
;
1179 bool SortModel::debugModel( TheoryModel
* m
){
1180 if( Trace
.isOn("uf-ss-warn") ){
1181 std::vector
< Node
> eqcs
;
1182 eq::EqClassesIterator eqcs_i
=
1183 eq::EqClassesIterator(m
->getEqualityEngine());
1184 while( !eqcs_i
.isFinished() ){
1185 Node eqc
= (*eqcs_i
);
1186 if( eqc
.getType()==d_type
){
1187 if( std::find( eqcs
.begin(), eqcs
.end(), eqc
)==eqcs
.end() ){
1188 eqcs
.push_back( eqc
);
1189 //we must ensure that this equivalence class has been accounted for
1190 if( d_regions_map
.find( eqc
)==d_regions_map
.end() ){
1191 Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc
<< " unaccounted for." << std::endl
;
1192 Trace("uf-ss-warn") << " type : " << d_type
<< std::endl
;
1193 Trace("uf-ss-warn") << " kind : " << eqc
.getKind() << std::endl
;
1200 RepSet
* rs
= m
->getRepSetPtr();
1201 int nReps
= (int)rs
->getNumRepresentatives(d_type
);
1202 if( nReps
!=(d_maxNegCard
+1) ){
1203 Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type
<< "." << std::endl
;
1204 Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard
<< std::endl
;
1205 Trace("uf-ss-warn") << " # Reps : " << nReps
<< std::endl
;
1206 if( d_maxNegCard
>=nReps
){
1207 while( (int)d_fresh_aloc_reps
.size()<=d_maxNegCard
){
1208 std::stringstream ss
;
1209 ss
<< "r_" << d_type
<< "_";
1210 Node nn
= NodeManager::currentNM()->mkSkolem( ss
.str(), d_type
, "enumeration to meet negative card constraint" );
1211 d_fresh_aloc_reps
.push_back( nn
);
1213 if( d_maxNegCard
==0 ){
1214 rs
->d_type_reps
[d_type
].push_back(d_fresh_aloc_reps
[0]);
1217 std::vector
< Node
> force_cl
;
1218 for( int i
=0; i
<=d_maxNegCard
; i
++ ){
1219 for( int j
=(i
+1); j
<=d_maxNegCard
; j
++ ){
1220 force_cl
.push_back( d_fresh_aloc_reps
[i
].eqNode( d_fresh_aloc_reps
[j
] ).negate() );
1223 Node cl
= getCardinalityLiteral( d_maxNegCard
);
1224 Node lem
= NodeManager::currentNM()->mkNode( OR
, cl
, NodeManager::currentNM()->mkNode( AND
, force_cl
) );
1225 Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem
<< std::endl
;
1226 d_thss
->getOutputChannel().lemma( lem
);
1234 int SortModel::getNumRegions(){
1236 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
1237 if( d_regions
[i
]->valid() ){
1244 Node
SortModel::getCardinalityLiteral(unsigned c
)
1247 std::map
<int, Node
>::iterator itcl
= d_cardinality_literal
.find(c
);
1248 if (itcl
!= d_cardinality_literal
.end())
1250 return itcl
->second
;
1252 // get the literal from the decision strategy
1253 Node lit
= d_c_dec_strat
->getLiteral(c
- 1);
1254 d_cardinality_literal
[c
] = lit
;
1256 // Since we are reasoning about cardinality c, we invoke a totality axiom
1257 if (!applyTotality(c
))
1259 // return if we are not using totality axioms
1263 NodeManager
* nm
= NodeManager::currentNM();
1265 if (c
== 1 && !options::ufssTotalitySymBreak())
1267 // get arbitrary ground term
1268 var
= d_cardinality_term
;
1272 std::stringstream ss
;
1274 var
= nm
->mkSkolem(ss
.str(), d_type
, "is a cardinality lemma term");
1276 if ((c
- 1) < d_totality_terms
[0].size())
1278 d_totality_terms
[0][c
- 1] = var
;
1282 d_totality_terms
[0].push_back(var
);
1284 // must be distinct from all other cardinality terms
1285 for (unsigned i
= 1, size
= d_totality_terms
[0].size(); i
< size
; i
++)
1287 Node lem
= var
.eqNode(d_totality_terms
[0][i
- 1]).notNode();
1288 Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem
1290 d_thss
->getOutputChannel().lemma(lem
);
1292 // must send totality axioms for each existing term
1293 for (NodeIntMap::iterator it
= d_regions_map
.begin();
1294 it
!= d_regions_map
.end();
1297 addTotalityAxiom((*it
).first
, c
, &d_thss
->getOutputChannel());
1302 CardinalityExtension::CardinalityExtension(context::Context
* c
,
1303 context::UserContext
* u
,
1308 d_conflict(c
, false),
1310 d_min_pos_com_card(c
, -1),
1311 d_cc_dec_strat(nullptr),
1312 d_initializedCombinedCardinality(u
, false),
1313 d_card_assertions_eqv_lemma(u
),
1314 d_min_pos_tn_master_card(c
, -1),
1317 if (options::ufssMode() == UF_SS_FULL
&& options::ufssFairness())
1319 // Register the strategy with the decision manager of the theory.
1320 // We are guaranteed that the decision manager is ready since we
1321 // construct this module during TheoryUF::finishInit.
1322 d_cc_dec_strat
.reset(
1323 new CombinedCardinalityDecisionStrategy(c
, th
->getValuation()));
1327 CardinalityExtension::~CardinalityExtension()
1329 for (std::map
<TypeNode
, SortModel
*>::iterator it
= d_rep_model
.begin();
1330 it
!= d_rep_model
.end(); ++it
) {
1335 SortInference
* CardinalityExtension::getSortInference()
1337 return d_th
->getQuantifiersEngine()->getTheoryEngine()->getSortInference();
1340 /** get default sat context */
1341 context::Context
* CardinalityExtension::getSatContext()
1343 return d_th
->getSatContext();
1346 /** get default output channel */
1347 OutputChannel
& CardinalityExtension::getOutputChannel()
1349 return d_th
->getOutputChannel();
1353 void CardinalityExtension::ensureEqc(SortModel
* c
, Node a
)
1356 d_rel_eqc
[a
] = true;
1357 Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a
<< " : "
1358 << a
.getType() << std::endl
;
1360 Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1365 void CardinalityExtension::ensureEqcRec(Node n
)
1368 SortModel
* c
= getSortModel( n
);
1372 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1373 ensureEqcRec( n
[i
] );
1379 bool CardinalityExtension::hasEqc(Node a
)
1381 NodeBoolMap::iterator it
= d_rel_eqc
.find( a
);
1382 return it
!=d_rel_eqc
.end() && (*it
).second
;
1386 void CardinalityExtension::newEqClass(Node a
)
1388 SortModel
* c
= getSortModel( a
);
1393 Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a
<< " : "
1394 << a
.getType() << std::endl
;
1396 Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1403 void CardinalityExtension::merge(Node a
, Node b
)
1405 //TODO: ensure they are relevant
1406 SortModel
* c
= getSortModel( a
);
1411 Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a
<< " " << b
1412 << " : " << a
.getType() << std::endl
;
1414 Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl
;
1416 //c->assignEqClass( b, a );
1417 d_rel_eqc
[b
] = true;
1420 Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a
<< " " << b
1421 << " : " << a
.getType() << std::endl
;
1423 Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl
;
1428 /** assert terms are disequal */
1429 void CardinalityExtension::assertDisequal(Node a
, Node b
, Node reason
)
1431 SortModel
* c
= getSortModel( a
);
1437 Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a
1438 << " " << b
<< " : " << a
.getType() << std::endl
;
1439 c
->assertDisequal( a
, b
, reason
);
1440 Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal."
1445 /** assert a node */
1446 void CardinalityExtension::assertNode(Node n
, bool isDecision
)
1448 Trace("uf-ss") << "Assert " << n
<< " " << isDecision
<< std::endl
;
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
;
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() ){
1469 if( d_th
->getQuantifiersEngine() ){
1470 isMonotonic
= getSortInference()->isMonotonic( tn
);
1472 //if ground, everything is monotonic
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
;
1480 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn
<< std::endl
;
1481 d_tn_mono_slave
[tn
] = true;
1484 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn
<< std::endl
;
1485 d_tn_mono_slave
[tn
] = false;
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
);
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();
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;
1511 }else if( lit
.getKind()==COMBINED_CARDINALITY_CONSTRAINT
){
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();
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.
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;
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();
1542 Trace("uf-ss") << "Assert: done " << n
<< " " << isDecision
<< std::endl
;
1545 bool CardinalityExtension::areDisequal(Node a
, Node b
)
1550 eq::EqualityEngine
* ee
= d_th
->getEqualityEngine();
1551 a
= ee
->getRepresentative(a
);
1552 b
= ee
->getRepresentative(b
);
1553 if (ee
->areDisequal(a
, b
, false))
1557 SortModel
* c
= getSortModel(a
);
1560 return c
->areDisequal(a
, b
);
1566 void CardinalityExtension::check(Theory::Effort level
)
1569 if( options::ufssMode()==UF_SS_FULL
){
1570 Trace("uf-ss-solver")
1571 << "CardinalityExtension: check " << level
<< std::endl
;
1572 if (level
== Theory::EFFORT_FULL
)
1574 if (Debug
.isOn("uf-ss-debug"))
1576 debugPrint("uf-ss-debug");
1578 if (Trace
.isOn("uf-ss-state"))
1580 Trace("uf-ss-state")
1581 << "CardinalityExtension::check " << level
<< std::endl
;
1582 for (std::pair
<const TypeNode
, SortModel
*>& rm
: d_rep_model
)
1584 Trace("uf-ss-state") << " " << rm
.first
<< " has cardinality "
1585 << rm
.second
->getCardinality() << std::endl
;
1589 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1590 it
->second
->check( level
, d_out
);
1591 if( it
->second
->isConflict() ){
1596 }else if( options::ufssMode()==UF_SS_NO_MINIMAL
){
1597 if( level
==Theory::EFFORT_FULL
){
1598 // split on an equality between two equivalence classes (at most one per type)
1599 std::map
< TypeNode
, std::vector
< Node
> > eqc_list
;
1600 std::map
< TypeNode
, bool > type_proc
;
1601 eq::EqClassesIterator
eqcs_i(d_th
->getEqualityEngine());
1602 while( !eqcs_i
.isFinished() ){
1604 TypeNode tn
= a
.getType();
1606 if( type_proc
.find( tn
)==type_proc
.end() ){
1607 std::map
< TypeNode
, std::vector
< Node
> >::iterator itel
= eqc_list
.find( tn
);
1608 if( itel
!=eqc_list
.end() ){
1609 for( unsigned j
=0; j
<itel
->second
.size(); j
++ ){
1610 Node b
= itel
->second
[j
];
1611 if( !d_th
->getEqualityEngine()->areDisequal( a
, b
, false ) ){
1612 Node eq
= Rewriter::rewrite( a
.eqNode( b
) );
1613 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, eq
.negate() );
1614 Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem
<< std::endl
;
1615 d_out
->lemma( lem
);
1616 d_out
->requirePhase( eq
, true );
1617 type_proc
[tn
] = true;
1622 eqc_list
[tn
].push_back( a
);
1629 // unhandled uf ss mode
1632 Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
1637 void CardinalityExtension::presolve()
1639 d_initializedCombinedCardinality
= false;
1640 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1641 it
->second
->presolve();
1642 it
->second
->initialize( d_out
);
1646 CardinalityExtension::CombinedCardinalityDecisionStrategy::
1647 CombinedCardinalityDecisionStrategy(context::Context
* satContext
,
1648 Valuation valuation
)
1649 : DecisionStrategyFmf(satContext
, valuation
)
1652 Node
CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
1655 NodeManager
* nm
= NodeManager::currentNM();
1656 return nm
->mkNode(COMBINED_CARDINALITY_CONSTRAINT
, nm
->mkConst(Rational(i
)));
1660 CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
1662 return std::string("uf_combined_card");
1665 void CardinalityExtension::preRegisterTerm(TNode n
)
1667 if( options::ufssMode()==UF_SS_FULL
){
1668 //initialize combined cardinality
1669 initializeCombinedCardinality();
1671 Trace("uf-ss-register") << "Preregister " << n
<< "." << std::endl
;
1672 //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
1673 TypeNode tn
= n
.getType();
1674 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1675 if( it
==d_rep_model
.end() ){
1676 SortModel
* rm
= NULL
;
1678 Trace("uf-ss-register") << "Create sort model " << tn
<< "." << std::endl
;
1679 rm
= new SortModel( n
, d_th
->getSatContext(), d_th
->getUserContext(), this );
1680 //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
1683 if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
1684 Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
1685 Debug("uf-ss-na") << " (" << f << ")";
1686 Debug("uf-ss-na") << std::endl;
1687 Unimplemented() << "Cannot perform finite model finding on arithmetic quantifier";
1688 }else if( tn.isDatatype() ){
1689 Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
1690 Debug("uf-ss-na") << " (" << f << ")";
1691 Debug("uf-ss-na") << std::endl;
1692 Unimplemented() << "Cannot perform finite model finding on datatype quantifier";
1697 rm
->initialize( d_out
);
1698 d_rep_model
[tn
] = rm
;
1699 //d_rep_model_init[tn] = true;
1702 //ensure sort model is initialized
1703 it
->second
->initialize( d_out
);
1708 SortModel
* CardinalityExtension::getSortModel(Node n
)
1710 TypeNode tn
= n
.getType();
1711 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1712 //pre-register the type if not done already
1713 if( it
==d_rep_model
.end() ){
1714 preRegisterTerm( n
);
1715 it
= d_rep_model
.find( tn
);
1717 if( it
!=d_rep_model
.end() ){
1724 /** get cardinality for sort */
1725 int CardinalityExtension::getCardinality(Node n
)
1727 SortModel
* c
= getSortModel( n
);
1729 return c
->getCardinality();
1735 int CardinalityExtension::getCardinality(TypeNode tn
)
1737 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1738 if( it
!=d_rep_model
.end() && it
->second
){
1739 return it
->second
->getCardinality();
1745 void CardinalityExtension::debugPrint(const char* c
)
1747 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1748 Debug( c
) << "Conflict find structure for " << it
->first
<< ": " << std::endl
;
1749 it
->second
->debugPrint( c
);
1750 Debug( c
) << std::endl
;
1754 bool CardinalityExtension::debugModel(TheoryModel
* m
)
1756 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1757 if( !it
->second
->debugModel( m
) ){
1765 void CardinalityExtension::initializeCombinedCardinality()
1767 if (d_cc_dec_strat
.get() != nullptr
1768 && !d_initializedCombinedCardinality
.get())
1770 d_initializedCombinedCardinality
= true;
1771 d_th
->getDecisionManager()->registerStrategy(
1772 DecisionManager::STRAT_UF_COMBINED_CARD
, d_cc_dec_strat
.get());
1777 void CardinalityExtension::checkCombinedCardinality()
1779 Assert(options::ufssMode() == UF_SS_FULL
);
1780 if( options::ufssFairness() ){
1781 Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl
;
1782 int totalCombinedCard
= 0;
1783 int maxMonoSlave
= 0;
1784 TypeNode maxSlaveType
;
1785 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1786 int max_neg
= it
->second
->getMaximumNegativeCardinality();
1787 if( !options::ufssFairnessMonotone() ){
1788 totalCombinedCard
+= max_neg
;
1790 std::map
< TypeNode
, bool >::iterator its
= d_tn_mono_slave
.find( it
->first
);
1791 if( its
==d_tn_mono_slave
.end() || !its
->second
){
1792 totalCombinedCard
+= max_neg
;
1794 if( max_neg
>maxMonoSlave
){
1795 maxMonoSlave
= max_neg
;
1796 maxSlaveType
= it
->first
;
1801 Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard
<< std::endl
;
1802 if( options::ufssFairnessMonotone() ){
1803 Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave
<< std::endl
;
1804 if( d_min_pos_tn_master_card
.get()!=-1 && maxMonoSlave
>d_min_pos_tn_master_card
.get() ){
1805 int mc
= d_min_pos_tn_master_card
.get();
1806 std::vector
< Node
> conf
;
1807 conf
.push_back( d_rep_model
[d_tn_mono_master
]->getCardinalityLiteral( mc
) );
1808 conf
.push_back( d_rep_model
[maxSlaveType
]->getCardinalityLiteral( maxMonoSlave
).negate() );
1809 Node cf
= NodeManager::currentNM()->mkNode( AND
, conf
);
1810 Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict"
1811 << " : " << cf
<< std::endl
;
1812 Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
1813 << " : " << cf
<< std::endl
;
1814 getOutputChannel().conflict( cf
);
1815 d_conflict
.set( true );
1819 int cc
= d_min_pos_com_card
.get();
1820 if( cc
!=-1 && totalCombinedCard
> cc
){
1822 Node com_lit
= d_cc_dec_strat
->getLiteral(cc
);
1823 std::vector
< Node
> conf
;
1824 conf
.push_back( com_lit
);
1826 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin();
1827 it
!= d_rep_model
.end(); ++it
){
1829 if( options::ufssFairnessMonotone() ){
1830 std::map
< TypeNode
, bool >::iterator its
=
1831 d_tn_mono_slave
.find( it
->first
);
1832 if( its
!=d_tn_mono_slave
.end() && its
->second
){
1837 int c
= it
->second
->getMaximumNegativeCardinality();
1839 conf
.push_back( it
->second
->getCardinalityLiteral( c
).negate() );
1842 if( totalAdded
>cc
){
1847 Node cf
= NodeManager::currentNM()->mkNode( AND
, conf
);
1848 Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
1850 Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
1852 getOutputChannel().conflict( cf
);
1853 d_conflict
.set( true );
1858 CardinalityExtension::Statistics::Statistics()
1859 : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
1860 d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
1861 d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
1862 d_disamb_term_lemmas("CardinalityExtension::Disambiguate_Term_Lemmas", 0),
1863 d_totality_lemmas("CardinalityExtension::Totality_Lemmas", 0),
1864 d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
1866 smtStatisticsRegistry()->registerStat(&d_clique_conflicts
);
1867 smtStatisticsRegistry()->registerStat(&d_clique_lemmas
);
1868 smtStatisticsRegistry()->registerStat(&d_split_lemmas
);
1869 smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas
);
1870 smtStatisticsRegistry()->registerStat(&d_totality_lemmas
);
1871 smtStatisticsRegistry()->registerStat(&d_max_model_size
);
1874 CardinalityExtension::Statistics::~Statistics()
1876 smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts
);
1877 smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas
);
1878 smtStatisticsRegistry()->unregisterStat(&d_split_lemmas
);
1879 smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas
);
1880 smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas
);
1881 smtStatisticsRegistry()->unregisterStat(&d_max_model_size
);
1884 }/* CVC4::theory namespace::uf */
1885 }/* CVC4::theory namespace */
1886 }/* CVC4 namespace */