diff --git a/coalgcompare.ml b/coalgcompare.ml index 787372aad07ae6116328576970f325ac1a955729..b05055cd7f6a4b55e0cd089b1e03f3d45ef9dac5 100644 --- a/coalgcompare.ml +++ b/coalgcompare.ml @@ -226,6 +226,27 @@ let doTestK (tboxsizes:int list) (szlist:int list) : testresults = ) (TList.prod szlist tboxsizes) in runTests solvs formulas timeout +let doTestGenericGML () : testresults = + let solvs = [(solvFact, "fact"); (solvCool "K", "cool")] 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 doTestGenericK () : testresults = let solvs = [(solvFact, "fact"); (solvCool "K", "cool")] in let timeout = !ptimeout in (* 5 minutes *) @@ -344,6 +365,8 @@ let _ = printRawData (doTestK tboxsizes szlist) | "genericK" -> printRawData (doTestGenericK ()) + | "genericGML" -> + printRawData (doTestGenericGML ()) | "genericCL" -> printRawData (doTestGenericCL ()) | "CL1" -> let sz = (5000 -- 5080) in