Merge pull request #1226 from diffblue/simplify_bitand_all_ones

simplifier: erase 'all ones' out of bitand

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -664,7 +664,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     result=false;
   }
 
-  // now erase zeros out of bitor, bitxor
+  // now erase 'all zeros' out of bitor, bitxor
 
   if(expr.id()==ID_bitor || expr.id()==ID_bitxor)
   {
@@ -683,6 +683,28 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     }
   }
 
+  // now erase 'all ones' out of bitand
+
+  if(expr.id()==ID_bitand)
+  {
+    for(exprt::operandst::iterator
+        it=expr.operands().begin();
+        it!=expr.operands().end();
+        ) // no it++
+    {
+      if(it->is_constant() &&
+         id2string(to_constant_expr(*it).get_value()).find('0')==
+           std::string::npos &&
+         expr.operands().size()>1)
+      {
+        it=expr.operands().erase(it);
+        result=false;
+      }
+      else
+        it++;
+    }
+  }
+
   // two operands that are syntactically the same
 
   if(expr.operands().size()==2 &&