diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml index c2fda8b7d888e94ee1c910cc1c6bd0190bc208a2..d2ebd6b81ec29a356bd5d1b2f276d96e102e1500 100644 --- a/src/lib/CoAlgReasoner.ml +++ b/src/lib/CoAlgReasoner.ml @@ -198,7 +198,8 @@ let propagateSatMu () = let verifyParent (state,_) = let rules = stateGetRules state in let ruleiter (dependencies, corelist) = - List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat) + List.exists (fun (core : core) -> setMemCore allowedCores core || + coreGetStatus core == Sat) corelist in if List.for_all ruleiter rules @@ -213,7 +214,8 @@ let propagateSatMu () = setAddState allowedStates state; let verifyParent core = let acceptable = - List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat) + List.exists (fun (state : state) -> setMemState allowedStates state || + stateGetStatus state == Sat) (coreGetChildren core) in if acceptable @@ -228,7 +230,9 @@ let propagateSatMu () = *) let checkFinishingState (state : state) = let ruleiter (dependencies, corelist) : bool = - List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist + List.for_all (fun (core : core) -> coreGetStatus core == Unsat || + coreGetStatus core == Expandable || + not (setMemCore setCores core)) corelist in if not (List.exists ruleiter (stateGetRules state)) then begin visitParentCores state @@ -238,7 +242,9 @@ let propagateSatMu () = * to be considered for the fixpoint *) and checkFinishingCore (core : core) = - if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state)) + if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || + stateGetStatus state == Expandable || + not (setMemState setStates state)) (coreGetChildren core)) then begin visitParentStates core @@ -252,7 +258,9 @@ let propagateSatMu () = (setLengthCore setCores) = (setLengthCore allowedCores) then begin setIterState (fun state -> stateSetStatus state Sat) setStates; - setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores; + setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () + then raise (CoAlg_finished true) + else ()) setCores; end else fixpointstep allowedStates allowedCores in @@ -311,7 +319,8 @@ let rec propagateUnsat = function let prop acc core = let turnsUnsat = match coreGetStatus core with - | Open -> List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) + | Open -> List.for_all (fun s -> stateGetStatus s = Unsat) + (coreGetChildren core) | Expandable | Unsat | Sat -> false @@ -474,7 +483,8 @@ let propagateUnsatMu () = let verifyParent (state,_) = let rules = stateGetRules state in let ruleiter (dependencies, corelist) = - List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) || coreGetStatus core == Sat) + List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) || + coreGetStatus core == Sat) corelist in if List.for_all ruleiter rules @@ -489,7 +499,8 @@ let propagateUnsatMu () = setRemoveState setUnsatStates state; let verifyParent core = let acceptable = - List.exists (fun (state : state) -> not (setMemState setUnsatStates state) || stateGetStatus state == Sat) + List.exists (fun (state : state) -> not (setMemState setUnsatStates state) || + stateGetStatus state == Sat) (coreGetChildren core) in if acceptable @@ -504,9 +515,11 @@ let propagateUnsatMu () = *) let checkFinishingState (state : state) = let ruleiter (dependencies, corelist) : bool = - List.for_all (fun (core : core) -> coreGetStatus core == Unsat || setMemCore setPrevUnsatCores core) corelist + List.for_all (fun (core : core) -> coreGetStatus core == Unsat || + setMemCore setPrevUnsatCores core) corelist in - if not (List.exists ruleiter (stateGetRules state)) || stateGetStatus state == Expandable then begin + if not (List.exists ruleiter (stateGetRules state)) || + stateGetStatus state == Expandable then begin visitParentCores state end @@ -514,7 +527,8 @@ let propagateUnsatMu () = * to be considered for the fixpoint *) and checkFinishingCore (core : core) = - if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state) + if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || + setMemState setPrevUnsatStates state) (coreGetChildren core)) || coreGetStatus core == Expandable then begin