Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.ml @ 7c4d2eb4

History | View | Annotate | Download (26.8 KB)

 1 ```(** Common types, functions, and data structures for the CoAlgebraic reasoner. ``` ``` @author Florian Widmann ``` ``` *) ``` ```module S = MiscSolver ``` ```module L = List ``` ```module C = CoAlgFormula ``` ```module HC = HashConsing ``` ```(** An instantiation of a set (of the standard library) for bitsets. ``` ``` *) ``` ```module BsSet = Set.Make( ``` ``` struct ``` ``` type t = S.bitset ``` ``` let (compare : t -> t -> int) = S.compareBS ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for bitsets. ``` ``` *) ``` ```module GHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = S.bitset ``` ``` let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0 ``` ``` let hash (bs : t) = S.hashBS bs ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for literals. ``` ``` *) ``` ```module LHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = Minisat.lit ``` ``` let equal (l1 : t) l2 = l1 = l2 ``` ``` let hash (l : t) = (l :> int) ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for formulae. ``` ``` *) ``` ```module FHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = int ``` ``` let equal (f1 : t) f2 = f1 = f2 ``` ``` let hash (f : t) = f ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for nominals. ``` ``` *) ``` ```module NHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = int * int ``` ``` let equal ((s1, f1) : t) (s2, f2) = (s1 = s2) && (f1 = f2) ``` ``` let hash ((s, f) : t) = (((s+f)*(s+f+1)) / 2) + f ``` ``` end ``` ```) ``` ```(*****************************************************************************) ``` ```(* Types that can be modified rather easily *) ``` ```(* (of course you then have to modify the implementations below too) *) ``` ```(*****************************************************************************) ``` ```(* This type must be extended for additional logics. *) ``` ```type functors = ``` ``` | MultiModalK ``` ``` | MultiModalKD ``` ``` | CoalitionLogic ``` ``` | GML ``` ``` | Choice ``` ``` | Fusion ``` ```(* This type may be extended for additional logics. *) ``` ```type formulaType = ``` ``` | Other ``` ``` | ConstF ``` ``` | AndF ``` ``` | OrF ``` ``` | AtF ``` ``` | NomF ``` ``` | ExF (* Existential / diamond *) ``` ``` | AxF (* Universal / box *) ``` ``` | EnforcesF (* diamond of CL *) ``` ``` | AllowsF (* box of CL *) ``` ``` | MoreThanF (* more than n successors = diamond in gml *) ``` ``` | MaxExceptF(* at most n exceptions = box in gml *) ``` ``` | ChcF (* Choice *) ``` ``` | FusF (* Fusion *) ``` ```type localFormula = int ``` ```type bset = S.bitset ``` ```type atFormula = int ``` ```type cset = S.bitset ``` ```type csetSet = BsSet.t ``` ```type lht = localFormula LHt.t ``` ```type fht = Minisat.lit FHt.t ``` ```type nht = bset NHt.t ``` ```type state = { sortS : sort; mutable bsS : bset; mutable statusS : nodeStatus; ``` ``` mutable parentsS : core list; mutable childrenS : (dependencies * core list) list; ``` ``` mutable constraintsS : csetSet; expandFkt : stateExpander } ``` ```and core = { sortC : sort; mutable bsC : bset; mutable statusC : nodeStatus; ``` ``` mutable parentsC : (state * int) list; mutable childrenC : state list; ``` ``` mutable constraintsC : csetSet; solver : Minisat.solver; fht : fht; ``` ``` mutable constraintParents : cset list } ``` ```and setState = state GHt.t ``` ```and setCore = core GHt.t ``` ```and setCnstr = unit GHt.t ``` ```(*****************************************************************************) ``` ```(* Types that are hard coded into the algorithm *) ``` ```(*****************************************************************************) ``` ```and stateExpander = unit -> ruleEnumeration ``` ```and sort = C.sort ``` ```and nodeStatus = ``` ``` | Expandable ``` ``` | Open ``` ``` | Sat ``` ``` | Unsat ``` ```and dependencies = bset list -> bset ``` ```and ruleEnumeration = ``` ``` | AllInOne of (dependencies * (sort * bset) list) list ``` ``` | NextRule of dependencies * (sort * bset) list ``` ``` | NoMoreRules ``` ```type nominal = sort * localFormula ``` ```type node = ``` ``` | State of state ``` ``` | Core of core ``` ```type constrnt = ``` ``` | UnsatC ``` ``` | SatC ``` ``` | OpenC of node list ``` ``` | UnexpandedC of node list ``` ```type propagateElement = ``` ``` | UState of state * int option ``` ``` | UCore of core * bool ``` ``` | UCnstr of cset ``` ```type queueElement = ``` ``` | QState of state ``` ``` | QCore of core ``` ``` | QCnstr of cset ``` ``` | QEmpty ``` ```type sortTable = (functors * int list) array ``` ```exception CoAlg_finished of bool ``` ```let sortTable = ref (Array.make 0 (MultiModalK, [1])) ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of the main queue *) ``` ```(*****************************************************************************) ``` ```let queueStates = ref ([] : state list) ``` ```let queueCores1 = ref ([] : core list) ``` ```let queueCores2 = ref ([] : core list) ``` ```let queueCnstrs = ref ([] : cset list) ``` ```let doPropagation = ref false ``` ```let queueInit () = ``` ``` queueStates := []; ``` ``` queueCores1 := []; ``` ``` queueCores2 := []; ``` ``` queueCnstrs := []; ``` ``` doPropagation := false ``` ```let queueIsEmpty () = ``` ``` !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = [] ``` ```let queueInsertState state = queueStates := state::!queueStates ``` ```let queueInsertCore core = queueCores2 := core::!queueCores2 ``` ```let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs ``` ```let queueGetElement () = ``` ``` if !queueCnstrs <> [] then ``` ``` let res = List.hd !queueCnstrs in ``` ``` queueCnstrs := List.tl !queueCnstrs; ``` ``` QCnstr res ``` ``` else if !queueStates <> [] then ``` ``` let res = List.hd !queueStates in ``` ``` queueStates := List.tl !queueStates; ``` ``` QState res ``` ``` else if !queueCores1 <> [] then ``` ``` let res = List.hd !queueCores1 in ``` ``` queueCores1 := List.tl !queueCores1; ``` ``` QCore res ``` ``` else if !queueCores2 = [] then QEmpty ``` ``` else ``` ``` let res = List.hd !queueCores2 in ``` ``` doPropagation := true; ``` ``` queueCores1 := List.tl !queueCores2; ``` ``` queueCores2 := []; ``` ``` QCore res ``` ```let doNominalPropagation () = !doPropagation ``` ```let doSatPropagation () = ``` ``` let res = !doPropagation in ``` ``` doPropagation := false; ``` ``` res ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of the graph *) ``` ```(*****************************************************************************) ``` ```let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t)) ``` ```let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t)) ``` ```let graphCnstrs = ref (GHt.create 0 : constrnt GHt.t) ``` ```let graphRoot = ref (None : core option) ``` ```let graphInit () = ``` ``` let size = Array.length !sortTable in ``` ``` graphStates := Array.init size (fun _ -> GHt.create 128); ``` ``` graphCores := Array.init size (fun _ -> GHt.create 128); ``` ``` graphCnstrs := GHt.create 128; ``` ``` graphRoot := None ``` ```let graphIterStates fkt = ``` ``` Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates ``` ```let graphIterCores fkt = ``` ``` Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores ``` ```let graphIterCnstrs fkt = GHt.iter fkt !graphCnstrs ``` ```let graphClearCnstr () = ``` ``` let newGraph = GHt.create (GHt.length !graphCnstrs) in ``` ``` let copyCnstr cset cnstr = ``` ``` match cnstr with ``` ``` | UnsatC ``` ``` | SatC -> GHt.add newGraph cset cnstr ``` ``` | OpenC _ -> GHt.add newGraph cset (OpenC []) ``` ``` | UnexpandedC _ -> GHt.add newGraph cset (UnexpandedC []) ``` ``` in ``` ``` GHt.iter copyCnstr !graphCnstrs; ``` ``` graphCnstrs := newGraph ``` ```let graphFindState sort bs = ``` ``` try ``` ``` Some (GHt.find !graphStates.(sort) bs) ``` ``` with Not_found -> None ``` ```let graphFindCore sort bs = ``` ``` try ``` ``` Some (GHt.find !graphCores.(sort) bs) ``` ``` with Not_found -> None ``` ```let graphFindCnstr cset = ``` ``` try ``` ``` Some (GHt.find !graphCnstrs cset) ``` ``` with Not_found -> None ``` ```let graphInsertState sort bs state = ``` ``` assert (not (GHt.mem !graphStates.(sort) bs)); ``` ``` GHt.add !graphStates.(sort) bs state ``` ```let graphInsertCore sort bs core = ``` ``` assert (not (GHt.mem !graphCores.(sort) bs)); ``` ``` GHt.add !graphCores.(sort) bs core ``` ```let graphInsertCnstr cset cnstr = ``` ``` assert (not (GHt.mem !graphCnstrs cset)); ``` ``` GHt.add !graphCnstrs cset cnstr ``` ```let graphReplaceCnstr cset cnstr = ``` ``` GHt.replace !graphCnstrs cset cnstr ``` ```let graphSizeState () = ``` ``` Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates ``` ```let graphSizeCore () = ``` ``` Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores ``` ```let graphSizeCnstr () = GHt.length !graphCnstrs ``` ```let graphAddRoot core = ``` ``` if !graphRoot = None then graphRoot := Some core ``` ``` else raise (C.CoAlgException "Root of graph is already set.") ``` ```let graphGetRoot () = ``` ``` match !graphRoot with ``` ``` | None -> raise (C.CoAlgException "Root of graph is not set.") ``` ``` | Some core -> core ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of sets of constraints *) ``` ```(*****************************************************************************) ``` ```let cssEmpty = BsSet.empty ``` ```let cssExists fkt css = BsSet.exists fkt css ``` ```let cssForall fkt css = BsSet.for_all fkt css ``` ```let cssUnion css1 css2 = BsSet.union css1 css2 ``` ```let cssAdd cset css = BsSet.add cset css ``` ```let cssFold fkt css init = BsSet.fold fkt css init ``` ```let cssSingleton cset = BsSet.singleton cset ``` ```let cssEqual css1 css2 = BsSet.equal css1 css2 ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of state nodes *) ``` ```(*****************************************************************************) ``` ```let stateMake sort bs exp = ``` ``` { sortS = sort; bsS = bs; statusS = Expandable; parentsS = []; childrenS = []; ``` ``` constraintsS = cssEmpty; expandFkt = exp } ``` ```let stateGetSort state = state.sortS ``` ```let stateGetBs state = state.bsS ``` ```let stateSetBs state bs = state.bsS <- bs ``` ```let stateGetStatus state = state.statusS ``` ```let stateSetStatus state status = state.statusS <- status ``` ```let stateGetParents state = state.parentsS ``` ```let stateAddParent state parent = state.parentsS <- parent::state.parentsS ``` ```let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx) ``` ```let stateGetRules state = state.childrenS ``` ```let stateAddRule state dep children = ``` ``` state.childrenS <- (dep, children)::state.childrenS; ``` ``` List.length state.childrenS ``` ```let stateGetConstraints state = state.constraintsS ``` ```let stateSetConstraints state csets = state.constraintsS <- csets ``` ```let stateNextRule state = state.expandFkt () ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of core nodes *) ``` ```(*****************************************************************************) ``` ```let coreMake sort bs solver fht = ``` ``` { sortC = sort; bsC = bs; statusC = Expandable; parentsC = []; childrenC = []; ``` ``` constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [] } ``` ```let coreGetSort core = core.sortC ``` ```let coreGetBs core = core.bsC ``` ```let coreSetBs core bs = core.bsC <- bs ``` ```let coreGetStatus core = core.statusC ``` ```let coreSetStatus core status = core.statusC <- status ``` ```let coreGetParents core = core.parentsC ``` ```let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC ``` ```let coreGetChildren core = core.childrenC ``` ```let coreAddChild core child = core.childrenC <- child::core.childrenC ``` ```let coreGetConstraints core = core.constraintsC ``` ```let coreSetConstraints core csets = core.constraintsC <- csets ``` ```let coreGetSolver core = core.solver ``` ```let coreGetFht core = core.fht ``` ```let coreGetConstraintParents core = core.constraintParents ``` ```let coreAddConstraintParent core cset = ``` ``` core.constraintParents <- cset::core.constraintParents ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of sets of *) ``` ```(* states, cores, and constraints for the sat propagation *) ``` ```(*****************************************************************************) ``` ```let setEmptyState () = GHt.create 16 ``` ```let setEmptyCore () = GHt.create 16 ``` ```let setEmptyCnstr () = GHt.create 16 ``` ```let setAddState set state = GHt.add set (stateGetBs state) state ``` ```let setAddCore set core = GHt.add set (coreGetBs core) core ``` ```let setAddCnstr set cset = GHt.add set cset () ``` ```let setMemState set state = GHt.mem set (stateGetBs state) ``` ```let setMemCore set core = GHt.mem set (coreGetBs core) ``` ```let setMemCnstr set cset = GHt.mem set cset ``` ```let setRemoveState set state = GHt.remove set (stateGetBs state) ``` ```let setRemoveCore set core = GHt.remove set (coreGetBs core) ``` ```let setRemoveCnstr set cset = GHt.remove set cset ``` ```let setIterState fkt set = GHt.iter (fun _ state -> fkt state) set ``` ```let setIterCore fkt set = GHt.iter (fun _ core -> fkt core) set ``` ```let setIterCnstr fkt set = GHt.iter (fun cset () -> fkt cset) set ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of the mapping *) ``` ```(* between (local) formulae and literals of the sat solver, *) ``` ```(* and of a mapping of nominals to sets of formulae *) ``` ```(*****************************************************************************) ``` ```let lhtInit () = LHt.create 16 ``` ```let lhtAdd lht lit f = LHt.add lht lit f ``` ```let lhtFind lht lit = ``` ``` try ``` ``` Some (LHt.find lht lit) ``` ``` with Not_found -> None ``` ```let fhtInit () = FHt.create 16 ``` ```let fhtAdd fht f lit = FHt.add fht f lit ``` ```let fhtFind fht f = ``` ``` try ``` ``` Some (FHt.find fht f) ``` ``` with Not_found -> None ``` ```let nhtInit () = NHt.create 8 ``` ```let nhtAdd nht nom bs = NHt.add nht nom bs ``` ```let nhtFind nht nom = ``` ``` try ``` ``` Some (NHt.find nht nom) ``` ``` with Not_found -> None ``` ```let nhtFold fkt nht init = NHt.fold fkt nht init ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of sets of *) ``` ```(* local formulae and @-formulae *) ``` ```(*****************************************************************************) ``` ```let tboxTable = ref (Array.make 0 S.dummyBS) ``` ```let bsetMake () = S.makeBS () ``` ```let bsetAdd bs lf = S.addBSNoChk bs lf ``` ```let bsetMem bs lf = S.memBS bs lf ``` ```let bsetRem bs lf = S.remBS bs lf ``` ```let bsetMakeRealEmpty () = ``` ``` let res = bsetMake () in ``` ``` bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *) ``` ``` res ``` ```let bsetCopy bs = S.copyBS bs ``` ```let bsetFold fkt bs init = S.foldBS fkt bs init ``` ```let bsetIter fkt bset = S.iterBS fkt bset ``` ```let bsetFilter (a: bset) (f: localFormula -> bool) : bset = ``` ``` let res = bsetMakeRealEmpty () in ``` ``` bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a; ``` ``` res ``` ```let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort) ``` ```let csetCompare cs1 cs2 = S.compareBS cs1 cs2 ``` ```let csetMake () = S.makeBS () ``` ```let csetAdd cs lf = S.addBSNoChk cs lf ``` ```let csetCopy cs = S.copyBS cs ``` ```let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2 ``` ```let csetHasDot cs = S.memBS cs !S.bsfalse ``` ```let csetAddDot cs = S.addBSNoChk cs !S.bsfalse ``` ```let csetRemDot cs = S.remBS cs !S.bsfalse ``` ```let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort) ``` ```let csetIter cs fkt = ``` ``` let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in ``` ``` S.iterBS fkt2 cs ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of *) ``` ```(* local formulae and @-formulae *) ``` ```(*****************************************************************************) ``` ```(** This table maps integers (representing formulae) to their corresponding formulae. ``` ``` *) ``` ```let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE)) ``` ```(** This table maps integers (representing formulae) to their corresponding type. ``` ``` *) ``` ```let arrayType = ref (Array.make 0 (Array.make 0 Other)) ``` ```(** This lookup table maps formulae (represented as integers) ``` ``` to their negation (in negation normal form). ``` ``` *) ``` ```let arrayNeg = ref (Array.make 0 (Array.make 0 (-1))) ``` ```(** These lookup tables map formulae (represented as integers) ``` ``` to their decompositions (represented as integers). ``` ``` This is done according to the rules of the tableau procedure ``` ``` and depends on the type of the formulae. ``` ``` *) ``` ```let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1))) (* first subformula *) ``` ```let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1))) (* second subformula *) ``` ```let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1))) (* a role *) ``` ```let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1))) (* an integer *) ``` ```let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *) ``` ```(** This lookup table maps formulae (represented as integers) ``` ``` to their @-wrapper. ``` ``` *) ``` ```let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64))) ``` ```let lfGetType sort f = !arrayType.(sort).(f) ``` ```let lfGetDest1 sort f = !arrayDest1.(sort).(f) ``` ```let lfGetDest2 sort f = !arrayDest2.(sort).(f) ``` ```let lfGetDest3 sort f = !arrayDest3.(sort).(f) ``` ```let lfGetDestNum sort f = !arrayDestNum.(sort).(f) ``` ```let lfGetDestAg sort f = !arrayDestAg.(sort).(f) ``` ```let lfGetNeg sort f = ``` ``` let nf = !arrayNeg.(sort).(f) in ``` ``` if nf >= 0 then Some nf else None ``` ```let lfGetAt (sort, nom) f = ``` ``` FHt.find !arrayAt.(sort).(f) nom ``` ```let lfToInt lf = lf ``` ```let lfFromInt num = num ``` ```let atFormulaGetSubformula f = !arrayDest1.(0).(f) ``` ```let atFormulaGetNominal f = ``` ``` let s = !arrayDest3.(0).(f) in ``` ``` let n = !arrayDest2.(0).(f) in ``` ``` (s, n) ``` ```let lfToAt _ lf = lf ``` ```let rec detClosure nomTbl hcF fset atset nomset s f = ``` ``` if s < 0 || s >= Array.length fset then ``` ``` let sstr = string_of_int s in ``` ``` raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr)) ``` ``` else (); ``` ``` if C.HcFHt.mem fset.(s) f then () ``` ``` else ``` ``` let () = C.HcFHt.add fset.(s) f () in ``` ``` let (func, sortlst) = !sortTable.(s) in ``` ``` match f.HC.node with ``` ``` | C.HCTRUE ``` ``` | C.HCFALSE -> () ``` ``` | C.HCAP name -> ``` ``` if C.isNominal name then begin ``` ``` Hashtbl.replace nomset name s; ``` ``` match nomTbl name with ``` ``` | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name)) ``` ``` | Some sort -> ``` ``` if sort <> s then ``` ``` let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in ``` ``` let str2 = " is used in sort " ^ (string_of_int s) ^ "." in ``` ``` raise (C.CoAlgException (str1 ^ str2)) ``` ``` else () ``` ``` end else () ``` ``` | C.HCNOT _ -> () ``` ``` | C.HCAT (name, f1) -> ``` ``` C.HcFHt.replace atset f (); ``` ``` let s1 = ``` ``` match nomTbl name with ``` ``` | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name)) ``` ``` | Some sort -> sort ``` ``` in ``` ``` let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in ``` ``` detClosure nomTbl hcF fset atset nomset s1 hcnom; ``` ``` detClosure nomTbl hcF fset atset nomset s1 f1 ``` ``` | C.HCOR (f1, f2) ``` ``` | C.HCAND (f1, f2) -> ``` ``` detClosure nomTbl hcF fset atset nomset s f1; ``` ``` detClosure nomTbl hcF fset atset nomset s f2 ``` ``` | C.HCEX (_, f1) ``` ``` | C.HCAX (_, f1) -> ``` ``` if (func <> MultiModalK && func <> MultiModalKD) ``` ``` || List.length sortlst <> 1 ``` ``` then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.") ``` ``` else (); ``` ``` detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1 ``` ``` | C.HCENFORCES (_, f1) ``` ``` | C.HCALLOWS (_, f1) -> ``` ``` if func <> CoalitionLogic || List.length sortlst <> 1 ``` ``` then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.") ``` ``` else (); ``` ``` detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1 ``` ``` | C.HCMORETHAN (_,_,f1) ``` ``` | C.HCMAXEXCEPT (_,_,f1) -> ``` ``` if func <> GML || List.length sortlst <> 1 ``` ``` then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.") ``` ``` else (); ``` ``` detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1 ``` ``` | C.HCCHC (f1, f2) ``` ``` | C.HCCHCN (f1, f2) -> ``` ``` if func <> Choice || List.length sortlst <> 2 then ``` ``` raise (C.CoAlgException "Choice formula is used in wrong sort.") ``` ``` else (); ``` ``` detClosure nomTbl hcF fset atset nomset (List.nth sortlst 0) f1; ``` ``` detClosure nomTbl hcF fset atset nomset (List.nth sortlst 1) f2 ``` ``` | C.HCFUS (first, f1) -> ``` ``` if func <> Fusion || List.length sortlst <> 2 then ``` ``` raise (C.CoAlgException "Fusion formula is used in wrong sort.") ``` ``` else (); ``` ``` let s1 = List.nth sortlst (if first then 0 else 1) in ``` ``` detClosure nomTbl hcF fset atset nomset s1 f1 ``` ```let detClosureAt hcF atset name f () = ``` ``` match f.HC.node with ``` ``` | C.HCTRUE ``` ``` | C.HCFALSE ``` ``` | C.HCOR _ ``` ``` | C.HCAND _ ``` ``` | C.HCAT _ -> () ``` ``` | _ -> ``` ``` let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in ``` ``` C.HcFHt.replace atset at () ``` ```(** Initialises the arrays for a formula and its integer representation. ``` ``` *) ``` ```let initTables nomTbl hcF htF htR s f n = ``` ``` !arrayFormula.(s).(n) <- f.HC.fml; ``` ``` let fneg = f.HC.neg in ``` ``` if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg; ``` ``` let (_, sortlst) = !sortTable.(s) in ``` ``` match f.HC.node with ``` ``` | C.HCTRUE ``` ``` | C.HCFALSE -> !arrayType.(s).(n) <- ConstF ``` ``` | C.HCAP name -> ``` ``` if C.isNominal name then !arrayType.(s).(n) <- NomF ``` ``` else !arrayType.(s).(n) <- Other ``` ``` | C.HCNOT _ -> !arrayType.(s).(n) <- Other ``` ``` | C.HCAT (name, f1) -> ``` ``` !arrayType.(s).(n) <- AtF; ``` ``` let s1 = ``` ``` match nomTbl name with ``` ``` | None -> assert false ``` ``` | Some sort -> sort ``` ``` in ``` ``` let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s1) hcnom; ``` ``` !arrayDest3.(s).(n) <- s1 ``` ``` | C.HCOR (f1, f2) -> ``` ``` !arrayType.(s).(n) <- OrF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2 ``` ``` | C.HCAND (f1, f2) -> ``` ``` !arrayType.(s).(n) <- AndF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2 ``` ``` | C.HCEX (role, f1) -> ``` ``` !arrayType.(s).(n) <- ExF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDest3.(s).(n) <- ``` ``` if Hashtbl.mem htR role then Hashtbl.find htR role ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR role size; ``` ``` size ``` ``` | C.HCAX (role, f1) -> ``` ``` !arrayType.(s).(n) <- AxF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDest3.(s).(n) <- ``` ``` if Hashtbl.mem htR role then Hashtbl.find htR role ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR role size; ``` ``` size ``` ``` | C.HCENFORCES (aglist, f1) -> (* aglist = list of agents *) ``` ``` !arrayType.(s).(n) <- EnforcesF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDestAg.(s).(n) <- Array.of_list aglist ``` ``` | C.HCALLOWS (aglist, f1) -> (* aglist = list of agents *) ``` ``` !arrayType.(s).(n) <- AllowsF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDestAg.(s).(n) <- Array.of_list aglist ``` ``` | C.HCMORETHAN (cnt,role,f1) -> ``` ``` !arrayType.(s).(n) <- MoreThanF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDestNum.(s).(n) <- cnt; ``` ``` !arrayDest3.(s).(n) <- ``` ``` if Hashtbl.mem htR role then Hashtbl.find htR role ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR role size; ``` ``` size ``` ``` | C.HCMAXEXCEPT (cnt,role,f1) -> ``` ``` !arrayType.(s).(n) <- MaxExceptF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDestNum.(s).(n) <- cnt; ``` ``` !arrayDest3.(s).(n) <- ``` ``` if Hashtbl.mem htR role then Hashtbl.find htR role ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR role size; ``` ``` size ``` ``` | C.HCCHC (f1, f2) ``` ``` | C.HCCHCN (f1, f2) -> ``` ``` !arrayType.(s).(n) <- ChcF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2 ``` ``` | C.HCFUS (first, f1) -> ``` ``` !arrayType.(s).(n) <- FusF; ``` ``` let s1 = List.nth sortlst (if first then 0 else 1) in ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1; ``` ``` !arrayDest3.(s).(n) <- if first then 0 else 1 ``` ```let initTablesAt hcF htF name sort = ``` ``` let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in ``` ``` let nom = C.HcFHt.find htF.(sort) hcnom in ``` ``` let addAt f n = ``` ``` match f.HC.node with ``` ``` | C.HCTRUE ``` ``` | C.HCFALSE ``` ``` | C.HCOR _ ``` ``` | C.HCAND _ ``` ``` | C.HCAT _ -> () ``` ``` | _ -> ``` ``` let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in ``` ``` let atn = C.HcFHt.find htF.(0) at in ``` ``` FHt.add !arrayAt.(sort).(n) nom atn ``` ``` in ``` ``` C.HcFHt.iter addAt htF.(sort) ``` ```let ppFormulae nomTbl tbox (s, f) = ``` ``` let card = Array.length !sortTable in ``` ``` if card <= 0 then ``` ``` raise (C.CoAlgException "Number of sorts must be positive.") ``` ``` else (); ``` ``` let nnfAndSimplify f = C.simplify (C.nnf f) in ``` ``` let f1 = nnfAndSimplify f in ``` ``` let nf1 = nnfAndSimplify (C.NOT f) in ``` ``` let tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in ``` ``` let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in ``` ``` let hcF = C.HcFormula.create true in ``` ``` let hcf = C.hc_formula hcF f1 in ``` ``` let nhcf = C.hc_formula hcF nf1 in ``` ``` let hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) tbox1 in ``` ``` let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in ``` ``` let hcfalse = C.hc_formula hcF C.FALSE in ``` ``` let hctrue = C.hc_formula hcF C.TRUE in ``` ``` let fset = Array.init card (fun _ -> C.HcFHt.create 128) in ``` ``` let atset = C.HcFHt.create 64 in ``` ``` let nomset = Hashtbl.create 16 in ``` ``` for i = 0 to card-1 do ``` ``` detClosure nomTbl hcF fset atset nomset i hcfalse; ``` ``` detClosure nomTbl hcF fset atset nomset i hctrue; ``` ``` done; ``` ``` detClosure nomTbl hcF fset atset nomset s hcf; ``` ``` detClosure nomTbl hcF fset atset nomset s nhcf; ``` ``` List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) hctbox; ``` ``` List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) nhctbox; ``` ``` Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset; ``` ``` let htF = Array.init card (fun _ -> C.HcFHt.create 128) in ``` ``` for i = 0 to card-1 do ``` ``` C.HcFHt.add htF.(i) hcfalse 0; ``` ``` C.HcFHt.add htF.(i) hctrue 1 ``` ``` done; ``` ``` let addAts f () idx = ``` ``` for i = 0 to card-1 do ``` ``` C.HcFHt.add htF.(i) f idx ``` ``` done; ``` ``` idx + 1 ``` ``` in ``` ``` let sizeAt = C.HcFHt.fold addAts atset 2 in ``` ``` let addFml i f () idx = ``` ``` if C.HcFHt.mem htF.(i) f then idx ``` ``` else begin ``` ``` C.HcFHt.add htF.(i) f idx; ``` ``` idx+1 ``` ``` end ``` ``` in ``` ``` let size = ref 0 in ``` ``` for i = 0 to card-1 do ``` ``` let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in ``` ``` if size2 > !size then size := size2 else () ``` ``` done; ``` ``` arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE); ``` ``` arrayType := Array.init card (fun _ -> Array.make !size Other); ``` ``` arrayDest1 := Array.init card (fun _ -> Array.make !size (-1)); ``` ``` arrayDest2 := Array.init card (fun _ -> Array.make !size (-1)); ``` ``` arrayDest3 := Array.init card (fun _ -> Array.make !size (-1)); ``` ``` arrayNeg := Array.init card (fun _ -> Array.make !size (-1)); ``` ``` arrayDestNum := Array.init card (fun _ -> Array.make !size (-1)); ``` ``` arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1))); ``` ``` let htR = Hashtbl.create 128 in ``` ``` Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR s) ht) htF; ``` ``` arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8)); ``` ``` Hashtbl.iter (initTablesAt hcF htF) nomset; ``` ``` S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1); ``` ``` let initbs = bsetMake () in ``` ``` bsetAdd initbs (C.HcFHt.find htF.(s) hcf); ``` ``` let tboxTbl = Array.init card (fun _ -> bsetMake ()) in ``` ``` List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox; ``` ``` tboxTable := tboxTbl; ``` ``` (tbox1, (s, f1), initbs) ```