From 584b38b87bbd1a52fb700465957e667f34b0a4db Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 13 Feb 2019 14:49:44 +0000
Subject: [PATCH] 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.
---
 src/util/simplify_expr.cpp         |  4 ++
 src/util/simplify_expr_boolean.cpp | 63 ++++++++++++++++++++++++++++++
 src/util/simplify_expr_class.h     |  1 +
 3 files changed, 68 insertions(+)

diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index c21b0d28250..ba5f0c47594 100644
--- a/src/util/simplify_expr.cpp
+++ b/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;
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index d7a92eb5a9d..a165316d9a8 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/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)
 {
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 2ff4bab6b9a..6f5caef8bbf 100644
--- a/src/util/simplify_expr_class.h
+++ b/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 &);