Fix -Wshadow warnings in common headers (#3826)

7 files changed, 38 insertions, 28 deletions

diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 047396506..463203118 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -867,8 +867,9 @@ void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>*
   std::vector<T> bits;
   bb->bbTerm(node[0], bits);
   
-  T sign_bit = bits.back(); 
-  unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; 
+  T sign_bit = bits.back();
+  unsigned amount =
+      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
 
   for (unsigned i = 0; i < bits.size(); ++i ) {
     res_bits.push_back(bits[i]); 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 22a12cc10..27fad165f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -452,7 +452,8 @@ template<> inline
 Node RewriteRule<EvalSignExtend>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
-  unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; 
+  unsigned amount =
+      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
   BitVector res = a.signExtend(amount);
   
   return utils::mkConst(res);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index aef20ee0a..6be1e7203 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -200,7 +200,8 @@ inline Node RewriteRule<RepeatEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
-  unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorRepeat>().d_repeatAmount;
   Assert(amount >= 1);
   if(amount == 1) {
     return a; 
@@ -224,7 +225,8 @@ inline Node RewriteRule<RotateLeftEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
-  unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
   amount = amount % utils::getSize(a); 
   if (amount == 0) {
     return a; 
@@ -248,7 +250,8 @@ inline Node RewriteRule<RotateRightEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
-  unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorRotateRight>().d_rotateRightAmount;
   amount = amount % utils::getSize(a); 
   if (amount == 0) {
     return a; 
@@ -506,7 +509,8 @@ inline Node RewriteRule<ZeroExtendEliminate>::apply(TNode node)
   Debug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
 
   TNode bv = node[0];
-  unsigned amount = node.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
   if (amount == 0) {
     return node[0]; 
   }
@@ -527,7 +531,8 @@ inline Node RewriteRule<SignExtendEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
 
-  unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+  unsigned amount =
+      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
   if(amount == 0) {
     return node[0]; 
   }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index c3e1b316c..9e6c31061 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1619,12 +1619,14 @@ template<> inline
 Node RewriteRule<MergeSignExtend>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl;
   unsigned amount1 =
-      node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
 
   NodeManager* nm = NodeManager::currentNM();
   if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
-    unsigned amount2 =
-        node[0].getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+    unsigned amount2 = node[0]
+                           .getOperator()
+                           .getConst<BitVectorZeroExtend>()
+                           .d_zeroExtendAmount;
     if (amount2 == 0)
     {
       NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
@@ -1642,7 +1644,7 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
   }
   Assert(node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND);
   unsigned amount2 =
-      node[0].getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+      node[0].getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
   return utils::mkSignExtend(node[0][0], amount1 + amount2);
 }
 
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 9d5c6f396..97b7a8a8f 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -240,7 +240,7 @@ class BitVectorBitOfTypeRule
       {
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
-      if (info.bitIndex >= t.getBitVectorSize())
+      if (info.d_bitIndex >= t.getBitVectorSize())
       {
         throw TypeCheckingExceptionPrivate(
             n, "extract index is larger than the bitvector size");
@@ -262,7 +262,7 @@ class BitVectorExtractTypeRule
     // NOTE: We're throwing a type-checking exception here even
     // if check is false, bc if we allow high < low the resulting
     // type will be illegal
-    if (extractInfo.high < extractInfo.low)
+    if (extractInfo.d_high < extractInfo.d_low)
     {
       throw TypeCheckingExceptionPrivate(
           n, "high extract index is smaller than the low extract index");
@@ -275,13 +275,14 @@ class BitVectorExtractTypeRule
       {
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
-      if (extractInfo.high >= t.getBitVectorSize())
+      if (extractInfo.d_high >= t.getBitVectorSize())
       {
         throw TypeCheckingExceptionPrivate(
             n, "high extract index is bigger than the size of the bit-vector");
       }
     }
-    return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
+    return nodeManager->mkBitVectorType(extractInfo.d_high - extractInfo.d_low
+                                        + 1);
   }
 }; /* class BitVectorExtractTypeRule */
 
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 44510c26b..b98aacb2f 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -43,17 +43,17 @@ const bool getBit(TNode node, unsigned i)
 
 unsigned getExtractHigh(TNode node)
 {
-  return node.getOperator().getConst<BitVectorExtract>().high;
+  return node.getOperator().getConst<BitVectorExtract>().d_high;
 }
 
 unsigned getExtractLow(TNode node)
 {
-  return node.getOperator().getConst<BitVectorExtract>().low;
+  return node.getOperator().getConst<BitVectorExtract>().d_low;
 }
 
 unsigned getSignExtendAmount(TNode node)
 {
-  return node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+  return node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
 }
 
 /* ------------------------------------------------------------------------- */
@@ -483,7 +483,7 @@ Node eliminateBv2Nat(TNode node)
 
 Node eliminateInt2Bv(TNode node)
 {
-  const uint32_t size = node.getOperator().getConst<IntToBitVector>().size;
+  const uint32_t size = node.getOperator().getConst<IntToBitVector>().d_size;
   NodeManager* const nm = NodeManager::currentNM();
   const Node bvzero = utils::mkZero(1);
   const Node bvone = utils::mkOne(1);
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 59e9aedcb..92f3e6d0d 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -619,14 +619,14 @@ struct SortBvExtractInterval
     Assert(j.getKind() == BITVECTOR_EXTRACT);
     BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>();
     BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>();
-    if (ie.high > je.high)
+    if (ie.d_high > je.d_high)
     {
       return true;
     }
-    else if (ie.high == je.high)
+    else if (ie.d_high == je.d_high)
     {
-      Assert(ie.low != je.low);
-      return ie.low > je.low;
+      Assert(ie.d_low != je.d_low);
+      return ie.d_low > je.d_low;
     }
     return false;
   }
@@ -675,15 +675,15 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
         Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i] << std::endl;
         BitVectorExtract e =
             curr_vec[i].getOperator().getConst<BitVectorExtract>();
-        if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
+        if (std::find(boundaries.begin(), boundaries.end(), e.d_high + 1)
             == boundaries.end())
         {
-          boundaries.push_back(e.high + 1);
+          boundaries.push_back(e.d_high + 1);
         }
-        if (std::find(boundaries.begin(), boundaries.end(), e.low)
+        if (std::find(boundaries.begin(), boundaries.end(), e.d_low)
             == boundaries.end())
         {
-          boundaries.push_back(e.low);
+          boundaries.push_back(e.d_low);
         }
       }
       std::sort(boundaries.rbegin(), boundaries.rend());