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

@@ -2936,6 +2936,10 @@ simplify_exprt::simplify_node_preorder(const exprt &expr)
   {
     result = simplify_unary_pointer_predicate_preorder(to_unary_expr(expr));
   }
+  else if(expr.id() == ID_not)
+  {
+    result = simplify_not_preorder(to_not_expr(expr));
+  }
   else if(expr.has_operands())
   {
     std::optional<exprt::operandst> new_operands;

src/util/simplify_expr_boolean.cpp

@@ -378,6 +378,69 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
   return unchanged(expr);
 }
 
+simplify_exprt::resultt<>
+simplify_exprt::simplify_not_preorder(const not_exprt &expr)
+{
+  const exprt &op = expr.op();
+
+  if(!expr.is_boolean() || !op.is_boolean())
+  {
+    return unchanged(expr);
+  }
+
+  if(op.id() == ID_not) // (not not a) == a
+  {
+    return changed(simplify_rec(to_not_expr(op).op()));
+  }
+  else if(op.is_false())
+  {
+    return true_exprt{};
+  }
+  else if(op.is_true())
+  {
+    return false_exprt{};
+  }
+  else if(op.id() == ID_and || op.id() == ID_or)
+  {
+    exprt tmp = op;
+
+    Forall_operands(it, tmp)
+    {
+      *it = boolean_negate(*it);
+    }
+
+    tmp.id(tmp.id() == ID_and ? ID_or : ID_and);
+
+    return changed(simplify_rec(tmp));
+  }
+  else if(op.id() == ID_notequal) // !(a!=b) <-> a==b
+  {
+    exprt tmp = op;
+    tmp.id(ID_equal);
+    return changed(simplify_rec(tmp));
+  }
+  else if(op.id() == ID_exists) // !(exists: a) <-> forall: not a
+  {
+    auto const &op_as_exists = to_exists_expr(op);
+    return changed(simplify_rec(
+      forall_exprt{op_as_exists.symbol(), not_exprt{op_as_exists.where()}}));
+  }
+  else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
+  {
+    auto const &op_as_forall = to_forall_expr(op);
+    return changed(simplify_rec(
+      exists_exprt{op_as_forall.symbol(), not_exprt{op_as_forall.where()}}));
+  }
+
+  auto op_result = simplify_rec(op);
+  if(!op_result.has_changed())
+    return unchanged(expr);
+
+  not_exprt tmp = expr;
+  tmp.op() = std::move(op_result.expr);
+  return std::move(tmp);
+}
+
 simplify_exprt::resultt<>
 simplify_exprt::simplify_quantifier_expr(const quantifier_exprt &expr)
 {

src/util/simplify_expr_class.h

@@ -174,6 +174,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 &);
+  [[nodiscard]] resultt<> simplify_not_preorder(const not_exprt &expr);
   [[nodiscard]] resultt<> simplify_boolean(const exprt &);
   [[nodiscard]] virtual resultt<>
   simplify_inequality(const binary_relation_exprt &);