From 53e9b267feb02f0540b20e14fb658ab5ba1b1e15 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Fri, 31 Jan 2014 17:24:27 +0100
Subject: [PATCH] Enable tboxes for tatl cl solver
---
CoolUtils.ml | 3 +++
CoolUtils.mli | 1 +
coalgcompare.ml | 6 +++++-
3 files changed, 9 insertions(+), 1 deletion(-)
diff --git a/CoolUtils.ml b/CoolUtils.ml
index 5fc2631..937064c 100644
--- a/CoolUtils.ml
+++ b/CoolUtils.ml
@@ -32,6 +32,9 @@ module TList = struct
let oth = List.map (fun x -> h::x) pt in
List.append pt oth
let prod la lb = List.concat (List.map (fun a -> List.map (fun b -> (a,b)) lb) la)
+ let empty l = match l with
+ | (_::_) -> false
+ | [] -> true
end
let agents = ref ([|1;2;3;4;5|])
diff --git a/CoolUtils.mli b/CoolUtils.mli
index 24016a4..9e2a544 100644
--- a/CoolUtils.mli
+++ b/CoolUtils.mli
@@ -14,6 +14,7 @@ module TList : sig
val zip : ('a list) -> ('b list) -> ('a * 'b) list
val powerset : ('a list) -> ('a list list)
val prod : ('a list) -> ('b list) -> (('a * 'b) list)
+ val empty : ('a list) -> bool
end
val cl_get_agents : unit -> int array
diff --git a/coalgcompare.ml b/coalgcompare.ml
index 44e7fda..de947d2 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -142,7 +142,11 @@ let solvFact (tbox, sf) timeout =
let solvTatl agents (tbox,(_,sf)) timeout = (* ignore the TBox... *)
let tatl = "./tatl" in
- let inp = CoAlgFormula.exportTatlFormula (C.AND (sf, C.ALLOWS (agents,C.TRUE))) in
+ let tboxlist = List.map (fun (_,f) -> CoAlgFormula.exportTatlFormula f) tbox in
+ let agstr = String.concat "," (List.map string_of_int agents) in
+ let tboxstr = "~<<"^agstr^">>F~ ("^(String.concat " /\\ " tboxlist) ^ ") /\\ " in
+ let inp = CoAlgFormula.exportTatlFormula sf in
+ let inp = if TList.empty tbox then inp else (tboxstr ^ "(" ^ inp ^ ")") in
G.callExt (Some ("1\n"^inp^"\n4")) tatl [] (Str.regexp_string "The formula is satisfiable") timeout
let solvCool functorname (tbox,sf) timeout =
--
GitLab