From 2cef7a7c08947b88785a87930bc78e8fe4efea57 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Tue, 28 Jan 2014 15:09:33 +0100
Subject: [PATCH] Make coalgcompare compile again
---
coalgcompare.ml | 35 +++++++++++++++--------------------
1 file changed, 15 insertions(+), 20 deletions(-)
diff --git a/coalgcompare.ml b/coalgcompare.ml
index 8f2ad95..d9329e4 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -127,7 +127,6 @@ let printUsage () =
exit 1
let doTestK () : testresults =
- let sorts = sortK in
let solvs = [(solvFact, "fact"); (solvCoalg sortK, "CoAlg")] in
(*
lF A list of pairs (f, n), e.g. (p, 1).
@@ -143,29 +142,25 @@ let doTestK () : testresults =
lPPP A list of pairs (p->p->p, n), e.g. (.+., 1).
*)
let timeout = 300 in (* 5 minutes *)
- let lF = List.map (fun p -> (string_of_int p, 1)) (0--10) in
- let lFF = [((fun x -> C.NOT x),1)] in
- let lFFF = [((fun x y -> C.AND x y),1), ((fun x y -> C.OR x y),1)] in
- let lPFF = [(fun p f -> C.EX p f,1),(fun p f -> C.AX p f,1)] in
+ let lF = List.map (fun p -> (C.AP (string_of_int p), 1)) (0--10) in
+ let lFF = [(C.const_not,1)] in
+ let lFFF = [(C.const_and,1); (C.const_or, 1)] in
+ let lPFF = [(C.const_ex,1); (C.const_ax, 1)] in
(* role names *)
- let lP = List.map (fun p -> (string_of_int p, 1)) (0--10) in
- let lPP = [] in
- let lFP = [] in
+ let lP : (string *int) list = List.map (fun p -> (string_of_int p, 1)) (0--10) in
+ let lPP : ((string -> string) * int) list= [] in
+ let lFP : ((C.formula -> string) * int) list = [] in
let lPPP = [] in
- let (genF,_) = mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP in
- let resonerNames = List.map (fun (_,s) -> s) solvs in
- let formulas = List.map (fun n -> ("size "^(string_of_int n),genF n)) (2--40) in
- let fillCell formula solver =
+ let (genF,_) = G.mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP in
+ let reasonerNames = List.map (fun (_,s) -> s) solvs in
+ let formulas : (string*C.sortedFormula) list = List.map (fun n -> ("size "^(string_of_int n),(0,genF n))) (2--40) in
+ let fillCell formula (solver,_) =
let (res, time, _) = solver ([],formula) timeout in
(ASAT, -10)
- (*match res with
- |
- |
- *)
in
- let results = List.map (fun f ->
- List.map (fun s ->
- fillCell f s) solvs) formulas
+ let results = List.map (fun (str,f) ->
+ (str,List.map (fun s ->
+ fillCell f s) solvs)) formulas
in
(reasonerNames,results)
@@ -173,7 +168,7 @@ let _ =
if Array.length Sys.argv < 1 then printUsage ()
else match Sys.argv.(1) with
| "K" -> doTestK ()
- | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Logic name »" ^ str ^ "«"))
+ | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Logic name »" ^ (Sys.argv.(1)) ^ "«"))
(*
--
GitLab