Unverified Commit 196d1de9 authored by Merlin's avatar Merlin 💧
Browse files

Executables compiling

parent efa16205
Pipeline #13738 waiting for manual action with stages
......@@ -13,16 +13,18 @@ type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of PG.partial_solver
| Cool
exception ReasonerError of string
module type S = sig
module G : CoolGraph.S
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> game_solver
-> G.propagation_rate -> sortTable
-> CoolGraph.propagation_rate -> sortTable
-> (string -> F.sort option) ->
F.sortedFormula list -> F.sortedFormula -> bool
val initReasoner : CoAlgMisc.fragment_spec -> game_solver -> G.propagation_rate
val initReasoner : CoAlgMisc.fragment_spec -> game_solver -> CoolGraph.propagation_rate
-> sortTable -> (string -> F.sort option) ->
F.sortedFormula list
-> F.sortedFormula -> unit
......
......@@ -13,15 +13,17 @@ type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of PG.partial_solver
| Cool
exception ReasonerError of string
module type S = sig
module G : CoolGraph.S
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> game_solver
-> G.propagation_rate -> M.sortTable
-> CoolGraph.propagation_rate -> M.sortTable
-> (string -> F.sort option) ->
F.sortedFormula list -> F.sortedFormula -> bool
val initReasoner : CoAlgMisc.fragment_spec -> game_solver -> G.propagation_rate
val initReasoner : CoAlgMisc.fragment_spec -> game_solver -> CoolGraph.propagation_rate
-> sortTable -> (string -> F.sort option) ->
F.sortedFormula list
-> F.sortedFormula -> unit
......
......@@ -11,8 +11,6 @@ module PG = Paritygame
module C = CoAlgFormula
module R_com = CoAlgReasoner
exception ReasonerError of string
module Make(T : FocusTracker) = struct
module G = CoolGraph.Make(T)
module Logics = CoAlgLogics.Make(T)
......@@ -190,7 +188,7 @@ let rec propagateUnsat = function
| UState (state, _idxopt) -> begin
match stateGetStatus state with
| Unsat -> tl
| Sat -> raise (ReasonerError ("Propagation tells state "
| Sat -> raise (R_com.ReasonerError ("Propagation tells state "
^(string_of_int (stateGetIdx state))
^" would be unsat, but it is already sat"))
| Open
......@@ -224,7 +222,7 @@ let rec propagateUnsat = function
| UCore (core, comesFromCnstr) -> begin
match coreGetStatus core with
| Unsat -> tl
| Sat -> raise (ReasonerError ("Propagation tells core "
| Sat -> raise (R_com.ReasonerError ("Propagation tells core "
^(string_of_int (coreGetIdx core))
^" would be unsat, but it is already sat"))
| Open
......
......@@ -10,8 +10,6 @@ module CU = CoolUtils
module PG = Paritygame
module R_com = CoAlgReasoner
exception ReasonerError of string
module Make(T : FocusTracker) = struct
module G = CoolGraph.Make(T)
module Logics = CoAlgLogics.Make(T)
......@@ -186,7 +184,7 @@ let rec propagateUnsat = function
| UState (state, _idxopt) -> begin
match stateGetStatus state with
| Unsat -> tl
| Sat -> raise (ReasonerError ("Propagation tells state "
| Sat -> raise (R_com.ReasonerError ("Propagation tells state "
^(string_of_int (stateGetIdx state))
^" would be unsat, but it is already sat"))
| Open
......@@ -220,7 +218,7 @@ let rec propagateUnsat = function
| UCore (core, comesFromCnstr) -> begin
match coreGetStatus core with
| Unsat -> tl
| Sat -> raise (ReasonerError ("Propagation tells core "
| Sat -> raise (R_com.ReasonerError ("Propagation tells core "
^(string_of_int (coreGetIdx core))
^" would be unsat, but it is already sat"))
| Open
......@@ -1055,8 +1053,6 @@ let reasonerFinished () =
| Sat -> true
| Open -> queueIsEmpty ()
type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
@param verbose An optional switch which determines
whether the procedure shall print some information on the standard output.
......
(** 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 C = CoAlgFormula
type sortTable = CoAlgMisc.sortTable
type nomTable = string -> CoAlgFormula.sort option
type assumptions = CoAlgFormula.sortedFormula list
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
exception ReasonerError of string
module type S = sig
module G : CoolGraph.S
type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
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 : ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver -> propagation_rate
-> sortTable -> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list
-> CoAlgFormula.sortedFormula -> unit
(** Run a single step of the reasoner. That is: Expand one node and perform sat
propagation.
This is used in the debugger.
*)
val runReasonerStep : unit -> unit
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 ?(onestep = false) () =
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.
*)
(*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_onestep resultStates (state : state) =
let stateSort = stateGetSort state in
let stateLabel = stateGetBs state in
let statePriority = T.priority (stateGetFocus state) in
let x_i = Array.get setsFPVarsCores statePriority in
let usableCores = List.filter (fun core -> ((setMemCore x_i core) || (coreGetStatus core = Sat))) (stateGetChildren state) in
let usableCoreLabels = CU.TList.safe_map coreGetBs usableCores in
let (func, _) = !sortTable.(stateSort) in
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.
*)
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
(* 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 ?(onestep = false) () =
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;
(*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_onestep resultStates (state : state) =
let stateSort = stateGetSort state in
let stateLabel = stateGetBs state in
let statePriority = T.priority (stateGetFocus state) in
let x_i = Array.get setsFPVarsCores statePriority in
let usableCores = List.filter (fun core -> (not (setMemCore x_i core)) && (coreGetStatus core <> Unsat)) (stateGetChildren state) in
let usableCoreLabels = CU.TList.safe_map coreGetBs usableCores in
let (func, _) = !sortTable.(stateSort) in
if (not (Logics.oneStepSatisfiability func usableCoreLabels (stateSort, stateLabel))) then begin
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)
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)