From 7369dd1481bfa16587f208f1818a2ec13d2561e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <re06huxa@stud.informatik.uni-erlangen.de> Date: Tue, 14 Jan 2014 13:57:52 +0100 Subject: [PATCH] Add CoAlgLogicUtils for helper functions --- CoAlgLogicUtils.ml | 26 ++++++++++++++++++++++++++ CoAlgLogicUtils.mli | 14 ++++++++++++++ CoAlgLogics.ml | 20 +------------------- Makefile | 6 ++++-- 4 files changed, 45 insertions(+), 21 deletions(-) create mode 100644 CoAlgLogicUtils.ml create mode 100644 CoAlgLogicUtils.mli diff --git a/CoAlgLogicUtils.ml b/CoAlgLogicUtils.ml new file mode 100644 index 0000000..53b9478 --- /dev/null +++ b/CoAlgLogicUtils.ml @@ -0,0 +1,26 @@ + + +(* open Graph *) + +open CoAlgMisc + +let elemArray (x: 'a) (arr: 'a array) = + let res = ref (false) in + let f y = if (x == y) then res := true else () in + Array.iter f arr; + !res + +let disjointAgents sort a b = + assert (lfGetType sort a = EnforcesF || lfGetType sort a = AllowsF); + assert (lfGetType sort b = EnforcesF || lfGetType sort b = AllowsF); + let la = lfGetDestAg sort a in + let lb = lfGetDestAg sort b in + let res = ref (true) in + let f idx = + if (elemArray idx lb) then res := false + else () + in + Array.iter f la; + !res + + diff --git a/CoAlgLogicUtils.mli b/CoAlgLogicUtils.mli new file mode 100644 index 0000000..f0319a7 --- /dev/null +++ b/CoAlgLogicUtils.mli @@ -0,0 +1,14 @@ + + +(* + CoAlg Logic Utils +*) + +open CoAlgMisc + +val disjointAgents : sort -> CoAlgMisc.localFormula -> CoAlgMisc.localFormula -> bool + + + + + diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml index 965295f..b95ee34 100644 --- a/CoAlgLogics.ml +++ b/CoAlgLogics.ml @@ -4,6 +4,7 @@ open CoAlgMisc +open CoAlgLogicUtils module S = MiscSolver @@ -168,25 +169,6 @@ let bsetForall (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool = let bsetExists (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool = not (bsetForall a (fun x -> not (f x))) -let elemArray (x: 'a) (arr: 'a array) = - let res = ref (false) in - let f y = if (x == y) then res := true else () in - Array.iter f arr; - !res - -let disjointAgents sort (a: CoAlgMisc.localFormula) (b: CoAlgMisc.localFormula) : bool = - assert (lfGetType sort a = EnforcesF || lfGetType sort a = AllowsF); - assert (lfGetType sort b = EnforcesF || lfGetType sort b = AllowsF); - let la = lfGetDestAg sort a in - let lb = lfGetDestAg sort b in - let res = ref (true) in - let f idx = - if (elemArray idx lb) then res := false - else () - in - Array.iter f la; - !res - let compatible sort (a: bset) formula1 = let res = ref (true) in let f formula2 = diff --git a/Makefile b/Makefile index 7a3cc88..25aee27 100644 --- a/Makefile +++ b/Makefile @@ -63,12 +63,14 @@ minisat.cma: minisat.cmo minisat_stub.o minisat.cmxa: minisat.cmx minisat_stub.o $(OCAMLOPT) -a -o minisat.cmxa minisat.cmx minisat_stub.o -cclib -lminisat +# Object files... sorted topologically by their dependency... COALG_OBJS := minisat$(SUFFIXLIB) \ + lib/ocamlgraph-1.8.3/graph$(SUFFIX) \ genAndComp$(SUFFIX) MiscSolver$(SUFFIX) altGenlex$(SUFFIX) HashConsing$(SUFFIX) \ ALCFormula$(SUFFIX) ALCMisc$(SUFFIX) ALCGraph$(SUFFIX) \ - CoAlgFormula$(SUFFIX) CoAlgMisc$(SUFFIX) CoAlgLogics$(SUFFIX) \ + CoAlgFormula$(SUFFIX) \ + CoAlgMisc$(SUFFIX) CoAlgLogicUtils$(SUFFIX) CoAlgLogics$(SUFFIX) \ CoAlgReasoner$(SUFFIX) \ - lib/ocamlgraph-1.8.3/graph$(SUFFIX) coalg: $(COALG_OBJS) coalg$(SUFFIX) $(OC) -o coalg $(FLAGS) $(LIBS) $^ -- GitLab