diff options
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 7 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 4 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 9 |
5 files changed, 25 insertions, 14 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index a079017cd..e82ab617a 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -882,9 +882,12 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in d_conj_count++; }else{ std::vector< Node > bvs; - for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){ - for( unsigned i=0; i<=it->second; i++ ){ - bvs.push_back( getFreeVar( it->first, i ) ); + for (const std::pair<TypeNode, unsigned>& lhs_pattern : + d_pattern_var_id[lhs]) + { + for (unsigned i = 0; i <= lhs_pattern.second; i++) + { + bvs.push_back(getFreeVar(lhs_pattern.first, i)); } } Node rsg; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index f0789a503..8d8bf7f50 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -459,18 +459,18 @@ void BoundedIntegers::checkOwnership(Node f) success = true; //set Attributes on literals for( unsigned b=0; b<2; b++ ){ - if (bound_lit_map[b].find(v) != bound_lit_map[b].end()) + std::map<Node, Node>& blm = bound_lit_map[b]; + if (blm.find(v) != blm.end()) { + std::map<Node, bool>& blmp = bound_lit_pol_map[b]; // WARNING_CANDIDATE: // This assertion may fail. We intentionally do not enable this in // production as it is considered safe for this to fail. We fail // the assertion in debug mode to have this instance raised to // our attention. - Assert(bound_lit_pol_map[b].find(v) - != bound_lit_pol_map[b].end()); + Assert(blmp.find(v) != blmp.end()); BoundIntLitAttribute bila; - bound_lit_map[b][v].setAttribute(bila, - bound_lit_pol_map[b][v] ? 1 : 0); + bound_lit_map[b][v].setAttribute(bila, blmp[v] ? 1 : 0); } else { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 5f5a84a6b..39c3baf5c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -1036,8 +1036,11 @@ int TransitionInference::incrementTrace( DetTrace& dt, Node loc, bool fwd ) { } } if( fwd ){ - std::map< Node, std::map< Node, Node > >::iterator it = d_com[0].d_const_eq.find( loc ); - if( it!=d_com[0].d_const_eq.end() ){ + Component& cm = d_com[0]; + std::map<Node, std::map<Node, Node> >::iterator it = + cm.d_const_eq.find(loc); + if (it != cm.d_const_eq.end()) + { std::vector< Node > next; for( unsigned i=0; i<d_prime_vars.size(); i++ ){ Node pv = d_prime_vars[i]; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 6c9c34123..6085b1f23 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -646,7 +646,9 @@ void TheorySep::check(Effort e) { if( assert_active[fact] ){ Assert( atom.getKind()==kind::SEP_LABEL ); TNode s_lbl = atom[1]; - if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){ + std::map<Node, std::map<int, Node> >& lms = d_label_map[s_atom]; + if (lms.find(s_lbl) != lms.end()) + { Trace("sep-process-debug") << "Active lbl : " << s_lbl << std::endl; active_lbl[s_lbl] = true; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 9346970d1..ab9fa6d54 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -611,11 +611,14 @@ void TheorySetsPrivate::fullEffortCheck(){ }else{ Node r1 = d_equalityEngine.getRepresentative( n[0] ); Node r2 = d_equalityEngine.getRepresentative( n[1] ); - if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){ - d_bop_index[n.getKind()][r1][r2] = n; + std::map<Node, Node>& binr1 = d_bop_index[n.getKind()][r1]; + std::map<Node, Node>::iterator itb = binr1.find(r2); + if (itb == binr1.end()) + { + binr1[r2] = n; d_op_list[n.getKind()].push_back( n ); }else{ - d_congruent[n] = d_bop_index[n.getKind()][r1][r2]; + d_congruent[n] = itb->second; } } d_nvar_sets[eqc].push_back( n ); |