Merge pull request #3923 from tautschnig/simplify-forall

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

Author: tautschnig

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/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;
 }