From 9c2018ffcbb832f3ecc86fbd99c99eec95622ef4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Thu, 30 Jan 2014 12:27:07 +0100
Subject: [PATCH] Add genericK
---
coalgcompare.ml | 24 ++++++++++++++++++++++++
1 file changed, 24 insertions(+)
diff --git a/coalgcompare.ml b/coalgcompare.ml
index 35bcecd..6e2a45d 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -226,6 +226,28 @@ let doTestK (tboxsizes:int list) (szlist:int list) : testresults =
) (TList.prod szlist tboxsizes) in
runTests solvs formulas timeout
+let doTestGenericK () : 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 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)) ;
@@ -298,6 +320,8 @@ let _ =
let tboxsizes = intlist_of_string (getarg ()) in
let szlist = intlist_of_string (getarg()) in
printRawData (doTestK tboxsizes szlist)
+ | "genericK" ->
+ printRawData (doTestGenericK ())
| "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))))
--
GitLab