Initial work towards -Wshadow (#3817)

3 files changed, 65 insertions, 50 deletions

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 788545b3c..2632a6f38 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -962,7 +962,7 @@ void TheoryFp::check(Effort level) {
   while (!done() && !d_conflict) {
     // Get all the assertions
     Assertion assertion = get();
-    TNode fact = assertion.assertion;
+    TNode fact = assertion.d_assertion;
 
     Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl;
 
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 8854b400d..338c1c871 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -46,9 +46,12 @@ namespace rewrite {
   RewriteResponse then (TNode node, bool isPreRewrite) {
     RewriteResponse result(first(node, isPreRewrite));
 
-    if (result.status == REWRITE_DONE) {
-      return second(result.node, isPreRewrite);
-    } else {
+    if (result.d_status == REWRITE_DONE)
+    {
+      return second(result.d_node, isPreRewrite);
+    }
+    else
+    {
       return result;
     }
   }
@@ -1268,9 +1271,11 @@ TheoryFpRewriter::TheoryFpRewriter()
   RewriteResponse TheoryFpRewriter::preRewrite(TNode node) {
     Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl;
     RewriteResponse res = d_preRewriteTable[node.getKind()](node, true);
-    if (res.node != node) {
+    if (res.d_node != node)
+    {
       Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl;
-      Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after  " << res.node << std::endl;
+      Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after  "
+                          << res.d_node << std::endl;
     }
     return res;
   }
@@ -1301,46 +1306,52 @@ TheoryFpRewriter::TheoryFpRewriter()
   RewriteResponse TheoryFpRewriter::postRewrite(TNode node) {
     Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl;
     RewriteResponse res = d_postRewriteTable[node.getKind()](node, false);
-    if (res.node != node) {
+    if (res.d_node != node)
+    {
       Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl;
-      Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after  " << res.node << std::endl;
+      Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after  "
+                          << res.d_node << std::endl;
     }
 
-    if (res.status == REWRITE_DONE) {
+    if (res.d_status == REWRITE_DONE)
+    {
       bool allChildrenConst = true;
       bool apartFromRoundingMode = false;
       bool apartFromPartiallyDefinedArgument = false;
-      for (Node::const_iterator i = res.node.begin();
-	   i != res.node.end();
-	   ++i) {
-
-	if ((*i).getMetaKind() != kind::metakind::CONSTANT) {
+      for (Node::const_iterator i = res.d_node.begin(); i != res.d_node.end();
+           ++i)
+      {
+        if ((*i).getMetaKind() != kind::metakind::CONSTANT) {
 	  if ((*i).getType().isRoundingMode() && !apartFromRoundingMode) {
 	    apartFromRoundingMode = true;
-	  } else if ((res.node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL ||
-		      res.node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL ||
-		      res.node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL ||
-		      res.node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL ||
-		      res.node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL) &&
-		     ((*i).getType().isBitVector() ||
-		      (*i).getType().isReal()) &&
-		     !apartFromPartiallyDefinedArgument) {
-	    apartFromPartiallyDefinedArgument = true;
-	  } else {
-	    allChildrenConst = false;
+          }
+          else if ((res.d_node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL
+                    || res.d_node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL
+                    || res.d_node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL
+                    || res.d_node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL
+                    || res.d_node.getKind()
+                           == kind::FLOATINGPOINT_TO_REAL_TOTAL)
+                   && ((*i).getType().isBitVector() || (*i).getType().isReal())
+                   && !apartFromPartiallyDefinedArgument)
+          {
+            apartFromPartiallyDefinedArgument = true;
+          }
+          else
+          {
+            allChildrenConst = false;
 	    break;
-	  }
-	}
+          }
+        }
       }
 
       if (allChildrenConst) {
 	RewriteStatus rs = REWRITE_DONE;    // This is a bit messy because
-	Node rn = res.node;                 // RewriteResponse is too functional..
+        Node rn = res.d_node;  // RewriteResponse is too functional..
 
-	if (apartFromRoundingMode) {
-          if (!(res.node.getKind() == kind::EQUAL)
+        if (apartFromRoundingMode) {
+          if (!(res.d_node.getKind() == kind::EQUAL)
               &&  // Avoid infinite recursion...
-              !(res.node.getKind() == kind::ROUNDINGMODE_BITBLAST))
+              !(res.d_node.getKind() == kind::ROUNDINGMODE_BITBLAST))
           {  // Don't eliminate the bit-blast
             // We are close to being able to constant fold this
             // and in many cases the rounding mode really doesn't matter.
@@ -1354,16 +1365,15 @@ TheoryFpRewriter::TheoryFpRewriter()
 	    Node RTN(nm->mkConst(roundTowardNegative));
 	    Node RTP(nm->mkConst(roundTowardZero));
 
-	    TNode RM(res.node[0]);
-
-	    Node wRNE(res.node.substitute(RM, TNode(RNE)));
-	    Node wRNA(res.node.substitute(RM, TNode(RNA)));
-	    Node wRTZ(res.node.substitute(RM, TNode(RTZ)));
-	    Node wRTN(res.node.substitute(RM, TNode(RTN)));
-	    Node wRTP(res.node.substitute(RM, TNode(RTP)));
+            TNode RM(res.d_node[0]);
 
+            Node wRNE(res.d_node.substitute(RM, TNode(RNE)));
+            Node wRNA(res.d_node.substitute(RM, TNode(RNA)));
+            Node wRTZ(res.d_node.substitute(RM, TNode(RTZ)));
+            Node wRTN(res.d_node.substitute(RM, TNode(RTN)));
+            Node wRTP(res.d_node.substitute(RM, TNode(RTP)));
 
-	    rs = REWRITE_AGAIN_FULL;
+            rs = REWRITE_AGAIN_FULL;
 	    rn = nm->mkNode(kind::ITE,
 			    nm->mkNode(kind::EQUAL, RM, RNE),
 			    wRNE,
@@ -1380,19 +1390,24 @@ TheoryFpRewriter::TheoryFpRewriter()
 	  }
 	} else {
           RewriteResponse tmp =
-              d_constantFoldTable[res.node.getKind()](res.node, false);
-          rs = tmp.status;
-          rn = tmp.node;
-	}
+              d_constantFoldTable[res.d_node.getKind()](res.d_node, false);
+          rs = tmp.d_status;
+          rn = tmp.d_node;
+        }
 
 	RewriteResponse constRes(rs,rn);
 
-	if (constRes.node != res.node) {
-	  Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before constant fold " << res.node << std::endl;
-	  Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after constant fold " << constRes.node << std::endl;
-	}
-
-	return constRes;
+        if (constRes.d_node != res.d_node)
+        {
+          Debug("fp-rewrite")
+              << "TheoryFpRewriter::postRewrite(): before constant fold "
+              << res.d_node << std::endl;
+          Debug("fp-rewrite")
+              << "TheoryFpRewriter::postRewrite(): after constant fold "
+              << constRes.d_node << std::endl;
+        }
+
+        return constRes;
       }
     }
 
diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h
index 790e9d83d..732eeab0a 100644
--- a/src/theory/fp/theory_fp_rewriter.h
+++ b/src/theory/fp/theory_fp_rewriter.h
@@ -42,7 +42,7 @@ class TheoryFpRewriter : public TheoryRewriter
   Node rewriteEquality(TNode equality)
   {
     // often this will suffice
-    return postRewrite(equality).node;
+    return postRewrite(equality).d_node;
   }
 
  protected: