Enable -Wshadow and fix warnings. (#3909)

Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. 

Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>

2 files changed, 303 insertions, 210 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6e5dc664e..6abaa30c6 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -129,75 +129,93 @@ static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction o
 CRef Solver::TCRef_Undef = CRef_Undef;
 CRef Solver::TCRef_Lazy = CRef_Lazy;
 
-class ScopedBool {
-  bool& watch;
-  bool oldValue;
-public:
-  ScopedBool(bool& watch, bool newValue)
-  : watch(watch), oldValue(watch) {
+class ScopedBool
+{
+  bool& d_watch;
+  bool d_oldValue;
+
+ public:
+  ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch)
+  {
     watch = newValue;
   }
-  ~ScopedBool() {
-    watch = oldValue;
-  }
+  ~ScopedBool() { d_watch = d_oldValue; }
 };
 
-
 //=================================================================================================
 // Constructor/Destructor:
 
-Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enable_incremental) :
-    proxy(proxy)
-  , context(context)
-  , assertionLevel(0)
-  , enable_incremental(enable_incremental)
-  , minisat_busy(false)
-    // Parameters (user settable):
-    //
-  , verbosity        (0)
-  , var_decay        (opt_var_decay)
-  , clause_decay     (opt_clause_decay)
-  , random_var_freq  (opt_random_var_freq)
-  , random_seed      (opt_random_seed)
-  , luby_restart     (opt_luby_restart)
-  , ccmin_mode       (opt_ccmin_mode)
-  , phase_saving     (opt_phase_saving)
-  , rnd_pol          (false)
-  , rnd_init_act     (opt_rnd_init_act)
-  , garbage_frac     (opt_garbage_frac)
-  , restart_first    (opt_restart_first)
-  , restart_inc      (opt_restart_inc)
-
-    // Parameters (the rest):
-    //
-  , learntsize_factor(1), learntsize_inc(1.5)
-
-    // Parameters (experimental):
-    //
-  , learntsize_adjust_start_confl (100)
-  , learntsize_adjust_inc         (1.5)
-
-    // Statistics: (formerly in 'SolverStats')
-    //
-  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0), resources_consumed(0)
-  , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
-
-  , ok                 (true)
-  , cla_inc            (1)
-  , var_inc            (1)
-  , watches            (WatcherDeleted(ca))
-  , qhead              (0)
-  , simpDB_assigns     (-1)
-  , simpDB_props       (0)
-  , order_heap         (VarOrderLt(activity))
-  , progress_estimate  (0)
-  , remove_satisfied   (!enable_incremental)
-
-    // Resource constraints:
-    //
-  , conflict_budget    (-1)
-  , propagation_budget (-1)
-  , asynch_interrupt   (false)
+Solver::Solver(CVC4::prop::TheoryProxy* proxy,
+               CVC4::context::Context* context,
+               bool enable_incremental)
+    : d_proxy(proxy),
+      d_context(context),
+      assertionLevel(0),
+      d_enable_incremental(enable_incremental),
+      minisat_busy(false)
+      // Parameters (user settable):
+      //
+      ,
+      verbosity(0),
+      var_decay(opt_var_decay),
+      clause_decay(opt_clause_decay),
+      random_var_freq(opt_random_var_freq),
+      random_seed(opt_random_seed),
+      luby_restart(opt_luby_restart),
+      ccmin_mode(opt_ccmin_mode),
+      phase_saving(opt_phase_saving),
+      rnd_pol(false),
+      rnd_init_act(opt_rnd_init_act),
+      garbage_frac(opt_garbage_frac),
+      restart_first(opt_restart_first),
+      restart_inc(opt_restart_inc)
+
+      // Parameters (the rest):
+      //
+      ,
+      learntsize_factor(1),
+      learntsize_inc(1.5)
+
+      // Parameters (experimental):
+      //
+      ,
+      learntsize_adjust_start_confl(100),
+      learntsize_adjust_inc(1.5)
+
+      // Statistics: (formerly in 'SolverStats')
+      //
+      ,
+      solves(0),
+      starts(0),
+      decisions(0),
+      rnd_decisions(0),
+      propagations(0),
+      conflicts(0),
+      resources_consumed(0),
+      dec_vars(0),
+      clauses_literals(0),
+      learnts_literals(0),
+      max_literals(0),
+      tot_literals(0)
+
+      ,
+      ok(true),
+      cla_inc(1),
+      var_inc(1),
+      watches(WatcherDeleted(ca)),
+      qhead(0),
+      simpDB_assigns(-1),
+      simpDB_props(0),
+      order_heap(VarOrderLt(activity)),
+      progress_estimate(0),
+      remove_satisfied(!enable_incremental)
+
+      // Resource constraints:
+      //
+      ,
+      conflict_budget(-1),
+      propagation_budget(-1),
+      asynch_interrupt(false)
 {
   PROOF(ProofManager::currentPM()->initSatProof(this);)
 
@@ -257,7 +275,7 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo
 }
 
 void Solver::resizeVars(int newSize) {
-  assert(enable_incremental);
+  assert(d_enable_incremental);
   assert(decisionLevel() == 0);
   Assert(newSize >= 2) << "always keep true/false";
   if (newSize < nVars()) {
@@ -288,7 +306,7 @@ CRef Solver::reason(Var x) {
   Debug("pf::sat") << "Solver::reason(" << x << ")" << std::endl;
 
   // If we already have a reason, just return it
-  if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
+  if (vardata[x].d_reason != CRef_Lazy) return vardata[x].d_reason;
 
   // What's the literal we are trying to explain
   Lit l = mkLit(x, value(x) != l_True);
@@ -296,7 +314,8 @@ CRef Solver::reason(Var x) {
   // Get the explanation from the theory
   SatClause explanation_cl;
   // FIXME: at some point return a tag with the theory that spawned you
-  proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
+  d_proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
+                              explanation_cl);
   vec<Lit> explanation;
   MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
 
@@ -352,9 +371,9 @@ CRef Solver::reason(Var x) {
       explanation.shrink(i - j);
 
       Debug("pf::sat") << "Solver::reason: explanation = ";
-      for (int i = 0; i < explanation.size(); ++i)
+      for (int k = 0; k < explanation.size(); ++k)
       {
-        Debug("pf::sat") << explanation[i] << " ";
+        Debug("pf::sat") << explanation[k] << " ";
       }
       Debug("pf::sat") << std::endl;
 
@@ -578,7 +597,7 @@ void Solver::removeClause(CRef cr) {
     Debug("minisat::remove-clause") << "Solver::removeClause(" << c << ")" << std::endl;
     detachClause(cr);
     // Don't leave pointers to free'd memory!
-    if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
+    if (locked(c)) vardata[var(c[0])].d_reason = CRef_Undef;
     c.mark(1);
     ca.free(cr);
 }
@@ -599,15 +618,15 @@ void Solver::cancelUntil(int level) {
     if (decisionLevel() > level){
         // Pop the SMT context
         for (int l = trail_lim.size() - level; l > 0; --l) {
-          context->pop();
+          d_context->pop();
           if(Dump.isOn("state")) {
-            proxy->dumpStatePop();
+            d_proxy->dumpStatePop();
           }
         }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
-            vardata[x].trail_index = -1;
+            vardata[x].d_trail_index = -1;
             if ((phase_saving > 1 ||
                  ((phase_saving == 1) && c > trail_lim.last())
                  ) && ((polarity[x] & 0x2) == 0)) {
@@ -622,9 +641,13 @@ void Solver::cancelUntil(int level) {
 
         // Register variables that have not been registered yet
         int currentLevel = decisionLevel();
-        for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) {
-          variables_to_register[i].level = currentLevel;
-          proxy->variableNotify(MinisatSatSolver::toSatVariable(variables_to_register[i].var));
+        for (int i = variables_to_register.size() - 1;
+             i >= 0 && variables_to_register[i].d_level > currentLevel;
+             --i)
+        {
+          variables_to_register[i].d_level = currentLevel;
+          d_proxy->variableNotify(
+              MinisatSatSolver::toSatVariable(variables_to_register[i].d_var));
         }
     }
 }
@@ -641,7 +664,7 @@ Lit Solver::pickBranchLit()
 
 #ifdef CVC4_REPLAY
 
-    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
+    nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextReplayDecision());
 
     if (nextLit != lit_Undef) {
       return nextLit;
@@ -649,7 +672,8 @@ Lit Solver::pickBranchLit()
 #endif /* CVC4_REPLAY */
 
     // Theory requests
-    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
+    nextLit =
+        MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest());
     while (nextLit != lit_Undef) {
       if(value(var(nextLit)) == l_Undef) {
         Debug("theoryDecision")
@@ -660,14 +684,15 @@ Lit Solver::pickBranchLit()
         // org-mode tracing -- theory decision
         if (Trace.isOn("dtview"))
         {
-          dtviewDecisionHelper(context->getLevel(),
-                               proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
-                               "THEORY");
+          dtviewDecisionHelper(
+              d_context->getLevel(),
+              d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
+              "THEORY");
         }
 
         if (Trace.isOn("dtview::prop"))
         {
-          dtviewPropagationHeaderHelper(context->getLevel());
+          dtviewPropagationHeaderHelper(d_context->getLevel());
         }
 
         return nextLit;
@@ -676,7 +701,8 @@ Lit Solver::pickBranchLit()
             << "getNextTheoryDecisionRequest(): would decide on " << nextLit
             << " but it already has an assignment" << std::endl;
       }
-      nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
+      nextLit = MinisatSatSolver::toMinisatLit(
+          d_proxy->getNextTheoryDecisionRequest());
     }
     Debug("theoryDecision")
         << "getNextTheoryDecisionRequest(): decide on another literal"
@@ -684,7 +710,8 @@ Lit Solver::pickBranchLit()
 
     // DE requests
     bool stopSearch = false;
-    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch));
+    nextLit = MinisatSatSolver::toMinisatLit(
+        d_proxy->getNextDecisionEngineRequest(stopSearch));
     if(stopSearch) {
       return lit_Undef;
     }
@@ -700,14 +727,15 @@ Lit Solver::pickBranchLit()
       // org-mode tracing -- decision engine decision
       if (Trace.isOn("dtview"))
       {
-        dtviewDecisionHelper(context->getLevel(),
-                             proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
-                             "DE");
+        dtviewDecisionHelper(
+            d_context->getLevel(),
+            d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
+            "DE");
       }
 
       if (Trace.isOn("dtview::prop"))
       {
-        dtviewPropagationHeaderHelper(context->getLevel());
+        dtviewPropagationHeaderHelper(d_context->getLevel());
       }
 
       return nextLit;
@@ -732,7 +760,9 @@ Lit Solver::pickBranchLit()
 
         if(!decision[next]) continue;
         // Check with decision engine about relevancy
-        if(proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next)) == false ) {
+        if (d_proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next))
+            == false)
+        {
           next = var_Undef;
         }
     }
@@ -742,8 +772,8 @@ Lit Solver::pickBranchLit()
     } else {
       decisions++;
       // Check with decision engine if it can tell polarity
-      lbool dec_pol = MinisatSatSolver::toMinisatlbool
-        (proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next)));
+      lbool dec_pol = MinisatSatSolver::toMinisatlbool(
+          d_proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next)));
       Lit decisionLit;
       if(dec_pol != l_Undef) {
         Assert(dec_pol == l_True || dec_pol == l_False);
@@ -759,14 +789,15 @@ Lit Solver::pickBranchLit()
       // org-mode tracing -- decision engine decision
       if (Trace.isOn("dtview"))
       {
-        dtviewDecisionHelper(context->getLevel(),
-                             proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)),
-                             "DE");
+        dtviewDecisionHelper(
+            d_context->getLevel(),
+            d_proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)),
+            "DE");
       }
 
       if (Trace.isOn("dtview::prop"))
       {
-        dtviewPropagationHeaderHelper(context->getLevel());
+        dtviewPropagationHeaderHelper(d_context->getLevel());
       }
 
       return decisionLit;
@@ -920,17 +951,18 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
     else{
         int max_i = 1;
         // Find the first literal assigned at the next-highest level:
-        for (int i = 2; i < out_learnt.size(); i++)
-            if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
-                max_i = i;
+        for (int k = 2; k < out_learnt.size(); k++)
+          if (level(var(out_learnt[k])) > level(var(out_learnt[max_i])))
+            max_i = k;
         // Swap-in this literal at index 1:
-        Lit p             = out_learnt[max_i];
+        Lit p2 = out_learnt[max_i];
         out_learnt[max_i] = out_learnt[1];
-        out_learnt[1]     = p;
-        out_btlevel       = level(var(p));
+        out_learnt[1] = p2;
+        out_btlevel = level(var(p2));
     }
 
-    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
+    for (int k = 0; k < analyze_toclear.size(); k++)
+      seen[var(analyze_toclear[k])] = 0;  // ('seen[]' is now cleared)
 
     // Return the maximal resolution level
     return max_resolution_level;
@@ -953,19 +985,24 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
         // Since calling reason might relocate to resize, c is not necesserily the right reference, we must
         // use the allocator each time
         for (int i = 1; i < c_size; i++){
-            Lit p  = ca[c_reason][i];
-            if (!seen[var(p)] && level(var(p)) > 0){
-                if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
-                    seen[var(p)] = 1;
-                    analyze_stack.push(p);
-                    analyze_toclear.push(p);
-                }else{
-                    for (int j = top; j < analyze_toclear.size(); j++)
-                        seen[var(analyze_toclear[j])] = 0;
-                    analyze_toclear.shrink(analyze_toclear.size() - top);
-                    return false;
-                }
+          Lit p2 = ca[c_reason][i];
+          if (!seen[var(p2)] && level(var(p2)) > 0)
+          {
+            if (reason(var(p2)) != CRef_Undef
+                && (abstractLevel(var(p2)) & abstract_levels) != 0)
+            {
+              seen[var(p2)] = 1;
+              analyze_stack.push(p2);
+              analyze_toclear.push(p2);
             }
+            else
+            {
+              for (int j = top; j < analyze_toclear.size(); j++)
+                seen[var(analyze_toclear[j])] = 0;
+              analyze_toclear.shrink(analyze_toclear.size() - top);
+              return false;
+            }
+          }
         }
     }
 
@@ -1022,7 +1059,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     trail.push_(p);
     if (theory[var(p)]) {
       // Enqueue to the theory
-      proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
+      d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
     }
 }
 
@@ -1057,7 +1094,7 @@ CRef Solver::propagate(TheoryCheckType type)
         confl = updateLemmas();
         return confl;
       } else {
-        recheck = proxy->theoryNeedCheck();
+        recheck = d_proxy->theoryNeedCheck();
         return confl;
       }
     }
@@ -1087,7 +1124,7 @@ CRef Solver::propagate(TheoryCheckType type)
           {
             if (confl != CRef_Undef)
             {
-              dtviewPropConflictHelper(decisionLevel(), ca[confl], proxy);
+              dtviewPropConflictHelper(decisionLevel(), ca[confl], d_proxy);
             }
           }
           // Even though in conflict, we still need to discharge the lemmas
@@ -1116,7 +1153,7 @@ void Solver::propagateTheory() {
   SatClause propagatedLiteralsClause;
   // Doesn't actually call propagate(); that's done in theoryCheck() now that combination
   // is online.  This just incorporates those propagations previously discovered.
-  proxy->theoryPropagate(propagatedLiteralsClause);
+  d_proxy->theoryPropagate(propagatedLiteralsClause);
 
   vec<Lit> propagatedLiterals;
   MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
@@ -1133,7 +1170,8 @@ void Solver::propagateTheory() {
       if (value(p) == l_False) {
         Debug("minisat") << "Conflict in theory propagation" << std::endl;
         SatClause explanation_cl;
-        proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl);
+        d_proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p),
+                                    explanation_cl);
         vec<Lit> explanation;
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
         ClauseId id; // FIXME: mark it as explanation here somehow?
