diff --git a/CoAlgLogicUtils.ml b/CoAlgLogicUtils.ml new file mode 100644 index 0000000000000000000000000000000000000000..53b947860bc03d2c1f0b4727f242150b97fa19b2 --- /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 0000000000000000000000000000000000000000..f0319a71fb34fde7d36db95803350ef436145484 --- /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 965295f19f09f2577b54101d75c2ca775219c1e9..b95ee3410e2fafeaf015d333b02ac9a0daa63672 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 7a3cc88aeed5c62199997a591413d7061f22f7ea..25aee272cdd31eb45ca13c409a63c21ff8639289 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) $^