Merge pull request #14 from Yag000/simp

Simplifications

bin/benchmark.ml

@@ -0,0 +1,115 @@
+open UIML.UIML_extraction
+open UIML.Formulas
+open Modal_expressions_parser
+
+let rec weight = function
+  | Bot -> 1
+  | Var _ -> 1
+  | And (f1, f2) -> 2 + weight f1 + weight f2
+  | Or (f1, f2) -> 3 + weight f1 + weight f2
+  | Implies (f1, f2) -> 1 + weight f1 + weight f2
+  | Box f -> 1 + weight f
+
+type 'a timed_result = { value : 'a; time : float }
+
+type bench_info = {
+  name : string;
+  before : int timed_result;
+  after : int timed_result;
+}
+
+let percentage_reduction before after = 100. -. (after /. before *. 100.)
+let percentage_increase before after = (after /. before *. 100.) -. 100.
+
+let time f x =
+  let t = Sys.time () in
+  let fx = f x in
+  { value = fx; time = Sys.time () -. t }
+
+let print_value_results { name; before; after } =
+  Printf.printf "| %s | %d | %d | %.2f |\n" name before.value after.value
+    (percentage_reduction
+       (float_of_int before.value)
+       (float_of_int after.value))
+
+let print_time_results { name; before; after } =
+  Printf.printf "| %s | %.4f | %.4f | %.2f |\n" name before.time after.time
+    (percentage_increase before.time after.time)
+
+let bench_one fs =
+  let f = eval fs in
+  [
+    {
+      name = "A " ^ fs;
+      before = time (fun f -> weight (isl_A [ 'p' ] f)) f;
+      after = time (fun f -> weight (isl_simplified_A [ 'p' ] f)) f;
+    };
+    {
+      name = "E " ^ fs;
+      before = time (fun f -> weight (isl_E [ 'p' ] f)) f;
+      after = time (fun f -> weight (isl_simplified_E [ 'p' ] f)) f;
+    };
+  ]
+
+let average f l =
+  let total, len =
+    List.fold_left (fun (total, len) e -> (f e +. total, len + 1)) (0., 0) l
+  in
+  total /. float_of_int len
+
+let print_bench_value_info benches =
+  Printf.printf
+    "| Formula | Interpolant weight | Simplified interpolant weight | \
+     Percentage reduction |\n\
+     |--|--|--|--|\n";
+  List.iter print_value_results benches;
+  print_newline ();
+  Printf.printf "Average percentage reduction: %.2f\n"
+    (average
+       (fun { before; after; _ } ->
+         percentage_reduction
+           (float_of_int before.value)
+           (float_of_int after.value))
+       benches)
+
+let print_bench_time_info benches =
+  Printf.printf
+    "| Formula | Interpolant computation time (s) | Simplified interpolant \
+     computation time (s) | Percentage increase |\n\
+     |--|--|--|--|\n";
+  List.iter print_time_results benches;
+  print_newline ();
+  Printf.printf "Average percentage increase: %.2f\n"
+    (average
+       (fun { before; after; _ } -> percentage_increase before.time after.time)
+       benches);
+  Printf.printf "Average absolute time increase (s): %.5f\n"
+    (average (fun { before; after; _ } -> after.time -. before.time) benches)
+
+let bench l =
+  let benches = List.map bench_one l |> List.flatten in
+  print_bench_value_info benches;
+  print_newline ();
+  print_bench_time_info benches
+
+let test_cases =
+  [
+    "(p ∧ q) -> ~p";
+    "t ∨ q ∨ t";
+    "~((F & p) -> ~p | F)";
+    "(q -> p) & (p -> ~r)";
+    "(q -> (p -> r)) -> r";
+    "((q -> p) -> r) -> r";
+    "(a → (q ∧ r)) → s";
+    "(a → (q ∧ r)) → ~p";
+    "(a → (q ∧ r)) → ~p → k";
+    "(q -> (p -> r)) -> ~t";
+    "(q -> (p -> r)) -> ~t";
+    "(q → (q ∧ (k -> p)) -> k)";
+    "(q -> (p ∨  r)) -> ~(t ∨ p)";
+    "((q -> (p ∨  r)) ∧ (t -> p)) -> t";
+    "((~t -> (q  ∧ p)) ∧ (t -> p)) -> t";
+    "(~p ∧ q) -> (p ∨ r -> t) -> o";
+  ]
+
+let _ = bench test_cases

bin/dune

@@ -1,5 +1,6 @@
-(executable
- (name uiml_demo)
+(executables
+ (public_names uiml_demo benchmark)
+ (names uiml_demo benchmark)
  (modes js native)
  (preprocess (pps js_of_ocaml-ppx))
  (libraries js_of_ocaml UIML angstrom))

bin/uiml_demo.ml

@@ -50,8 +50,8 @@ there should really at least be a function that checks that
 iE and iA are given box-free formulas as input.*)
        method iA s =  catch_e (fun () -> s |> eval |> fail_on_modality |> isl_A v |> string_of_formula)
        method iE s =  catch_e (fun () -> s |> eval |> fail_on_modality |> isl_E v |> string_of_formula)
-       method islA s = catch_e (fun () -> s |> eval |> isl_A v |> string_of_formula)
-       method islE s = catch_e (fun () -> s |> eval |> isl_E v |> string_of_formula)
+       method islA s = catch_e (fun () -> s |> eval |> isl_simplified_A v |> string_of_formula)
+       method islE s = catch_e (fun () -> s |> eval |> isl_simplified_E v |> string_of_formula)
        method k s = catch_e (fun () -> s |> eval |> isl_E v |> string_of_formula ~classical: true)
        method gl s = catch_e (fun () -> s |> eval |> isl_E v |> string_of_formula ~classical: true)
        method parse s = catch_e (fun () -> s |> eval |> string_of_formula)

theories/extraction/UIML_extraction.v

@@ -10,6 +10,8 @@ Require Import K.Interpolation.UIK_braga.
 Require Import KS_export.
 Require Import ISL.PropQuantifiers.
 
+Require Import ISL.Simp.
+
 Fixpoint MPropF_of_form (f : Formulas.form) : MPropF  :=
 match f with
 | Formulas.Var n => Var n
@@ -32,9 +34,13 @@ end.
 Definition gl_UI p s := form_of_MPropF (proj1_sig (GL.Interpolation.UIGL_braga.GUI_tot p ([],[MPropF_of_form s]))).
 Definition k_UI p s := form_of_MPropF(proj1_sig (K.Interpolation.UIK_braga.GUI_tot p ([],[MPropF_of_form s]))).
 
-Definition isl_E  v f :=Ef v f.
+Definition isl_E v f := Ef v f.
 Definition isl_A v f := Af v f.
 
-Separate Extraction gl_UI k_UI isl_E isl_A.
+
+Definition isl_simplified_E v f := E_simplified v f.
+Definition isl_simplified_A v f := A_simplified v f.
+
+Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A.
 
 Cd "..".