### Profile

Statistics
| Branch: | Revision:

## cool / src / lib / ALCMisc.ml @ 40a714df

History | View | Annotate | Download (31.5 KB)

 1 ```(** Common functions and data structures ``` ``` which are shared by the decision procedures for ALC-satisfiability. ``` ``` @author Florian Widmann ``` ``` *) ``` ```module A = ALCFormula ``` ```module HC = HashConsing ``` ```open MiscSolver ``` ```(** This exception is thrown when the status of the root node in the graph ``` ``` becomes (un)satisfiable and the procedure can stop. ``` ``` *) ``` ```exception ALC_finished of bool ``` ```(** This table maps integers (representing formulae) to their corresponding formulae. ``` ``` *) ``` ```let arrayFormula = ref (Array.make 0 A.TRUE) ``` ```(** This lookup table maps EX/AX-formulae to their inverse concept. ``` ``` *) ``` ```let arrayInv = ref (Array.make 0 (-1)) ``` ```(** This table maps integers (representing formulae) to their corresponding definitions. ``` ``` *) ``` ```let arrayDef = ref (Array.make 0 (-1)) ``` ```(** The lowest integer representing an OR-formula. ``` ``` *) ``` ```let lposOR = ref (-1) ``` ```(** The greatest integer representing an OR-formula. ``` ``` *) ``` ```let hposOR = ref (-1) ``` ```(** A dependency is defined between two nodes: a node n and one of its children c. ``` ``` It maps some formulae f of c to the formulae of n that caused the creation of f. ``` ``` If n is an or-node, formulae of c that are not mapped are implicitly assumed ``` ``` to map to themselves (and are hence in n and c). ``` ``` If n is a state, formulae of c that are not mapped do not derive from ``` ``` formulae in c but are inserted because of the TBox. ``` ``` If n is a state the value -1 (which is not a formula) is mapped to the ``` ``` <>-formula in n that caused the creation of c. ``` ``` *) ``` ```type dependency = (int list) FMap.t ``` ```(** An empty dependency map. ``` ``` *) ``` ```let (emptyDep : dependency) = FMap.empty ``` ```(** Returns the dependencies of a formula. ``` ``` @param dep A dependency map. ``` ``` @param f A formula. ``` ``` @return The list of formulae assigned to f in dep. ``` ``` @raise Not_found If nothing is assigned to f in dep. ``` ``` *) ``` ```let findDep (dep : dependency) f = FMap.find f dep ``` ```(** Adds new dependencies for a formula to a dependency map. ``` ``` Old dependencies for the formula are overridden. ``` ``` @param dep A dependency map. ``` ``` @param f The formula that gets new dependencies. ``` ``` @param fl A list of formulae that is assigned to f in dep. ``` ``` @return A dependency map that assigns fl to f ``` ``` and behaves like dep otherwise. ``` ``` *) ``` ```let addDep (dep : dependency) f fl = FMap.add f fl dep ``` ```(** Converts a dependency map into a string representation. ``` ``` @param expF A function which converts the formula in integer ``` ``` representations into a readable string. ``` ``` @param dep A dependency map. ``` ``` @return A string representing dep. ``` ``` *) ``` ```let exportDep expF dep = ``` ``` let expFl fl = List.map expF fl in ``` ``` let fld k e acc = ``` ``` let kstr = if k = (-1) then "-1" else expF k in ``` ``` let estr = exportAsSet "" expFl e in ``` ``` (kstr ^ " --> " ^ estr)::acc ``` ``` in ``` ``` let expD d = FMap.fold fld d [] in ``` ``` exportAsSet "" expD dep ``` ```(** Tests whether a formula is an element of a set of formulae. ``` ``` The function takes into account that and-formulae are split automatically. ``` ``` An or-formula is considered to be in the set ``` ``` if one of its subformulae is in the set (this applies recursively). ``` ``` Atomic concepts that are defined in the definitional TBox ``` ``` are expanded automatically. ``` ``` @param fs A bitset of formulae. ``` ``` @param f The integer representation of a formula. ``` ``` @return True iff f is an element of fs. ``` ``` *) ``` ```let rec containsFormula fs f = ``` ``` match !arrayType.(f) with ``` ``` | 5 -> ``` ``` containsFormula fs !arrayDest1.(f) && ``` ``` containsFormula fs !arrayDest2.(f) ``` ``` | 4 -> ``` ``` (memBS fs f || ``` ``` containsFormula fs !arrayDest1.(f) || ``` ``` containsFormula fs !arrayDest2.(f)) ``` ``` | 2 -> ``` ``` if memBS fs f then true ``` ``` else ``` ``` let fdef = !arrayDef.(f) in ``` ``` if fdef >= 0 && !arrayDef.(!arrayNeg.(f)) >= 0 then ``` ``` containsFormula fs fdef ``` ``` else false ``` ``` | 3 -> ``` ``` if memBS fs f then true ``` ``` else ``` ``` let fdef = !arrayDef.(f) in ``` ``` if fdef >= 0 then containsFormula fs fdef else false ``` ``` | _ -> memBS fs f ``` ```let containsFormulaChk fs f = f >= 0 && containsFormula fs f ``` ```(** Tests whether a formula is an element of a set of formulae. ``` ``` The function takes into account that and-formulae are split automatically. ``` ``` An or-formula is considered to be in the set ``` ``` if one of its subformulae is in the set (this applies recursively). ``` ``` Atomic concepts that are defined in the definitional TBox ``` ``` are expanded automatically. ``` ``` @param fs A bitset of formulae. ``` ``` @param f The integer representation of a formula. ``` ``` @return None iff f is not an element of fs; ``` ``` Some l iff f is an element of fs ``` ``` where l is a list of formula in fs that "make up" f. ``` ``` *) ``` ```let rec containsFormulaDep fs f = ``` ``` match !arrayType.(f) with ``` ``` | 5 -> begin ``` ``` let res1 = containsFormulaDep fs !arrayDest1.(f) in ``` ``` match res1 with ``` ``` | Some l1 -> begin ``` ``` let res2 = containsFormulaDep fs !arrayDest2.(f) in ``` ``` match res2 with ``` ``` | Some l2 -> Some (l1 @ l2) ``` ``` | None -> None ``` ``` end ``` ``` | None -> None ``` ``` end ``` ``` | 4 -> ``` ``` if memBS fs f then Some [f] ``` ``` else begin ``` ``` let res1 = containsFormulaDep fs !arrayDest1.(f) in ``` ``` match res1 with ``` ``` | Some _ -> res1 ``` ``` | None -> containsFormulaDep fs !arrayDest2.(f) ``` ``` end ``` ``` | 2 -> ``` ``` if memBS fs f then Some [f] ``` ``` else ``` ``` let fdef = !arrayDef.(f) in ``` ``` if fdef >= 0 && !arrayDef.(!arrayNeg.(f)) >= 0 then ``` ``` containsFormulaDep fs fdef ``` ``` else None ``` ``` | 3 -> ``` ``` if memBS fs f then Some [f] ``` ``` else ``` ``` let fdef = !arrayDef.(f) in ``` ``` if fdef >= 0 then containsFormulaDep fs fdef else None ``` ``` | _ -> if memBS fs f then Some [f] else None ``` ```let containsFormulaDepChk fs f = ``` ``` if f >= 0 then containsFormulaDep fs f else None ``` ```(** Adds a formula to a set of formulae. ``` ``` And-formulae are split, i.e. both their direct subformulae are inserted ``` ``` (and maybe split themselves recursively). ``` ``` Atomic concepts that are defined in the definitional TBox ``` ``` are expanded automatically. ``` ``` If a contradiction is found, the state of fs is undefined. ``` ``` @param fs A bitset of formulae. ``` ``` @param f The integer representation of a formula that is to be added to bs. ``` ``` @return True iff inserting f into fs causes a contradiction. ``` ``` *) ``` ```let rec insertFormula fs f = ``` ``` match !arrayType.(f) with ``` ``` | 5 -> ``` ``` let notf = !arrayNeg.(f) in ``` ``` ((notf >= 0 && memBS fs notf) || ``` ``` insertFormula fs !arrayDest1.(f) || ``` ``` insertFormula fs !arrayDest2.(f)) ``` ``` | 4 -> ``` ``` addBSNoChk fs f; ``` ``` containsFormulaChk fs !arrayNeg.(f) ``` ``` | 2 ``` ``` | 3 -> ``` ``` let fdef = !arrayDef.(f) in ``` ``` if fdef >= 0 then addBS fs f || insertFormula fs fdef ``` ``` else addBS fs f ``` ``` | _ -> addBS fs f ``` ```(** Adds a formula to a set of formulae. ``` ``` And-formulae are split, i.e. both their direct subformulae are inserted ``` ``` (and maybe split themselves recursively). ``` ``` Atomic concepts that are defined in the definitional TBox ``` ``` are expanded automatically. ``` ``` If a contradiction is found, the state of fs is undefined. ``` ``` @param fs A bitset of formulae. ``` ``` @param f The integer representation of a formula that is to be added to bs. ``` ``` @param dep The dependency map of fs. ``` ``` @param fDepl A list of formula that f depends on. ``` ``` @return A pair (ndep, cntr) where ``` ``` ndep is the new dependency map of fs ``` ``` (that is it extends dep such that all formula ``` ``` that are actually inserted into fs have fDepl as their dependencies); and ``` ``` cntr is None iff inserting f into fs did not cause a contradiction, ``` ``` and Some cfs otherwise where cfs is a "minimal subset" of fs ``` ``` that already contains the contradiction. ``` ``` *) ``` ```let rec insertFormulaDep fs f dep fDepl = ``` ``` match !arrayType.(f) with ``` ``` | 5 -> begin ``` ``` let (dep1, cntr1) as res1 = insertFormulaDep fs !arrayDest1.(f) dep fDepl in ``` ``` match cntr1 with ``` ``` | None -> begin ``` ``` let (dep2, cntr2) as res2 = insertFormulaDep fs !arrayDest2.(f) dep1 fDepl in ``` ``` match cntr2 with ``` ``` | None -> ``` ``` let notf = !arrayNeg.(f) in ``` ``` if notf >= 0 && memBS fs notf then ``` ``` let dep3 = addDep dep2 f fDepl in ``` ``` let cfs = makeBS () in ``` ``` addBSNoChk cfs f; ``` ``` addBSNoChk cfs notf; ``` ``` (dep3, Some cfs) ``` ``` else res2 ``` ``` | Some _ -> res2 ``` ``` end ``` ``` | Some _ -> res1 ``` ``` end ``` ``` | 4 -> begin ``` ``` let dep1 = if memBS fs f then dep else addDep dep f fDepl in ``` ``` addBSNoChk fs f; ``` ``` let iscont = containsFormulaDepChk fs !arrayNeg.(f) in ``` ``` match iscont with ``` ``` | None -> (dep1, None) ``` ``` | Some notfl -> ``` ``` let cfs = makeBS () in ``` ``` addBSNoChk cfs f; ``` ``` List.iter (addBSNoChk cfs) notfl; ``` ``` (dep1, Some cfs) ``` ``` end ``` ``` | 2 ``` ``` | 3 -> ``` ``` let dep1 = if memBS fs f then dep else addDep dep f fDepl in ``` ``` if addBS fs f then ``` ``` let cfs = makeBS () in ``` ``` addBSNoChk cfs f; ``` ``` if f <> !bsfalse then addBSNoChk cfs !arrayNeg.(f) else (); ``` ``` (dep1, Some cfs) ``` ``` else ``` ``` let fdef = !arrayDef.(f) in ``` ``` if fdef >= 0 then insertFormulaDep fs fdef dep1 fDepl ``` ``` else (dep1, None) ``` ``` | _ -> ``` ``` let dep1 = if memBS fs f then dep else addDep dep f fDepl in ``` ``` if addBS fs f then ``` ``` let cfs = makeBS () in ``` ``` addBSNoChk cfs f; ``` ``` if f <> !bsfalse then addBSNoChk cfs !arrayNeg.(f) else (); ``` ``` (dep1, Some cfs) ``` ``` else (dep1, None) ``` ```(** Removes or-formulae from a set ``` ``` if one of its direct subformulae are already in the set, ``` ``` or replaces them by one of its direct subformulae ``` ``` if the negation of the other direct subformula is in the set. ``` ``` @param fs A set of formulae. ``` ``` @return True if a contradiction is detected in fs. ``` ``` *) ``` ```let rec subsume fs = ``` ``` let rec chkOr bnd acc i = ``` ``` if i <= bnd then ``` ``` if memBS fs i then ``` ``` let f1 = !arrayDest1.(i) in ``` ``` let f2 = !arrayDest2.(i) in ``` ``` if containsFormula fs f1 || containsFormula fs f2 then begin ``` ``` remBS fs i; ``` ``` chkOr bnd acc (succ i) ``` ``` end ``` ``` else ``` ``` let iscont1 = containsFormulaChk fs !arrayNeg.(f1) in ``` ``` if iscont1 then begin ``` ``` remBS fs i; ``` ``` if insertFormula fs f2 then 1 else chkOr bnd 2 (succ i) ``` ``` end ``` ``` else ``` ``` let iscont2 = containsFormulaChk fs !arrayNeg.(f2) in ``` ``` if iscont2 then begin ``` ``` remBS fs i; ``` ``` if insertFormula fs f1 then 1 else chkOr bnd 2 (succ i) ``` ``` end ``` ``` else chkOr bnd acc (succ i) ``` ``` else chkOr bnd acc (succ i) ``` ``` else acc ``` ``` in ``` ``` match chkOr !hposOR 0 !lposOR with ``` ``` | 0 -> false ``` ``` | 1 -> true ``` ``` | _ -> subsume fs ``` ```(** Removes or-formulae from a set ``` ``` if one of its direct subformulae are already in the set, ``` ``` or replaces them by one of its direct subformulae ``` ``` if the negation of the other direct subformula is in the set. ``` ``` @param isor True iff the node that is responsible ``` ``` for invoking this function is an or-node (otherwise it is a state). ``` ``` @param dep The dependency map of fs. ``` ``` @param fs A set of formulae. ``` ``` @return A pair (ndep, cntr) where ``` ``` ndep is the new dependency map of fs; and ``` ``` cntr is None iff the subsumption did not cause a contradiction, ``` ``` and Some cfs otherwise where cfs is a "minimal subset" of fs ``` ``` that already contains the contradiction. ``` ``` *) ``` ```let rec subsumeDep isor dep fs = ``` ``` let subsumeFold dep acc f = ``` ``` try ``` ``` let dl = findDep dep f in ``` ``` dl @ acc ``` ``` with Not_found -> if isor then f::acc else acc ``` ``` in ``` ``` let rec chkOr bnd acc i dep = ``` ``` if i <= bnd then ``` ``` if memBS fs i then ``` ``` let f1 = !arrayDest1.(i) in ``` ``` let f2 = !arrayDest2.(i) in ``` ``` if containsFormula fs f1 || containsFormula fs f2 then begin ``` ``` remBS fs i; ``` ``` chkOr bnd acc (succ i) dep ``` ``` end ``` ``` else ``` ``` let iscont1 = containsFormulaDepChk fs !arrayNeg.(f1) in ``` ``` match iscont1 with ``` ``` | Some negf1l -> begin ``` ``` remBS fs i; ``` ``` let f2Depl = List.fold_left (subsumeFold dep) [] (i::negf1l) in ``` ``` let (dep1, cntr1) as res1 = insertFormulaDep fs f2 dep f2Depl in ``` ``` match cntr1 with ``` ``` | None -> chkOr bnd true (succ i) dep1 ``` ``` | Some _ -> (true, res1) ``` ``` end ``` ``` | None -> ``` ``` let iscont2 = containsFormulaDepChk fs !arrayNeg.(f2) in ``` ``` match iscont2 with ``` ``` | Some negf2l -> begin ``` ``` remBS fs i; ``` ``` let f1Depl = List.fold_left (subsumeFold dep) [] (i::negf2l) in ``` ``` let (dep2, cntr2) as res2 = insertFormulaDep fs f1 dep f1Depl in ``` ``` match cntr2 with ``` ``` | None -> chkOr bnd true (succ i) dep2 ``` ``` | Some _ -> (false, res2) ``` ``` end ``` ``` | None -> chkOr bnd acc (succ i) dep ``` ``` else chkOr bnd acc (succ i) dep ``` ``` else (acc, (dep, None)) ``` ``` in ``` ``` let (modified, ((dep3, contr3) as res3)) = chkOr !hposOR false !lposOR dep in ``` ``` match contr3 with ``` ``` | None -> if modified then subsumeDep isor dep3 fs else res3 ``` ``` | Some _ -> res3 ``` ```(** Invokes subsume on a set unless it already contains a contradiction. ``` ``` @param isor True iff the node that is responsible ``` ``` for invoking this function is an or-node (otherwise it is a state). ``` ``` @param fs A set of formulae. ``` ``` @param dep The dependency map of fs. ``` ``` @param cntr None iff fs does not contain a contradiction. ``` ``` @return If cntr is not None then (dep, cntr), ``` ``` otherwise a pair (ndep, ncntr) where ``` ``` ndep is the new dependency map of fs; and ``` ``` cntr is None iff the subsumption did not cause a contradiction, ``` ``` and Some cfs otherwise where cfs is a "minimal subset" of fs ``` ``` that already contains the contradiction. ``` ```*) ``` ```let testSubsume isor fs ((dep, cntr) as res) = ``` ``` match cntr with ``` ``` | None -> subsumeDep isor dep fs ``` ``` | Some _ -> res ``` ```(** Creates a "minimal" contradictory set for a node ``` ``` according to a "minimal" contradictory set of a child ``` ``` and a corresponding dependency map. ``` ``` @param isor True iff the node that is responsible ``` ``` for invoking this function is an or-node (otherwise it is a state). ``` ``` @param ocfs The "minimal" contradictory set of a child. ``` ``` @param dep The corresponding dependency map. ``` ``` @param ncfs The resulting "minimal" contradictory set of a child. ``` ``` It does not have to be empty (e.g. for or-formula ``` ``` this function is invoked twice). ``` ``` *) ``` ```let makeCSDep isor ocfs dep ncfs = ``` ``` for i = 0 to pred !nrFormulae do ``` ``` if memBS ocfs i then ``` ``` try ``` ``` let dl = findDep dep i in ``` ``` List.iter (addBSNoChk ncfs) dl ``` ``` with Not_found -> if isor then addBSNoChk ncfs i else () ``` ``` else () ``` ``` done ``` ```(** Adds all [a]-formulae of a set, where a is a given program, ``` ``` to another set after stripping the outermost [a]. ``` ``` If a contradiction is found the result may not contain ``` ``` all stripped [a]-formulae. ``` ``` @param bs The bitset of formulae containing the [a]-formulae. ``` ``` @param ap The integer representation of an atomic program. ``` ``` @param nbs The bitset to which the stripped [a]-formulae are added. ``` ``` @param bnd The greatest integer representing a [a]-formula. ``` ``` @param i The current index of the array. ``` ``` @return True iff adding the formulae to nbs caused a contradiction. ``` ``` *) ``` ```let rec intern_mkDelta bs ap nbs bnd i = ``` ``` if i <= bnd then ``` ``` if memBS bs i && ap = !arrayDest2.(i) then ``` ``` if insertFormula nbs !arrayDest1.(i) then true ``` ``` else intern_mkDelta bs ap nbs bnd (succ i) ``` ``` else intern_mkDelta bs ap nbs bnd (succ i) ``` ``` else false ``` ```let mkDelta bs ap nbs = intern_mkDelta bs ap nbs !hposAX !lposAX ``` ```(** Adds all [a]-formulae of a set, where a is a given atomic program, ``` ``` to another set after stripping the outermost [a]. ``` ``` If a contradiction is found the result may not contain ``` ``` all stripped [a]-formulae. ``` ``` @param bs The bitset of formulae containing the [a]-formulae. ``` ``` @param ap The integer representation of an atomic program. ``` ``` @param dep The dependency map of bs. ``` ``` @param nbs The bitset to which the stripped [a]-formulae are added. ``` ``` @param bnd The greatest integer representing a [a]-formula. ``` ``` @param i The current index of the array. ``` ``` @return A pair (ndep, cntr) where ``` ``` ndep is the new dependency map of bs; and ``` ``` cntr is None iff inserting the formulae did not cause a contradiction, ``` ``` and Some cfs otherwise where cfs is a "minimal subset" of bs ``` ``` that already contains the contradiction. ``` ``` *) ``` ```let rec intern_mkDeltaDep bs ap dep nbs bnd i = ``` ``` if i <= bnd then ``` ``` if memBS bs i && ap = !arrayDest2.(i) then ``` ``` let (dep1, cntr1) as res1 = insertFormulaDep nbs !arrayDest1.(i) dep [i] in ``` ``` match cntr1 with ``` ``` | None -> intern_mkDeltaDep bs ap dep1 nbs bnd (succ i) ``` ``` | Some _ -> res1 ``` ``` else intern_mkDeltaDep bs ap dep nbs bnd (succ i) ``` ``` else (dep, None) ``` ```(** For a principal formula A, ``` ``` this function adds A and all [a]-formulae of a set ``` ``` to another set (which may already contain formulae of a TBox) ``` ``` after stripping the outermost [a]. ``` ``` If a contradiction is found the result may not contain ``` ``` all stripped [a]-formulae. ``` ``` @param bs The bitset of formulae containing the [a]-formulae. ``` ``` @param pf The principal formula. ``` ``` @param nbs The bitset to which the formulae are added. ``` ``` @return A pair (ndep, cntr) where ``` ``` ndep is the new dependency map of bs; and ``` ``` cntr is None iff inserting the formulae did not cause a contradiction, ``` ``` and Some cfs otherwise where cfs is a "minimal subset" of bs ``` ``` that already contains the contradiction. ``` ``` *) ``` ```let mkDeltaDep bs pf nbs = ``` ``` let f = !arrayDest1.(pf) in ``` ``` let (dep, cntr) as res = insertFormulaDep nbs f emptyDep [pf] in ``` ``` match cntr with ``` ``` | None -> ``` ``` let ap = !arrayDest2.(pf) in ``` ``` intern_mkDeltaDep bs ap dep nbs !hposAX !lposAX ``` ``` | Some _ -> res ``` ```(** Extends a pair by a third element and adds the result to a list. ``` ``` @param c The element that is added to (a, b). ``` ``` @param lst A list of triples. ``` ``` @param (a, b) A pair. ``` ``` @return (a, b, c)::lst ``` ``` *) ``` ```let addTuple c lst (a, b) = (a, b, c)::lst ``` ```(** Test whether all AX-formulae of a set of formulae ``` ``` stripped of their outermost [r] ``` ``` are contained in another set of formulae. ``` ``` @param bs1 The bitset of formulae containing the AX-formulae. ``` ``` @param bs2 The other bitset. ``` ``` @param ap The integer representation of a role. ``` ``` @param bnd The greatest integer representing a [a]-formula. ``` ``` @param i The current index of the array. ``` ``` @return True iff all formula (as described above) are contained in bs2. ``` ``` *) ``` ```let rec intern_isConsistent bs1 bs2 ap bnd i = ``` ``` if i <= bnd then ``` ``` if memBS bs1 i && ap = !arrayDest2.(i) then ``` ``` if containsFormula bs2 !arrayDest1.(i) then ``` ``` intern_isConsistent bs1 bs2 ap bnd (succ i) ``` ``` else false ``` ``` else intern_isConsistent bs1 bs2 ap bnd (succ i) ``` ``` else true ``` ```let isConsistent bs1 bs2 ap = intern_isConsistent bs1 bs2 ap !hposAX !lposAX ``` ```(** Initialises the arrays for a formula and its integer representation. ``` ``` @param htF A hashtable that maps formulae to their integer representation. ``` ``` @param htR A hashtable that maps role names to their integer representation. ``` ``` @param tboxD A list of definitions ``` ``` representing the definitional part of a TBox. ``` ``` The definitions must not be cyclic ``` ``` and each concept must not be defined more than once. ``` ``` @param f A formula. ``` ``` @param n The integer representation of f. ``` ``` @raise ACLException if f is not in negation normal form. ``` ``` *) ``` ```let initTables htF htR tboxD f n = ``` ``` let rec getDef isneg cn = function ``` ``` | [] -> None ``` ``` | h::tl -> ``` ``` match h with ``` ``` | A.PRIMITIVE (s, f) -> ``` ``` if cn = s then ``` ``` if not isneg then Some f else None ``` ``` else getDef isneg cn tl ``` ``` | A.NECANDSUFF (s, f) -> ``` ``` if cn = s then Some f ``` ``` else getDef isneg cn tl ``` ``` in ``` ``` !arrayFormula.(n) <- f; ``` ``` let fneg = A.nnfNeg f in ``` ``` if Hashtbl.mem htF fneg then !arrayNeg.(n) <- Hashtbl.find htF fneg else (); ``` ``` match f with ``` ``` | A.TRUE -> !arrayType.(n) <- 0 ``` ``` | A.FALSE -> !arrayType.(n) <- 1 ``` ``` | A.AP s -> begin ``` ``` !arrayType.(n) <- 2; ``` ``` let defopt = getDef false s tboxD in ``` ``` match defopt with ``` ``` | None -> () ``` ``` | Some fdef -> !arrayDef.(n) <- Hashtbl.find htF fdef ``` ``` end ``` ``` | A.NOT (A.AP s) -> begin ``` ``` !arrayType.(n) <- 3; ``` ``` let defopt = getDef true s tboxD in ``` ``` match defopt with ``` ``` | None -> () ``` ``` | Some nfdef -> ``` ``` let fdef = A.nnfNeg nfdef in ``` ``` !arrayDef.(n) <- Hashtbl.find htF fdef ``` ``` end ``` ``` | A.OR (f1, f2) -> ``` ``` !arrayType.(n) <- 4; ``` ``` !arrayDest1.(n) <- Hashtbl.find htF f1; ``` ``` !arrayDest2.(n) <- Hashtbl.find htF f2 ``` ``` | A.AND (f1, f2) -> ``` ``` !arrayType.(n) <- 5; ``` ``` !arrayDest1.(n) <- Hashtbl.find htF f1; ``` ``` !arrayDest2.(n) <- Hashtbl.find htF f2 ``` ``` | A.EX (s, inv, f1) -> ``` ``` !arrayType.(n) <- 6; ``` ``` !arrayDest1.(n) <- Hashtbl.find htF f1; ``` ``` !arrayDest2.(n) <- ``` ``` if Hashtbl.mem htR (s, inv) then Hashtbl.find htR (s, inv) ``` ``` else begin ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR (s, inv) size; ``` ``` size ``` ``` end; ``` ``` !arrayInv.(n) <- ``` ``` let ninv = not inv in ``` ``` if Hashtbl.mem htR (s, ninv) then Hashtbl.find htR (s, ninv) ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR (s, ninv) size; ``` ``` size ``` ``` | A.AX (s, inv, f1) -> ``` ``` !arrayType.(n) <- 7; ``` ``` !arrayDest1.(n) <- Hashtbl.find htF f1; ``` ``` !arrayDest2.(n) <- ``` ``` if Hashtbl.mem htR (s, inv) then Hashtbl.find htR (s, inv) ``` ``` else begin ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR (s, inv) size; ``` ``` size ``` ``` end; ``` ``` !arrayInv.(n) <- ``` ``` let ninv = not inv in ``` ``` if Hashtbl.mem htR (s, ninv) then Hashtbl.find htR (s, ninv) ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR (s, ninv) size; ``` ``` size ``` ``` | _ -> raise (A.ALCException "Formula is not in negation normal form.") ``` ```(** Initialises the arrays for a formula and its integer representation. ``` ``` @param hcF A hash-cons table. ``` ``` @param htF A hashtable that maps formulae to their integer representation. ``` ``` @param htR A hashtable that maps role names to their integer representation. ``` ``` @param tboxD A list of definitions ``` ``` representing the definitional part of a TBox. ``` ``` The definitions must not be cyclic ``` ``` and each concept must not be defined more than once. ``` ``` @param f A hash-consed formula (in negation normal form). ``` ``` @param n The integer representation of f. ``` ``` *) ``` ```let initTablesHc hcF htF htR tboxD f n = ``` ``` let rec getDef isneg cn = function ``` ``` | [] -> None ``` ``` | (true, s, f)::tl -> ``` ``` if cn = s then ``` ``` if not isneg then Some f else None ``` ``` else getDef isneg cn tl ``` ``` | (false, s, f)::tl -> ``` ``` if cn = s then Some f ``` ``` else getDef isneg cn tl ``` ``` in ``` ``` !arrayFormula.(n) <- f.HC.fml; ``` ``` let fneg = f.HC.neg in ``` ``` if A.HcFHt.mem htF fneg then ``` ``` !arrayNeg.(n) <- A.HcFHt.find htF fneg; ``` ``` match f.HC.node with ``` ``` | A.HCTRUE -> !arrayType.(n) <- 0 ``` ``` | A.HCFALSE -> !arrayType.(n) <- 1 ``` ``` | A.HCAP s -> begin ``` ``` !arrayType.(n) <- 2; ``` ``` let defopt = getDef false s tboxD in ``` ``` match defopt with ``` ``` | None -> () ``` ``` | Some fdef -> !arrayDef.(n) <- A.HcFHt.find htF fdef ``` ``` end ``` ``` | A.HCNOT s -> begin ``` ``` !arrayType.(n) <- 3; ``` ``` let defopt = getDef true s tboxD in ``` ``` match defopt with ``` ``` | None -> () ``` ``` | Some nfdef -> ``` ``` let fdef = nfdef.HC.neg in ``` ``` !arrayDef.(n) <- A.HcFHt.find htF fdef ``` ``` end ``` ``` | A.HCOR (f1, f2) -> ``` ``` !arrayType.(n) <- 4; ``` ``` !arrayDest1.(n) <- A.HcFHt.find htF f1; ``` ``` !arrayDest2.(n) <- A.HcFHt.find htF f2 ``` ``` | A.HCAND (f1, f2) -> ``` ``` !arrayType.(n) <- 5; ``` ``` !arrayDest1.(n) <- A.HcFHt.find htF f1; ``` ``` !arrayDest2.(n) <- A.HcFHt.find htF f2 ``` ``` | A.HCEX (s, inv, f1) -> ``` ``` !arrayType.(n) <- 6; ``` ``` !arrayDest1.(n) <- A.HcFHt.find htF f1; ``` ``` !arrayDest2.(n) <- ``` ``` if Hashtbl.mem htR (s, inv) then Hashtbl.find htR (s, inv) ``` ``` else begin ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR (s, inv) size; ``` ``` size ``` ``` end; ``` ``` !arrayInv.(n) <- ``` ``` let ninv = not inv in ``` ``` if Hashtbl.mem htR (s, ninv) then Hashtbl.find htR (s, ninv) ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR (s, ninv) size; ``` ``` size ``` ``` | A.HCAX (s, inv, f1) -> ``` ``` !arrayType.(n) <- 7; ``` ``` !arrayDest1.(n) <- A.HcFHt.find htF f1; ``` ``` !arrayDest2.(n) <- ``` ``` if Hashtbl.mem htR (s, inv) then Hashtbl.find htR (s, inv) ``` ``` else begin ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR (s, inv) size; ``` ``` size ``` ``` end; ``` ``` !arrayInv.(n) <- ``` ``` let ninv = not inv in ``` ``` if Hashtbl.mem htR (s, ninv) then Hashtbl.find htR (s, ninv) ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR (s, ninv) size; ``` ``` size ``` ```(** Converts the formula in the given lists in negation normal form ``` ``` and simplifies them. ``` ``` Initialises the internal tables of this module. ``` ``` @param fl The list of initial formulae that are to be tested for satisfiability. ``` ``` @param tboxND A list of formulae representing ``` ``` the non-definitional part of a TBox. ``` ``` @param tboxD A list of definitions ``` ``` representing the definitional part of a TBox. ``` ``` The definitions must not be cyclic ``` ``` and each concept must not be defined more than once. ``` ``` @param rankingF A complete ranking of the different types of formulae. ``` ``` @param noty The number of types in rankingF, ``` ``` starting from the beginning of the list, ``` ``` whose formulae are stored in the bitsets explicitly. ``` ``` @param allowIR Indicates whether inverse roles are allowed. ``` ``` @return A tuple (nfl, ntbND, ntbD, initset, tbox, cntr) where: ``` ``` nfl is the result of converting all formulae in fl in negation normal form ``` ``` and simplifying them; ``` ``` ntboxl is the result of converting all formulae in tboxND in negation normal form ``` ``` and simplifying them; ``` ``` ntboxD is the result of converting all formulae in tboxD in negation normal form ``` ``` and simplifying them; ``` ``` initset is a bitset containing the formulae in nfl and ntbND (in integer representation); ``` ``` tbox is a bitset containing the formulae in ntboxl (in integer representation); ``` ``` cntr is smaller than 0 iff initset contains a contradiction. ``` ``` @raise A.ALCException If fl is the empty list. ``` ``` *) ``` ```let ppFormulae fl tboxND tboxD rankingF noty allowIR = ``` ``` let testD = function ``` ``` | A.PRIMITIVE (_, f) ``` ``` | A.NECANDSUFF (_, f) -> A.containsInverse f ``` ``` in ``` ``` if (not allowIR) && ``` ``` (List.exists A.containsInverse fl || List.exists A.containsInverse tboxND || List.exists testD tboxD) ``` ``` then raise (A.ALCException "Query contains inverse roles.") else (); ``` ``` if fl = [] then raise (A.ALCException "Initial formula list is empty.") else (); ``` ``` let mapD g = function ``` ``` | A.PRIMITIVE (s, f) -> A.PRIMITIVE (s, g f) ``` ``` | A.NECANDSUFF (s, f) -> A.NECANDSUFF (s, g f) ``` ``` in ``` ``` let nfl = List.map A.nnf fl in ``` ``` let ntboxND = List.map A.nnf tboxND in ``` ``` let ntboxD = List.map (mapD A.nnf) tboxD in ``` ``` let nfl = List.map A.simplifyFormula nfl in ``` ``` let ntboxND = List.map A.simplifyFormula ntboxND in ``` ``` let ntboxD = List.map (mapD A.simplifyFormula) ntboxD in ``` ```(* ``` ``` let compF = A.generateCompare A.aRanking in ``` ``` let module FSet = Set.Make( ``` ``` struct ``` ``` type t = A.formula ``` ``` let (compare : t -> t -> int) = compF ``` ``` end ``` ``` ) ``` ``` in ``` ``` let fld acc = function ``` ``` | A.PRIMITIVE (s, f) -> ``` ``` let c = A.AP s in ``` ``` let notc = A.NOT c in ``` ``` c::f::notc::acc ``` ``` | A.NECANDSUFF (s, f) -> ``` ``` let c = A.AP s in ``` ``` let notc = A.NOT c in ``` ``` let notf = A.nnfNeg f in ``` ``` c::f::notc::notf::acc ``` ``` in ``` ``` let ntboxDFl = List.fold_left fld [] ntboxD in ``` ``` let allf = List.rev_append ntboxDFl (List.rev_append nfl ntboxND) in ``` ``` let ppF acc f = ``` ``` let fl = A.detClosure compF f in ``` ``` List.fold_left (fun a f -> FSet.add f a) acc fl ``` ``` in ``` ``` let getFml f = f in ``` ``` let module Ht = Hashtbl in ``` ``` *) ``` ``` let module FSet = Set.Make( ``` ``` struct ``` ``` type t = A.hcFormula ``` ``` let compare (f1 : t) f2 = compare f1.HC.tag f2.HC.tag ``` ``` end ``` ``` ) ``` ``` in ``` ``` let hcF = A.HcFormula.create ~size:100 true in ``` ``` let hcnfl = List.map (A.hc_formula hcF) nfl in ``` ``` let hcntboxND = List.map (A.hc_formula hcF) ntboxND in ``` ``` let mapD = function ``` ``` | A.PRIMITIVE (s, f) -> (true, s, A.hc_formula hcF f) ``` ``` | A.NECANDSUFF (s, f) -> (false, s, A.hc_formula hcF f) ``` ``` in ``` ``` let hcntboxD = List.map mapD ntboxD in ``` ``` let fld acc = function ``` ``` | (true, s, f) -> ``` ``` let c = A.HcFormula.hashcons hcF (A.HCAP s) in ``` ``` let notc = c.HC.neg in ``` ``` c::f::notc::acc ``` ``` | (false, s, f) -> ``` ``` let c = A.HcFormula.hashcons hcF (A.HCAP s) in ``` ``` let notc = c.HC.neg in ``` ``` let notf = f.HC.neg in ``` ``` c::f::notc::notf::acc ``` ``` in ``` ``` let hcntboxDFl = List.fold_left fld [] hcntboxD in ``` ``` let allf = List.rev_append hcntboxDFl (List.rev_append hcnfl hcntboxND) in ``` ``` let ppF acc f = ``` ``` let fl = A.detClosureHc hcF f in ``` ``` List.fold_left (fun a f -> FSet.add f a) acc fl ``` ``` in ``` ``` let getFml f = f.HC.fml in ``` ``` let module Ht = A.HcFHt in ``` ``` let fset = List.fold_left ppF FSet.empty allf in ``` ``` let noF = Array.make A.numberOfTypes 0 in ``` ``` let liter f = ``` ``` let ty = A.getTypeFormula (getFml f) in ``` ``` noF.(ty) <- succ noF.(ty) ``` ``` in ``` ``` FSet.iter liter fset; ``` ``` let idxF = Array.make A.numberOfTypes 0 in ``` ``` let len = List.fold_left (fun idx ty -> idxF.(ty) <- idx; idx + noF.(ty)) 0 rankingF in ``` ``` let countSize (size, idx) ty = ``` ``` let nsize = if idx > 0 then size + noF.(ty) else size in ``` ``` (nsize, pred idx) ``` ``` in ``` ``` let (size, _) = List.fold_left countSize (0, noty) rankingF in ``` ``` let tyEX = A.getTypeFormula (A.EX ("", false, A.TRUE)) in ``` ``` let idxEX = idxF.(tyEX) in ``` ``` let noEX = noF.(tyEX) in ``` ``` let tyAX = A.getTypeFormula (A.AX ("", false, A.TRUE)) in ``` ``` let noAX = noF.(tyAX) in ``` ``` let tyOR = A.getTypeFormula (A.OR (A.TRUE, A.TRUE)) in ``` ``` lposOR := idxF.(tyOR); ``` ``` hposOR := !lposOR + noF.(tyOR) - 1; ``` ``` arrayFormula := Array.make len A.TRUE; ``` ``` arrayType := Array.make len (-1); ``` ``` arrayDest1 := Array.make len (-1); ``` ``` arrayDest2 := Array.make len (-1); ``` ``` arrayNeg := Array.make len (-1); ``` ``` arrayInv := Array.make len (-1); ``` ``` arrayDef := Array.make len (-1); ``` ``` let htF = Ht.create (2 * size) in ``` ``` let htR = Hashtbl.create size in ``` ``` let fillHt f = ``` ``` let ty = A.getTypeFormula (getFml f) in ``` ``` Ht.add htF f idxF.(ty); ``` ``` idxF.(ty) <- succ idxF.(ty) ``` ``` in ``` ``` FSet.iter fillHt fset; ``` ```(* ``` ``` let ff = A.FALSE in ``` ``` let tt = A.TRUE in ``` ``` let nflFl = nfl in ``` ``` let ntboxNDFl = ntboxND in ``` ``` let initTbl = initTables htF htR ntboxD in ``` ``` *) ``` ``` let ff = A.HcFormula.hashcons hcF A.HCFALSE in ``` ``` let tt = A.HcFormula.hashcons hcF A.HCTRUE in ``` ``` let nflFl = hcnfl in ``` ``` let ntboxNDFl = hcntboxND in ``` ``` let initTbl = initTablesHc hcF htF htR hcntboxD in ``` ``` Ht.iter initTbl htF; ``` ``` initMisc size (Ht.find htF ff) (Ht.find htF tt) idxEX noEX noAX; ``` ``` let toSet bs acc f = acc || insertFormula bs (Ht.find htF f) in ``` ``` let tbox = makeBS () in ``` ``` let cntr = List.fold_left (toSet tbox) false ntboxNDFl in ``` ``` let initset = copyBS tbox in ``` ``` let cntr = List.fold_left (toSet initset) cntr nflFl in ``` ``` (nfl, ntboxND, ntboxD, initset, tbox, cntr) ``` ```(** Converts a formula into a string. ``` ``` @param f A formula in integer representation. ``` ``` @return A string representing f. ``` ``` *) ``` ```let exportF f = A.exportFormula !arrayFormula.(f) ``` ```(** A ranking of formulae where the and-like formulae, ``` ``` with the exception of [*]-formulae, ``` ``` are not stored in the bitsets explicitly. ``` ``` *) ``` ```let rankingNoAnd = [ A.getTypeFormula (A.OR (A.TRUE, A.TRUE)); ``` ``` A.getTypeFormula (A.EX ("", false, A.TRUE)); ``` ``` A.getTypeFormula (A.AX ("", false, A.TRUE)); ``` ``` A.getTypeFormula A.TRUE; ``` ``` A.getTypeFormula A.FALSE; ``` ``` A.getTypeFormula (A.AP ""); ``` ``` A.getTypeFormula (A.NOT A.TRUE); ``` ``` A.getTypeFormula (A.AND (A.TRUE, A.TRUE)); ``` ``` A.getTypeFormula (A.EQU (A.TRUE, A.TRUE)); ``` ``` A.getTypeFormula (A.IMP (A.TRUE, A.TRUE)) ] ``` ```(** The number of types in rankingFNoAnd, ``` ``` starting from the beginning of the list, ``` ``` whose formulae are stored in the bitsets explicitly. ``` ``` *) ``` ```let notyNoAnd = 7 ```