### Profile

Statistics
| Branch: | Revision:

## cool / src / lib / CoAlgReasoner.ml @ e765822b

 1 ```(** A graph-tableau-based decision procedure framework for coalgebraic logics. ``` ``` @author Florian Widmann, Daniel Hausmann ``` ``` *) ``` ```open CoAlgMisc ``` ```open FocusTracking ``` ```module M = Minisat ``` ```module CU = CoolUtils ``` ```module PG = Paritygame ``` ```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 ``` ```val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable ``` ``` -> (string -> CoAlgFormula.sort option) -> ``` ``` CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool ``` ```val initReasoner : CoAlgMisc.fragment_spec -> 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 ``` ``` type 'a t = ('a, unit) Hashtbl.t ``` ``` 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 = ref 0 in ``` ``` (* get highest priority that occurs in open or expandable states or cores *) ``` ``` (* alternative: *) ``` ``` (* let maxPrio = (!MiscSolver.nrFormulae * (maxAlternationDepth ()))+2 in *) ``` ``` let getMaxPrioStates state = ``` ``` let prioState state = T.priority (stateGetFocus state) in ``` ``` if (prioState state > !maxPrio) then (maxPrio := prioState state;) ``` ``` in ``` ``` let getMaxPrioCores core = ``` ``` let prioCore core = T.priority (coreGetFocus core) in ``` ``` if (prioCore core > !maxPrio) then (maxPrio := prioCore core;) ``` ``` in ``` ``` graphIterStates getMaxPrioStates; ``` ``` graphIterCores getMaxPrioCores; ``` ``` let setStates = setEmptyState () in ``` ``` let setCores = setEmptyCore () in ``` ``` let setStartersStates = setEmptyState () in ``` ``` let setStartersCores = setEmptyCore () in ``` ``` let openstates = ref 0 in ``` ``` let emptySet = bsetMakeRealEmpty () 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; ``` ``` setPropagationCounter !openstates; ``` ``` 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 propagateUnsatMu () = ``` ``` (* let maxPrio = (!MiscSolver.nrFormulae * (maxAlternationDepth ()))+2 in *) ``` ``` let maxPrio = ref 0 in ``` ``` (* get highest priority that occurs in open or expandable states or cores *) ``` ``` let getMaxPrioStates state = ``` ``` let prioState state = T.priority (stateGetFocus state) in ``` ``` if (prioState state > !maxPrio) then (maxPrio := prioState state;) ``` ``` in ``` ``` let getMaxPrioCores core = ``` ``` let prioCore core = T.priority (coreGetFocus core) in ``` ``` if (prioCore core > !maxPrio) then (maxPrio := prioCore core;) ``` ``` in ``` ``` graphIterStates getMaxPrioStates; ``` ``` graphIterCores getMaxPrioCores; ``` ``` (* Partition set of nodes according to their priorities ``` ``` * ``` ``` * This also marks trivially successful nodes. ``` ``` *) ``` ``` let setStates = setEmptyState () in ``` ``` let setCores = setEmptyCore () in ``` ``` let setStartersStates = setEmptyState () in ``` ``` let setStartersCores = setEmptyCore () in ``` ``` let openstates = ref 0 in ``` ``` let emptySet = bsetMakeRealEmpty () 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; ``` ``` setPropagationCounter !openstates; ``` ``` 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 ``` ```(*****************************************************************************) ``` ```(* Node Expansions *) ``` ```(*****************************************************************************) ``` ```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 ``` ```let getLit sort fht solver f = ``` ``` match fhtFind fht f with ``` ``` | Some lit -> lit ``` ``` | None -> ``` ``` let var = M.new_variable solver in ``` ``` let lit = M.var_to_lit var true in ``` ``` fhtAdd fht f lit; ``` ``` let () = ``` ``` match lfGetNeg sort f with ``` ``` | None -> () ``` ``` | Some nf -> ``` ``` let nlit = M.neg_lit lit in ``` ``` fhtAdd fht nf nlit; ``` ``` in ``` ``` lit ``` ```let newCore sort bs defer = ``` ``` (* when creating a now core from a set of formulas bs ``` ``` bs = { x_1, ...., x_n } ``` ``` = "x_1 /\ .... /\ x_n" ``` ``` Then we do this by: ``` ``` 1. creating a new literal in the sat solver for each ``` ``` "boolean subformula" from the x_i. "boolean subformula" means that ``` ``` this subformula is not hidden under modalities but only under ``` ``` boolean connectives (/\, \/). ``` ``` 2. encoding the relation between a formula and its intermediate boolean ``` ``` subformulas by a clause: ``` ``` *) ``` ``` let fht = fhtInit () in ``` ``` let solver = M.new_solver () in ``` ``` let rec addClauses f = ``` ``` (* step 1: create a literal in the satsolver representing the formula f *) ``` ``` let lf = getLit sort fht solver f in ``` ``` (* step 2: encode relation to possible subformulas *) ``` ``` match lfGetType sort f with ``` ``` | OrF -> ``` ``` (* ``` ``` case 2.(a) f = f1 \/ f2 ``` ``` fill fht such that it says: ``` ``` f |---> lf ``` ``` f1 |---> lf1 ``` ``` f2 |---> lf2 ``` ``` *) ``` ``` let f1 = lfGetDest1 sort f in ``` ``` let f2 = lfGetDest2 sort f in ``` ``` addClauses f1; ``` ``` addClauses f2; ``` ``` let lf1 = fhtMustFind fht f1 in ``` ``` let lf2 = fhtMustFind fht f2 in ``` ``` (* ``` ``` encode the structure of f by adding the clause (lf -> lf1 \/ lf2) ``` ``` *) ``` ``` let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in ``` ``` assert (okay) ``` ``` | AndF -> ``` ``` (* ``` ``` case 2.(b) f = f1 /\ f2 ``` ``` fill fht such that it says: ``` ``` f |---> lf ``` ``` f1 |---> lf1 ``` ``` f2 |---> lf2 ``` ``` *) ``` ``` let f1 = lfGetDest1 sort f in ``` ``` let f2 = lfGetDest2 sort f in ``` ``` addClauses f1; ``` ``` addClauses f2; ``` ``` let lf1 = fhtMustFind fht f1 in ``` ``` let lf2 = fhtMustFind fht f2 in ``` ``` (* ``` ``` encode the structure of f by adding the clauses ``` ``` (lf -> lf1) /\ (lf -> lf2) ``` ``` *) ``` ``` let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in ``` ``` assert (okay1); ``` ``` let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in ``` ``` assert (okay2) ``` ``` | MuF ``` ``` | NuF -> ``` ``` (* ``` ``` Dest of a fixpoint is it's unfolded version. This adds just ``` ``` an simple forward implication that could be optimised out ``` ``` though not without nontrivial transformation of code ``` ``` f = \u03bc X . \u03c6 |---> lf ``` ``` \u03c6[X |-> f] |---> lf1 ``` ``` Then adding lf -> lf1 to minisat ``` ``` *) ``` ``` let f1 = lfGetDest1 sort f in ``` ``` addClauses f1; ``` ``` let lf1 = fhtMustFind fht f1 in ``` ``` let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in ``` ``` assert (okay1); ``` ``` | _ -> () ``` ``` (* case 2.(c) ``` ``` We don't need to do anything except adding f to the fht ``` ``` *) ``` ``` in ``` ``` bsetIter addClauses bs; ``` ``` coreMake sort bs defer (Some solver) fht ``` ```let getNextState core = ``` ``` (* Create a new state, which is obtained by a satisfying assignment of the ``` ``` literals of the minisat solver. ``` ``` In addition to that, feed the negation of the satisfying assignment back ``` ``` to the minisat solver in order to obtain different solutions on successive ``` ``` minisat calls. ``` ``` *) ``` ``` let bs = coreGetBs core in ``` ``` let focus = T.make_transient (coreGetFocus core) in ``` ``` let fht = coreGetFht core in ``` ``` let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in ``` ``` let solver = coreGetSolver core in ``` ``` let isSat = M.invoke_solver solver litset in ``` ``` (* Clearly, if the current core is unsatisfiable, no further child state can ``` ``` be created *) ``` ``` if not isSat then None ``` ``` else ``` ``` let sort = coreGetSort core in ``` ``` (* create a new set of formulas newbs with the property: ``` ``` if the conjunction of newbs is satisfiable, then the present core is ``` ``` satisfiable. ``` ``` *) ``` ``` let newbs = bsetMake () in ``` ``` (* if newbs = { l_1, .... l_n }, i.e. ``` ``` newbs = l_1 /\ ... /\ l_n ``` ``` then we can get essentially different satisfying assignments of bs by ``` ``` adding another clause ``` ``` clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n ``` ``` By mkExclClause, newbs is filled, and clause is built in the accumulator acc. ``` ``` *) ``` ``` let rec mkExclClause tracker f acc = ``` ``` (* f is a formula that is true in the current satisfying assignment *) ``` ``` match lfGetType sort f with ``` ``` | OrF -> ``` ``` (* if f is true and a disjunction, then one of its disjuncts is true *) ``` ``` let f1 = lfGetDest1 sort f in ``` ``` let lf1 = fhtMustFind fht f1 in ``` ``` (* if the first disjunct f1 is true, then we need to add subformulas ``` ``` of f1 to newbs&clause *) ``` ``` if M.literal_status solver lf1 = M.LTRUE then ``` ``` mkExclClause (T.track1 tracker f1) f1 acc ``` ``` else ``` ``` (* otherwise f2 must be true *) ``` ``` let f2 = lfGetDest2 sort f in ``` ``` let lf2 = fhtMustFind fht f2 in ``` ``` assert (M.literal_status solver lf2 = M.LTRUE); ``` ``` mkExclClause (T.track1 tracker f2) f2 acc ``` ``` | AndF -> ``` ``` (* if the true f is a conjuction, then both conjunctions must be true *) ``` ``` let f1 = lfGetDest1 sort f in ``` ``` let lf1 = fhtMustFind fht f1 in ``` ``` assert (M.literal_status solver lf1 = M.LTRUE); ``` ``` let acc1 = mkExclClause (T.track1 tracker f1) f1 acc in ``` ``` let f2 = lfGetDest2 sort f in ``` ``` let lf2 = fhtMustFind fht f2 in ``` ``` assert (M.literal_status solver lf2 = M.LTRUE); ``` ``` mkExclClause (T.track1 tracker f2) f2 acc1 ``` ``` | MuF ``` ``` | NuF -> ``` ``` let f1 = lfGetDest1 sort f in ``` ``` mkExclClause (T.track1 tracker f1) f1 acc ``` ``` | _ -> ``` ``` (* if f is a trivial formula or modality, then add it ... *) ``` ``` (* ... to newbs *) ``` ``` bsetAdd newbs f; ``` ``` T.apply tracker focus; ``` ``` (* ... and to the new clause *) ``` ``` (M.neg_lit (fhtMustFind fht f))::acc ``` ``` in ``` ``` let init_clause f acc = ``` ``` let tracker = T.begin_tracking (coreGetFocus core) focus sort f in ``` ``` mkExclClause tracker f acc ``` ``` in ``` ``` let clause = bsetFold init_clause bs [] in ``` ``` let okay = M.add_clause solver clause in ``` ``` assert (okay); ``` ``` Some (sort, newbs, T.finalize focus) ``` ```let newState sort bs focus = ``` ``` let (func, sl) = !sortTable.(sort) in ``` ``` let producer = Logics.getExpandingFunctionProducer func in ``` ``` let exp = producer sort bs focus sl in ``` ``` stateMake sort bs focus exp ``` ```let insertState parent sort bs focus = ``` ``` let child = ``` ``` match graphFindState sort (bs, focus) with ``` ``` | None -> ``` ``` let s = newState sort bs focus in ``` ``` graphInsertState sort (bs, focus) s; ``` ``` queueInsertState s; ``` ``` s ``` ``` | Some s -> s ``` ``` in ``` ``` coreAddChild parent child; ``` ``` stateAddParent child parent ``` ```let expandCore core = ``` ``` match getNextState core with ``` ``` | Some (sort, bs, focus) -> ``` ``` insertState core sort bs focus; ``` ``` queueInsertCore core ``` ``` | None -> ``` ``` let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in ``` ``` if isUnsat ``` ``` then ``` ``` coreSetStatus core Unsat ``` ``` else ``` ``` coreSetStatus core Open ``` ```let insertCore sort bs focus = ``` ``` match graphFindCore sort (bs, focus) with ``` ``` | None -> ``` ``` let c = newCore sort bs focus in ``` ``` graphInsertCore sort (bs, focus) c; ``` ``` queueInsertCore c; ``` ``` c ``` ``` | Some c -> c ``` ```(** Insert cores for the children generated by a modal rule application. ``` ``` * ``` ``` * @return true if all new cores are already unsatisfiable, false otherwise ``` ``` *) ``` ```let insertRule state dep chldrn = ``` ``` let chldrn = listFromLazylist chldrn in ``` ``` let mkCores (sort, bs, defer) = ``` ``` let bs1 = bsetAddTBox sort bs in ``` ``` (* For the aconjunctive fragment, instead of adding a core annotated with ``` ``` * all deferrals, we add a core for each formula in the deferral set. *) ``` ``` let deferSingletons = [defer] in ``` ``` List.map (insertCore sort (bsetCopy bs1)) deferSingletons ``` ``` in ``` ``` (* A list of cores for each child: [[child1a;child1b]; [child2a;child2b]] *) ``` ``` let coresPerChild = List.map mkCores chldrn in ``` ``` (* All combinations that take a core from each child: ``` ``` * [[ch1a;ch2a]; [ch1a;ch2b]; [ch1b;ch2a]; [ch1b;ch2b]] ``` ``` * Neccesary because stateAddRule expects each child to have only one core. *) ``` ``` let coresPerRule = CU.TList.combinations coresPerChild in ``` ``` let addRule cores = ``` ``` let idx = stateAddRule state dep cores in ``` ``` List.iter (fun c -> coreAddParent c state idx) cores; ``` ``` if List.for_all (fun core -> coreGetStatus core = Unsat) cores then begin ``` ``` stateSetStatus state Unsat; ``` ``` true ``` ``` end else ``` ``` false ``` ``` in ``` ``` List.mem true (List.map (fun r -> addRule r) coresPerRule) ``` ``` ``` ```(** Call insertRule on all rules ``` ``` * @return true if any rule application generated only unsat cores ``` ``` *) ``` ```let rec insertAllRules state rules = ``` ``` List.mem true (List.map (fun (dep, children) -> insertRule state dep children) rules) ``` ```let expandState state = ``` ``` let setSatOrOpen () = ``` ``` if CU.TList.empty (stateGetRules state) then ``` ``` stateSetStatus state Sat ``` ``` else ``` ``` stateSetStatus state Open ``` ``` in ``` ``` match stateNextRule state with ``` ``` | MultipleElements rules -> ``` ``` let unsat = insertAllRules state rules in ``` ``` if not unsat then setSatOrOpen () ``` ``` | SingleElement (dep, chldrn) -> ``` ``` let unsat = insertRule state dep chldrn in ``` ``` if not unsat then queueInsertState state else () ``` ``` | NoMoreElements -> ``` ``` setSatOrOpen () ``` ```let expandCnstr cset = ``` ``` let nht = nhtInit () in ``` ``` let mkCores f = ``` ``` let (sort, lf) as nom = atFormulaGetNominal f in ``` ``` let nomset = ``` ``` match nhtFind nht nom with ``` ``` | Some ns -> ns ``` ``` | None -> ``` ``` let cset1 = csetCopy cset in ``` ``` csetRemDot cset1; ``` ``` let bs = csetAddTBox sort cset1 in ``` ``` bsetAdd bs lf; ``` ``` nhtAdd nht nom bs; ``` ``` bs ``` ``` in ``` ``` bsetAdd nomset (atFormulaGetSubformula f) ``` ``` in ``` ``` csetIter cset mkCores; ``` ``` let inCores (sort, _) bs (isUns, acc) = ``` ``` let core = insertCore sort bs (T.init sort bs) in ``` ``` coreAddConstraintParent core cset; ``` ``` (coreGetStatus core = Unsat || isUns, core::acc) ``` ``` in ``` ``` let (isUnsat, children) = nhtFold inCores nht (false, []) in ``` ``` if isUnsat then () ``` ``` else ``` ``` match graphFindCnstr cset with ``` ``` | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents) ``` ``` | _ -> assert false ``` ```(*****************************************************************************) ``` ```(* The Main Loop *) ``` ```(*****************************************************************************) ``` ```let expandNodesLoop (recursiveAction: unit -> unit) = ``` ``` match queueGetElement () with ``` ``` | QState state -> ``` ``` if stateGetStatus state = Expandable then begin ``` ``` expandState state; ``` ``` if doSatPropagation () then begin propagateSatMu (); propagateUnsatMu () end; ``` ``` end else (); ``` ``` recursiveAction () ``` ``` | QCore core -> ``` ``` if coreGetStatus core = Expandable then begin ``` ``` expandCore core; ``` ``` if doSatPropagation () then begin propagateSatMu (); propagateUnsatMu () end; ``` ``` end else (); ``` ``` recursiveAction () ``` ``` | QCnstr cset -> ``` ``` expandCnstr cset; ``` ``` recursiveAction () ``` ``` | QEmpty -> () ``` ```let runReasonerStep () = ``` ``` let void () = () in ``` ``` expandNodesLoop void; (* expand at most one node *) ``` ``` propagateSatMu (); ``` ``` propagateUnsatMu (); ``` ``` (* if this emptied the queue *) ``` ``` if queueIsEmpty () then begin ``` ``` end else () (* else: the next step would be to expand another node *) ``` ```let rec buildGraphLoop () = ``` ``` let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in ``` ``` expandNodesFurther (); (* expand as many queue elements as possible *) ``` ``` if queueIsEmpty () then () else buildGraphLoop () ``` ```let initReasoner fragSpec sorts nomTable tbox sf = ``` ``` sortTable := Array.copy sorts; ``` ``` let (tbox1, sf1, bs) = ppFormulae fragSpec nomTable tbox sf in ``` ``` let sort = fst sf in ``` ``` let bs1 = bsetAddTBox sort bs in ``` ``` let focus = T.init sort bs in ``` ``` graphInit (); ``` ``` queueInit (); ``` ``` PG_Map.reset (); ``` ``` let root = insertCore sort bs1 focus in ``` ``` graphAddRoot root ``` ```let isRootSat () = ``` ``` match coreGetStatus (graphGetRoot ()) with ``` ``` | Expandable -> None ``` ``` | Unsat -> Some false ``` ``` | Sat -> Some true ``` ``` | Open -> if (queueIsEmpty()) then Some true else None ``` ```let reasonerFinished () = ``` ``` match coreGetStatus (graphGetRoot ()) with ``` ``` | Expandable -> false ``` ``` | Unsat ``` ``` | Sat -> true ``` ``` | Open -> queueIsEmpty () ``` ```(** 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. ``` ``` The default is false. ``` ``` @param sorts An array mapping each sort (represented as an integer) ``` ``` to a functor and a list of sorts which are the arguments of the functor. ``` ``` @param nomTable A partial function mapping nominals (represented as strings) ``` ``` to their sorts. ``` ``` @param tbox A list of sorted formulae. ``` ``` @param sf A sorted formula. ``` ``` @return True if sf is satisfiable wrt tbox, false otherwise. ``` ``` *) ``` ```let isSat ?(verbose = false) fragSpec sorts nomTable tbox sf = ``` ``` let start = if verbose then Unix.gettimeofday () else 0. in ``` ``` initReasoner fragSpec sorts nomTable tbox sf; ``` ``` let sat = ``` ``` try ``` ``` buildGraphLoop (); ``` ``` propagateSatMu (); ``` ``` propagateUnsatMu (); ``` ``` (* print_endline ("Tableau fully expanded, final propagation gave no winner! "); *) ``` ``` (* get whether the root is satisfiable *) ``` ``` (* we know that the reasoner finished, so the value is there, *) ``` ``` (* i.e. isRootSat() will give a "Some x" and not "None" *) ``` ``` CU.fromSome (isRootSat()) ``` ``` with CoAlg_finished res -> res ``` ``` in ``` ``` (* print some statistics *) ``` ``` if verbose then ``` ``` let stop = Unix.gettimeofday () in ``` ``` let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in ``` ``` print_newline (); ``` ``` print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf)); ``` ``` let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in ``` ``` print_endline ("Added Size: " ^ (string_of_int size)); ``` ``` (* ``` ``` print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1)); ``` ``` let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in ``` ``` print_endline ("Added Size: " ^ (string_of_int nsize)); ``` ``` *) ``` ``` print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable."); ``` ``` print_endline ("Time: " ^ (string_of_float (stop -. start))); ``` ``` print_endline ("Generated states: " ^ (string_of_int (graphSizeState ()))); ``` ``` print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ()))); ``` ``` print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ()))); ``` ``` print_newline () ``` ``` else (); ``` ``` sat ``` ```end ``` ```(* vim: set et sw=2 sts=2 ts=8 : *) ```