Skip to content
GitLab
Commit b856538d authored by Thorsten Wißmann's avatar Thorsten Wißmann
Browse files

Make junctions compile

parent 5ebac877
Hide whitespace changes
Inline Side-by-side
src/lib/CoAlgLogics.ml
View file @ b856538d
......@@ -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
......
src/lib/CoAlgMisc.ml
View file @ b856538d
......@@ -173,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 *)
......
src/lib/CoAlgMisc.mli
View file @ b856538d
......@@ -55,7 +55,6 @@ type setCore
type setCnstr
(*****************************************************************************)
(* Types that are hard coded into the algorithm *)
(*****************************************************************************)
......@@ -94,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
......@@ -112,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 *)
......
src/lib/CoAlgReasoner.ml
View file @ b856538d
......@@ -515,40 +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 : rule list junction -> bool = function (* tells whether it is notUnsat *)
| [] -> 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 =
let (junction, rules) =
match stateNextRule state with
| Disjunctive r -> (fun x -> Disjunctive x, r)
| Conjunctive r -> (fun x -> Conjunctive x, r)
in
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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment