Rewrite !forall expressions in the simplifier [depends-on: #3922]

regression/cbmc/Quantifiers-simplify/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  __CPROVER_assert(
+    !__CPROVER_forall {
+      int i;
+      i >= 0
+    },
+    "simplify");
+
+  return 0;
+}

regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--program-only
+ASSERT\(exists \{ signed int i!0#0; !\(i!0#0 >= 0\) \}\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-simplify/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/util/mathematical_expr.h

@@ -337,6 +337,24 @@ class forall_exprt : public quantifier_exprt
   }
 };
 
+inline const forall_exprt &to_forall_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_forall);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "forall expressions have exactly two operands");
+  return static_cast<const forall_exprt &>(expr);
+}
+
+inline forall_exprt &to_forall_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_forall);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "forall expressions have exactly two operands");
+  return static_cast<forall_exprt &>(expr);
+}
+
 /// \brief An exists expression
 class exists_exprt : public quantifier_exprt
 {

src/util/simplify_expr_boolean.cpp

@@ -222,6 +222,15 @@ bool simplify_exprt::simplify_not(exprt &expr)
     expr = rewritten_op;
     return false;
   }
+  else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
+  {
+    auto const &op_as_forall = to_forall_expr(op);
+    exists_exprt rewritten_op(
+      op_as_forall.symbol(), not_exprt(op_as_forall.where()));
+    simplify_node(rewritten_op.where());
+    expr = rewritten_op;
+    return false;
+  }
 
   return true;
 }