[wp] improves forall_intro

src/plugins/wp/Conditions.ml

@@ -478,6 +478,13 @@ let rec forall_intro p =
       let hs = exist_intros hs in
       let hp,p = forall_intro p in
       hs @ hp , p
+  | Or qs -> (* analogy with Imply *)
+      let hps,ps = List.fold_left (fun (hs,ps) q ->
+          let hp,p = forall_intro q in (* q <==> (hp ==> p) *)
+          (hp @ hs), (p::ps)) ([],[]) qs
+      in (* ORs qs  <==> ORs (hps ==> ps)
+                    <==> ((ANDs hps) ==> ORs ps) *)
+      hps, (p_disj ps)
   | _ -> [] , p
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle

@@ -29,14 +29,12 @@
        /\ (P_A \/ P_A1 \/ P_A2 \/ P_B1 \/ P_B2 \/ P_C)
 [wp] [Alt-Ergo] Goal typed_f_ensures_a6 : Valid
 [wp:cnf] 
-  CNF=((not P_A) \/ (not P_A1) \/ P_A2 \/ P_C)
-       /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B) \/ P_C)
-       /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B1) \/ P_C)
-       /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ P_B2 \/ P_C)
-       /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B) \/ (not P_B1) \/ P_B2)
-       /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B) \/ (not P_B1) \/ P_C)
-       /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B) \/ P_B2 \/ P_C)
-       /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B1) \/ P_B2 \/ P_C)
+  CNF=(P_A2 \/ P_C) /\ (P_A2 \/ (not P_B) \/ P_C)
+       /\ (P_A2 \/ (not P_B1) \/ P_C) /\ (P_A2 \/ P_B2 \/ P_C)
+       /\ (P_A2 \/ (not P_B) \/ (not P_B1) \/ P_B2)
+       /\ (P_A2 \/ (not P_B) \/ (not P_B1) \/ P_C)
+       /\ (P_A2 \/ (not P_B) \/ P_B2 \/ P_C)
+       /\ (P_A2 \/ (not P_B1) \/ P_B2 \/ P_C)
 [wp] [Alt-Ergo] Goal typed_f_ensures_a7 : Valid
 [wp:cnf] 
   CNF=((not P_A1) \/ P_A2 \/ P_C) /\ (P_A1 \/ (not P_A2) \/ P_C)
@@ -145,8 +143,8 @@
 [wp] [Alt-Ergo] Goal typed_f_ensures_c0 : Valid
 [wp:cnf] CNF=P_B \/ P_B1 \/ P_B2 \/ P_C
 [wp] [Qed] Goal typed_f_ensures_c1 : Valid
-[wp:cnf] CNF=(not P_B) \/ (not P_B1) \/ P_B2 \/ P_C
-[wp] [Alt-Ergo] Goal typed_f_ensures_c2 : Valid
+[wp:cnf] CNF=P_B2 \/ P_C
+[wp] [Qed] Goal typed_f_ensures_c2 : Valid
 [wp:cnf] CNF=((not P_B1) \/ P_B2 \/ P_C) /\ (P_B1 \/ (not P_B2) \/ P_C)
 [wp] [Alt-Ergo] Goal typed_f_ensures_c3 : Valid
 [wp:cnf] 
@@ -301,12 +299,12 @@
 [wp:cnf] CNF=P_C /\ ((not P_B) \/ P_C) /\ ((not P_A) \/ (not P_B) \/ P_C)
 [wp] [Alt-Ergo] Goal typed_f_ensures_e2 : Valid
 [wp] Proved goals:   43 / 43
-  Qed:            11 
-  Alt-Ergo:       32
+  Qed:            12 
+  Alt-Ergo:       31
 [wp] Report in:  'tests/wp_acsl/oracle_qualif/cnf.0.report.json'
 [wp] Report out: 'tests/wp_acsl/result_qualif/cnf.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
-f                   11     32 (336..384)    43       100%
+f                   12     31 (336..384)    43       100%
 -------------------------------------------------------------
 [wp] Logging keys: success-only,shell,cnf.

src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle

@@ -175,7 +175,7 @@ Prove: (i + L_f(i)) != b.
 ------------------------------------------------------------
 
 Goal Post-condition 'ko4' in 'forall':
-Prove: P_P(i) \/ (forall i_1 : Z. L_f(i_1) != i).
+Prove: (L_f(i) != i_1) \/ P_P(i_1).
 
 ------------------------------------------------------------
 

src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle

@@ -119,7 +119,7 @@ hash                 6      1 (12..24)       7       100%
 size                 2     -                 2       100%
 init                 8      5 (72..96)      13       100%
 add                 24     15 (384..432)    39       100%
-mem_binding         18      8 (192..240)    26       100%
+mem_binding         18      8 (336..384)    26       100%
 -------------------------------------------------------------
 [wp] Running WP plugin...
 [rte] annotating function add

src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle

@@ -43,7 +43,7 @@
 [wp] Report out: 'tests/wp_typed/result_qualif/user_init.1.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
-init_t2_v2           3     -  (16..28)       8       100%
+init_t2_v2           3     -  (20..32)       8       100%
 init_t2_v3           4     -  (20..32)       7       100%
 init_t2_bis_v2       4     -  (28..40)       8       100%
 -------------------------------------------------------------