Commit 762decab authored by Simon Prucker's avatar Simon Prucker
Browse files

CoAlgReasoner oneStepFunctionState imported from master

parent b847077d
Pipeline #13258 waiting for manual action with stages
......@@ -125,6 +125,16 @@ end
(* All rule applications need to still be potentially won by Eloise for a
* State to be a valid startingpoint for this fixpoint.
*)
(*Copied function from the master for tableaux*)
let _onestepFunctionState_master resultStates (state : state) =
let ruleiter (_dependencies, corelist) : bool =
List.exists (fun (core : core) -> coreGetStatus core == Sat ||
(setMemCore (Array.get setsFPVarsCores (T.priority (stateGetFocus state)) ) core)) corelist
in
if (List.for_all ruleiter (stateGetRules state)) then begin
setAddState resultStates state
end
in
let onestepFunctionState resultStates (state : state) =
let stateSort = stateGetSort state in
let stateLabel = stateGetBs state in
......@@ -391,6 +401,16 @@ let rec propagateUnsat = function
let setsFPVarsCores = initializeFPCores (maxPrio+1) in
let resetLevel = ref 0 in
if (maxPrio mod 2 == 0) then resetLevel := maxPrio + 1 else resetLevel := maxPrio;
(*Copied function from the master for tableaux*)
let _onestepFunctionState_master resultStates (state : state) =
let ruleiter (_dependencies, corelist) : bool =
List.for_all (fun (core : core) -> (coreGetStatus core <> Sat) && ( (coreGetStatus core == Unsat) ||
(setMemCore (Array.get setsFPVarsCores (T.priority (stateGetFocus state)) ) core) )) corelist
in
if (List.exists ruleiter (stateGetRules state)) then begin
setAddState resultStates state
end
in
let onestepFunctionState resultStates (state : state) =
let stateSort = stateGetSort state in
let stateLabel = stateGetBs state in
......
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