Improve K formula generator

CoolUtils.ml

@@ -44,3 +44,7 @@ let cl_set_agents arr = ignore (
 
 
 let intlist_of_string str = List.map int_of_string (Str.split (Str.regexp "[ \t,]+") str)
+
+let compose f g x = f (g (x))
+let flip f y x = f x y
+

CoolUtils.mli

@@ -21,3 +21,5 @@ val cl_set_agents : int array -> unit
 
 val intlist_of_string : string -> int list
 
+val compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)
+val flip : ('a -> 'b -> 'c) -> ('b -> 'a -> 'c)

coalgcompare.ml

@@ -204,16 +204,20 @@ let doTestK (tboxsizes:int list) (szlist:int list) : testresults =
     lPPP A list of pairs (p->p->p, n), e.g. (.+., 1).
   *)
   let timeout = !ptimeout in (* 5 minutes *)
-  let lF = List.map (fun p -> (C.AP ("p"^(string_of_int p)), 1)) (1--3) in
-  let lFF = [(C.const_not,1)] in
-  let lFFF = [(C.const_and,1)] in (* Warning: This forbids disjunctions! *)
-  let lPFF = [(C.const_ex,1); (C.const_ax, 1)] in
-  (* role names *)
-  let lP : (string *int) list = List.map (fun p -> ("R"^(string_of_int p), 1)) (1--3) in
-  let lPP : ((string -> string) * int) list= [] in
-  let lFP : ((C.formula -> string) * int) list = [] in
-  let lPPP = [] in
-  let (genF,_) = G.mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP in
+  let lF = List.map (fun p -> C.AP ("p"^(string_of_int p))) (1--3) in
+  let lF = List.append lF (List.map (C.const_not) lF) in
+  let lF = C.TRUE :: C.FALSE :: lF in
+  let lF = List.map (fun v -> (v,1)) lF in
+  let roles : string list = List.map (fun p -> "R"^(string_of_int p)) (1--3) in
+  let exs : (C.formula -> C.formula) list = List.map C.const_ex roles in
+  let axs : (C.formula -> C.formula) list = List.map C.const_ax roles in
+  let lFF = List.map (fun v -> (v,1)) (List.append exs axs) in
+  let lFFF : (C.formula -> C.formula -> C.formula) list = List.append
+                (List.map (fun x y z -> x (C.const_and y z)) exs)
+                (List.map (fun x y z -> x (C.const_or y z))  axs)
+  in
+  let lFFF = List.map (fun v -> (v,1)) lFFF in
+  let (genF,_) = G.mk_generator lF lFF lFFF [] [] [] [] [] in
   let reasonerNames = List.map (fun (_,s) -> s) solvs in
   let s1 = 0 in (* probably the correct formula... *)
   let formulas = List.map (fun (sz,cnt) ->