}
}
-void SortModel::assertCardinality(int c, bool val)
+void SortModel::assertCardinality(uint32_t c, bool val)
{
if (!d_state.isInConflict())
{
bool doCheckRegions = !d_hasCard;
bool prevHasCard = d_hasCard;
d_hasCard = true;
- if( !prevHasCard || c<d_cardinality ){
+ if (!prevHasCard || c < d_cardinality)
+ {
d_cardinality = c;
simpleCheckCardinality();
if (d_state.isInConflict())
}
}
//should check all regions now
- if( doCheckRegions ){
- for( int i=0; i<(int)d_regions_index; i++ ){
+ if (doCheckRegions)
+ {
+ for (size_t i = 0; i < d_regions_index; i++)
+ {
if( d_regions[i]->valid() ){
checkRegion( i );
if (d_state.isInConflict())
}
}
// we assert it positively, if its beyond the bound, abort
- if (options::ufssAbortCardinality() != -1
- && c >= options::ufssAbortCardinality())
+ if (options::ufssAbortCardinality() >= 0
+ && c >= static_cast<uint32_t>(options::ufssAbortCardinality()))
{
std::stringstream ss;
ss << "Maximum cardinality (" << options::ufssAbortCardinality()
if( isValid(ri) && d_hasCard ){
Assert(d_cardinality > 0);
if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
- ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
- //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
- // if( it->second ){
- // int inDeg = d_regions[i]->d_disequalities_size[1][ it-> first ];
- // int outDeg = d_regions[i]->d_disequalities_size[0][ it-> first ];
- // if( inDeg<outDeg ){
- // }
- // }
- //}
int riNew = forceCombineRegion( ri, true );
if( riNew>=0 ){
checkRegion( riNew, checkCombine );
{
Assert(d_hasCard);
Assert(d_cardinality > 0);
- while( clique.size()>size_t(d_cardinality+1) ){
+ while (clique.size() > d_cardinality + 1)
+ {
clique.pop_back();
}
// add as lemma
}
}
RepSet* rs = m->getRepSetPtr();
- int nReps = (int)rs->getNumRepresentatives(d_type);
- if( nReps!=(d_maxNegCard+1) ){
+ size_t nReps = rs->getNumRepresentatives(d_type);
+ if (nReps != d_maxNegCard + 1)
+ {
Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard << std::endl;
Trace("uf-ss-warn") << " # Reps : " << nReps << std::endl;
- if( d_maxNegCard>=nReps ){
- while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){
+ if (d_maxNegCard >= nReps)
+ {
+ while (d_fresh_aloc_reps.size() <= d_maxNegCard)
+ {
std::stringstream ss;
ss << "r_" << d_type << "_";
Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
d_fresh_aloc_reps.push_back( nn );
}
- if( d_maxNegCard==0 ){
+ if (d_maxNegCard == 0)
+ {
rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]);
- }else{
+ }
+ else
+ {
//must add lemma
std::vector< Node > force_cl;
- for( int i=0; i<=d_maxNegCard; i++ ){
- for( int j=(i+1); j<=d_maxNegCard; j++ ){
+ for (size_t i = 0; i <= d_maxNegCard; i++)
+ {
+ for (size_t j = (i + 1); j <= d_maxNegCard; j++)
+ {
force_cl.push_back( d_fresh_aloc_reps[i].eqNode( d_fresh_aloc_reps[j] ).negate() );
}
}
return count;
}
-Node SortModel::getCardinalityLiteral(size_t c)
+Node SortModel::getCardinalityLiteral(uint32_t c)
{
Assert(c > 0);
- std::map<size_t, Node>::iterator itcl = d_cardinality_literal.find(c);
+ std::map<uint32_t, Node>::iterator itcl = d_cardinality_literal.find(c);
if (itcl != d_cardinality_literal.end())
{
return itcl->second;
d_im(im),
d_th(th),
d_rep_model(),
- d_min_pos_com_card(state.getSatContext(), -1),
+ d_min_pos_com_card(state.getSatContext(), 0),
+ d_min_pos_com_card_set(state.getSatContext(), false),
d_cc_dec_strat(nullptr),
d_initializedCombinedCardinality(state.getUserContext(), false),
d_card_assertions_eqv_lemma(state.getUserContext()),
- d_min_pos_tn_master_card(state.getSatContext(), -1),
+ d_min_pos_tn_master_card(state.getSatContext(), 0),
+ d_min_pos_tn_master_card_set(state.getSatContext(), false),
d_rel_eqc(state.getSatContext())
{
if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness())
TypeNode tn = lit[0].getType();
Assert(tn.isSort());
Assert(d_rep_model[tn]);
- int nCard = lit[1].getConst<Rational>().getNumerator().getSignedInt();
+ uint32_t nCard =
+ lit[1].getConst<Rational>().getNumerator().getUnsignedInt();
Node ct = d_rep_model[tn]->getCardinalityTerm();
Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
if( lit[0]==ct ){
//set the minimum positive cardinality for master if necessary
if( polarity && tn==d_tn_mono_master ){
Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl;
- if( d_min_pos_tn_master_card.get()==-1 || nCard<d_min_pos_tn_master_card.get() ){
+ if (!d_min_pos_tn_master_card_set.get()
+ || nCard < d_min_pos_tn_master_card.get())
+ {
+ d_min_pos_tn_master_card_set.set(true);
d_min_pos_tn_master_card.set( nCard );
}
}
}else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
if( polarity ){
//safe to assume int here
- int nCard = lit[0].getConst<Rational>().getNumerator().getSignedInt();
- if( d_min_pos_com_card.get()==-1 || nCard<d_min_pos_com_card.get() ){
+ uint32_t nCard =
+ lit[0].getConst<Rational>().getNumerator().getUnsignedInt();
+ if (!d_min_pos_com_card_set.get() || nCard < d_min_pos_com_card.get())
+ {
+ d_min_pos_com_card_set.set(true);
d_min_pos_com_card.set( nCard );
checkCombinedCardinality();
}
Assert(options::ufssMode() == options::UfssMode::FULL);
if( options::ufssFairness() ){
Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
- int totalCombinedCard = 0;
- int maxMonoSlave = 0;
+ uint32_t totalCombinedCard = 0;
+ uint32_t maxMonoSlave = 0;
TypeNode maxSlaveType;
for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
- int max_neg = it->second->getMaximumNegativeCardinality();
+ uint32_t max_neg = it->second->getMaximumNegativeCardinality();
if( !options::ufssFairnessMonotone() ){
totalCombinedCard += max_neg;
}else{
Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl;
if( options::ufssFairnessMonotone() ){
Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave << std::endl;
- if( d_min_pos_tn_master_card.get()!=-1 && maxMonoSlave>d_min_pos_tn_master_card.get() ){
- int mc = d_min_pos_tn_master_card.get();
+ if (!d_min_pos_tn_master_card_set.get()
+ && maxMonoSlave > d_min_pos_tn_master_card.get())
+ {
+ uint32_t mc = d_min_pos_tn_master_card.get();
std::vector< Node > conf;
conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) );
conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() );
return;
}
}
- int cc = d_min_pos_com_card.get();
- if( cc !=-1 && totalCombinedCard > cc ){
+ uint32_t cc = d_min_pos_com_card.get();
+ if (d_min_pos_com_card_set.get() && totalCombinedCard > cc)
+ {
//conflict
Node com_lit = d_cc_dec_strat->getLiteral(cc);
std::vector< Node > conf;
conf.push_back( com_lit );
- int totalAdded = 0;
+ uint32_t totalAdded = 0;
for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin();
it != d_rep_model.end(); ++it ){
bool doAdd = true;
}
}
if( doAdd ){
- int c = it->second->getMaximumNegativeCardinality();
+ uint32_t c = it->second->getMaximumNegativeCardinality();
if( c>0 ){
conf.push_back( it->second->getCardinalityLiteral( c ).negate() );
totalAdded += c;
/** conflict find pointer */
SortModel* d_cf;
- context::CDO< unsigned > d_testCliqueSize;
+ context::CDO<size_t> d_testCliqueSize;
context::CDO< unsigned > d_splitsSize;
//a postulated clique
NodeBoolMap d_testClique;
//disequalities needed for this clique to happen
NodeBoolMap d_splits;
//number of valid representatives in this region
- context::CDO< unsigned > d_reps_size;
+ context::CDO<size_t> d_reps_size;
//total disequality size (external)
context::CDO< unsigned > d_total_diseq_external;
//total disequality size (internal)
//set n1 != n2 to value 'valid', type is whether it is internal/external
void setDisequal( Node n1, Node n2, int type, bool valid );
//get num reps
- int getNumReps() { return d_reps_size; }
+ size_t getNumReps() const { return d_reps_size; }
//get test clique size
- int getTestCliqueSize() { return d_testCliqueSize; }
+ size_t getTestCliqueSize() const { return d_testCliqueSize; }
// has representative
bool hasRep( Node n ) {
return d_nodes.find(n) != d_nodes.end() && d_nodes[n]->valid();
/** add clique lemma */
void addCliqueLemma(std::vector<Node>& clique);
/** cardinality */
- context::CDO<size_t> d_cardinality;
+ context::CDO<uint32_t> d_cardinality;
/** cardinality lemma term */
Node d_cardinality_term;
/** cardinality literals */
- std::map<size_t, Node> d_cardinality_literal;
+ std::map<uint32_t, Node> d_cardinality_literal;
/** whether a positive cardinality constraint has been asserted */
context::CDO< bool > d_hasCard;
/** clique lemmas that have been asserted */
std::map< int, std::vector< std::vector< Node > > > d_cliques;
/** maximum negatively asserted cardinality */
- context::CDO<size_t> d_maxNegCard;
+ context::CDO<uint32_t> d_maxNegCard;
/** list of fresh representatives allocated */
std::vector< Node > d_fresh_aloc_reps;
/** whether we are initialized */
/** presolve */
void presolve();
/** assert cardinality */
- void assertCardinality(int c, bool val);
+ void assertCardinality(uint32_t c, bool val);
/** get cardinality */
- int getCardinality() { return d_cardinality; }
+ uint32_t getCardinality() const { return d_cardinality; }
/** has cardinality */
- bool hasCardinalityAsserted() { return d_hasCard; }
+ bool hasCardinalityAsserted() const { return d_hasCard; }
/** get cardinality term */
- Node getCardinalityTerm() { return d_cardinality_term; }
+ Node getCardinalityTerm() const { return d_cardinality_term; }
/** get cardinality literal */
- Node getCardinalityLiteral(size_t c);
+ Node getCardinalityLiteral(uint32_t c);
/** get maximum negative cardinality */
- int getMaximumNegativeCardinality() { return d_maxNegCard.get(); }
+ uint32_t getMaximumNegativeCardinality() const
+ {
+ return d_maxNegCard.get();
+ }
//print debug
void debugPrint( const char* c );
/**
std::map<TypeNode, SortModel*> d_rep_model;
/** minimum positive combined cardinality */
- context::CDO<int> d_min_pos_com_card;
+ context::CDO<uint32_t> d_min_pos_com_card;
+ /** Whether the field above has been set */
+ context::CDO<bool> d_min_pos_com_card_set;
/**
* Decision strategy for combined cardinality constraints. This asserts
* the minimal combined cardinality constraint positively in the SAT
/** the master monotone type (if ufssFairnessMonotone enabled) */
TypeNode d_tn_mono_master;
std::map<TypeNode, bool> d_tn_mono_slave;
- context::CDO<int> d_min_pos_tn_master_card;
+ /** The minimum positive asserted master cardinality */
+ context::CDO<uint32_t> d_min_pos_tn_master_card;
+ /** Whether the field above has been set */
+ context::CDO<bool> d_min_pos_tn_master_card_set;
/** relevant eqc */
NodeBoolMap d_rel_eqc;
}; /* class CardinalityExtension */
projects / cvc5.git / commitdiff