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-2020 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_state
.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 TheoryInferenceManager
& im
,
465 CardinalityExtension
* thss
)
466 : d_type(n
.getType()),
470 d_regions_index(d_state
.getSatContext(), 0),
471 d_regions_map(d_state
.getSatContext()),
472 d_split_score(d_state
.getSatContext()),
473 d_disequalities_index(d_state
.getSatContext(), 0),
474 d_reps(d_state
.getSatContext(), 0),
475 d_cardinality(d_state
.getSatContext(), 1),
476 d_hasCard(d_state
.getSatContext(), false),
477 d_maxNegCard(d_state
.getSatContext(), 0),
478 d_initialized(d_state
.getUserContext(), 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
, d_state
.getSatContext(), 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()
505 if (d_c_dec_strat
.get() != nullptr && !d_initialized
)
507 d_initialized
= true;
508 // Strategy is user-context-dependent, since it is in sync with
509 // user-context-dependent flag d_initialized.
510 d_thss
->getTheory()->getDecisionManager()->registerStrategy(
511 DecisionManager::STRAT_UF_CARD
, d_c_dec_strat
.get());
516 void SortModel::newEqClass( Node n
){
517 if (!d_state
.isInConflict())
519 if( d_regions_map
.find( n
)==d_regions_map
.end() ){
520 // Must generate totality axioms for every cardinality we have
521 // allocated thus far.
522 for( std::map
< int, Node
>::iterator it
= d_cardinality_literal
.begin();
523 it
!= d_cardinality_literal
.end(); ++it
){
524 if( applyTotality( it
->first
) ){
525 addTotalityAxiom(n
, it
->first
);
528 if( options::ufssTotality() ){
529 // Regions map will store whether we need to equate this term
530 // with a constant equivalence class.
531 if( std::find( d_totality_terms
[0].begin(), d_totality_terms
[0].end(), n
)==d_totality_terms
[0].end() ){
532 d_regions_map
[n
] = 0;
534 d_regions_map
[n
] = -1;
537 d_regions_map
[n
] = d_regions_index
;
538 Debug("uf-ss") << "CardinalityExtension: New Eq Class " << n
540 Debug("uf-ss-debug") << d_regions_index
<< " "
541 << (int)d_regions
.size() << std::endl
;
542 if( d_regions_index
<d_regions
.size() ){
543 d_regions
[ d_regions_index
]->debugPrint("uf-ss-debug",true);
544 d_regions
[ d_regions_index
]->setValid(true);
545 Assert(d_regions
[d_regions_index
]->getNumReps() == 0);
547 d_regions
.push_back(new Region(this, d_state
.getSatContext()));
549 d_regions
[ d_regions_index
]->addRep( n
);
550 d_regions_index
= d_regions_index
+ 1;
558 void SortModel::merge( Node a
, Node b
){
559 if (!d_state
.isInConflict())
561 if( options::ufssTotality() ){
562 if( d_regions_map
[b
]==-1 ){
563 d_regions_map
[a
] = -1;
565 d_regions_map
[b
] = -1;
567 Debug("uf-ss") << "CardinalityExtension: Merging " << a
<< " = " << b
568 << "..." << std::endl
;
570 Assert(d_regions_map
.find(a
) != d_regions_map
.end());
571 Assert(d_regions_map
.find(b
) != d_regions_map
.end());
572 int ai
= d_regions_map
[a
];
573 int bi
= d_regions_map
[b
];
574 Debug("uf-ss") << " regions: " << ai
<< " " << bi
<< std::endl
;
576 if( d_regions
[ai
]->getNumReps()==1 ){
577 int ri
= combineRegions( bi
, ai
);
578 d_regions
[ri
]->setEqual( a
, b
);
580 }else if( d_regions
[bi
]->getNumReps()==1 ){
581 int ri
= combineRegions( ai
, bi
);
582 d_regions
[ri
]->setEqual( a
, b
);
585 // Either move a to d_regions[bi], or b to d_regions[ai].
586 RegionNodeInfo
* a_region_info
= d_regions
[ai
]->getRegionInfo(a
);
587 RegionNodeInfo
* b_region_info
= d_regions
[bi
]->getRegionInfo(b
);
588 int aex
= ( a_region_info
->getNumInternalDisequalities() -
589 getNumDisequalitiesToRegion( a
, bi
) );
590 int bex
= ( b_region_info
->getNumInternalDisequalities() -
591 getNumDisequalitiesToRegion( b
, ai
) );
592 // Based on which would produce the fewest number of
593 // external disequalities.
596 d_regions
[bi
]->setEqual( a
, b
);
599 d_regions
[ai
]->setEqual( a
, b
);
605 d_regions
[ai
]->setEqual( a
, b
);
608 d_regions_map
[b
] = -1;
615 /** assert terms are disequal */
616 void SortModel::assertDisequal( Node a
, Node b
, Node reason
){
617 if (!d_state
.isInConflict())
619 if( options::ufssTotality() ){
622 //if they are not already disequal
623 eq::EqualityEngine
* ee
= d_thss
->getTheory()->getEqualityEngine();
624 a
= ee
->getRepresentative(a
);
625 b
= ee
->getRepresentative(b
);
626 int ai
= d_regions_map
[a
];
627 int bi
= d_regions_map
[b
];
628 if( !d_regions
[ai
]->isDisequal( a
, b
, ai
==bi
) ){
629 Debug("uf-ss") << "Assert disequal " << a
<< " != " << b
<< "..." << std::endl
;
630 //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL ||
631 // a!=reason[0][0] || b!=reason[0][1] ){
632 // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
634 Debug("uf-ss-disequal") << "Assert disequal " << a
<< " != " << b
<< "..." << std::endl
;
635 //add to list of disequalities
636 if( d_disequalities_index
<d_disequalities
.size() ){
637 d_disequalities
[d_disequalities_index
] = reason
;
639 d_disequalities
.push_back( reason
);
641 d_disequalities_index
= d_disequalities_index
+ 1;
642 //now, add disequalities to regions
643 Assert(d_regions_map
.find(a
) != d_regions_map
.end());
644 Assert(d_regions_map
.find(b
) != d_regions_map
.end());
645 Debug("uf-ss") << " regions: " << ai
<< " " << bi
<< std::endl
;
647 //internal disequality
648 d_regions
[ai
]->setDisequal( a
, b
, 1, true );
649 d_regions
[ai
]->setDisequal( b
, a
, 1, true );
650 checkRegion( ai
, false ); //do not need to check if it needs to combine (no new ext. disequalities)
652 //external disequality
653 d_regions
[ai
]->setDisequal( a
, b
, 0, true );
654 d_regions
[bi
]->setDisequal( b
, a
, 0, true );
663 bool SortModel::areDisequal( Node a
, Node b
) {
664 Assert(a
== d_thss
->getTheory()->getEqualityEngine()->getRepresentative(a
));
665 Assert(b
== d_thss
->getTheory()->getEqualityEngine()->getRepresentative(b
));
666 if( d_regions_map
.find( a
)!=d_regions_map
.end() &&
667 d_regions_map
.find( b
)!=d_regions_map
.end() ){
668 int ai
= d_regions_map
[a
];
669 int bi
= d_regions_map
[b
];
670 return d_regions
[ai
]->isDisequal(a
, b
, ai
==bi
? 1 : 0);
677 void SortModel::check(Theory::Effort level
)
679 Assert(options::ufssMode() == options::UfssMode::FULL
);
680 if (level
>= Theory::EFFORT_STANDARD
&& d_hasCard
&& !d_state
.isInConflict())
682 Debug("uf-ss") << "CardinalityExtension: Check " << level
<< " " << d_type
684 if( level
==Theory::EFFORT_FULL
){
685 Debug("fmf-full-check") << std::endl
;
686 Debug("fmf-full-check") << "Full check for SortModel " << d_type
<< ", status : " << std::endl
;
687 debugPrint("fmf-full-check");
688 Debug("fmf-full-check") << std::endl
;
690 if( d_reps
<=(unsigned)d_cardinality
){
691 Debug("uf-ss-debug") << "We have " << d_reps
<< " representatives for type " << d_type
<< ", <= " << d_cardinality
<< std::endl
;
692 if( level
==Theory::EFFORT_FULL
){
693 Debug("uf-ss-sat") << "We have " << d_reps
<< " representatives for type " << d_type
<< ", <= " << d_cardinality
<< std::endl
;
694 //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl;
695 //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl;
696 //Notice() << cardinality << " ";
700 //first check if we can generate a clique conflict
701 if( !options::ufssTotality() ){
702 //do a check within each region
703 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
704 if( d_regions
[i
]->valid() ){
705 std::vector
< Node
> clique
;
706 if( d_regions
[i
]->check( level
, d_cardinality
, clique
) ){
708 addCliqueLemma(clique
);
711 Trace("uf-ss-debug") << "No clique in Region #" << i
<< std::endl
;
716 if( !applyTotality( d_cardinality
) ){
717 //do splitting on demand
718 bool addedLemma
= false;
719 if (level
==Theory::EFFORT_FULL
)
721 Trace("uf-ss-debug") << "Add splits?" << std::endl
;
722 //see if we have any recommended splits from large regions
723 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
724 if( d_regions
[i
]->valid() && d_regions
[i
]->getNumReps()>d_cardinality
){
725 int sp
= addSplit(d_regions
[i
]);
728 #ifdef ONE_SPLIT_REGION
738 //If no added lemmas, force continuation via combination of regions.
739 if( level
==Theory::EFFORT_FULL
){
741 Trace("uf-ss-debug") << "No splits added. " << d_cardinality
743 Trace("uf-ss-si") << "Must combine region" << std::endl
;
744 bool recheck
= false;
745 SortInference
* si
= d_thss
->getSortInference();
748 //If sort inference is enabled, search for regions with same sort.
749 std::map
< int, int > sortsFound
;
750 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
751 if( d_regions
[i
]->valid() ){
752 Node op
= d_regions
[i
]->frontKey();
753 int sort_id
= si
->getSortId(op
);
754 if( sortsFound
.find( sort_id
)!=sortsFound
.end() ){
755 Debug("fmf-full-check") << "Combined regions " << i
<< " " << sortsFound
[sort_id
] << std::endl
;
756 combineRegions( sortsFound
[sort_id
], i
);
760 sortsFound
[sort_id
] = i
;
766 //naive strategy, force region combination involving the first valid region
767 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
768 if( d_regions
[i
]->valid() ){
769 int fcr
= forceCombineRegion( i
, false );
770 Debug("fmf-full-check") << "Combined regions " << i
<< " " << fcr
<< std::endl
;
771 Trace("uf-ss-debug") << "Combined regions " << i
<< " " << fcr
<< std::endl
;
778 Trace("uf-ss-debug") << "Must recheck." << std::endl
;
788 void SortModel::presolve() {
789 d_initialized
= false;
792 int SortModel::getNumDisequalitiesToRegion( Node n
, int ri
){
793 int ni
= d_regions_map
[n
];
795 DiseqList
* del
= d_regions
[ni
]->getRegionInfo(n
)->get(0);
796 for( DiseqList::iterator it
= del
->begin(); it
!= del
->end(); ++it
){
798 if( d_regions_map
[ (*it
).first
]==ri
){
806 void SortModel::getDisequalitiesToRegions(int ri
,
807 std::map
< int, int >& regions_diseq
)
809 Region
* region
= d_regions
[ri
];
810 for(Region::iterator it
= region
->begin(); it
!= region
->end(); ++it
){
811 if( it
->second
->valid() ){
812 DiseqList
* del
= it
->second
->get(0);
813 for( DiseqList::iterator it2
= del
->begin(); it2
!= del
->end(); ++it2
){
815 Assert(isValid(d_regions_map
[(*it2
).first
]));
816 //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
817 regions_diseq
[ d_regions_map
[ (*it2
).first
] ]++;
824 void SortModel::setSplitScore( Node n
, int s
){
825 if( d_split_score
.find( n
)!=d_split_score
.end() ){
826 int ss
= d_split_score
[ n
];
827 d_split_score
[ n
] = s
>ss
? s
: ss
;
829 d_split_score
[ n
] = s
;
831 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
832 setSplitScore( n
[i
], s
+1 );
836 void SortModel::assertCardinality(int c
, bool val
)
838 if (!d_state
.isInConflict())
840 Trace("uf-ss-assert")
841 << "Assert cardinality " << d_type
<< " " << c
<< " " << val
843 << d_thss
->getTheory()->getValuation().getAssertionLevel() << std::endl
;
845 Node cl
= getCardinalityLiteral( c
);
847 bool doCheckRegions
= !d_hasCard
;
848 bool prevHasCard
= d_hasCard
;
850 if( !prevHasCard
|| c
<d_cardinality
){
852 simpleCheckCardinality();
853 if (d_state
.isInConflict())
858 //should check all regions now
859 if( doCheckRegions
){
860 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
861 if( d_regions
[i
]->valid() ){
863 if (d_state
.isInConflict())
870 // we assert it positively, if its beyond the bound, abort
871 if (options::ufssAbortCardinality() != -1
872 && c
>= options::ufssAbortCardinality())
874 std::stringstream ss
;
875 ss
<< "Maximum cardinality (" << options::ufssAbortCardinality()
876 << ") for finite model finding exceeded." << std::endl
;
877 throw LogicException(ss
.str());
882 if( c
>d_maxNegCard
.get() ){
883 Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for " << d_type
<< " is now " << c
<< std::endl
;
884 d_maxNegCard
.set( c
);
885 simpleCheckCardinality();
891 void SortModel::checkRegion( int ri
, bool checkCombine
){
892 if( isValid(ri
) && d_hasCard
){
893 Assert(d_cardinality
> 0);
894 if( checkCombine
&& d_regions
[ri
]->getMustCombine( d_cardinality
) ){
895 ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
896 //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
898 // int inDeg = d_regions[i]->d_disequalities_size[1][ it-> first ];
899 // int outDeg = d_regions[i]->d_disequalities_size[0][ it-> first ];
900 // if( inDeg<outDeg ){
904 int riNew
= forceCombineRegion( ri
, true );
906 checkRegion( riNew
, checkCombine
);
909 //now check if region is in conflict
910 std::vector
< Node
> clique
;
911 if( d_regions
[ri
]->check( Theory::EFFORT_STANDARD
, d_cardinality
, clique
) ){
913 addCliqueLemma(clique
);
918 int SortModel::forceCombineRegion( int ri
, bool useDensity
){
920 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
921 if( ri
!=i
&& d_regions
[i
]->valid() ){
922 return combineRegions( ri
, i
);
927 //this region must merge with another
928 if( Debug
.isOn("uf-ss-check-region") ){
929 Debug("uf-ss-check-region") << "We must combine Region #" << ri
<< ". " << std::endl
;
930 d_regions
[ri
]->debugPrint("uf-ss-check-region");
932 //take region with maximum disequality density
935 std::map
< int, int > regions_diseq
;
936 getDisequalitiesToRegions( ri
, regions_diseq
);
937 for( std::map
< int, int >::iterator it
= regions_diseq
.begin(); it
!= regions_diseq
.end(); ++it
){
938 Debug("uf-ss-check-region") << it
->first
<< " : " << it
->second
<< std::endl
;
940 for( std::map
< int, int >::iterator it
= regions_diseq
.begin(); it
!= regions_diseq
.end(); ++it
){
941 Assert(it
->first
!= ri
);
942 Assert(isValid(it
->first
));
943 Assert(d_regions
[it
->first
]->getNumReps() > 0);
944 double tempScore
= double(it
->second
)/double(d_regions
[it
->first
]->getNumReps() );
945 if( tempScore
>maxScore
){
946 maxRegion
= it
->first
;
947 maxScore
= tempScore
;
951 if( Debug
.isOn("uf-ss-check-region") ){
952 Debug("uf-ss-check-region") << "Combine with region #" << maxRegion
<< ":" << std::endl
;
953 d_regions
[maxRegion
]->debugPrint("uf-ss-check-region");
955 return combineRegions( ri
, maxRegion
);
962 int SortModel::combineRegions( int ai
, int bi
){
963 #ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
964 if( d_regions
[ai
]->getNumReps()<d_regions
[bi
]->getNumReps() ){
965 return combineRegions( bi
, ai
);
968 Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi
<< " with Region #" << ai
<< std::endl
;
969 Assert(isValid(ai
) && isValid(bi
));
970 Region
* region_bi
= d_regions
[bi
];
971 for(Region::iterator it
= region_bi
->begin(); it
!= region_bi
->end(); ++it
){
972 Region::RegionNodeInfo
* rni
= it
->second
;
974 d_regions_map
[ it
->first
] = ai
;
977 //update regions disequal DO_THIS?
978 d_regions
[ai
]->combine( d_regions
[bi
] );
979 d_regions
[bi
]->setValid( false );
983 void SortModel::moveNode( Node n
, int ri
){
984 Debug("uf-ss-region") << "uf-ss: Move node " << n
<< " to Region #" << ri
<< std::endl
;
985 Assert(isValid(d_regions_map
[n
]));
987 //move node to region ri
988 d_regions
[ri
]->takeNode( d_regions
[ d_regions_map
[n
] ], n
);
989 d_regions_map
[n
] = ri
;
992 int SortModel::addSplit(Region
* r
)
995 if( r
->hasSplits() ){
996 //take the first split you find
997 for( Region::split_iterator it
= r
->begin_splits();
998 it
!= r
->end_splits(); ++it
){
1004 Assert(s
!= Node::null());
1007 //add lemma to output channel
1008 Assert(s
.getKind() == EQUAL
);
1009 Node ss
= Rewriter::rewrite( s
);
1010 if( ss
.getKind()!=EQUAL
){
1011 Node b_t
= NodeManager::currentNM()->mkConst( true );
1012 Node b_f
= NodeManager::currentNM()->mkConst( false );
1014 Trace("uf-ss-lemma") << "....Assert disequal directly : "
1015 << s
[0] << " " << s
[1] << std::endl
;
1016 assertDisequal( s
[0], s
[1], b_t
);
1019 Trace("uf-ss-warn") << "Split on unknown literal : " << ss
<< std::endl
;
1022 Message() << "Bad split " << s
<< std::endl
;
1023 AlwaysAssert(false);
1026 SortInference
* si
= d_thss
->getSortInference();
1029 for( int i
=0; i
<2; i
++ ){
1030 int sid
= si
->getSortId(ss
[i
]);
1031 Trace("uf-ss-split-si") << sid
<< " ";
1033 Trace("uf-ss-split-si") << std::endl
;
1035 //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
1036 //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
1037 //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
1038 //Notice() << "*** Split on " << s << std::endl;
1039 //split on the equality s
1040 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, ss
, ss
.negate() );
1041 // send lemma, with caching
1042 if (d_im
.lemma(lem
))
1044 Trace("uf-ss-lemma") << "*** Split on " << s
<< std::endl
;
1045 //tell the sat solver to explore the equals branch first
1046 d_im
.requirePhase(ss
, true);
1047 ++( d_thss
->d_statistics
.d_split_lemmas
);
1055 void SortModel::addCliqueLemma(std::vector
<Node
>& clique
)
1058 Assert(d_cardinality
> 0);
1059 while( clique
.size()>size_t(d_cardinality
+1) ){
1063 std::vector
<Node
> eqs
;
1064 for (unsigned i
= 0, size
= clique
.size(); i
< size
; i
++)
1066 for (unsigned j
= 0; j
< i
; j
++)
1068 eqs
.push_back(clique
[i
].eqNode(clique
[j
]));
1071 eqs
.push_back(d_cardinality_literal
[d_cardinality
].notNode());
1072 Node lem
= NodeManager::currentNM()->mkNode(OR
, eqs
);
1073 // send lemma, with caching
1074 if (d_im
.lemma(lem
))
1076 Trace("uf-ss-lemma") << "*** Add clique lemma " << lem
<< std::endl
;
1077 ++(d_thss
->d_statistics
.d_clique_lemmas
);
1081 void SortModel::addTotalityAxiom(Node n
, int cardinality
)
1083 if( std::find( d_totality_terms
[0].begin(), d_totality_terms
[0].end(), n
)==d_totality_terms
[0].end() ){
1084 if( std::find( d_totality_lems
[n
].begin(), d_totality_lems
[n
].end(), cardinality
) == d_totality_lems
[n
].end() ){
1085 NodeManager
* nm
= NodeManager::currentNM();
1086 d_totality_lems
[n
].push_back( cardinality
);
1087 Node cardLit
= d_cardinality_literal
[ cardinality
];
1089 SortInference
* si
= d_thss
->getSortInference();
1092 sort_id
= si
->getSortId(n
);
1094 Trace("uf-ss-totality") << "Add totality lemma for " << n
<< " " << cardinality
<< ", sort id is " << sort_id
<< std::endl
;
1095 int use_cardinality
= cardinality
;
1096 if( options::ufssTotalitySymBreak() ){
1097 if( d_sym_break_index
.find(n
)!=d_sym_break_index
.end() ){
1098 use_cardinality
= d_sym_break_index
[n
];
1099 }else if( (int)d_sym_break_terms
[n
.getType()][sort_id
].size()<cardinality
-1 ){
1100 use_cardinality
= d_sym_break_terms
[n
.getType()][sort_id
].size() + 1;
1101 d_sym_break_terms
[n
.getType()][sort_id
].push_back( n
);
1102 d_sym_break_index
[n
] = use_cardinality
;
1103 Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n
<< ", index = " << use_cardinality
<< std::endl
;
1104 if( d_sym_break_terms
[n
.getType()][sort_id
].size()>1 ){
1105 //enforce canonicity
1106 for( int i
=2; i
<use_cardinality
; i
++ ){
1107 //can only be assigned to domain constant d if someone has been assigned domain constant d-1
1108 Node eq
= n
.eqNode( getTotalityLemmaTerm( cardinality
, i
) );
1109 std::vector
< Node
> eqs
;
1110 for( unsigned j
=0; j
<(d_sym_break_terms
[n
.getType()][sort_id
].size()-1); j
++ ){
1111 eqs
.push_back( d_sym_break_terms
[n
.getType()][sort_id
][j
].eqNode( getTotalityLemmaTerm( cardinality
, i
-1 ) ) );
1113 Node ax
= eqs
.size()==1 ? eqs
[0] : NodeManager::currentNM()->mkNode( OR
, eqs
);
1114 Node lem
= NodeManager::currentNM()->mkNode( IMPLIES
, eq
, ax
);
1115 Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem
<< std::endl
;
1116 d_im
.lemma(lem
, LemmaProperty::NONE
, false);
1122 std::vector
< Node
> eqs
;
1123 for( int i
=0; i
<use_cardinality
; i
++ ){
1124 eqs
.push_back( n
.eqNode( getTotalityLemmaTerm( cardinality
, i
) ) );
1126 Node ax
= eqs
.size() == 1 ? eqs
[0] : nm
->mkNode(OR
, eqs
);
1127 Node lem
= NodeManager::currentNM()->mkNode( IMPLIES
, cardLit
, ax
);
1128 Trace("uf-ss-lemma") << "*** Add totality axiom " << lem
<< std::endl
;
1129 //send as lemma to the output channel
1130 d_im
.lemma(lem
, LemmaProperty::NONE
, false);
1131 ++( d_thss
->d_statistics
.d_totality_lemmas
);
1136 /** apply totality */
1137 bool SortModel::applyTotality( int cardinality
){
1138 return options::ufssTotality() || cardinality
<=options::ufssTotalityLimited();
1141 /** get totality lemma terms */
1142 Node
SortModel::getTotalityLemmaTerm( int cardinality
, int i
){
1143 return d_totality_terms
[0][i
];
1146 void SortModel::simpleCheckCardinality() {
1147 if( d_maxNegCard
.get()!=0 && d_hasCard
.get() && d_cardinality
.get()<d_maxNegCard
.get() ){
1148 Node lem
= NodeManager::currentNM()->mkNode( AND
, getCardinalityLiteral( d_cardinality
.get() ),
1149 getCardinalityLiteral( d_maxNegCard
.get() ).negate() );
1150 Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem
<< std::endl
;
1155 void SortModel::debugPrint( const char* c
){
1156 if( Debug
.isOn( c
) ){
1157 Debug( c
) << "Number of reps = " << d_reps
<< std::endl
;
1158 Debug( c
) << "Cardinality req = " << d_cardinality
<< std::endl
;
1159 unsigned debugReps
= 0;
1160 for( unsigned i
=0; i
<d_regions_index
; i
++ ){
1161 Region
* region
= d_regions
[i
];
1162 if( region
->valid() ){
1163 Debug( c
) << "Region #" << i
<< ": " << std::endl
;
1164 region
->debugPrint( c
, true );
1165 Debug( c
) << std::endl
;
1166 for( Region::iterator it
= region
->begin(); it
!= region
->end(); ++it
){
1167 if( it
->second
->valid() ){
1168 if( d_regions_map
[ it
->first
]!=(int)i
){
1169 Debug( c
) << "***Bad regions map : " << it
->first
1170 << " " << d_regions_map
[ it
->first
].get() << std::endl
;
1174 debugReps
+= region
->getNumReps();
1178 if( debugReps
!=d_reps
){
1179 Debug( c
) << "***Bad reps: " << d_reps
<< ", "
1180 << "actual = " << debugReps
<< std::endl
;
1185 bool SortModel::checkLastCall()
1187 TheoryModel
* m
= d_state
.getModel();
1188 if( Trace
.isOn("uf-ss-warn") ){
1189 std::vector
< Node
> eqcs
;
1190 eq::EqClassesIterator eqcs_i
=
1191 eq::EqClassesIterator(m
->getEqualityEngine());
1192 while( !eqcs_i
.isFinished() ){
1193 Node eqc
= (*eqcs_i
);
1194 if( eqc
.getType()==d_type
){
1195 if( std::find( eqcs
.begin(), eqcs
.end(), eqc
)==eqcs
.end() ){
1196 eqcs
.push_back( eqc
);
1197 //we must ensure that this equivalence class has been accounted for
1198 if( d_regions_map
.find( eqc
)==d_regions_map
.end() ){
1199 Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc
<< " unaccounted for." << std::endl
;
1200 Trace("uf-ss-warn") << " type : " << d_type
<< std::endl
;
1201 Trace("uf-ss-warn") << " kind : " << eqc
.getKind() << std::endl
;
1208 RepSet
* rs
= m
->getRepSetPtr();
1209 int nReps
= (int)rs
->getNumRepresentatives(d_type
);
1210 if( nReps
!=(d_maxNegCard
+1) ){
1211 Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type
<< "." << std::endl
;
1212 Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard
<< std::endl
;
1213 Trace("uf-ss-warn") << " # Reps : " << nReps
<< std::endl
;
1214 if( d_maxNegCard
>=nReps
){
1215 while( (int)d_fresh_aloc_reps
.size()<=d_maxNegCard
){
1216 std::stringstream ss
;
1217 ss
<< "r_" << d_type
<< "_";
1218 Node nn
= NodeManager::currentNM()->mkSkolem( ss
.str(), d_type
, "enumeration to meet negative card constraint" );
1219 d_fresh_aloc_reps
.push_back( nn
);
1221 if( d_maxNegCard
==0 ){
1222 rs
->d_type_reps
[d_type
].push_back(d_fresh_aloc_reps
[0]);
1225 std::vector
< Node
> force_cl
;
1226 for( int i
=0; i
<=d_maxNegCard
; i
++ ){
1227 for( int j
=(i
+1); j
<=d_maxNegCard
; j
++ ){
1228 force_cl
.push_back( d_fresh_aloc_reps
[i
].eqNode( d_fresh_aloc_reps
[j
] ).negate() );
1231 Node cl
= getCardinalityLiteral( d_maxNegCard
);
1232 Node lem
= NodeManager::currentNM()->mkNode( OR
, cl
, NodeManager::currentNM()->mkNode( AND
, force_cl
) );
1233 Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem
<< std::endl
;
1234 d_im
.lemma(lem
, LemmaProperty::NONE
, false);
1242 int SortModel::getNumRegions(){
1244 for( int i
=0; i
<(int)d_regions_index
; i
++ ){
1245 if( d_regions
[i
]->valid() ){
1252 Node
SortModel::getCardinalityLiteral(unsigned c
)
1255 std::map
<int, Node
>::iterator itcl
= d_cardinality_literal
.find(c
);
1256 if (itcl
!= d_cardinality_literal
.end())
1258 return itcl
->second
;
1260 // get the literal from the decision strategy
1261 Node lit
= d_c_dec_strat
->getLiteral(c
- 1);
1262 d_cardinality_literal
[c
] = lit
;
1264 // Since we are reasoning about cardinality c, we invoke a totality axiom
1265 if (!applyTotality(c
))
1267 // return if we are not using totality axioms
1271 NodeManager
* nm
= NodeManager::currentNM();
1273 if (c
== 1 && !options::ufssTotalitySymBreak())
1275 // get arbitrary ground term
1276 var
= d_cardinality_term
;
1280 std::stringstream ss
;
1282 var
= nm
->mkSkolem(ss
.str(), d_type
, "is a cardinality lemma term");
1284 if ((c
- 1) < d_totality_terms
[0].size())
1286 d_totality_terms
[0][c
- 1] = var
;
1290 d_totality_terms
[0].push_back(var
);
1292 // must be distinct from all other cardinality terms
1293 for (unsigned i
= 1, size
= d_totality_terms
[0].size(); i
< size
; i
++)
1295 Node lem
= var
.eqNode(d_totality_terms
[0][i
- 1]).notNode();
1296 Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem
1298 d_im
.lemma(lem
, LemmaProperty::NONE
, false);
1300 // must send totality axioms for each existing term
1301 for (NodeIntMap::iterator it
= d_regions_map
.begin();
1302 it
!= d_regions_map
.end();
1305 addTotalityAxiom((*it
).first
, c
);
1310 CardinalityExtension::CardinalityExtension(TheoryState
& state
,
1311 TheoryInferenceManager
& im
,
1317 d_min_pos_com_card(state
.getSatContext(), -1),
1318 d_cc_dec_strat(nullptr),
1319 d_initializedCombinedCardinality(state
.getUserContext(), false),
1320 d_card_assertions_eqv_lemma(state
.getUserContext()),
1321 d_min_pos_tn_master_card(state
.getSatContext(), -1),
1322 d_rel_eqc(state
.getSatContext())
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(new CombinedCardinalityDecisionStrategy(
1330 state
.getSatContext(), 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();
1357 void CardinalityExtension::ensureEqc(SortModel
* c
, Node a
)
1360 d_rel_eqc
[a
] = true;
1361 Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a
<< " : "
1362 << a
.getType() << std::endl
;
1364 Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1369 void CardinalityExtension::ensureEqcRec(Node n
)
1372 SortModel
* c
= getSortModel( n
);
1376 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1377 ensureEqcRec( n
[i
] );
1383 bool CardinalityExtension::hasEqc(Node a
)
1385 NodeBoolMap::iterator it
= d_rel_eqc
.find( a
);
1386 return it
!=d_rel_eqc
.end() && (*it
).second
;
1390 void CardinalityExtension::newEqClass(Node a
)
1392 SortModel
* c
= getSortModel( a
);
1397 Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a
<< " : "
1398 << a
.getType() << std::endl
;
1400 Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1407 void CardinalityExtension::merge(Node a
, Node b
)
1409 //TODO: ensure they are relevant
1410 SortModel
* c
= getSortModel( a
);
1415 Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a
<< " " << b
1416 << " : " << a
.getType() << std::endl
;
1418 Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl
;
1420 //c->assignEqClass( b, a );
1421 d_rel_eqc
[b
] = true;
1424 Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a
<< " " << b
1425 << " : " << a
.getType() << std::endl
;
1427 Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl
;
1432 /** assert terms are disequal */
1433 void CardinalityExtension::assertDisequal(Node a
, Node b
, Node reason
)
1435 SortModel
* c
= getSortModel( a
);
1441 Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a
1442 << " " << b
<< " : " << a
.getType() << std::endl
;
1443 c
->assertDisequal( a
, b
, reason
);
1444 Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal."
1449 /** assert a node */
1450 void CardinalityExtension::assertNode(Node n
, bool isDecision
)
1452 Trace("uf-ss") << "Assert " << n
<< " " << isDecision
<< std::endl
;
1456 bool polarity
= n
.getKind() != kind::NOT
;
1457 TNode lit
= polarity
? n
: n
[0];
1458 if (options::ufssMode() == options::UfssMode::FULL
)
1460 if( lit
.getKind()==CARDINALITY_CONSTRAINT
){
1461 TypeNode tn
= lit
[0].getType();
1462 Assert(tn
.isSort());
1463 Assert(d_rep_model
[tn
]);
1464 int nCard
= lit
[1].getConst
<Rational
>().getNumerator().getSignedInt();
1465 Node ct
= d_rep_model
[tn
]->getCardinalityTerm();
1466 Trace("uf-ss-debug") << "...check cardinality terms : " << lit
[0] << " " << ct
<< std::endl
;
1468 if( options::ufssFairnessMonotone() ){
1469 Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl
;
1470 if( tn
!=d_tn_mono_master
){
1471 std::map
< TypeNode
, bool >::iterator it
= d_tn_mono_slave
.find( tn
);
1472 if( it
==d_tn_mono_slave
.end() ){
1474 SortInference
* si
= getSortInference();
1477 isMonotonic
= si
->isMonotonic(tn
);
1479 //if ground, everything is monotonic
1483 if( d_tn_mono_master
.isNull() ){
1484 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn
<< std::endl
;
1485 d_tn_mono_master
= tn
;
1487 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn
<< std::endl
;
1488 d_tn_mono_slave
[tn
] = true;
1491 Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn
<< std::endl
;
1492 d_tn_mono_slave
[tn
] = false;
1496 //set the minimum positive cardinality for master if necessary
1497 if( polarity
&& tn
==d_tn_mono_master
){
1498 Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl
;
1499 if( d_min_pos_tn_master_card
.get()==-1 || nCard
<d_min_pos_tn_master_card
.get() ){
1500 d_min_pos_tn_master_card
.set( nCard
);
1504 Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl
;
1505 d_rep_model
[tn
]->assertCardinality(nCard
, polarity
);
1506 //check if combined cardinality is violated
1507 checkCombinedCardinality();
1509 //otherwise, make equal via lemma
1510 if( d_card_assertions_eqv_lemma
.find( lit
)==d_card_assertions_eqv_lemma
.end() ){
1511 Node eqv_lit
= NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT
, ct
, lit
[1] );
1512 eqv_lit
= lit
.eqNode( eqv_lit
);
1513 Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit
<< std::endl
;
1514 d_im
.lemma(eqv_lit
, LemmaProperty::NONE
, false);
1515 d_card_assertions_eqv_lemma
[lit
] = true;
1518 }else if( lit
.getKind()==COMBINED_CARDINALITY_CONSTRAINT
){
1520 //safe to assume int here
1521 int nCard
= lit
[0].getConst
<Rational
>().getNumerator().getSignedInt();
1522 if( d_min_pos_com_card
.get()==-1 || nCard
<d_min_pos_com_card
.get() ){
1523 d_min_pos_com_card
.set( nCard
);
1524 checkCombinedCardinality();
1528 if( Trace
.isOn("uf-ss-warn") ){
1529 ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
1530 //// a theory propagation is not a decision.
1532 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1533 if( !it
->second
->hasCardinalityAsserted() ){
1534 Trace("uf-ss-warn") << "WARNING: Assert " << n
<< " as a decision before cardinality for " << it
->first
<< "." << std::endl
;
1535 //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
1545 if( lit
.getKind()==CARDINALITY_CONSTRAINT
|| lit
.getKind()==COMBINED_CARDINALITY_CONSTRAINT
){
1546 // cardinality constraint from user input, set incomplete
1547 Trace("uf-ss") << "Literal " << lit
<< " not handled when uf ss mode is not FULL, set incomplete." << std::endl
;
1548 d_im
.setIncomplete();
1551 Trace("uf-ss") << "Assert: done " << n
<< " " << isDecision
<< std::endl
;
1554 bool CardinalityExtension::areDisequal(Node a
, Node b
)
1559 eq::EqualityEngine
* ee
= d_th
->getEqualityEngine();
1560 a
= ee
->getRepresentative(a
);
1561 b
= ee
->getRepresentative(b
);
1562 if (ee
->areDisequal(a
, b
, false))
1566 SortModel
* c
= getSortModel(a
);
1569 return c
->areDisequal(a
, b
);
1575 void CardinalityExtension::check(Theory::Effort level
)
1577 if (level
== Theory::EFFORT_LAST_CALL
)
1579 // if last call, call last call check for each sort
1580 for (std::pair
<const TypeNode
, SortModel
*>& r
: d_rep_model
)
1582 if (!r
.second
->checkLastCall())
1589 if (!d_state
.isInConflict())
1591 if (options::ufssMode() == options::UfssMode::FULL
)
1593 Trace("uf-ss-solver")
1594 << "CardinalityExtension: check " << level
<< std::endl
;
1595 if (level
== Theory::EFFORT_FULL
)
1597 if (Debug
.isOn("uf-ss-debug"))
1599 debugPrint("uf-ss-debug");
1601 if (Trace
.isOn("uf-ss-state"))
1603 Trace("uf-ss-state")
1604 << "CardinalityExtension::check " << level
<< std::endl
;
1605 for (std::pair
<const TypeNode
, SortModel
*>& rm
: d_rep_model
)
1607 Trace("uf-ss-state") << " " << rm
.first
<< " has cardinality "
1608 << rm
.second
->getCardinality() << std::endl
;
1612 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1613 it
->second
->check(level
);
1614 if (d_state
.isInConflict())
1620 else if (options::ufssMode() == options::UfssMode::NO_MINIMAL
)
1622 if( level
==Theory::EFFORT_FULL
){
1623 // split on an equality between two equivalence classes (at most one per type)
1624 std::map
< TypeNode
, std::vector
< Node
> > eqc_list
;
1625 std::map
< TypeNode
, bool > type_proc
;
1626 eq::EqClassesIterator
eqcs_i(d_th
->getEqualityEngine());
1627 while( !eqcs_i
.isFinished() ){
1629 TypeNode tn
= a
.getType();
1631 if( type_proc
.find( tn
)==type_proc
.end() ){
1632 std::map
< TypeNode
, std::vector
< Node
> >::iterator itel
= eqc_list
.find( tn
);
1633 if( itel
!=eqc_list
.end() ){
1634 for( unsigned j
=0; j
<itel
->second
.size(); j
++ ){
1635 Node b
= itel
->second
[j
];
1636 if( !d_th
->getEqualityEngine()->areDisequal( a
, b
, false ) ){
1637 Node eq
= Rewriter::rewrite( a
.eqNode( b
) );
1638 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, eq
.negate() );
1639 Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem
<< std::endl
;
1640 d_im
.lemma(lem
, LemmaProperty::NONE
, false);
1641 d_im
.requirePhase(eq
, true);
1642 type_proc
[tn
] = true;
1647 eqc_list
[tn
].push_back( a
);
1656 // unhandled uf ss mode
1659 Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
1664 void CardinalityExtension::presolve()
1666 d_initializedCombinedCardinality
= false;
1667 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1668 it
->second
->presolve();
1669 it
->second
->initialize();
1673 CardinalityExtension::CombinedCardinalityDecisionStrategy::
1674 CombinedCardinalityDecisionStrategy(context::Context
* satContext
,
1675 Valuation valuation
)
1676 : DecisionStrategyFmf(satContext
, valuation
)
1679 Node
CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
1682 NodeManager
* nm
= NodeManager::currentNM();
1683 return nm
->mkNode(COMBINED_CARDINALITY_CONSTRAINT
, nm
->mkConst(Rational(i
)));
1687 CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
1689 return std::string("uf_combined_card");
1692 void CardinalityExtension::preRegisterTerm(TNode n
)
1694 if (options::ufssMode() == options::UfssMode::FULL
)
1696 //initialize combined cardinality
1697 initializeCombinedCardinality();
1699 Trace("uf-ss-register") << "Preregister " << n
<< "." << std::endl
;
1700 //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
1701 TypeNode tn
= n
.getType();
1702 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1703 if( it
==d_rep_model
.end() ){
1704 SortModel
* rm
= NULL
;
1706 Trace("uf-ss-register") << "Create sort model " << tn
<< "." << std::endl
;
1707 rm
= new SortModel(n
, d_state
, d_im
, this);
1711 d_rep_model
[tn
] = rm
;
1712 //d_rep_model_init[tn] = true;
1715 //ensure sort model is initialized
1716 it
->second
->initialize();
1721 SortModel
* CardinalityExtension::getSortModel(Node n
)
1723 TypeNode tn
= n
.getType();
1724 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1725 //pre-register the type if not done already
1726 if( it
==d_rep_model
.end() ){
1727 preRegisterTerm( n
);
1728 it
= d_rep_model
.find( tn
);
1730 if( it
!=d_rep_model
.end() ){
1737 /** get cardinality for sort */
1738 int CardinalityExtension::getCardinality(Node n
)
1740 SortModel
* c
= getSortModel( n
);
1742 return c
->getCardinality();
1748 int CardinalityExtension::getCardinality(TypeNode tn
)
1750 std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.find( tn
);
1751 if( it
!=d_rep_model
.end() && it
->second
){
1752 return it
->second
->getCardinality();
1758 void CardinalityExtension::debugPrint(const char* c
)
1760 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1761 Debug( c
) << "Conflict find structure for " << it
->first
<< ": " << std::endl
;
1762 it
->second
->debugPrint( c
);
1763 Debug( c
) << std::endl
;
1768 void CardinalityExtension::initializeCombinedCardinality()
1770 if (d_cc_dec_strat
.get() != nullptr
1771 && !d_initializedCombinedCardinality
.get())
1773 d_initializedCombinedCardinality
= true;
1774 d_th
->getDecisionManager()->registerStrategy(
1775 DecisionManager::STRAT_UF_COMBINED_CARD
, d_cc_dec_strat
.get());
1780 void CardinalityExtension::checkCombinedCardinality()
1782 Assert(options::ufssMode() == options::UfssMode::FULL
);
1783 if( options::ufssFairness() ){
1784 Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl
;
1785 int totalCombinedCard
= 0;
1786 int maxMonoSlave
= 0;
1787 TypeNode maxSlaveType
;
1788 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin(); it
!= d_rep_model
.end(); ++it
){
1789 int max_neg
= it
->second
->getMaximumNegativeCardinality();
1790 if( !options::ufssFairnessMonotone() ){
1791 totalCombinedCard
+= max_neg
;
1793 std::map
< TypeNode
, bool >::iterator its
= d_tn_mono_slave
.find( it
->first
);
1794 if( its
==d_tn_mono_slave
.end() || !its
->second
){
1795 totalCombinedCard
+= max_neg
;
1797 if( max_neg
>maxMonoSlave
){
1798 maxMonoSlave
= max_neg
;
1799 maxSlaveType
= it
->first
;
1804 Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard
<< std::endl
;
1805 if( options::ufssFairnessMonotone() ){
1806 Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave
<< std::endl
;
1807 if( d_min_pos_tn_master_card
.get()!=-1 && maxMonoSlave
>d_min_pos_tn_master_card
.get() ){
1808 int mc
= d_min_pos_tn_master_card
.get();
1809 std::vector
< Node
> conf
;
1810 conf
.push_back( d_rep_model
[d_tn_mono_master
]->getCardinalityLiteral( mc
) );
1811 conf
.push_back( d_rep_model
[maxSlaveType
]->getCardinalityLiteral( maxMonoSlave
).negate() );
1812 Node cf
= NodeManager::currentNM()->mkNode( AND
, conf
);
1813 Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict"
1814 << " : " << cf
<< std::endl
;
1815 Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
1816 << " : " << cf
<< std::endl
;
1821 int cc
= d_min_pos_com_card
.get();
1822 if( cc
!=-1 && totalCombinedCard
> cc
){
1824 Node com_lit
= d_cc_dec_strat
->getLiteral(cc
);
1825 std::vector
< Node
> conf
;
1826 conf
.push_back( com_lit
);
1828 for( std::map
< TypeNode
, SortModel
* >::iterator it
= d_rep_model
.begin();
1829 it
!= d_rep_model
.end(); ++it
){
1831 if( options::ufssFairnessMonotone() ){
1832 std::map
< TypeNode
, bool >::iterator its
=
1833 d_tn_mono_slave
.find( it
->first
);
1834 if( its
!=d_tn_mono_slave
.end() && its
->second
){
1839 int c
= it
->second
->getMaximumNegativeCardinality();
1841 conf
.push_back( it
->second
->getCardinalityLiteral( c
).negate() );
1844 if( totalAdded
>cc
){
1849 Node cf
= NodeManager::currentNM()->mkNode( AND
, conf
);
1850 Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
1852 Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
1859 CardinalityExtension::Statistics::Statistics()
1860 : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
1861 d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
1862 d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
1863 d_disamb_term_lemmas("CardinalityExtension::Disambiguate_Term_Lemmas", 0),
1864 d_totality_lemmas("CardinalityExtension::Totality_Lemmas", 0),
1865 d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
1867 smtStatisticsRegistry()->registerStat(&d_clique_conflicts
);
1868 smtStatisticsRegistry()->registerStat(&d_clique_lemmas
);
1869 smtStatisticsRegistry()->registerStat(&d_split_lemmas
);
1870 smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas
);
1871 smtStatisticsRegistry()->registerStat(&d_totality_lemmas
);
1872 smtStatisticsRegistry()->registerStat(&d_max_model_size
);
1875 CardinalityExtension::Statistics::~Statistics()
1877 smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts
);
1878 smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas
);
1879 smtStatisticsRegistry()->unregisterStat(&d_split_lemmas
);
1880 smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas
);
1881 smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas
);
1882 smtStatisticsRegistry()->unregisterStat(&d_max_model_size
);
1885 }/* CVC4::theory namespace::uf */
1886 }/* CVC4::theory namespace */
1887 }/* CVC4 namespace */