Perform simplification of not_exprt as preorder step

Each of the possible simplifications has an impact on its operands,
which in turn mostly needs to be simplified. Instead of doing this again
(as the operand has already been simplified), do most of the work as a
preorder step so that only the modified operand is subject to
simplification.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -2735,6 +2735,8 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
     result=simplify_if_preorder(to_if_expr(expr));
   else if(expr.id() == ID_typecast)
     result = simplify_typecast_preorder(to_typecast_expr(expr));
+  else if(expr.id() == ID_not)
+    result = simplify_not_preorder(to_not_expr(expr));
   else
   {
     if(expr.has_operands())

src/util/simplify_expr_boolean.cpp

@@ -377,3 +377,85 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
 
   return unchanged(expr);
 }
+
+bool simplify_exprt::simplify_not_preorder(not_exprt &expr)
+{
+  exprt &op = expr.op();
+
+  if(!expr.is_boolean() || !op.is_boolean())
+  {
+    return true;
+  }
+
+  if(op.id() == ID_not) // (not not a) == a
+  {
+    if(as_const(op).operands().size() == 1)
+    {
+      exprt tmp = simplify_rec(to_not_expr(op).op()).expr;
+      expr.swap(tmp);
+      return false;
+    }
+  }
+  else if(op.is_false())
+  {
+    true_exprt tmp;
+    expr.swap(tmp);
+    return false;
+  }
+  else if(op.is_true())
+  {
+    false_exprt tmp;
+    expr.swap(tmp);
+    return false;
+  }
+  else if(op.id() == ID_and || op.id() == ID_or)
+  {
+    Forall_operands(it, op)
+    {
+      *it = boolean_negate(*it);
+    }
+
+    op.id(op.id() == ID_and ? ID_or : ID_and);
+
+    exprt tmp = simplify_rec(op);
+    expr.swap(tmp);
+
+    return false;
+  }
+  else if(op.id() == ID_notequal) // !(a!=b) <-> a==b
+  {
+    op.id(ID_equal);
+    exprt tmp = simplify_rec(op).expr;
+    expr.swap(tmp);
+    return false;
+  }
+  else if(op.id() == ID_exists) // !(exists: a) <-> forall: not a
+  {
+    auto const &op_as_exists = to_exists_expr(op);
+    exprt rewritten_op =
+      simplify_rec(
+        forall_exprt{op_as_exists.symbol(), not_exprt{op_as_exists.where()}})
+        .expr;
+    expr.swap(rewritten_op);
+    return false;
+  }
+  else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
+  {
+    auto const &op_as_forall = to_forall_expr(op);
+    exprt rewritten_op =
+      simplify_rec(
+        exists_exprt{op_as_forall.symbol(), not_exprt{op_as_forall.where()}})
+        .expr;
+    expr.swap(rewritten_op);
+    return false;
+  }
+
+  auto op_result = simplify_rec(op);
+  if(op_result.has_changed())
+  {
+    op = op_result.expr;
+    return false;
+  }
+  else
+    return true;
+}

src/util/simplify_expr_class.h

@@ -167,6 +167,7 @@ class simplify_exprt
   NODISCARD resultt<> simplify_if(const if_exprt &);
   NODISCARD resultt<> simplify_bitnot(const bitnot_exprt &);
   NODISCARD resultt<> simplify_not(const not_exprt &);
+  bool simplify_not_preorder(not_exprt &expr);
   NODISCARD resultt<> simplify_boolean(const exprt &);
   NODISCARD resultt<> simplify_inequality(const binary_relation_exprt &);
   NODISCARD resultt<>