diff --git a/CoAlgFormula.ml b/CoAlgFormula.ml
index 890e3d92f4bf310d9b0e93613049ed6c3b25f313..4097ef91917eb8e29a125dd1719028d6778d5f7e 100644
--- a/CoAlgFormula.ml
+++ b/CoAlgFormula.ml
@@ -361,8 +361,11 @@ and parse_rest ts =
(n, s)
in
let rec agentlist es =
+ let allAgents = CoolUtils.cl_get_agents () in
match Stream.next ts with
- | A.Int n -> n::(agentlist es)
+ | A.Int n -> if CoolUtils.TArray.elem n allAgents
+ then n::(agentlist es)
+ else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ")
| A.Kwd c when c = es -> []
| _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ")
in
diff --git a/CoAlgLogicUtils.ml b/CoAlgLogicUtils.ml
index 32c35cd395f77298bbe845b3c6868146bba0235f..8438f63fa934d6a057d19184e9ff6021b33c2f5d 100644
--- a/CoAlgLogicUtils.ml
+++ b/CoAlgLogicUtils.ml
@@ -3,20 +3,7 @@
open Graph
open CoAlgMisc
-
-module TArray = struct
- let any f arr =
- let rec g idx =
- if idx >= Array.length arr then false
- else if f arr.(idx) then true
- else g (idx + 1)
- in g 0
- let all f arr = not (any (fun x -> not (f x)) arr)
- let elem (x: 'a) (arr: 'a array) =
- any (fun y -> x == y) arr
- let included sub sup = all (fun x -> elem x sup) sub
- let to_string ts arr = "[| " ^ (Array.fold_right (fun i str -> (ts i) ^" "^ str) arr "|]")
-end
+open CoolUtils
let disjointAgents sort a b =
assert (lfGetType sort a = EnforcesF || lfGetType sort a = AllowsF);
diff --git a/CoAlgLogicUtils.mli b/CoAlgLogicUtils.mli
index 867064d4529565267ff08a93dd831b111ca0da3c..5fc525bbac2e3903f81bfda6c0b027b0a0c4d535 100644
--- a/CoAlgLogicUtils.mli
+++ b/CoAlgLogicUtils.mli
@@ -5,14 +5,7 @@
*)
open CoAlgMisc
-
-module TArray : sig
- val all : ('a -> bool) -> 'a array -> bool
- val any : ('a -> bool) -> 'a array -> bool
- val elem : 'a -> 'a array -> bool
- val included : 'a array -> 'a array -> bool
- val to_string : ('a -> string) -> 'a array -> string
-end
+open CoolUtils
val disjointAgents : sort -> localFormula -> localFormula -> bool
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index b599064c19ea586ade630f898c1e9b73abde6a2f..029747ae27ab716c267cb25181f0aea1b5f18d4f 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -4,6 +4,7 @@
open CoAlgMisc
+open CoolUtils
open CoAlgLogicUtils
(* open Gmlmip *)
@@ -194,10 +195,6 @@ let compatible sort (a: bset) formula1 =
/\ n /\ m all C_i ⊆ D
/ \i=1 a_i /\ b / \j=1 c_j
*)
-let agents = ref ([|1;2;3;4;5;6;7;8;9;10|])
-
-let cl_get_agents () = !agents
-let cl_set_agents arr = ignore (agents := arr)
let mkRule_CL sort bs sl =
assert (List.length sl = 1); (* TODO: Why? *)
@@ -208,7 +205,7 @@ let mkRule_CL sort bs sl =
let nCands = bsetMakeRealEmpty () in (* all N-diamonds *)
let hasFullAgentList formula =
let aglist = lfGetDestAg sort formula in
- let value = TArray.all (fun x -> TArray.elem x aglist) !agents in
+ let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in
if (value) then bsetAdd nCands formula else () ;
value
in
diff --git a/CoAlgLogics.mli b/CoAlgLogics.mli
index 5cc4b28d1e32cd9bc33811527418484ed8d5c473..48d0958b68bceec89898bf9788866dea0e7084bc 100644
--- a/CoAlgLogics.mli
+++ b/CoAlgLogics.mli
@@ -6,7 +6,4 @@
open CoAlgMisc
-val cl_get_agents : unit -> int array
-val cl_set_agents : int array -> unit
-
val getExpandingFunctionProducer : functors -> sort -> bset -> sort list -> stateExpander
diff --git a/CoolUtils.ml b/CoolUtils.ml
new file mode 100644
index 0000000000000000000000000000000000000000..bcd50436c7fa9dbb42074062312a87441a0d69b1
--- /dev/null
+++ b/CoolUtils.ml
@@ -0,0 +1,20 @@
+
+module TArray = struct
+ let any f arr =
+ let rec g idx =
+ if idx >= Array.length arr then false
+ else if f arr.(idx) then true
+ else g (idx + 1)
+ in g 0
+ let all f arr = not (any (fun x -> not (f x)) arr)
+ let elem (x: 'a) (arr: 'a array) =
+ any (fun y -> x == y) arr
+ let included sub sup = all (fun x -> elem x sup) sub
+ let to_string ts arr = "[| " ^ (Array.fold_right (fun i str -> (ts i) ^" "^ str) arr "|]")
+end
+
+let agents = ref ([|1;2;3;4;5;6;7;8;9;10|])
+
+let cl_get_agents () = !agents
+let cl_set_agents arr = ignore (agents := arr)
+
diff --git a/CoolUtils.mli b/CoolUtils.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bc2dfe9c234d09b44c13d24b4b2cd2edd34bac3e
--- /dev/null
+++ b/CoolUtils.mli
@@ -0,0 +1,14 @@
+
+(* Some basic utilities as they are known from haskell prelude and so on... *)
+
+module TArray : sig
+ val all : ('a -> bool) -> 'a array -> bool
+ val any : ('a -> bool) -> 'a array -> bool
+ val elem : 'a -> 'a array -> bool
+ val included : 'a array -> 'a array -> bool
+ val to_string : ('a -> string) -> 'a array -> string
+end
+
+val cl_get_agents : unit -> int array
+val cl_set_agents : int array -> unit
+
diff --git a/Makefile b/Makefile
index e3b3c6373098f4765a1c29e827491c769ace43f8..cc064a32bd632e1fca5e8d986af5c612c05d6540 100644
--- a/Makefile
+++ b/Makefile
@@ -101,6 +101,7 @@ gmlmip.cmxa: gmlmip.cmx gmlmip_stub.o $(GMLOBJS)
# Object files... sorted topologically by their dependency...
COALG_OBJS := minisat$(SUFFIXLIB) \
+ CoolUtils$(SUFFIX) \
genAndComp$(SUFFIX) MiscSolver$(SUFFIX) altGenlex$(SUFFIX) HashConsing$(SUFFIX) \
ALCFormula$(SUFFIX) ALCMisc$(SUFFIX) ALCGraph$(SUFFIX) \
CoAlgFormula$(SUFFIX) \
diff --git a/coalg.ml b/coalg.ml
index 93933ed80c59198647ff5724adcf28a0ba991a85..c36f0e32bade7df02028679552211a380ff3bae7 100644
--- a/coalg.ml
+++ b/coalg.ml
@@ -117,7 +117,7 @@ let rec parseFlags arr offs : unit =
| "--agents" ->
let strAglist = getParam () in
let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
- CoAlgLogics.cl_set_agents (Array.of_list aglist)
+ CoolUtils.cl_set_agents (Array.of_list aglist)
| _ ->
raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«"))
) ; parseFlags arr (!offs + 1)