diff --git a/CoAlgFormula.ml b/CoAlgFormula.ml
index 54a19c40fa524f2703059a86da5a76519d3aa03f..5fb3292921089f7f114da2d188647aeb0600d7aa 100644
--- a/CoAlgFormula.ml
+++ b/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]"
diff --git a/CoAlgFormula.mli b/CoAlgFormula.mli
index 8d99da64016de628139e8d425295a07584c7efde..27b369c79d04bfc0dd37a1667f06ac26b8f22c68 100644
--- a/CoAlgFormula.mli
+++ b/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
diff --git a/CoolUtils.ml b/CoolUtils.ml
index d2da1160ba8df39e4deb221b5828d4c0dc8916d9..c525032fbc2070f1aded3475efc7e0cd8d625dfa 100644
--- a/CoolUtils.ml
+++ b/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|])
diff --git a/CoolUtils.mli b/CoolUtils.mli
index d8cd77144cda90b1efa6c0bd4a8affe88d791e10..24af1e8a09b690e4e6282ff635ab428e0770934a 100644
--- a/CoolUtils.mli
+++ b/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
diff --git a/coalgcompare.ml b/coalgcompare.ml
index 6c6d69487d3e4fcc384b150ca1584d5c1c5d43e8..26bc05f73be13167909fd4f4dac88abbe596c2d6 100644
--- a/coalgcompare.ml
+++ b/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