Fixed a bunch of clang warnings. (#5637)

23 files changed, 31 insertions, 49 deletions

diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 8f0441c28..17eb518a2 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -228,7 +228,7 @@ void IAndUtils::addDefaultValue(
   {
     counters[i] = 0;
   }
-  for (const std::pair<std::pair<int64_t, int64_t>, uint64_t>& element : table)
+  for (const auto& element : table)
   {
     uint64_t result = element.second;
     counters[result]++;
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 9434a0491..dff43e568 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -38,7 +38,6 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                        eq::EqualityEngine* ee)
     : d_containing(containing),
       d_im(containing.getInferenceManager()),
-      d_ee(ee),
       d_needsLastCall(false),
       d_checkCounter(0),
       d_extTheoryCb(ee),
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 88706350b..2de5daeb6 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -226,8 +226,6 @@ class NonlinearExtension
   // The theory of arithmetic containing this extension.
   TheoryArith& d_containing;
   InferenceManager& d_im;
-  // pointer to used equality engine
-  eq::EqualityEngine* d_ee;
   /** The statistics class */
   NlStats d_stats;
   // needs last call effort
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index ba60b6a0e..6dbb847a6 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -23,21 +23,6 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
-namespace {
-
-/**
- * Ensure a is in the main phase:
- *   -pi <= a <= pi
- */
-inline Node mkValidPhase(TNode a, TNode pi)
-{
-  return mkBounded(
-      NodeManager::currentNM()->mkNode(Kind::MULT, mkRationalNode(-1), pi),
-      a,
-      pi);
-}
-}  // namespace
-
 TranscendentalState::TranscendentalState(InferenceManager& im, NlModel& model)
     : d_im(im), d_model(model)
 {
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 4d4ec89b4..b13bd6926 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1758,7 +1758,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
   Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
 }
 
-void TheoryArrays::propagate(RowLemmaType lem)
+void TheoryArrays::propagateRowLemma(RowLemmaType lem)
 {
   Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
                      << options::arraysPropagate() << std::endl;
@@ -1845,7 +1845,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   // If propagating, check propagations
   int prop = options::arraysPropagate();
   if (prop > 0) {
-    propagate(lem);
+    propagateRowLemma(lem);
   }
 
   // Prefer equality between indexes so as not to introduce new read terms
@@ -1975,7 +1975,7 @@ bool TheoryArrays::dischargeLemmas()
 
     int prop = options::arraysPropagate();
     if (prop > 0) {
-      propagate(l);
+      propagateRowLemma(l);
       if (d_state.isInConflict())
       {
         return true;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 5236324bc..7e4f0e36c 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -442,7 +442,7 @@ class TheoryArrays : public Theory {
   void checkStore(TNode a);
   void checkRowForIndex(TNode i, TNode a);
   void checkRowLemmas(TNode a, TNode b);
-  void propagate(RowLemmaType lem);
+  void propagateRowLemma(RowLemmaType lem);
   void queueRowLemma(RowLemmaType lem);
   bool dischargeLemmas();
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index dbee65d8c..69500fea0 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -142,7 +142,7 @@ Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions)
   if (all.size() == 1) { return conjunctions[0]; }
 
   NodeBuilder<> conjunction(kind::AND);
-  for (const Node& n : all) { conjunction << n; }
+  for (TNode n : all) { conjunction << n; }
   return conjunction;
 }
 
@@ -161,7 +161,7 @@ Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes)
   if (all.size() == 1) { return nodes[0]; }
 
   NodeBuilder<> disjunction(kind::OR);
-  for (const Node& n : all) { disjunction << n; }
+  for (TNode n : all) { disjunction << n; }
   return disjunction;
 }
 /* Create node of kind XOR. */
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index fde28fd26..18b75e631 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1196,7 +1196,7 @@ void SygusExtension::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz,
         sca.d_search_terms[tn].find(d);
     if (itt != sca.d_search_terms[tn].end())
     {
-      for (const TNode& t : itt->second)
+      for (const Node& t : itt->second)
       {
         if (!options::sygusSymBreakLazy()
             || d_active_terms.find(t) != d_active_terms.end())
@@ -1469,7 +1469,7 @@ void SygusExtension::incrementCurrentSearchSize( Node m, std::vector< Node >& le
           int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz);
           std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth );
           if( itt!=itc->second.d_search_terms[tn].end() ){
-            for (const TNode& t : itt->second)
+            for (const Node& t : itt->second)
             {
               if (!options::sygusSymBreakLazy()
                   || (d_active_terms.find(t) != d_active_terms.end()
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index eeaa678d4..e13902077 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -905,7 +905,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
               d_conj_count++;
             }else{
               std::vector< Node > bvs;
-              for (const std::pair<TypeNode, unsigned>& lhs_pattern :
+              for (const std::pair<const TypeNode, unsigned>& lhs_pattern :
                    d_pattern_var_id[lhs])
               {
                 for (unsigned j = 0; j <= lhs_pattern.second; j++)
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 20d807793..1f45fd85f 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1114,7 +1114,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body,
   std::vector<Node> inactive_vars;
   std::map<Node, std::map<int, bool> > visited;
   std::map<Node, int> exclude;
-  for (const std::pair<Node, bool>& pr : qpr.d_phase_reqs)
+  for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
   {
     if (pr.first.getKind() == GEQ)
     {
@@ -1188,7 +1188,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body,
   } while (!evisit.empty() && !elig_vars.empty());
 
   bool ret = false;
-  for (const std::pair<Node, bool>& ev : elig_vars)
+  for (const std::pair<const Node, bool>& ev : elig_vars)
   {
     Node v = ev.first;
     Trace("var-elim-ineq-debug")
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 55beea4ca..f0999a5da 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -83,7 +83,7 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out)
     }
     if (threshCount < 2)
     {
-      for (const std::pair<Node, std::vector<unsigned>>& etp : ev_to_pt)
+      for (const auto& etp : ev_to_pt)
       {
         if (etp.second.size() < d_deqThresh)
         {
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 098af62a7..360476399 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -88,7 +88,7 @@ void EnumStreamPermutation::reset(Node value)
       d_var_classes[ti.getSubclassForVar(var)].push_back(var);
     }
   }
-  for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
+  for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
   {
     d_perm_state_class.push_back(PermutationState(p.second));
     if (Trace.isOn("synth-stream-concrete"))
@@ -383,7 +383,7 @@ void EnumStreamSubstitution::resetValue(Node value)
   d_curr_ind = 0;
   d_comb_state_class.clear();
   Trace("synth-stream-concrete") << " ..combining vars  :";
-  for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
+  for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
   {
     // ignore classes without variables being permuted
     unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first);
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 92754ebfe..62eef124a 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -126,7 +126,7 @@ void SygusSampler::initializeSygus(TermDbSygus* tds,
   {
     TypeNode svt = sv.getType();
     // is it equivalent to a previous variable?
-    for (const std::pair<Node, unsigned>& v : var_to_type_id)
+    for (const auto& v : var_to_type_id)
     {
       Node svc = v.first;
       if (svc.getType() == svt)
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 42677fa3f..f91cda36b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -276,14 +276,14 @@ void TermDb::computeUfEqcTerms( TNode f ) {
     ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
   }
   eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
-  for (const Node& ff : ops)
+  for (TNode ff : ops)
   {
-    for (const TNode& n : d_op_map[ff])
+    for (const Node& n : d_op_map[ff])
     {
       if (hasTermCurrent(n) && isTermActive(n))
       {
         computeArgReps(n);
-        TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : n;
+        TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n);
         d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]);
       }
     }
@@ -312,7 +312,7 @@ void TermDb::computeUfTerms( TNode f ) {
   unsigned relevantCount = 0;
   eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
   NodeManager* nm = NodeManager::currentNM();
-  for (const Node& ff : ops)
+  for (TNode ff : ops)
   {
     std::map<Node, std::vector<Node> >::iterator it = d_op_map.find(ff);
     if (it == d_op_map.end())
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index d03cc8570..d9d9415fc 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -755,7 +755,7 @@ void TheorySep::postCheck(Effort level)
 
       // get model values
       std::map<int, Node> mvals;
-      for (const std::pair<int, Node>& sub_element : d_label_map[satom][slbl])
+      for (const std::pair<const int, Node>& sub_element : d_label_map[satom][slbl])
       {
         int sub_index = sub_element.first;
         Node sub_lbl = sub_element.second;
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index cb0540b86..5997d1217 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -165,7 +165,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
       const std::map<Node, Node>& negativeMembers =
           d_state.getNegativeMembers(representative);
 
-      for (const std::pair<Node, Node>& negativeMember : negativeMembers)
+      for (const auto& negativeMember : negativeMembers)
       {
         Node member = nm->mkNode(MEMBER, negativeMember.first, univ);
         // negativeMember.second is the reason for the negative membership and
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index e44c3c7a6..4390b3e6e 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1163,7 +1163,7 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
   {
     const std::map<TypeNode, std::vector<TNode> >& slackElements =
         d_cardSolver->getFiniteTypeSlackElements();
-    for (const std::pair<TypeNode, std::vector<TNode> >& pair : slackElements)
+    for (const auto& pair : slackElements)
     {
       const std::vector<Node>& members =
           d_cardSolver->getFiniteTypeMembers(pair.first);
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index edd00c954..48116bc24 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -2575,7 +2575,7 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii)
     addNormalFormPair(cii.d_nfPair[0], cii.d_nfPair[1]);
   }
   // send phase requirements
-  for (const std::pair<const Node, bool> pp : cii.d_pendingPhase)
+  for (const std::pair<const Node, bool>& pp : cii.d_pendingPhase)
   {
     Node ppr = Rewriter::rewrite(pp.first);
     d_im.addPendingPhaseRequirement(ppr, pp.second);
diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index 7724b5137..5beaa4a00 100644
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -61,9 +61,9 @@ void NormalForm::splitConstant(unsigned index, Node c1, Node c2)
   // notice this is not critical for soundness: not doing the below incrementing
   // will only lead to overapproximating when antecedants are required in
   // explanations
-  for (const std::pair<Node, std::map<bool, unsigned> >& pe : d_expDep)
+  for (const std::pair<const Node, std::map<bool, unsigned> >& pe : d_expDep)
   {
-    for (const std::pair<bool, unsigned>& pep : pe.second)
+    for (const auto& pep : pe.second)
     {
       // See if this can be incremented: it can if this literal is not relevant
       // to the current index, and hence it is not relevant for both c1 and c2.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c8812b160..7b38bd844 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1823,7 +1823,7 @@ theory::TrustNode TheoryEngine::getExplanation(
     if (Trace.isOn("te-proof-exp"))
     {
       Trace("te-proof-exp") << "Explanation is:" << std::endl;
-      for (const Node& e : exp)
+      for (TNode e : exp)
       {
         Trace("te-proof-exp") << "  " << e << std::endl;
       }
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index f04ebbb60..2173c6922 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1286,7 +1286,7 @@ void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions)
     explainPredicate(atom, polarity, tassumptions);
   }
   // ensure that duplicates are removed
-  for (const TNode a : tassumptions)
+  for (TNode a : tassumptions)
   {
     if (std::find(assumptions.begin(), assumptions.end(), a)
         == assumptions.end())
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 6377f78b6..f04bc5ec1 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -518,7 +518,7 @@ void ProofEqEngine::explainWithProof(Node lit,
   }
   Trace("pfee-proof") << "...got " << tassumps << std::endl;
   // avoid duplicates
-  for (const TNode a : tassumps)
+  for (TNode a : tassumps)
   {
     if (a == lit)
     {
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index c4d6c9c82..2e0a9adf5 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -594,7 +594,7 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
   subs.push_back(p1);
   repls.push_back(p1);
   repls.push_back(p0);
-  for (const Node nn : d_phi)
+  for (const Node& nn : d_phi)
   {
     Node s =
         nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
@@ -629,7 +629,7 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
     subs.clear();
     repls.clear();
     bool first = true;
-    for (const Node& nn : p)
+    for (TNode nn : p)
     {
       subs.push_back(nn);
       if(!first) {