Merge pull request #4990 from diffblue/boolean_negate

use simplify_not instead of boolean_negate

Author: Daniel Kroening

src/util/simplify_expr_boolean.cpp

@@ -40,7 +40,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
 
     binary_exprt new_expr = implies_expr;
     new_expr.id(ID_or);
-    new_expr.op0() = boolean_negate(new_expr.op0());
+    new_expr.op0() = simplify_not(not_exprt(new_expr.op0()));
     return changed(simplify_node(new_expr));
   }
   else if(expr.id()==ID_xor)
@@ -82,7 +82,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
     else if(new_operands.size() == 1)
     {
       if(negate)
-        return boolean_negate(new_operands.front());
+        return changed(simplify_not(not_exprt(new_operands.front())));
       else
         return std::move(new_operands.front());
     }
@@ -191,7 +191,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
 
     Forall_operands(it, tmp)
     {
-      *it = simplify_node(boolean_negate(*it));
+      *it = simplify_not(not_exprt(*it));
     }
 
     tmp.id(tmp.id() == ID_and ? ID_or : ID_and);

src/util/simplify_expr_if.cpp

@@ -350,7 +350,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
       else if(truevalue.is_false() && falsevalue.is_true())
       {
         // a?0:1 <-> !a
-        return changed(simplify_node(boolean_negate(cond)));
+        return changed(simplify_not(not_exprt(cond)));
       }
       else if(falsevalue.is_false())
       {
@@ -360,8 +360,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
       else if(falsevalue.is_true())
       {
         // a?b:1 <-> !a OR b
-        return changed(simplify_node(
-          or_exprt(simplify_node(boolean_negate(cond)), truevalue)));
+        return changed(
+          simplify_node(or_exprt(simplify_not(not_exprt(cond)), truevalue)));
       }
       else if(truevalue.is_true())
       {
@@ -371,8 +371,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
       else if(truevalue.is_false())
       {
         // a?0:b <-> !a && b
-        return changed(simplify_node(
-          and_exprt(simplify_node(boolean_negate(cond)), falsevalue)));
+        return changed(
+          simplify_node(and_exprt(simplify_not(not_exprt(cond)), falsevalue)));
       }
     }
   }

src/util/simplify_expr_int.cpp

@@ -1481,8 +1481,7 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
     auto new_expr = expr;
     new_expr.id(ID_equal);
     new_expr = simplify_inequality_no_constant(new_expr);
-    new_expr = boolean_negate(new_expr);
-    return changed(simplify_node(new_expr));
+    return changed(simplify_not(not_exprt(new_expr)));
   }
   else if(expr.id()==ID_gt)
   {
@@ -1491,16 +1490,14 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
     // swap operands
     new_expr.op0().swap(new_expr.op1());
     new_expr = simplify_inequality_no_constant(new_expr);
-    new_expr = boolean_negate(new_expr);
-    return changed(simplify_node(new_expr));
+    return changed(simplify_not(not_exprt(new_expr)));
   }
   else if(expr.id()==ID_lt)
   {
     auto new_expr = expr;
     new_expr.id(ID_ge);
     new_expr = simplify_inequality_no_constant(new_expr);
-    new_expr = boolean_negate(new_expr);
-    return changed(simplify_node(new_expr));
+    return changed(simplify_not(not_exprt(new_expr)));
   }
   else if(expr.id()==ID_le)
   {
@@ -1616,8 +1613,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
       auto new_expr = expr;
       new_expr.id(ID_equal);
       new_expr = simplify_inequality_rhs_is_constant(new_expr);
-      new_expr = boolean_negate(new_expr);
-      return changed(simplify_node(new_expr));
+      return changed(simplify_not(not_exprt(new_expr)));
     }
 
     // very special case for pointers
@@ -1806,7 +1802,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
     // we re-write (TYPE)boolean == 0 -> !boolean
     if(expr.op1().is_zero() && expr.id()==ID_equal)
     {
-      return boolean_negate(expr.op0().op0());
+      return changed(simplify_not(not_exprt(expr.op0().op0())));
     }
 
     // we re-write (TYPE)boolean != 0 -> boolean
@@ -1829,8 +1825,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
       auto new_expr = expr;
       new_expr.id(ID_equal);
       new_expr = simplify_inequality_rhs_is_constant(new_expr);
-      new_expr = boolean_negate(new_expr);
-      return changed(simplify_node(new_expr));
+      return changed(simplify_not(not_exprt(new_expr)));
     }
     else if(expr.id()==ID_gt)
     {
@@ -1852,8 +1847,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
       auto new_expr = expr;
       new_expr.id(ID_ge);
       new_expr = simplify_inequality_rhs_is_constant(new_expr);
-      new_expr = boolean_negate(new_expr);
-      return changed(simplify_node(new_expr));
+      return changed(simplify_not(not_exprt(new_expr)));
     }
     else if(expr.id()==ID_le)
     {
@@ -1869,8 +1863,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
       ++i;
       new_expr.op1() = from_integer(i, new_expr.op1().type());
       new_expr = simplify_inequality_rhs_is_constant(new_expr);
-      new_expr = boolean_negate(new_expr);
-      return changed(simplify_node(new_expr));
+      return changed(simplify_not(not_exprt(new_expr)));
     }
   }
 #endif