Many statistics optimizations

CoAlgFormula.ml

@@ -268,6 +268,26 @@ let exportQuery tbox f =
   exportSortedFormula_buffer sb f;
   Buffer.contents sb
 
+(** Converts a (sorted) formula query into a string representation. Such that
+    coalg can read it again using importQuery
+    @param tbox A list of sorted formulae representing a TBox.
+    @param f A sorted formula.
+    @return A string representing tbox |- f.
+ *)
+let exportQueryParsable tbox (_,f) =
+  let sb = Buffer.create 1000 in
+  let rec expFl = function
+    | [] -> ()
+    | (_,h)::tl ->
+        exportFormula_buffer sb h;
+        if tl <> [] then Buffer.add_string sb "; " else ();
+        expFl tl
+  in
+  expFl tbox;
+  Buffer.add_string sb "  |-  ";
+  exportFormula_buffer sb f;
+  Buffer.contents sb
+
 
 let lexer = A.make_lexer 
     [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"

CoAlgFormula.mli

@@ -40,6 +40,7 @@ val sizeSortedFormula : sortedFormula -> int
 val exportFormula : formula -> string
 val exportSortedFormula : sortedFormula -> string
 val exportQuery : sortedFormula list -> sortedFormula -> string
+val exportQueryParsable : sortedFormula list -> sortedFormula -> string
 val importFormula : string -> formula
 val importSortedFormula : string -> sortedFormula
 val importQuery : string -> sortedFormula list * sortedFormula

CoolUtils.ml

@@ -31,6 +31,7 @@ module TList = struct
         | h::t -> let pt = powerset t in
                   let oth = List.map (fun x -> h::x) pt in
                   List.append pt oth
+    let prod la lb = List.concat (List.map (fun a -> List.map (fun b -> (a,b)) lb) la)
 end
 
 let agents = ref ([|1;2;3;4;5;6;7;8;9;10|])

CoolUtils.mli

@@ -13,6 +13,7 @@ end
 module TList : sig
     val zip : ('a list) -> ('b list) -> ('a * 'b) list
     val powerset : ('a list) -> ('a list list)
+    val prod : ('a list) -> ('b list) -> (('a * 'b) list)
 end
 
 val cl_get_agents : unit -> int array

coalgcompare.ml

@@ -136,14 +136,16 @@ let solvFact (tbox, sf) timeout =
   if ignore_exception then try call () with _ -> (G.FAILED, -1.0, 0)
                       else call ()
 
-let solvTatl (_,sf) timeout = (* ignore the TBox... *)
+let solvTatl (tbox,(_,sf)) timeout = (* ignore the TBox... *)
   let tatl = "./tatl-compatibility-wrapper.sh" in
   let inp = CoAlgFormula.exportFormula sf in
   G.callExt (Some inp) tatl [] (Str.regexp_string "The formula is satisfiable") timeout
 
-let solvCoolCL (_,sf) timeout = (* ignore the TBox... *)
-  let inp = CoAlgFormula.exportFormula sf in
-  G.callExt (Some inp) "./coalg" ["sat"; "CL"] (Str.regexp_string "1: satisfiable") timeout
+let solvCool functorname (tbox,sf) timeout =
+  let inp = CoAlgFormula.exportQueryParsable tbox sf in
+  G.callExt (Some inp) "./coalg" ["sat"; functorname] (Str.regexp_string "1: satisfiable") timeout
+
+let solvCoolCL = solvCool "CL"
 
 let solvers =
   let _ = [(solvCoalg sortK, "CoAlg"); (solvALC, "alc"); (solvFact, "fact")] in
@@ -153,7 +155,8 @@ let printUsage () =
   print_endline "Usage: \"coalgcompare [<flags>] <logic> <logicargs>\" does tests where";
   print_endline "       <flags> in { --seed INITIALSEED }";
   print_endline "       <logic> in {";
-  print_endline "                     K";
+  print_endline "                     K <formula counts in tbox> <list of sizes>";
+  print_endline "                     (e.g. »K 0,5,10 10000,15000,20000«)";
   print_endline "                     genCL <agents> <list of sizes>";
   print_endline "                     (e.g. »genCL 1,2,3 4000,42«)";
   print_endline "                  }";
@@ -163,7 +166,7 @@ let runTests solvs formulas timeout : testresults =
   let reasonerNames = List.map (fun (_,s) -> s) solvs in
   let fillCell (fn,formula) (solver,sn) =
     debugMsg ("running " ^ sn ^ " on " ^ fn);
-    let (res, time, _) = solver ([],formula) timeout in
+    let (res, time, _) = solver formula timeout in
     let answer = match res with
                  | G.FINISHED (v) -> if (v) then ASAT else AUNSAT
                  | G.TIMED_OUT -> ATIMEOUT
@@ -185,8 +188,8 @@ let runTests solvs formulas timeout : testresults =
   (reasonerNames,results)
 
 
-let doTestK () : testresults =
-  let solvs = [(solvFact, "fact"); (solvCoalg sortK, "cool")] in
+let doTestK (tboxsizes:int list) (szlist:int list) : testresults =
+  let solvs = [(solvFact, "fact"); (solvCool "K", "cool")] in
   (*
     lF A list of pairs (f, n), e.g. (p, 1).
     The list must not be empty.
@@ -201,36 +204,23 @@ let doTestK () : 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)) (0--3) in
+  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 -> (string_of_int p, 1)) (0--10) in
+  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 reasonerNames = List.map (fun (_,s) -> s) solvs in
-  let form_maxsize = 900000 in
-  let form_count = 8 in
-  let form_sizes = ((form_maxsize-form_count)--form_maxsize) in
-  let formulas : (string*C.sortedFormula) list = List.map (fun n -> ("randsize"^(string_of_int n),(0,genF n))) form_sizes in
-  let fillCell (fn,formula) (solver,sn) =
-    debugMsg ("K: running " ^ sn ^ " on " ^ fn);
-    let (res, time, _) = solver ([],formula) timeout in
-    let answer = match res with
-                 | G.FINISHED (v) -> if (v) then ASAT else AUNSAT
-                 | G.TIMED_OUT -> ATIMEOUT
-                 | G.FAILED -> AFAILED
-    in
-    (answer, int_of_float time)
-  in
-  let results = List.map (fun (str,f) ->
-                    (str,List.map (fun s ->
-                        fillCell (str,f) s) solvs)) formulas
-  in
-  (reasonerNames,results)
+  let s1 = 0 in (* probably the correct formula... *)
+  let formulas = List.map (fun (sz,cnt) ->
+                            let tbox = List.map (fun _ -> (s1,genF sz)) (1 -- cnt) in
+                            ("sz"^(string_of_int sz)^"tb"^(string_of_int cnt),(tbox,(s1,genF sz)))
+                          ) (TList.prod szlist tboxsizes) in
+  runTests solvs formulas timeout
 
 let printRawData ((rn,results):testresults) : unit =
     let doubler l = List.fold_right (fun a b -> (a ^ "_state")::(a^"_time")::b) l [] in
@@ -293,16 +283,20 @@ let _ =
     parseflags ();
     Random.init !pseed;
     let alarmHandler (n : int) = raise G.Timeout in
-    let sigintHandler (n : int) = raise UserInterupt in
+    let sigintHandler (n : int) = prerr_endline "" ; raise UserInterupt in
     let oldHandler = Sys.signal Sys.sigalrm (Sys.Signal_handle alarmHandler) in
     let oldSigint = Sys.signal Sys.sigint (Sys.Signal_handle sigintHandler) in
     debugMsg ("seed is " ^ (string_of_int (!pseed)));
     let cmd = !pcmd in
     (
     match cmd with
-    | "K" -> printRawData (doTestK ())
-    | "CL1" -> let sz = (5000 -- 5020) in
-               printRawData (doTestCL (TList.zip (List.map string_of_int sz) (doGenCL [1;2;3;4;5] sz)))
+    | "K" ->
+             let tboxsizes = intlist_of_string (getarg ()) in
+             let szlist = intlist_of_string (getarg()) in
+             printRawData (doTestK tboxsizes szlist)
+    | "CL1" -> let sz = (5000 -- 5080) in
+               let ats (str,f) = (str, ([], (0, f))) in (* add tbox and sort *)
+               printRawData (doTestCL (List.map ats (TList.zip (List.map string_of_int sz) (doGenCL [1;2;3;4;5] sz))))
     | "genCL" -> let p1 = getarg () in
                  let p2 = getarg () in
                  let forms = doGenCL (intlist_of_string p1) (intlist_of_string p2) in