@@ -1158,7 +1196,7 @@ void Solver::propagateTheory() {
 |________________________________________________________________________________________________@*/
 void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
 {
-  proxy->theoryCheck(effort);
+  d_proxy->theoryCheck(effort);
 }
 
 /*_________________________________________________________________________________________________
@@ -1187,7 +1225,7 @@ CRef Solver::propagateBool()
         // if propagation tracing enabled, print boolean propagation
         if (Trace.isOn("dtview::prop"))
         {
-          dtviewBoolPropagationHelper(decisionLevel(), p, proxy);
+          dtviewBoolPropagationHelper(decisionLevel(), p, d_proxy);
         }
 
         for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
@@ -1443,7 +1481,7 @@ lbool Solver::search(int nof_conflicts)
 
 	    // If this was a final check, we are satisfiable
             if (check_type == CHECK_FINAL) {
-	      bool decisionEngineDone = proxy->isDecisionEngineDone();
+              bool decisionEngineDone = d_proxy->isDecisionEngineDone();
               // Unless a lemma has added more stuff to the queues
               if (!decisionEngineDone  &&
 		  (!order_heap.empty() || qhead < trail.size()) ) {
@@ -1468,7 +1506,7 @@ lbool Solver::search(int nof_conflicts)
               cancelUntil(0);
               // [mdeters] notify theory engine of restarts for deferred
               // theory processing
-              proxy->notifyRestart();
+              d_proxy->notifyRestart();
               return l_Undef;
             }
 
@@ -1490,8 +1528,8 @@ lbool Solver::search(int nof_conflicts)
                     // Dummy decision level:
                     newDecisionLevel();
                 } else if (value(p) == l_False) {
-                    analyzeFinal(~p, conflict);
-                    return l_False;
+                  analyzeFinal(~p, d_conflict);
+                  return l_False;
                 } else {
                     next = p;
                     break;
@@ -1511,7 +1549,7 @@ lbool Solver::search(int nof_conflicts)
                 }
 
 #ifdef CVC4_REPLAY
-                proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
+                d_proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
 #endif /* CVC4_REPLAY */
             }
 
@@ -1575,7 +1613,7 @@ lbool Solver::solve_()
     assert(decisionLevel() == 0);
 
     model.clear();
-    conflict.clear();
+    d_conflict.clear();
     if (!ok){
       minisat_busy = false;
       return l_False;
@@ -1619,8 +1657,9 @@ lbool Solver::solve_()
           model[i] = value(i);
           Debug("minisat") << i << " = " << model[i] << std::endl;
         }
-    }else if (status == l_False && conflict.size() == 0)
-        ok = false;
+    }
+    else if (status == l_False && d_conflict.size() == 0)
+      ok = false;
 
     return status;
 }
@@ -1728,7 +1767,7 @@ void Solver::relocAll(ClauseAllocator& to)
 
         if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
           ca.reloc(
-              vardata[v].reason, to, NULLPROOF(ProofManager::getSatProof()));
+              vardata[v].d_reason, to, NULLPROOF(ProofManager::getSatProof()));
     }
     // All learnt:
     //
