From ad63163ecdc461a46eb271e5a3812c19f76a80cb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Wed, 29 Jan 2014 14:32:14 +0100
Subject: [PATCH] Improve K formula generator
---
CoolUtils.ml | 4 ++++
CoolUtils.mli | 2 ++
coalgcompare.ml | 24 ++++++++++++++----------
3 files changed, 20 insertions(+), 10 deletions(-)
diff --git a/CoolUtils.ml b/CoolUtils.ml
index c525032..24b6486 100644
--- a/CoolUtils.ml
+++ b/CoolUtils.ml
@@ -44,3 +44,7 @@ let cl_set_agents arr = ignore (
let intlist_of_string str = List.map int_of_string (Str.split (Str.regexp "[ \t,]+") str)
+
+let compose f g x = f (g (x))
+let flip f y x = f x y
+
diff --git a/CoolUtils.mli b/CoolUtils.mli
index 24af1e8..24016a4 100644
--- a/CoolUtils.mli
+++ b/CoolUtils.mli
@@ -21,3 +21,5 @@ val cl_set_agents : int array -> unit
val intlist_of_string : string -> int list
+val compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)
+val flip : ('a -> 'b -> 'c) -> ('b -> 'a -> 'c)
diff --git a/coalgcompare.ml b/coalgcompare.ml
index 26bc05f..35bcecd 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -204,16 +204,20 @@ let doTestK (tboxsizes:int list) (szlist:int list) : 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)) (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 -> ("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 lF = List.map (fun p -> C.AP ("p"^(string_of_int p))) (1--3) in
+ let lF = List.append lF (List.map (C.const_not) lF) in
+ let lF = C.TRUE :: C.FALSE :: lF in
+ let lF = List.map (fun v -> (v,1)) lF in
+ let roles : string list = List.map (fun p -> "R"^(string_of_int p)) (1--3) in
+ let exs : (C.formula -> C.formula) list = List.map C.const_ex roles in
+ let axs : (C.formula -> C.formula) list = List.map C.const_ax roles in
+ let lFF = List.map (fun v -> (v,1)) (List.append exs axs) in
+ let lFFF : (C.formula -> C.formula -> C.formula) list = List.append
+ (List.map (fun x y z -> x (C.const_and y z)) exs)
+ (List.map (fun x y z -> x (C.const_or y z)) axs)
+ in
+ let lFFF = List.map (fun v -> (v,1)) lFFF in
+ let (genF,_) = G.mk_generator lF lFF lFFF [] [] [] [] [] in
let reasonerNames = List.map (fun (_,s) -> s) solvs in
let s1 = 0 in (* probably the correct formula... *)
let formulas = List.map (fun (sz,cnt) ->
--
GitLab