Unverified Commit 1ed47632 authored by Merlin's avatar Merlin 💧
Browse files

Bit of refactoring and got it to compile

parent 1853b71b
Pipeline #13729 waiting for manual action with stages
......@@ -282,6 +282,10 @@ let lhtFind lht lit =
try
Some (LHt.find lht lit)
with Not_found -> None
let lhtMustFind lht l =
match lhtFind lht l with
| Some f -> f
| None -> assert false
let fhtInit () = FHt.create 16
let fhtAdd fht f lit = FHt.add fht f lit
......@@ -289,6 +293,10 @@ let fhtFind fht f =
try
Some (FHt.find fht f)
with Not_found -> None
let fhtMustFind fht f =
match fhtFind fht f with
| Some l -> l
| None -> assert false
let fhtReset fht = FHt.reset fht
let nhtInit () = NHt.create 8
......
......@@ -132,10 +132,12 @@ val formulaTypeIsModality: formulaType -> bool
val lhtInit : unit -> lht
val lhtAdd : lht -> Minisat_cool.lit -> localFormula -> unit
val lhtFind : lht -> Minisat_cool.lit -> localFormula option
val lhtMustFind : lht -> Minisat_cool.lit -> localFormula
val fhtInit : unit -> fht
val fhtAdd : fht -> localFormula -> Minisat_cool.lit -> unit
val fhtFind : fht -> localFormula -> Minisat_cool.lit option
val fhtMustFind : fht -> localFormula -> Minisat_cool.lit
val fhtReset : fht -> unit
val nhtInit : unit -> nht
......
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
@author Florian Widmann, Daniel Hausmann
*)
open CoAlgMisc
open FocusTracking
module M = Minisat_cool
module CU = CoolUtils
module PG = Paritygame
module R_com = CoAlgReasoner_common
module F = CoAlgFormula
module M = CoAlgMisc
type sortTable = CoAlgMisc.sortTable
type sortTable = M.sortTable
type nomTable = string -> F.sort option
type nomTable = string -> CoAlgFormula.sort option
type assumptions = F.sortedFormula list
type assumptions = CoAlgFormula.sortedFormula list
type input = sortTable * nomTable * assumptions * F.sortedFormula
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
exception ReasonerError of string
type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of PG.partial_solver
| Cool
module type S = sig
module G : CoolGraph.S
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> game_solver
-> G.propagation_rate -> sortTable
-> (string -> F.sort option) ->
F.sortedFormula list -> F.sortedFormula -> bool
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> R_com.game_solver
-> R_com.propagation_rate -> sortTable
-> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
val initReasoner : CoAlgMisc.fragment_spec -> R_com.game_solver -> R_com.propagation_rate
-> sortTable -> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list
-> CoAlgFormula.sortedFormula -> unit
val initReasoner : CoAlgMisc.fragment_spec -> game_solver -> G.propagation_rate
-> sortTable -> (string -> F.sort option) ->
F.sortedFormula list
-> F.sortedFormula -> unit
(** Run a single step of the reasoner. That is: Expand one node and perform sat
propagation.
......@@ -46,1114 +38,3 @@ val reasonerFinished : unit -> bool
val isRootSat : unit -> bool option
end
module Make(T : FocusTracker) = struct
module G = CoolGraph.Make(T)
module Logics = CoAlgLogics.Make(T)
open G
module PG_Map = ParityGameMapping
(*****************************************************************************)
(* Propagation of Satisfiability *)
(*****************************************************************************)
module HashSet = struct
let create size = Hashtbl.create size
let add set value =
Hashtbl.replace set value ()
let iter f set =
let f_intern k _ = f k in
Hashtbl.iter f_intern set
end
let propagateSatMu () =
let maxPrio = graphMaxPriority () in
let setStates = setEmptyState () in
let setCores = setEmptyCore () in
let openstates = ref 0 in
let setsEmptyState ind = Array.init ind (fun _ -> setEmptyState ()) in
let setsEmptyCore ind = Array.init ind (fun _ -> setEmptyCore ()) in
let setsPriorityStates = setsEmptyState (maxPrio + 1) in
let setsPriorityCores = setsEmptyCore (maxPrio + 1) in
(* Partition set of nodes according to their priorities
*)
let stateCollector state =
match stateGetStatus state with
| Unsat -> ()
| Sat -> ()
| Expandable -> ()
| Open ->
openstates := !openstates + 1;
setAddState (Array.get setsPriorityStates (T.priority (stateGetFocus state))) state;
setAddState setStates state;
(* As it is enough for a core to have one child that Eloise wins, we can
* also handle (some) expandable cores.
*)
and coreCollector core =
match coreGetStatus core with
| Unsat -> ()
| Sat -> ()
| Expandable ->
setAddCore (Array.get setsPriorityCores (T.priority (coreGetFocus core))) core;
setAddCore setCores core;
| Open ->
setAddCore (Array.get setsPriorityCores (T.priority (coreGetFocus core))) core;
setAddCore setCores core;
in
graphIterStates stateCollector;
graphIterCores coreCollector;
if getPropagationRate () == Adaptive then
setPropagationCounter !openstates
else ();
let initializeFPStates ind = Array.init ind (fun i -> if (i mod 2 == 0) then setStates else (setEmptyState ())) in
let initializeFPCores ind = Array.init ind (fun i -> if (i mod 2 == 0) then setCores else (setEmptyCore ())) in
let setsFPVarsStates = initializeFPStates (maxPrio+1) in
let setsFPVarsCores = initializeFPCores (maxPrio+1) in
let resetLevel = ref 0 in
if (maxPrio mod 2 == 1) then resetLevel := maxPrio + 1 else resetLevel := maxPrio;
(* All rule applications need to still be potentially won by Eloise for a
* State to be a valid startingpoint for this fixpoint.
*)
let onestepFunctionState 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
(* 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)
then begin
setAddCore resultCores core
end
in
(* given the input arrays of sets (setsFPVars{States,Cores}), compute starters for this
* vector and then compute nodes for which Eloise can enforce reaching a starter
*)
let rec computeFixpoint ind =
if (ind == 0) then begin
let resultStates = setEmptyState () in
let resultCores = setEmptyCore () in
setIterState (onestepFunctionState resultStates) setStates;
setIterCore (onestepFunctionCore resultCores) setCores;
if ((setLengthState (Array.get setsFPVarsStates ind)) == (setLengthState resultStates)) &&
((setLengthCore (Array.get setsFPVarsCores ind)) == (setLengthCore resultCores))
then begin
(resultStates, resultCores)
end
else begin
Array.set setsFPVarsStates ind (resultStates);
Array.set setsFPVarsCores ind (resultCores);
computeFixpoint ind
end
end
else begin
if (ind mod 2 == 1) && (ind < !resetLevel) then begin
Array.set setsFPVarsStates ind (setEmptyState ());
Array.set setsFPVarsCores ind (setEmptyCore ());
resetLevel := ind;
end;
let (resultStates, resultCores) = computeFixpoint (ind - 1) in
if (((setLengthState (Array.get setsFPVarsStates ind)) == (setLengthState resultStates)) &&
((setLengthCore (Array.get setsFPVarsCores ind)) == (setLengthCore resultCores))) ||
((setLengthState (Array.get setsPriorityStates ind) == 0) && (setLengthCore (Array.get setsPriorityCores ind) == 0))
then begin
resetLevel := ind + 1;
(resultStates, resultCores)
end
else begin
Array.set setsFPVarsStates ind (resultStates);
Array.set setsFPVarsCores ind (resultCores);
computeFixpoint ind;
end
end
in
let (resultStates, resultCores) = computeFixpoint maxPrio in
setIterState (fun state -> stateSetStatus state Sat) resultStates;
setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot ()
then begin
raise (CoAlg_finished true)
end
else ()) resultCores
(*****************************************************************************)
(* Propagation of Unsatisfiability *)
(*****************************************************************************)
let isConstraintUnsat cset =
match graphFindCnstr cset with
| None -> assert false
| Some UnsatC -> true
| _ -> false
let fhtMustFind fht f =
match fhtFind fht f with
| Some l -> l
| None -> assert false
let lhtMustFind lht l =
match lhtFind lht l with
| Some f -> f
| None -> assert false
(* Gets a list of Things we know are unsatisfiable and propagates this
information backwards *)
let rec propagateUnsat = function
| [] -> ()
| propElem::tl ->
let tl1 =
match propElem with
| UState (state, _idxopt) -> begin
match stateGetStatus state with
| Unsat -> tl
| Sat -> raise (ReasonerError ("Propagation tells state "
^(string_of_int (stateGetIdx state))
^" would be unsat, but it is already sat"))
| Open
| Expandable ->
let mbs = stateGetBs state
(* match idxopt with *)
(* | None -> stateGetBs state *)
(* | Some idx -> *)
(* let (dep, children) = stateGetRule state idx in *)
(* let getBs core = *)
(* assert (coreGetStatus core = Unsat); *)
(* coreGetBs core *)
(* in *)
(* dep (List.map getBs children) *)
in
stateSetBs state mbs;
stateSetStatus state Unsat;
let prop acc core =
let turnsUnsat =
match coreGetStatus core with
| Open -> List.for_all (fun s -> stateGetStatus s = Unsat)
(coreGetChildren core)
| Expandable
| Unsat
| Sat -> false
in
if turnsUnsat then (UCore (core, false))::acc else acc
in
List.fold_left prop tl (stateGetParents state)
end
| UCore (core, comesFromCnstr) -> begin
match coreGetStatus core with
| Unsat -> tl
| Sat -> raise (ReasonerError ("Propagation tells core "
^(string_of_int (coreGetIdx core))
^" would be unsat, but it is already sat"))
| Open
| Expandable ->
let mbs =
if comesFromCnstr then coreGetBs core
else
let bs = coreGetBs core in
let solver = coreGetSolver core in
let fht = coreGetFht core in
let lht = lhtInit () in
let addLits f acc =
let lit = fhtMustFind fht f in
lhtAdd lht lit f;
lit::acc
in
let litset = bsetFold addLits bs [] in
let addClauses state =
let cbs = stateGetBs state in
let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in
let okay = M.add_clause solver clause in
assert okay
in
List.iter addClauses (coreGetChildren core);
let isSat = M.invoke_solver solver litset in
assert (not isSat);
let res = bsetMake () in
let confls = M.get_conflict solver in
List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls;
res
in
coreSetBs core mbs;
coreSetStatus core Unsat;
coreDeallocateSolver core;
if core == graphGetRoot () then raise (CoAlg_finished false) else ();
let prop acc (state, idx) =
let turnsUnsat =
match stateGetStatus state with
| Open
| Expandable ->
List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
| Unsat
| Sat -> false
in
if turnsUnsat then (UState (state, Some idx))::acc else acc
in
let tl2 = List.fold_left prop tl (coreGetParents core) in
List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
end
| UCnstr cset ->
match graphFindCnstr cset with
| None
| Some SatC -> assert false
| Some UnsatC -> tl
| Some (UnexpandedC nodes)
| Some (OpenC nodes) ->
graphReplaceCnstr cset UnsatC;
let prop acc node =
match node with
| State state ->
let turnsUnsat =
match stateGetStatus state with
| Expandable
| Open -> cssForall isConstraintUnsat (stateGetConstraints state)
| Unsat
| Sat -> false
in
if turnsUnsat then (UState (state, None))::acc else acc
| Core core ->
let turnsUnsat =
match coreGetStatus core with
| Expandable
| Open -> cssForall isConstraintUnsat (coreGetConstraints core)
| Unsat
| Sat -> false
in
if turnsUnsat then (UCore (core, true))::acc else acc
in
List.fold_left prop tl nodes
in
propagateUnsat tl1
let propagateUnsatMu () =
let maxPrio = graphMaxPriority () in
(* Partition set of nodes according to their priorities
*
* This also marks trivially successful nodes.
*)
let setStates = setEmptyState () in
let setCores = setEmptyCore () in
let openstates = ref 0 in
let setsEmptyState ind = Array.init ind (fun _ -> setEmptyState ()) in
let setsEmptyCore ind = Array.init ind (fun _ -> setEmptyCore ()) in
let setsPriorityStates = setsEmptyState (maxPrio + 1) in
let setsPriorityCores = setsEmptyCore (maxPrio + 1) in
let stateCollector state =
match stateGetStatus state with
| Sat -> ()
| Unsat -> ()
| Expandable -> ()
| Open ->
openstates := !openstates + 1;
setAddState (Array.get setsPriorityStates (T.priority (stateGetFocus state))) state;
setAddState setStates state;
and coreCollector core =
match coreGetStatus core with
| Sat -> ()
| Unsat -> ()
| Expandable -> ()
| Open ->
setAddCore (Array.get setsPriorityCores (T.priority (coreGetFocus core))) core;
setAddCore setCores core;
in
graphIterStates stateCollector;
graphIterCores coreCollector;
if getPropagationRate () == Adaptive then
setPropagationCounter !openstates
else ();
let initializeFPStates ind = Array.init ind (fun i -> if (i mod 2 == 1) then setStates else (setEmptyState ())) in
let initializeFPCores ind = Array.init ind (fun i -> if (i mod 2 == 1) then setCores else (setEmptyCore ())) in
let setsFPVarsStates = initializeFPStates (maxPrio+1) in
let setsFPVarsCores = initializeFPCores (maxPrio+1) in
let resetLevel = ref 0 in
if (maxPrio mod 2 == 0) then resetLevel := maxPrio + 1 else resetLevel := maxPrio;
let onestepFunctionState 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 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)
then begin
setAddCore resultCores core
end
in
let rec computeFixpoint ind =
if (ind == 0) then begin
if (ind mod 2 == 0) && (ind < !resetLevel) then begin
Array.set setsFPVarsStates ind (setEmptyState ());
Array.set setsFPVarsCores ind (setEmptyCore ());
resetLevel := ind;
end;
let resultStates = setEmptyState () in
let resultCores = setEmptyCore () in
setIterState (onestepFunctionState resultStates) setStates;
setIterCore (onestepFunctionCore resultCores) setCores;
if ((setLengthState (Array.get setsFPVarsStates ind)) == (setLengthState resultStates)) &&
((setLengthCore (Array.get setsFPVarsCores ind)) == (setLengthCore resultCores))
then begin
resetLevel := ind + 1;
(resultStates, resultCores)
end
else begin
Array.set setsFPVarsStates ind (resultStates);
Array.set setsFPVarsCores ind (resultCores);
computeFixpoint ind
end
end
else begin
if (ind mod 2 == 1) && (ind < !resetLevel) then begin
Array.set setsFPVarsStates ind (setStates);
Array.set setsFPVarsCores ind (setCores);
resetLevel := ind;
end;
let (resultStates, resultCores) = computeFixpoint (ind - 1) in
if (((setLengthState (Array.get setsFPVarsStates ind)) == (setLengthState resultStates)) &&
((setLengthCore (Array.get setsFPVarsCores ind)) == (setLengthCore resultCores))) ||
((setLengthState (Array.get setsPriorityStates ind) == 0) && (setLengthCore (Array.get setsPriorityCores ind) == 0))
then begin
resetLevel := ind + 1;
(resultStates, resultCores)
end
else begin
Array.set setsFPVarsStates ind (resultStates);
Array.set setsFPVarsCores ind (resultCores);
computeFixpoint ind;
end
end
in
let (resultStates, resultCores) = computeFixpoint maxPrio in
setIterState (fun state -> stateSetStatus state Unsat) resultStates;
setIterCore (fun core -> coreSetStatus core Unsat; if core == graphGetRoot ()
then begin
raise (CoAlg_finished false)
end
else ()) resultCores
(*****************************************************************************)
(* Game solging with pgsolver *)
(*****************************************************************************)
let solveGameWithPGsolver algo =
let seenOpen = HashSet.create (graphSizeCore ()) in
let stateGetIdxOr node state =
match stateGetStatus state with
| Expandable ->
(match node with | None -> stateGetIdx state | Some idx -> idx)
| Sat -> PG_Map.sat_node
| Unsat -> PG_Map.unsat_node
| Open -> stateGetIdx state
in
let coreGetIdxOr node core =
match coreGetStatus core with
| Expandable ->
(match node with | None -> coreGetIdx core | Some idx -> idx)
| Sat -> PG_Map.sat_node
| Unsat -> PG_Map.unsat_node
| Open -> coreGetIdx core
in
let coreGetIdxOr1 core =
match coreGetStatus core with
| Expandable -> begin match coreGetChildren core with
| [] -> PG_Map.unsat_node
| _ -> coreGetIdx core
end
| Sat -> PG_Map.sat_node
| Unsat -> PG_Map.unsat_node
| Open -> coreGetIdx core
in
let emptyToSat = function
| [] -> [PG_Map.sat_node]
| x -> x
in
let nodeSucessors1 node =
match PG_Map.find node with
| PG_Map.State state -> emptyToSat (List.map fst (stateGetRulesWithIndex state))
| PG_Map.Core core -> List.map (stateGetIdxOr (Some PG_Map.unsat_node)) (coreGetChildren core)
| PG_Map.Rule (_,cores) -> List.map coreGetIdxOr1 cores
| PG_Map.Sat -> [PG_Map.sat_node]
| PG_Map.Unsat -> [PG_Map.unsat_node]
in
let nodeSucessors2 node =
match PG_Map.find node with
| PG_Map.State state -> emptyToSat (List.map fst (stateGetRulesWithIndex state))
| PG_Map.Core core -> List.map (stateGetIdxOr (Some PG_Map.sat_node)) (coreGetChildren core)
| PG_Map.Rule (_,cores) -> List.map (coreGetIdxOr (Some PG_Map.sat_node)) cores
| PG_Map.Sat -> [PG_Map.sat_node]
| PG_Map.Unsat -> [PG_Map.unsat_node]
in
let eloise = PG.plr_Even in
let abelard = PG.plr_Odd in
let nodeData node =
match PG_Map.find node with
| PG_Map.State state ->
HashSet.add seenOpen node;
(T.priority (stateGetFocus state), abelard)
| PG_Map.Core core ->
HashSet.add seenOpen node;
(T.priority (coreGetFocus core), eloise)
| PG_Map.Rule (state,_) -> (T.priority (stateGetFocus state), eloise)
| PG_Map.Sat -> (2, eloise)
| PG_Map.Unsat -> (1, abelard)
in
let root_idx1 = coreGetIdxOr1 (graphGetRoot ()) in
let root_idx2 = coreGetIdxOr (Some PG_Map.sat_node) (graphGetRoot ()) in
(* Generate data as required by PG.pg_init *)
let game1 = PG.pg_create (PG_Map.size ()) in
let game2 = PG.pg_create (PG_Map.size ()) in
let rec populate game succ node =
if PG.pg_get_owner game node <> PG.plr_undef then () else begin
let (prio, player) = nodeData node in
let children = succ node in
PG.pg_set_owner game node player;
PG.pg_set_priority game node prio;
List.iter (fun child -> begin
populate game succ child;
PG.pg_add_edge game node child
end) children
end
in