From 408bccf70b41b1f41c8be04ffe7f7002fb57e182 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 23 Aug 2018 14:59:20 -0500 Subject: [PATCH] Fixing some coverity warnings (#2357) --- .../quantifiers/ematching/inst_match_generator.cpp | 9 +++++++-- src/theory/quantifiers/ematching/trigger.cpp | 10 +++++++--- src/theory/quantifiers/sygus/sygus_grammar_cons.h | 2 -- src/theory/quantifiers/sygus/sygus_invariance.h | 5 ++++- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 12 ++++++------ src/theory/quantifiers/sygus/sygus_unif_io.h | 2 -- src/theory/quantifiers/sygus/sygus_unif_rl.h | 5 ++++- src/theory/quantifiers/sygus/sygus_unif_strat.h | 2 +- src/theory/strings/theory_strings.cpp | 8 ++++++-- 9 files changed, 35 insertions(+), 20 deletions(-) diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 192a6b433..eb3f6232d 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -627,7 +627,8 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto // score is lexographic ( bound vars, shared vars ) int score_max_1 = -1; int score_max_2 = -1; - int score_index = -1; + unsigned score_index = 0; + bool set_score_index = false; for( unsigned i=0; iscore_max_1 || ( score_1==score_max_1 && score_2>score_max_2 ) ){ + if (!set_score_index || score_1 > score_max_1 + || (score_1 == score_max_1 && score_2 > score_max_2)) + { score_index = i; + set_score_index = true; score_max_1 = score_1; score_max_2 = score_2; } } } + Assert(set_score_index); //update the variable bounds Node mp = pats[score_index]; for( unsigned i=0; i >& consts ); /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 9e3553a0b..20cd1fd03 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -97,7 +97,10 @@ class SygusInvarianceTest class EvalSygusInvarianceTest : public SygusInvarianceTest { public: - EvalSygusInvarianceTest() : d_kind(kind::UNDEFINED_KIND) {} + EvalSygusInvarianceTest() + : d_kind(kind::UNDEFINED_KIND), d_is_conjunctive(false) + { + } /** initialize this invariance test * diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index c36bdbcbf..d36566d63 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1177,7 +1177,8 @@ Node SygusUnifIo::constructSol( // for ITE Node split_cond_enum; - int split_cond_res_index = -1; + unsigned split_cond_res_index = 0; + bool set_split_cond_res_index = false; for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++) { @@ -1204,9 +1205,8 @@ Node SygusUnifIo::constructSol( if (strat == strat_ITE && sc > 0) { EnumCache& ecache_cond = d_ecache[split_cond_enum]; - Assert(split_cond_res_index >= 0); - Assert(split_cond_res_index - < (int)ecache_cond.d_enum_vals_res.size()); + Assert(set_split_cond_res_index); + Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size()); prev = x.d_vals; bool ret = x.updateContext( this, @@ -1361,10 +1361,10 @@ Node SygusUnifIo::constructSol( Assert(ecache_child.d_enum_val_to_index.find(rec_c) != ecache_child.d_enum_val_to_index.end()); split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c]; + set_split_cond_res_index = true; split_cond_enum = ce; - Assert(split_cond_res_index >= 0); Assert(split_cond_res_index - < (int)ecache_child.d_enum_vals_res.size()); + < ecache_child.d_enum_vals_res.size()); } } else diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index f1aa08c65..967226e94 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -310,8 +310,6 @@ class SygusUnifIo : public SygusUnif * register a new value for an enumerator. */ bool d_check_sol; - /** whether we have solved the overall conjecture */ - bool d_solved; /** The number of values we have enumerated for all enumerators. */ unsigned d_cond_count; /** The solution for the function of this class, if one has been found */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 072766b21..af6be2e97 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -193,7 +193,10 @@ class SygusUnifRl : public SygusUnif class DecisionTreeInfo { public: - DecisionTreeInfo() {} + DecisionTreeInfo() + : d_unif(nullptr), d_strategy(nullptr), d_strategy_index(0) + { + } ~DecisionTreeInfo() {} /** initializes this class */ void initialize(Node cond_enum, diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index b94ae0654..41923f7a1 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -277,7 +277,7 @@ struct StrategyRestrictions class SygusUnifStrategy { public: - SygusUnifStrategy() {} + SygusUnifStrategy() : d_qe(nullptr) {} /** initialize * * This initializes this class with function-to-synthesize f. We also call diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c777a0976..ce0100686 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2625,7 +2625,8 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form } if( !pinfer.empty() ){ //now, determine which of the possible inferences we want to add - int use_index = -1; + unsigned use_index = 0; + bool set_use_index = false; Trace("strings-solve") << "Possible inferences (" << pinfer.size() << ") : " << std::endl; unsigned min_id = 9; unsigned max_index = 0; @@ -2634,10 +2635,13 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form Trace("strings-solve") << "From " << pinfer[i].d_i << " / " << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev << ") : "; Trace("strings-solve") << pinfer[i].d_conc << " by " << pinfer[i].d_id << std::endl; - if( use_index==-1 || pinfer[i].d_idmax_index ) ){ + if (!set_use_index || pinfer[i].d_id < min_id + || (pinfer[i].d_id == min_id && pinfer[i].d_index > max_index)) + { min_id = pinfer[i].d_id; max_index = pinfer[i].d_index; use_index = i; + set_use_index = true; } } //send the inference -- 2.30.2