From a0ccf529025b86d368dac6b8c4f6b78a97857f4b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Oct 2020 13:33:34 -0500 Subject: [PATCH] Fix miscellaneous warnings (#5256) Mostly in cardinality extension, which was cleaned in the previous PR. --- src/smt/listeners.cpp | 8 +- src/theory/builtin/proof_checker.cpp | 1 - src/theory/bv/bv_subtheory_algebraic.cpp | 1 - src/theory/uf/cardinality_extension.cpp | 97 ++++++++++++++---------- src/theory/uf/cardinality_extension.h | 38 ++++++---- 5 files changed, 84 insertions(+), 61 deletions(-) diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index bc227beef..7d34f3373 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -69,10 +69,12 @@ void SmtNodeManagerListener::nmNotifyNewDatatypes( { if ((flags & NodeManager::DATATYPE_FLAG_PLACEHOLDER) == 0) { - std::vector types; - for (const TypeNode& dt : dtts) + if (Configuration::isAssertionBuild()) { - Assert(dt.isDatatype()); + for (CVC4_UNUSED const TypeNode& dt : dtts) + { + Assert(dt.isDatatype()); + } } DeclareDatatypeNodeCommand c(dtts); d_dm.addToModelCommandAndDump(c); diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index e59f48fff..73d39f417 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -253,7 +253,6 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } else if (id == PfRule::SCOPE) { - NodeManager * nm = NodeManager::currentNM(); Assert(children.size() == 1); if (args.empty()) { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index b0688c4f9..50a509517 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -275,7 +275,6 @@ bool AlgebraicSolver::check(Theory::Effort e) uint64_t original_bb_cost = 0; - NodeManager* nm = NodeManager::currentNM(); NodeSet seen_assertions; // Processing assertions from scratch for (AssertionQueue::const_iterator it = assertionsBegin(); it != assertionsEnd(); ++it) { diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 688a8b645..f24a058a3 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -838,7 +838,7 @@ void SortModel::setSplitScore( Node n, int s ){ } } -void SortModel::assertCardinality(int c, bool val) +void SortModel::assertCardinality(uint32_t c, bool val) { if (!d_state.isInConflict()) { @@ -852,7 +852,8 @@ void SortModel::assertCardinality(int c, bool val) bool doCheckRegions = !d_hasCard; bool prevHasCard = d_hasCard; d_hasCard = true; - if( !prevHasCard || cvalid() ){ checkRegion( i ); if (d_state.isInConflict()) @@ -873,8 +876,8 @@ void SortModel::assertCardinality(int c, bool val) } } // we assert it positively, if its beyond the bound, abort - if (options::ufssAbortCardinality() != -1 - && c >= options::ufssAbortCardinality()) + if (options::ufssAbortCardinality() >= 0 + && c >= static_cast(options::ufssAbortCardinality())) { std::stringstream ss; ss << "Maximum cardinality (" << options::ufssAbortCardinality() @@ -897,15 +900,6 @@ void SortModel::checkRegion( int ri, bool checkCombine ){ 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=0 ){ checkRegion( riNew, checkCombine ); @@ -1056,7 +1050,8 @@ void SortModel::addCliqueLemma(std::vector& clique) { 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 @@ -1141,25 +1136,33 @@ bool SortModel::checkLastCall() } } 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() ); } } @@ -1184,10 +1187,10 @@ int SortModel::getNumRegions(){ return count; } -Node SortModel::getCardinalityLiteral(size_t c) +Node SortModel::getCardinalityLiteral(uint32_t c) { Assert(c > 0); - std::map::iterator itcl = d_cardinality_literal.find(c); + std::map::iterator itcl = d_cardinality_literal.find(c); if (itcl != d_cardinality_literal.end()) { return itcl->second; @@ -1207,11 +1210,13 @@ CardinalityExtension::CardinalityExtension(TheoryState& state, 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()) @@ -1330,7 +1335,8 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) TypeNode tn = lit[0].getType(); Assert(tn.isSort()); Assert(d_rep_model[tn]); - int nCard = lit[1].getConst().getNumerator().getSignedInt(); + uint32_t nCard = + lit[1].getConst().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 ){ @@ -1365,7 +1371,10 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) //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().getNumerator().getSignedInt(); - if( d_min_pos_com_card.get()==-1 || nCard().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(); } @@ -1651,11 +1663,11 @@ void CardinalityExtension::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{ @@ -1673,8 +1685,10 @@ void CardinalityExtension::checkCombinedCardinality() 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() ); @@ -1687,13 +1701,14 @@ void CardinalityExtension::checkCombinedCardinality() 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; @@ -1705,7 +1720,7 @@ void CardinalityExtension::checkCombinedCardinality() } } 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; diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index cbef690b1..6b5349ce7 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -133,14 +133,14 @@ class CardinalityExtension /** conflict find pointer */ SortModel* d_cf; - context::CDO< unsigned > d_testCliqueSize; + context::CDO 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 d_reps_size; //total disequality size (external) context::CDO< unsigned > d_total_diseq_external; //total disequality size (internal) @@ -188,9 +188,9 @@ class CardinalityExtension //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(); @@ -266,17 +266,17 @@ class CardinalityExtension /** add clique lemma */ void addCliqueLemma(std::vector& clique); /** cardinality */ - context::CDO d_cardinality; + context::CDO d_cardinality; /** cardinality lemma term */ Node d_cardinality_term; /** cardinality literals */ - std::map d_cardinality_literal; + std::map 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 d_maxNegCard; + context::CDO d_maxNegCard; /** list of fresh representatives allocated */ std::vector< Node > d_fresh_aloc_reps; /** whether we are initialized */ @@ -305,17 +305,20 @@ class CardinalityExtension /** 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 ); /** @@ -426,7 +429,9 @@ class CardinalityExtension std::map d_rep_model; /** minimum positive combined cardinality */ - context::CDO d_min_pos_com_card; + context::CDO d_min_pos_com_card; + /** Whether the field above has been set */ + context::CDO d_min_pos_com_card_set; /** * Decision strategy for combined cardinality constraints. This asserts * the minimal combined cardinality constraint positively in the SAT @@ -454,7 +459,10 @@ class CardinalityExtension /** the master monotone type (if ufssFairnessMonotone enabled) */ TypeNode d_tn_mono_master; std::map d_tn_mono_slave; - context::CDO d_min_pos_tn_master_card; + /** The minimum positive asserted master cardinality */ + context::CDO d_min_pos_tn_master_card; + /** Whether the field above has been set */ + context::CDO d_min_pos_tn_master_card_set; /** relevant eqc */ NodeBoolMap d_rel_eqc; }; /* class CardinalityExtension */ -- 2.30.2