Commit b90164e6 authored by Simon Prucker's avatar Simon Prucker
Browse files

optional onestep argument for CoalgReasoner isSat

parent 762decab
Pipeline #13297 waiting for manual action with stages
......@@ -29,12 +29,14 @@ type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> game_solver
val isSat : ?verbose:bool -> ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver
-> propagation_rate -> sortTable
-> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
val initReasoner : CoAlgMisc.fragment_spec -> game_solver -> propagation_rate
val initReasoner : ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver -> propagation_rate
-> sortTable -> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list
-> CoAlgFormula.sortedFormula -> unit
......@@ -73,7 +75,7 @@ module HashSet = struct
Hashtbl.iter f_intern set
end
let propagateSatMu () =
let propagateSatMu ?(onestep = false) () =
let maxPrio = graphMaxPriority () in
let setStates = setEmptyState () in
......@@ -126,7 +128,7 @@ end
* State to be a valid startingpoint for this fixpoint.
*)
(*Copied function from the master for tableaux*)
let _onestepFunctionState_master resultStates (state : state) =
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
......@@ -135,7 +137,7 @@ end
setAddState resultStates state
end
in
let onestepFunctionState resultStates (state : state) =
let onestepFunctionState_onestep resultStates (state : state) =
let stateSort = stateGetSort state in
let stateLabel = stateGetBs state in
let statePriority = T.priority (stateGetFocus state) in
......@@ -146,11 +148,17 @@ end
if (Logics.oneStepSatisfiability func usableCoreLabels (stateSort, stateLabel)) then begin
setAddState resultStates state
end
in
let onestepFunctionState =
if onestep (*somehow access onestep flag from options*)
then onestepFunctionState_onestep
else onestepFunctionState_master
in
(* There needs to be a State still potentially Sat for this core
* to be considered for the fixpoint.
*)
in
let onestepFunctionCore resultCores (core : core) =
if (List.exists (fun (state : state) -> stateGetStatus state == Sat ||
(setMemState (Array.get setsFPVarsStates (T.priority (coreGetFocus core))) state))) (coreGetChildren core)
......@@ -355,7 +363,7 @@ let rec propagateUnsat = function
in
propagateUnsat tl1
let propagateUnsatMu () =
let propagateUnsatMu ?(onestep = false) () =
let maxPrio = graphMaxPriority () in
(* Partition set of nodes according to their priorities
......@@ -402,7 +410,7 @@ let rec propagateUnsat = function
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 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
......@@ -411,7 +419,7 @@ let rec propagateUnsat = function
setAddState resultStates state
end
in
let onestepFunctionState resultStates (state : state) =
let onestepFunctionState_onestep resultStates (state : state) =
let stateSort = stateGetSort state in
let stateLabel = stateGetBs state in
let statePriority = T.priority (stateGetFocus state) in
......@@ -423,6 +431,11 @@ let rec propagateUnsat = function
setAddState resultStates state
end
in
let onestepFunctionState =
if onestep (*access onestep flag from options*)
then onestepFunctionState_onestep
else onestepFunctionState_master
in
let onestepFunctionCore resultCores (core : core) =
if (List.for_all (fun (state : state) -> (stateGetStatus state <> Sat) && ((stateGetStatus state == Unsat) ||
(setMemState (Array.get setsFPVarsStates (T.priority (coreGetFocus core))) state)))) (coreGetChildren core)
......@@ -1089,10 +1102,10 @@ let expandCnstr cset =
(* The Main Loop *)
(*****************************************************************************)
let propagateMu () = propagateSatMu (); propagateUnsatMu ()
let propagateMu ?(_onestep=false) () = propagateSatMu ~onestep:_onestep (); propagateUnsatMu ~onestep:_onestep ()
(* Solver to use. Will be set by initReasoner. *)
let solver = ref propagateMu
let solver = ref (propagateMu ~_onestep: false)
let expandNodesLoop (recursiveAction: unit -> unit) =
match queueGetElement () with
......@@ -1130,7 +1143,7 @@ type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
let initReasoner fragSpec game_solver propagation_rate sorts nomTable tbox sf =
let initReasoner ?(onestep=false) fragSpec game_solver propagation_rate sorts nomTable tbox sf =
sortTable := Array.copy sorts;
let (_tbox1, _sf1, bs) = ppFormulae fragSpec nomTable tbox sf in
let sort = fst sf in
......@@ -1138,7 +1151,7 @@ let initReasoner fragSpec game_solver propagation_rate sorts nomTable tbox sf =
let focus = T.init sort bs in
begin
match game_solver with
| Cool -> solver := propagateMu
| Cool -> solver := propagateMu ~_onestep: onestep
| PGSolver algo -> solver := fun () -> solveGameWithPGsolver algo
| PGSolverLocal algo -> solver := fun () -> solveGameWithPGsolverLocal algo
end;
......@@ -1177,9 +1190,9 @@ type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
@return True if sf is satisfiable wrt tbox, false otherwise.
*)
let isSat ?(verbose = false) fragSpec game_solver propagation_rate sorts nomTable tbox sf =
let isSat ?(verbose = false) ?(onestep = false)fragSpec game_solver propagation_rate sorts nomTable tbox sf =
let start = if verbose then Unix.gettimeofday () else 0. in
initReasoner fragSpec game_solver propagation_rate sorts nomTable tbox sf;
initReasoner ~onestep: onestep fragSpec game_solver propagation_rate sorts nomTable tbox sf;
let sat =
try
buildGraphLoop ();
......
......@@ -27,13 +27,15 @@ type game_solver = PGSolver of Paritygame.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> game_solver
val isSat : ?verbose:bool -> ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver
-> propagation_rate -> sortTable
-> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
val initReasoner : CoAlgMisc.fragment_spec -> game_solver -> propagation_rate
val initReasoner : ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver -> propagation_rate
-> sortTable -> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list
-> CoAlgFormula.sortedFormula -> unit
......
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