Fix CL for diamond formula sets with all agents

For the case of two (or more) diamond formulas who all mention the full
agent list, no rule was created, because the former CL algorithm only
created rules for proper subsets of the agent list. This adds the
missing rule and lets cool correctly answer the following query:

    $ ./coalg.native sat CL --agents '1' <<< '(~[{1}] p) & ~[{1}] ~p'
    unsatisfiable

src/lib/CoAlgLogics.ml

@@ -209,18 +209,32 @@ let mkRule_CL sort bs sl : stateExpander =
   let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
   let disjoints = maxDisjoints sort boxes in
   (*print_endline ("disjoints: "^(string_of_coalition_list sort disjoints)); *)
+  let nCandsEmpty = ref (true) in
   let nCands = bsetMakeRealEmpty () in (* all N-diamonds *)
+  let dCandsEmpty = ref (true) in
   let hasFullAgentList formula =
     let aglist = lfGetDestAg sort formula in
     let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in
-    if (value) then bsetAdd nCands formula else () ;
+    if (value) then
+    begin
+        bsetAdd nCands formula;
+        nCandsEmpty := false
+    end
+    else dCandsEmpty := false;
     value
   in
   (* Candidates for D in Rule 2 *)
+  (* implicitly fill nCands *)
   let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
+  (*
+  print_endline ("For set " ^(CoAlgMisc.bsetToString sort bs));
+  print_endline ("N-Cands: " ^(CoAlgMisc.bsetToString sort nCands));
+  print_endline ("D-Cands: " ^(CoAlgMisc.bsetToString sort dCands));
+  *)
   let c_j : localFormula list =
     bsetFold (fun f a -> (lfGetDest1 sort f)::a) nCands []
   in
+  (* rule 2 for diamaonds where D is a proper subset of the agent set N *)
   let getRule2 diamDb acc = (* diamDb = <D> b *)
     (* print_endline "Rule2" ; *)
     let d = lfGetDestAg sort diamDb in (* the agent list *)
@@ -247,6 +261,31 @@ let mkRule_CL sort bs sl : stateExpander =
     List.fold_left createSingleRule acc maxdisj
   in
   let rules = bsetFold getRule2 dCands [] in
+  let getRule2ForFullAgents acc =
+    (* if there are N-diamonds but no diamonds with a proper subset of the agents,
+       then we need an explicit rule 2
+    *)
+    if not !nCandsEmpty && !dCandsEmpty then begin
+        (* create rule 2 once for all the diamonds with a full agent set *)
+        let maxdisj = maxDisjoints sort boxes in
+        let createSingleRule acc coalitions =
+            let a_i : localFormula list =
+                bsetFold (fun f a -> (lfGetDest1 sort f)::a) coalitions []
+            in
+            (* now do rule 2:
+                coalitions  /\ nCands
+               ———————————————————————
+                  a_i       /\ c_j
+            *)
+            let children = bsetMakeRealEmpty () in
+            List.iter (bsetAdd children) (c_j) ;
+            List.iter (bsetAdd children) (a_i) ;
+            ((fun bs1 -> bs), lazylistFromList [(s1, children)])::acc
+        in
+        List.fold_left createSingleRule acc maxdisj
+    end else acc
+  in
+  let rules = getRule2ForFullAgents rules in
   let getRule1 acc coalitions =
     (* print_endline "Rule1" ; *)
     (* do rule 1:

src/testsuite/Testsuite.ml

@@ -62,7 +62,7 @@ let runSatCheckVerbose (sc:satCheck) =
     let res = runSatCheck sc in
     (if (res = expectation)
     then PF.printf "%s\n" (cs "1;32" "Yes")
-    else PF.printf "%s, it is %s\n"
+    else PF.printf "%s, cool claims it is %s\n"
                     (cs "1;31" "No")
                     (sotr res));
     flush stdout;

src/testsuite/cool-testsuite.ml

@@ -74,6 +74,7 @@ let cl_testcases : testcase_section =
     ; unsat "[{1}] C & <{ 1 2 }> ~C"
     ; sat   "<{ 1 2 }> C & <{ 1 2 }> ~C"
     ; unsat "<{ 1 2 }> C & [{ 1 2 }] ~C"
+    ; unsat "<{ 1 2 3 4 5 }> C & <{ 1 2 3 4 5 }> ~C"
     ; sat   "([{1 3}] C) & ([{ 2 3 }] ~C )"
     ]