From bb2deed142d63d9433bd6b1c884c5bed27e01768 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Sat, 20 Jul 2024 12:39:43 +0200 Subject: [PATCH 1/2] Define form_size in coq and add more info on the benchmark It will now also display the sum of all the sizes of the formulas before and after the simplification, and the time it took to simplify them and to compute their interpolants. --- bin/benchmark.ml | 34 ++++++++++++--------------- theories/extraction/UIML_extraction.v | 2 +- theories/iSL/Formulas.v | 10 ++++++++ 3 files changed, 26 insertions(+), 20 deletions(-) diff --git a/bin/benchmark.ml b/bin/benchmark.ml index 2b311c8..4e9ed5f 100644 --- a/bin/benchmark.ml +++ b/bin/benchmark.ml @@ -11,14 +11,6 @@ type bench_info = { after : int timed_result; } -let rec form_size = function - | Var _ -> 1 - | Bot -> 1 - | Or (f1, f2) -> 1 + form_size f1 + form_size f2 - | And (f1, f2) -> 1 + form_size f1 + form_size f2 - | Implies (f1, f2) -> 1 + form_size f1 + form_size f2 - | Box f -> 1 + form_size f - let percentage_reduction before after = 100. -. (after /. before *. 100.) let time f x = @@ -43,13 +35,13 @@ let bench_one fs = [ { name = "A " ^ fs; - before = { value = form_size resA.value; time = resA.time }; - after = { value = form_size simpA.value; time = simpA.time }; + before = { value = form_size resA.value |> int_of_nat; time = resA.time }; + after = { value = form_size simpA.value |> int_of_nat; time = simpA.time }; }; { name = "E " ^ fs; - before = { value = form_size resE.value; time = resE.time }; - after = { value = form_size simpE.value; time = simpE.time }; + before = { value = form_size resE.value |> int_of_nat; time = resE.time }; + after = { value = form_size simpE.value |> int_of_nat; time = simpE.time }; }; ] @@ -60,15 +52,19 @@ let print_bench_value_info benches = computation time (s)|\n\ |--|--|--|--|--|--|\n"; List.iter print_value_results benches; - print_newline (); - - let sum_before = - List.fold_left (fun acc x -> acc + x.before.value) 0 benches + let sum_before, sum_after, sum_comp_time, sum_simp_time = + List.fold_left + (fun (sum_before, sum_after, sum_comp_time, sum_simp_time) bench -> + ( sum_before + bench.before.value, + sum_after + bench.after.value, + bench.before.time +. sum_comp_time, + bench.after.time +. sum_simp_time )) + (0, 0, 0., 0.) benches in - let sum_after = List.fold_left (fun acc x -> acc + x.after.value) 0 benches in - - Printf.printf "Average percentage reduction: %.2f\n" + Printf.printf "| Total | %d | %d | %.2f | %.4f | %.4f |\n" sum_before + sum_after (percentage_reduction (float_of_int sum_before) (float_of_int sum_after)) + sum_comp_time sum_simp_time let bench l = let benches = List.map bench_one l |> List.flatten in diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v index 231e955..a84e900 100644 --- a/theories/extraction/UIML_extraction.v +++ b/theories/extraction/UIML_extraction.v @@ -41,5 +41,5 @@ Definition isl_simplified_A v f := A_simplified v f. Set Extraction Output Directory "extraction". -Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A Formulas.weight isl_simp. +Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A Formulas.weight Formulas.form_size isl_simp. diff --git a/theories/iSL/Formulas.v b/theories/iSL/Formulas.v index ca5da0e..8854bc8 100644 --- a/theories/iSL/Formulas.v +++ b/theories/iSL/Formulas.v @@ -135,3 +135,13 @@ Global Instance irreflexive_form_order : Irreflexive form_order. Proof. unfold form_order. intros x y. lia. Qed. Notation "φ ≺f ψ" := (form_order ψ φ) (at level 149). + + +Fixpoint form_size (φ : form) : nat := match φ with +| ⊥ => 1 +| Var _ => 1 +| φ ∧ ψ => 1 + form_size φ + form_size ψ +| φ ∨ ψ => 1 + form_size φ + form_size ψ +| φ → ψ => 1 + form_size φ + form_size ψ +| □φ => 1 + form_size φ +end. From e54184a2e8b27298cc3598b8bf4e334ea4fb640e Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Sat, 20 Jul 2024 12:40:52 +0200 Subject: [PATCH 2/2] Prove that simplifications reduce the size of formulas --- theories/iSL/Simp.v | 77 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 76 insertions(+), 1 deletion(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index eabe41a..5085d8e 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -843,7 +843,7 @@ clear Heqw. revert φ Hle. induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]; destruct φ; simpl; try (split ; apply generalised_axiom); [eapply (simp_equiv_and φ1 φ2)| - eapply (simp_equiv_or φ1 φ2)| + eapply (simp_equiv_or φ1 φ2) | eapply (simp_equiv_imp φ1 φ2)| eapply simp_equiv_box]; apply IHw; @@ -1070,6 +1070,81 @@ Qed. +Lemma simp_simplifies_conj_disj φ ψ: + (form_size (φ ⊼ ψ) ≤ 1 + form_size φ + form_size ψ) * + (form_size (φ ⊻ ψ) ≤ 1 + form_size φ + form_size ψ). +Proof. +split; [unfold simp_and | unfold simp_or]; destruct φ; destruct ψ; +repeat match goal with + | |- form_size (choose_or _ _) ≤ _ => unfold choose_or + | |- form_size (choose_and _ _) ≤ _ => unfold choose_and + | |- form_size (match ?x with _ => _ end) ≤ _ => destruct x + | _ => simpl; lia +end. +Qed. + + +Ltac large_conj_disj_solver := +match goal with + | |- form_size (?simp_f ?x (?connector ?φ1 ?φ2)) ≤ _ => + assert (H: form_size (simp_f x (connector φ1 φ2)) ≤ 1 + (form_size x + (1 + form_size φ1 + form_size φ2))) + by apply simp_simplifies_conj_disj; + simpl in H; lia + + | IHφ2 : ∀ ψ : form, form_size (?simp_f_large ?φ2 ψ) ≤ form_size (?connector ?φ2 ψ) + |- form_size (?simp_f ?φ1 (?simp_f ?ψ0_1 (?simp_f_large ?φ2 ?ψ0_2))) ≤ _ => + assert (H1: form_size (simp_f φ1 (simp_f ψ0_1 ( simp_f_large φ2 ψ0_2))) ≤ 1 + form_size φ1 + form_size (simp_f ψ0_1 (simp_f_large φ2 ψ0_2))) + by apply simp_simplifies_conj_disj; + assert (H2: form_size ((simp_f ψ0_1 (simp_f_large φ2 ψ0_2))) ≤ 1 + form_size (ψ0_1) + form_size (simp_f_large φ2 ψ0_2)) + by apply simp_simplifies_conj_disj; + assert ( H3: form_size (simp_f_large φ2 ψ0_2) ≤ 1 + form_size φ2 + form_size ψ0_2) by apply IHφ2; + lia + + | _ => lia +end. + +Lemma simp_simplifies_ands φ ψ: + form_size (simp_ands φ ψ) ≤ form_size (And φ ψ). +Proof. +generalize ψ. +induction φ; intro ψ0; destruct ψ0; try apply simp_simplifies_conj_disj; simpl; +large_conj_disj_solver. +Qed. + +Lemma simp_simplifies_ors φ ψ: + form_size (simp_ors φ ψ) ≤ form_size (Or φ ψ). +Proof. +generalize ψ. +induction φ; intro ψ0; destruct ψ0; try apply simp_simplifies_conj_disj; simpl; +large_conj_disj_solver. +Qed. + +Lemma simp_simplifies_imp φ ψ: + form_size (simp_imp φ ψ) ≤ form_size (Implies φ ψ). +Proof. +unfold simp_or. +destruct φ; destruct ψ; unfold simp_imp; +repeat match goal with + | |- form_size (if decide _ then _ else _) ≤ _=> case decide; intro + | _ => simpl; lia +end. +Qed. + +Theorem simp_simplifies φ: + form_size (simp φ) <= form_size φ. +Proof. +induction φ; auto; simpl; +[ assert (H: form_size (simp_ands (simp φ1) (simp φ2)) ≤ S (form_size (simp φ1) + form_size (simp φ2))) + by apply simp_simplifies_ands| + assert (H: form_size (simp_ors (simp φ1) (simp φ2)) ≤ S (form_size (simp φ1) + form_size (simp φ2))) + by apply simp_simplifies_ors| + assert (H: form_size (simp_imp (simp φ1) (simp φ2)) ≤ S (form_size (simp φ1) + form_size (simp φ2))) + by apply simp_simplifies_imp| + idtac +]; lia. +Qed. + + Require Import String. Local Open Scope string_scope.