From e4cd869a76f1212fadcf2ffb463a1b3f82f4c6a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Wed, 15 Jan 2014 20:57:55 +0100
Subject: [PATCH] A bit of cleaning code

---
 CoAlgLogics.ml | 12 +++++-------
 CoAlgMisc.ml   |  5 +++++
 CoAlgMisc.mli  |  1 +
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index 9671694..fffff30 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -11,7 +11,7 @@ module S = MiscSolver
 (** directly return a list of rules **)
 let mkRuleList_MultiModalK sort bs sl =
   assert (List.length sl = 1);
-  let dep f bsl =                 (* dependencies for formula f *)
+  let dep f bsl =                 (* dependencies for formula f (f is a diamond) *)
     assert (List.length bsl = 1); (* -+                 *)
     let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
     let res = bsetMake () in
@@ -29,7 +29,7 @@ let mkRuleList_MultiModalK sort bs sl =
     res
   in
   let getRules f acc =
-    if lfGetType sort f = ExF then (* f = ∃R.C *)
+    if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *)
       let bs1 = bsetMake () in
       bsetAdd bs1 (lfGetDest1 sort f); (* bs1 := { C }          *)
       let (role : int) = lfGetDest3 sort f in (* role := R *)
@@ -153,11 +153,6 @@ let subset (a: bset) (b: bset) : bool =
     bsetIter f a;
     !res && (bsetlen a < bsetlen b)
 
-let bsetFilter (a: bset) (f: CoAlgMisc.localFormula -> bool) : bset =
-    let res = bsetMake () in
-    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
-    res
-
 let bsetForall (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool =
     let res = ref (true) in
     let helper formula =
@@ -202,6 +197,9 @@ let compatible sort (a: bset) formula1 =
 let mkRule_CL sort bs sl =
   assert (List.length sl = 1); (* TODO: Why? *)
   let s1 = List.hd sl in (* [s1] = List.hd sl *)
+  let boxes = bsetFilter bs (fun f -> lfGetType sort f = EnforcesF) in
+  let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
+  let disjoints = maxDisjoints sort boxes in
   (*
     mkRule_CL sort bs [s1]
     = { (λ[bs1]. { ∀R.D
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index a8e5d30..3107752 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -429,6 +429,11 @@ let bsetRem bs lf = S.remBS bs lf
 let bsetCopy bs = S.copyBS bs
 let bsetFold fkt bs init = S.foldBS fkt bs init
 let bsetIter fkt bset = S.iterBS fkt bset
+let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
+    let res = bsetMake () in
+    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
+    res
+
 let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)
 
 let csetCompare cs1 cs2 = S.compareBS cs1 cs2
diff --git a/CoAlgMisc.mli b/CoAlgMisc.mli
index 51e86c5..de8f1c5 100644
--- a/CoAlgMisc.mli
+++ b/CoAlgMisc.mli
@@ -250,6 +250,7 @@ val bsetAdd : bset -> localFormula -> unit
 val bsetMem : bset -> localFormula -> bool
 val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
 val bsetIter : (localFormula -> unit) -> bset -> unit
+val bsetFilter : bset -> (localFormula -> bool) -> bset
 val bsetAddTBox : sort -> bset -> bset
 val bsetCopy : bset -> bset
 
-- 
GitLab