diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-23 14:59:20 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-23 12:59:20 -0700 |
commit | 408bccf70b41b1f41c8be04ffe7f7002fb57e182 (patch) | |
tree | a9a11516fd218ed9c8b99a8c289e3f39b9f82207 | |
parent | 4dc48596188c0550e625434cdd893d909810f9de (diff) |
Fixing some coverity warnings (#2357)
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_invariance.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.h | 2 | ||||
-rw-r--r-- | 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; i<pats.size(); i++ ){ Node p = pats[i]; if( std::find( pats_ordered.begin(), pats_ordered.end(), p )==pats_ordered.end() ){ @@ -641,13 +642,17 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto score_2++; } } - if( score_index==-1 || score_1>score_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<var_contains[mp].size(); i++ ){ diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 3615ef6f4..b50deea11 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -838,6 +838,7 @@ Node Trigger::getInversion( Node n, Node x ) { return x; }else if( n.getKind()==PLUS || n.getKind()==MULT ){ int cindex = -1; + bool cindexSet = false; for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){ if( n.getKind()==PLUS ){ @@ -859,12 +860,15 @@ Node Trigger::getInversion( Node n, Node x ) { } x = Rewriter::rewrite( x ); }else{ - Assert( cindex==-1 ); + Assert(!cindexSet); cindex = i; + cindexSet = true; } } - Assert( cindex!=-1 ); - return getInversion( n[cindex], x ); + if (cindexSet) + { + return getInversion(n[cindex], x); + } } return Node::null(); } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 84104e51c..33c0a836b 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -117,8 +117,6 @@ public: CegConjecture* d_parent; /** is the syntax restricted? */ bool d_is_syntax_restricted; - /** does the syntax allow ITE expressions? */ - bool d_has_ite; /** collect terms */ void collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& 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_id<min_id || ( pinfer[i].d_id==min_id && pinfer[i].d_index>max_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 |