diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 6474c4526532a6b9653321661be90ae70dfac1fc..1b89a2b3975bc1a775a52aa4c2dd6408bcdbffec 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -59,20 +59,20 @@ let mkRuleList_MultiModalK sort bs sl =
*)
bsetFold getRules bs []
-let mkRule_MultiModalK sort bs sl =
+let mkRule_MultiModalK sort bs sl : stateExpander =
let rules = mkRuleList_MultiModalK sort bs sl in
let res = ref (Some rules) in
fun () ->
- match !res with
+ Conjunctive (match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules
+ AllInOne rules)
(* TODO: test it with:
make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True'
*)
-let mkRule_MultiModalKD sort bs sl =
+let mkRule_MultiModalKD sort bs sl : stateExpander =
assert (List.length sl = 1); (* TODO: Why? *)
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let roles = S.makeBS () in
@@ -131,11 +131,12 @@ let mkRule_MultiModalKD sort bs sl =
(* TODO: replace cannonical wrapper by helper function *)
let res = ref (Some rules) in
fun () ->
- match !res with
+ Conjunctive (match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
AllInOne rules
+ )
(* CoalitionLogic: helper functions *)
@@ -196,7 +197,7 @@ let compatible sort (a: bset) formula1 =
/ \i=1 a_i /\ b / \j=1 c_j
*)
-let mkRule_CL sort bs sl =
+let mkRule_CL sort bs sl : stateExpander =
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
@@ -263,13 +264,13 @@ let mkRule_CL sort bs sl =
(* standard return procedure *)
let res = ref (Some rules) in
fun () ->
- match !res with
+ Conjunctive (match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules
+ AllInOne rules)
-let mkRule_GML sort bs sl =
+let mkRule_GML sort bs sl : stateExpander =
assert (List.length sl = 1);
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
@@ -316,13 +317,13 @@ let mkRule_GML sort bs sl =
(* standard return procedure *)
let res = ref (Some rules) in
fun () ->
- match !res with
+ Conjunctive (match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules
+ AllInOne rules)
-let mkRule_Choice sort bs sl =
+let mkRule_Choice sort bs sl : stateExpander =
assert (List.length sl = 2);
let dep bsl =
assert (List.length bsl = 2);
@@ -351,14 +352,14 @@ let mkRule_Choice sort bs sl =
let s2 = List.nth sl 1 in
let res = ref (Some [(dep, [(s1, bs1); (s2, bs2)])]) in
fun () ->
- match !res with
+ Conjunctive (match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules
+ AllInOne rules)
-let mkRule_Fusion sort bs sl =
+let mkRule_Fusion sort bs sl : stateExpander =
assert (List.length sl = 2);
let dep proj bsl =
assert (List.length bsl = 1);
@@ -386,11 +387,11 @@ let mkRule_Fusion sort bs sl =
let s2 = List.nth sl 1 in
let res = ref (Some [(dep 0, [(s1, bs1)]); (dep 1, [(s2, bs2)])]) in
fun () ->
- match !res with
+ Conjunctive (match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules
+ AllInOne rules)
(* Maps a logic represented by the type "functors" to the corresponding
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 3d9c9643dbc58d277c94368c4f3ef473fdf21024..995698d40ebca456c24b0035e7982cb6e9088373 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -121,7 +121,10 @@ and setCnstr = unit GHt.t
(* Types that are hard coded into the algorithm *)
(*****************************************************************************)
-and stateExpander = unit -> ruleEnumeration
+and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
+ | Conjunctive of 'a (*specifies that all of the 'a need to be satifsfied *)
+
+and stateExpander = unit -> ruleEnumeration junction
and sort = C.sort
@@ -132,9 +135,12 @@ and nodeStatus =
| Unsat
and dependencies = bset list -> bset
+
+and rule = (dependencies * (sort * bset) list)
+
and ruleEnumeration =
- | AllInOne of (dependencies * (sort * bset) list) list
- | NextRule of dependencies * (sort * bset) list
+ | AllInOne of rule list
+ | NextRule of rule
| NoMoreRules
type nominal = sort * localFormula
@@ -167,6 +173,35 @@ exception CoAlg_finished of bool
let sortTable = ref (Array.make 0 (MultiModalK, [1]))
+let junctionEvalBool : (bool list junction) -> bool = function
+ | Disjunctive l -> List.fold_right (||) l false
+ | Conjunctive l -> List.fold_right (&&) l true
+
+let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function
+ | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false
+ | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true
+
+let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option =
+ match x with
+ | None -> None
+ | Some x -> (match y with
+ | None -> None
+ | Some y -> Some (f x y))
+
+let junctionEvalBoolOption : bool option list junction -> bool option =
+ let f extreme op x y = (* ensure that: (Some True) || None = Some True *)
+ if x = extreme || y = extreme
+ then extreme
+ else optionalizeOperator op x y
+ in function
+ | Disjunctive l ->
+ List.fold_right (f (Some true) (||)) l (Some false)
+ | Conjunctive l ->
+ List.fold_right (f (Some false) (&&)) l (Some true)
+
+let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function
+ | Disjunctive l -> (l, fun x -> Disjunctive x)
+ | Conjunctive l -> (l, fun x -> Conjunctive x)
(*****************************************************************************)
(* "Module type" and a specific implementation of the main queue *)
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 2c80349a9d14ac63b7e789051b54ef18c8703c93..15fdb34c9effa31a597f4a55ed17f52aaf4dab12 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -55,12 +55,14 @@ type setCore
type setCnstr
-
(*****************************************************************************)
(* Types that are hard coded into the algorithm *)
(*****************************************************************************)
-and stateExpander = unit -> ruleEnumeration
+and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
+ | Conjunctive of 'a (*specifies that all of the 'a need to be satifsfied *)
+
+and stateExpander = unit -> ruleEnumeration junction
and sort = CoAlgFormula.sort
@@ -71,9 +73,12 @@ and nodeStatus =
| Unsat
and dependencies = bset list -> bset
+
+and rule = (dependencies * (sort * bset) list)
+
and ruleEnumeration =
- | AllInOne of (dependencies * (sort * bset) list) list
- | NextRule of dependencies * (sort * bset) list
+ | AllInOne of rule list
+ | NextRule of rule
| NoMoreRules
type nominal = sort * localFormula
@@ -88,7 +93,7 @@ type constrnt =
| OpenC of node list
| UnexpandedC of node list
-type propagateElement =
+type propagateElement = (* TODO: What does the prefix "U" mean? unsat? *)
| UState of state * int option
| UCore of core * bool
| UCnstr of cset
@@ -106,6 +111,17 @@ exception CoAlg_finished of bool
val sortTable : sortTable ref
+(* evaluate a junction in the obvious way *)
+val junctionEvalBool : bool list junction -> bool
+val junctionEval: ('a -> bool) -> 'a list junction -> bool
+val optionalizeOperator: ('a -> 'b -> 'c) -> ('a option -> 'b option -> 'c option)
+val junctionEvalBoolOption : bool option list junction -> bool option
+
+(* decompose a junction in it's content and its constructor,
+ such that: eval∘junctionExtract = id
+ (with eval: X × (X -> Y) -> Y)
+ *)
+val junctionExtract: 'a junction -> ('a * ('b -> 'b junction))
(*****************************************************************************)
(* "Module type" and a specific implementation of the main queue *)
@@ -176,7 +192,7 @@ val stateGetRules : state -> (dependencies * core list) list
val stateAddRule : state -> dependencies -> core list -> int
val stateGetConstraints : state -> csetSet
val stateSetConstraints : state -> csetSet -> unit
-val stateNextRule : state -> ruleEnumeration
+val stateNextRule : state -> ruleEnumeration junction
(*****************************************************************************)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 58caaa08a50f6b5a830f97005f50c2801b36b341..81eb2ffee7fb10a0a0dd2a2528ecb5d85a223958 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -515,35 +515,68 @@ let insertCore sort bs =
c
| Some c -> c
-let insertRule state dep chldrn =
- let insert (isUns, acc) (sort, bs) =
+ (* tells whether inserting the rule makes it satisfiable:
+ Some true -> surely satisfiable
+ Some false -> surely unsat
+ None -> Not known yet
+ *)
+let insertRule state dep (chldrn: (sort * bset) list junction) : bool option =
+ let (chldrn, junc) = junctionExtract chldrn in
+ let insert (sort, bs) = (* checks if the given child node has some sat-state *)
let bs1 = bsetAddTBox sort bs in
- let core = insertCore sort bs1 in
- let isUns1 = if coreGetStatus core = Unsat then isUns else false in
- (isUns1, core::acc)
+ insertCore sort bs1
in
- let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
+ let children : core list = List.map insert chldrn in
+ (* get the sat-states of all the children, throw it back into a junction
+ (i.e. disjunction or conjunction) and then evaluate it *)
+ let satStateChildren =
+ let child2satState core = match (coreGetStatus core) with
+ | Unsat -> Some false
+ | Sat -> Some true
+ | Expandable -> None (* unknown state *)
+ | Open -> None (* unknown state *)
+ in
+ junctionEvalBoolOption (junc (List.map child2satState children))
+ in
+ let isUnsat = (satStateChildren = Some false) in
+ (* find out satisfiability *)
let idx = stateAddRule state dep (List.rev children) in
List.iter (fun c -> coreAddParent c state idx) children;
if isUnsat then begin
propagateUnsat [UState (state, Some idx)];
- false
- end else true
-
-let rec insertAllRules state = function
- | [] -> true
- | (dep, chldrn)::tl ->
- let notUnsat = insertRule state dep chldrn in
- if notUnsat then insertAllRules state tl else false
+ Some false
+ end else None
+
+ (* tells whether it is satisfiable:
+ Some true -> surely satisfiable
+ Some false -> surely unsat
+ None -> Not known yet
+ *)
+let rec insertAllRules state : rule list junction -> bool option = function
+ | Conjunctive [] -> Some true
+ | Disjunctive [] -> Some false
+ | Conjunctive ((dep, chldrn)::tl) ->
+ let satState = insertRule state dep (Conjunctive chldrn) in
+ if satState <> Some false (* if notUnsat*)
+ then insertAllRules state (Conjunctive tl)
+ else Some false
+ | Disjunctive ((dep, chldrn)::tl) ->
+ let satState = insertRule state dep (Disjunctive chldrn) in
+ if satState <> Some true (* if not Sat *)
+ then insertAllRules state (Disjunctive tl)
+ else Some true
let expandState state =
- match stateNextRule state with
+ let (rules, _) = junctionExtract (stateNextRule state) in
+ match rules with
| AllInOne rules ->
- let notUnsat = insertAllRules state rules in
- if notUnsat then stateSetStatus state Open
+ let (_, junction) = junctionExtract (stateNextRule state) in
+ let satState = insertAllRules state (junction rules) in
+ if satState <> Some false (* i.e. if not Unsat *) then stateSetStatus state Open
| NextRule (dep, chldrn) ->
- let notUnsat = insertRule state dep chldrn in
- if notUnsat then queueInsertState state else ()
+ let (_, junction) = junctionExtract (stateNextRule state) in
+ let satState = insertRule state dep (junction chldrn) in
+ if satState <> Some false (* if notUnsat *) then queueInsertState state else ()
| NoMoreRules -> stateSetStatus state Open