(** 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