@@ -1761,7 +1800,7 @@ void Solver::garbageCollect()
 
 void Solver::push()
 {
-  assert(enable_incremental);
+  assert(d_enable_incremental);
   assert(decisionLevel() == 0);
 
   ++assertionLevel;
@@ -1769,14 +1808,14 @@ void Solver::push()
   trail_ok.push(ok);
   assigns_lim.push(assigns.size());
 
-  context->push(); // SAT context for CVC4
+  d_context->push();  // SAT context for CVC4
 
   Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
 }
 
 void Solver::pop()
 {
-  assert(enable_incremental);
+  assert(d_enable_incremental);
 
   assert(decisionLevel() == 0);
 
@@ -1804,7 +1843,7 @@ void Solver::pop()
   removeClausesAboveLevel(clauses_removable, assertionLevel);
 
   // Pop the SAT context to notify everyone
-  context->pop(); // SAT context for CVC4
+  d_context->pop();  // SAT context for CVC4
 
   // Pop the created variables
   resizeVars(assigns_lim.last());
@@ -1821,7 +1860,7 @@ CRef Solver::updateLemmas() {
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
   // Avoid adding lemmas indefinitely without resource-out
-  proxy->spendResource(ResourceManager::Resource::LemmaStep);
+  d_proxy->spendResource(ResourceManager::Resource::LemmaStep);
 
   CRef conflict = CRef_Undef;
 
@@ -1881,11 +1920,11 @@ CRef Solver::updateLemmas() {
   PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
 
   // Attach all the clauses and enqueue all the propagations
-  for (int i = 0; i < lemmas.size(); ++ i)
+  for (int j = 0; j < lemmas.size(); ++j)
   {
     // The current lemma
-    vec<Lit>& lemma = lemmas[i];
-    bool removable = lemmas_removable[i];
+    vec<Lit>& lemma = lemmas[j];
+    bool removable = lemmas_removable[j];
 
     // Attach it if non-unit
     CRef lemma_ref = CRef_Undef;
@@ -1895,22 +1934,22 @@ CRef Solver::updateLemmas() {
       if (removable && !assertionLevelOnly())
       {
         clauseLevel = 0;
-        for (int i = 0; i < lemma.size(); ++ i) {
-          clauseLevel = std::max(clauseLevel, intro_level(var(lemma[i])));
+        for (int k = 0; k < lemma.size(); ++k)
+        {
+          clauseLevel = std::max(clauseLevel, intro_level(var(lemma[k])));
         }
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      PROOF
-        (
-         TNode cnf_assertion = lemmas_cnf_assertion[i].first;
-         TNode cnf_def = lemmas_cnf_assertion[i].second;
-
-         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
-         ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
-         ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
-         ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
-         );
+      PROOF(TNode cnf_assertion = lemmas_cnf_assertion[j].first;
+            TNode cnf_def = lemmas_cnf_assertion[j].second;
+
+            Debug("pf::sat")
+            << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
+            ClauseId id = ProofManager::getSatProof()->registerClause(
+                lemma_ref, THEORY_LEMMA);
+            ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+            ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def););
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
@@ -1920,8 +1959,8 @@ CRef Solver::updateLemmas() {
     } else {
       PROOF
         (
-         Node cnf_assertion = lemmas_cnf_assertion[i].first;
-         Node cnf_def = lemmas_cnf_assertion[i].second;
+         Node cnf_assertion = lemmas_cnf_assertion[j].first;
+         Node cnf_def = lemmas_cnf_assertion[j].second;
 
          Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl;
          ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
@@ -1993,10 +2032,10 @@ void ClauseAllocator::reloc(CRef& cr,
 
 inline bool Solver::withinBudget(ResourceManager::Resource r) const
 {
-  Assert(proxy);
+  Assert(d_proxy);
   // spendResource sets async_interrupt or throws UnsafeInterruptException
   // depending on whether hard-limit is enabled
-  proxy->spendResource(r);
+  d_proxy->spendResource(r);
 
   bool within_budget =
       !asynch_interrupt
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 0cec30d24..508947456 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -66,14 +66,13 @@ public:
   typedef Clause TClause; 
   typedef CRef TCRef;
   typedef vec<Lit> TLitVec;
-  
-protected:
 
+ protected:
   /** The pointer to the proxy that provides interfaces to the SMT engine */
-  CVC4::prop::TheoryProxy* proxy;
+  CVC4::prop::TheoryProxy* d_proxy;
 
   /** The context from the SMT solver */
-  CVC4::context::Context* context;
+  CVC4::context::Context* d_context;
 
   /** The current assertion level (user) */
   int assertionLevel;
@@ -84,21 +83,22 @@ protected:
   /** Variable representing false */
   Var varFalse;
 
-public:
+ public:
   /** Returns the current user assertion level */
   int getAssertionLevel() const { return assertionLevel; }
-protected:
+
+ protected:
   /** Do we allow incremental solving */
-  bool enable_incremental;
+  bool d_enable_incremental;
 
   /** Literals propagated by lemmas */
-  vec< vec<Lit> > lemmas;
+  vec<vec<Lit> > lemmas;
 
   /** Is the lemma removable */
   vec<bool> lemmas_removable;
 
   /** Nodes being converted to CNF */
-  std::vector< std::pair<CVC4::Node, CVC4::Node > >lemmas_cnf_assertion;
+  std::vector<std::pair<CVC4::Node, CVC4::Node> > lemmas_cnf_assertion;
 
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
@@ -110,11 +110,11 @@ protected:
   bool minisat_busy;
 
   // Information about registration of variables
-  struct VarIntroInfo {
-    Var var;
-    int level;
-    VarIntroInfo(Var var, int level)
-    : var(var), level(level) {}
+  struct VarIntroInfo
+  {
+    Var d_var;
+    int d_level;
+    VarIntroInfo(Var var, int level) : d_var(var), d_level(level) {}
   };
 
   /** Variables to re-register with theory solvers on backtracks */
@@ -138,30 +138,38 @@ public:
 
     // Less than for literals in a lemma
     struct lemma_lt {
-        Solver& solver;
-        lemma_lt(Solver& solver) : solver(solver) {}
-        bool operator () (Lit x, Lit y) {
-          lbool x_value = solver.value(x);
-          lbool y_value = solver.value(y);
-          // Two unassigned literals are sorted arbitrarily
-          if (x_value == l_Undef && y_value == l_Undef) {
-            return x < y;
+      Solver& d_solver;
+      lemma_lt(Solver& solver) : d_solver(solver) {}
+      bool operator()(Lit x, Lit y)
+      {
+        lbool x_value = d_solver.value(x);
+        lbool y_value = d_solver.value(y);
+        // Two unassigned literals are sorted arbitrarily
+        if (x_value == l_Undef && y_value == l_Undef)
+        {
+          return x < y;
+        }
+        // Unassigned literals are put to front
+        if (x_value == l_Undef) return true;
+        if (y_value == l_Undef) return false;
+        // Literals of the same value are sorted by decreasing levels
+        if (x_value == y_value)
+        {
+          return d_solver.trail_index(var(x)) > d_solver.trail_index(var(y));
+        }
+        else
+        {
+          // True literals go up front
+          if (x_value == l_True)
+          {
+            return true;
           }
-          // Unassigned literals are put to front
-          if (x_value == l_Undef) return true;
-          if (y_value == l_Undef) return false;
-          // Literals of the same value are sorted by decreasing levels
-          if (x_value == y_value) {
-            return solver.trail_index(var(x)) > solver.trail_index(var(y));
-          } else {
-            // True literals go up front
-            if (x_value == l_True) {
-              return true;
-            } else {
-              return false;
-            }
+          else
+          {
+            return false;
           }
         }
+      }
     };
 
 
@@ -246,8 +254,9 @@ public:
     // Extra results: (read-only member variable)
     //
     vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
-    vec<Lit>   conflict;          // If problem is unsatisfiable (possibly under assumptions),
-                                  // this vector represent the final conflict clause expressed in the assumptions.
+    vec<Lit> d_conflict;          // If problem is unsatisfiable (possibly under
+                          // assumptions), this vector represent the final
+                          // conflict clause expressed in the assumptions.
 
     // Mode of operation:
     //
@@ -282,22 +291,26 @@ protected:
     //
     struct VarData {
       // Reason for the literal being in the trail
-      CRef reason;
+      CRef d_reason;
       // Sat level when the literal was added to the trail
-      int level;
+      int d_level;
       // User level when the literal was added to the trail
-      int user_level;
+      int d_user_level;
       // User level at which this literal was introduced
-      int intro_level;
+      int d_intro_level;
       // The index in the trail
-      int trail_index;
-
-      VarData(CRef reason, int level, int user_level, int intro_level, int trail_index)
-      : reason(reason)
-      , level(level)
-      , user_level(user_level)
-      , intro_level(intro_level)
-      , trail_index(trail_index)
+      int d_trail_index;
+
+      VarData(CRef reason,
+              int level,
+              int user_level,
+              int intro_level,
+              int trail_index)
+          : d_reason(reason),
+            d_level(level),
+            d_user_level(user_level),
+            d_intro_level(intro_level),
+            d_trail_index(trail_index)
       {}
     };
 
@@ -464,21 +477,53 @@ public:
 //=================================================================================================
 // Implementation of inline methods:
 
-inline bool Solver::hasReasonClause(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; }
+inline bool Solver::hasReasonClause(Var x) const
+{
+  return vardata[x].d_reason != CRef_Undef && vardata[x].d_reason != CRef_Lazy;
+}
 
-inline bool Solver::isPropagated(Var x) const { return vardata[x].reason != CRef_Undef; }
+inline bool Solver::isPropagated(Var x) const
+{
+  return vardata[x].d_reason != CRef_Undef;
+}
 
-inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy && ca.lea(vardata[var(c[0])].reason) == &c; }
+inline bool Solver::isPropagatedBy(Var x, const Clause& c) const
+{
+  return vardata[x].d_reason != CRef_Undef && vardata[x].d_reason != CRef_Lazy
+         && ca.lea(vardata[var(c[0])].d_reason) == &c;
+}
 
-inline bool Solver::isDecision(Var x) const { Debug("minisat") << "var " << x << " is a decision iff " << (vardata[x].reason == CRef_Undef) << " && " << level(x) << " > 0" << std::endl; return vardata[x].reason == CRef_Undef && level(x) > 0; }
+inline bool Solver::isDecision(Var x) const
+{
+  Debug("minisat") << "var " << x << " is a decision iff "
+                   << (vardata[x].d_reason == CRef_Undef) << " && " << level(x)
+                   << " > 0" << std::endl;
+  return vardata[x].d_reason == CRef_Undef && level(x) > 0;
+}
 
-inline int  Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; }
+inline int Solver::level(Var x) const
+{
+  assert(x < vardata.size());
+  return vardata[x].d_level;
+}
 
-inline int  Solver::user_level(Var x) const { assert(x < vardata.size()); return vardata[x].user_level; }
+inline int Solver::user_level(Var x) const
+{
+  assert(x < vardata.size());
+  return vardata[x].d_user_level;
+}
 
-inline int  Solver::intro_level(Var x) const { assert(x < vardata.size()); return vardata[x].intro_level; }
+inline int Solver::intro_level(Var x) const
+{
+  assert(x < vardata.size());
+  return vardata[x].d_intro_level;
+}
 
-inline int  Solver::trail_index(Var x) const { assert(x < vardata.size()); return vardata[x].trail_index; }
+inline int Solver::trail_index(Var x) const
+{
+  assert(x < vardata.size());
+  return vardata[x].d_trail_index;
+}
 
 inline void Solver::insertVarOrder(Var x) {
     assert(x < vardata.size());
@@ -522,7 +567,16 @@ inline bool     Solver::addClause       (Lit p, Lit q, bool removable, ClauseId&
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
                                                                 { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
 inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } }
+inline void Solver::newDecisionLevel()
+{
+  trail_lim.push(trail.size());
+  flipped.push(false);
+  d_context->push();
+  if (Dump.isOn("state"))
+  {
+    Dump("state") << CVC4::PushCommand();
+  }
+}
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }