diff --git a/coalgcompare.ml b/coalgcompare.ml index 6e2a45d064e83150e4eecbd59c34e2f42e8aed1d..787372aad07ae6116328576970f325ac1a955729 100644 --- a/coalgcompare.ml +++ b/coalgcompare.ml @@ -248,6 +248,28 @@ let doTestGenericK () : testresults = +let doTestGenericCL () : testresults = + let solvs = [(solvCoolCL, "cool"); (solvTatl, "tatl")] in + let timeout = !ptimeout in (* 5 minutes *) + let formulas = ref [] in + let counter = ref 0 in + let s1 = 0 in + (try + while true do + let input = read_line () in + if not (GenAndComp.isEmptyString input) then + let (tbox, f) = CoAlgFormula.importQuery input in + incr counter; + let test = ("line" ^ (string_of_int !counter), (tbox,f)) in + formulas := test::(!formulas) + else () + done + with End_of_file -> ()); + let formulas = List.rev !formulas 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 print_endline (String.concat ";" ("formula"::doubler rn)) ; @@ -322,6 +344,8 @@ let _ = printRawData (doTestK tboxsizes szlist) | "genericK" -> printRawData (doTestGenericK ()) + | "genericCL" -> + printRawData (doTestGenericCL ()) | "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))))