1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
|
package uk.ac.ox.cs.pagoda.rules;
import org.semanticweb.HermiT.model.*;
import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
import uk.ac.ox.cs.pagoda.util.Namespace;
import java.util.*;
public class OverApproxExist implements Approximator {
public static final String negativeSuffix = "_neg";
public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
private static final Variable X = Variable.create("X");
private static int individualCounter = 0;
private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>();
private static int noOfExistential(DLClause originalClause) {
int no = 0;
for (Atom atom: originalClause.getHeadAtoms())
if (atom.getDLPredicate() instanceof AtLeast)
no += ((AtLeast) atom.getDLPredicate()).getNumber();
return no;
}
private static int indexOfExistential(Atom headAtom, DLClause originalClause) {
if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1;
AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
if (alc.getToConcept() instanceof AtomicConcept) {
AtomicConcept ac = (AtomicConcept) alc.getToConcept();
if (ac.getIRI().endsWith(negativeSuffix)) {
alc = AtLeastConcept.create(alc.getNumber(), alc.getOnRole(), AtomicNegationConcept.create(getNegationConcept(ac)));
headAtom = Atom.create(alc, headAtom.getArgument(0));
}
}
int index = 0;
for (Atom atom: originalClause.getHeadAtoms()) {
if (atom.equals(headAtom))
return index;
if (atom.getDLPredicate() instanceof AtLeast)
index += ((AtLeast) atom.getDLPredicate()).getNumber();
}
return -1;
}
public static AtomicConcept getNegationConcept(DLPredicate p) {
if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING;
if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING;
if (p instanceof AtomicConcept) {
String iri = ((AtomicConcept) p).getIRI();
if (iri.endsWith(negativeSuffix))
iri = iri.substring(0, iri.length() - 4);
else
iri += negativeSuffix;
return AtomicConcept.create(iri);
}
if (p instanceof AtLeastConcept) {
// FIXME !!! here
return null;
}
return null;
}
public static int getNumberOfSkolemisedIndividual() {
return individualCounter;
}
public static Individual getNewIndividual(DLClause originalClause, int offset) {
Individual ret;
if (individualNumber.containsKey(originalClause)) {
ret = Individual.create(skolemisedIndividualPrefix + (individualNumber.get(originalClause) + offset));
}
else {
individualNumber.put(originalClause, individualCounter);
ret = Individual.create(skolemisedIndividualPrefix + (individualCounter + offset));
individualCounter += noOfExistential(originalClause);
}
return ret;
}
public static int indexOfSkolemisedIndividual(Atom atom) {
Term t;
for (int index = 0; index < atom.getArity(); ++index) {
t = atom.getArgument(index);
if (t instanceof Individual && ((Individual) t).getIRI().contains(skolemisedIndividualPrefix)) return index;
}
return -1;
}
@Override
public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
Collection<DLClause> ret;
switch (clause.getHeadLength()) {
case 1:
return overApprox(clause.getHeadAtom(0), clause.getBodyAtoms(), originalClause);
case 0:
ret = new LinkedList<DLClause>();
ret.add(clause);
return ret;
default:
ret = new LinkedList<DLClause>();
for (Iterator<DLClause> iter = new DisjunctiveHeads(clause, originalClause); iter.hasNext(); )
ret.add(iter.next());
return ret;
}
}
public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause) {
return overApprox(headAtom, bodyAtoms, originalClause, indexOfExistential(headAtom, originalClause));
}
public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause, int offset) {
Collection<DLClause> ret = new LinkedList<DLClause>();
DLPredicate predicate = headAtom.getDLPredicate();
if (predicate instanceof AtLeastConcept) {
AtLeastConcept atLeastConcept = (AtLeastConcept) predicate;
LiteralConcept concept = atLeastConcept.getToConcept();
Role role = atLeastConcept.getOnRole();
AtomicConcept atomicConcept = null;
if (concept instanceof AtomicNegationConcept) {
// TODO CHECK: is this already in MultiStageUpperProgram?
Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
Atom atom2 = Atom.create(atomicConcept = getNegationConcept(atomicConcept), X);
ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2}));
}
else {
atomicConcept = (AtomicConcept) concept;
if (atomicConcept.equals(AtomicConcept.THING))
atomicConcept = null;
}
int card = atLeastConcept.getNumber();
Individual[] individuals = new Individual[card];
for (int i = 0; i < card; ++i) individuals[i] = getNewIndividual(originalClause, offset + i);
for (int i = 0; i < card; ++i) {
if (atomicConcept != null)
ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, bodyAtoms));
Atom atom = role instanceof AtomicRole ?
Atom.create((AtomicRole) role, X, individuals[i]) :
Atom.create(((InverseRole) role).getInverseOf(), individuals[i], X);
ret.add(DLClause.create(new Atom[] {atom}, bodyAtoms));
}
for (int i = 0; i < card; ++i)
for (int j = i + 1; j < card; ++j)
// TODO to be checked ... different as
ret.add(DLClause.create(new Atom[] {Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, bodyAtoms));
//DLClauseHelper.contructor_differentAs(individuals[i], individuals[j]));
}
else if (predicate instanceof AtLeastDataRange) {
// TODO to be implemented ...
}
else
ret.add(DLClause.create(new Atom[] {headAtom}, bodyAtoms));
return ret;
}
class DisjunctiveHeads implements Iterator<DLClause> {
Atom[] bodyAtoms;
Atom[][] disjunctHeadAtoms;
int[] pointer;
int length, l;
LinkedList<DLClause> auxiliaryClauses = new LinkedList<DLClause>();
public DisjunctiveHeads(DLClause clause, DLClause originalClause) {
length = clause.getHeadLength();
bodyAtoms = clause.getBodyAtoms();
disjunctHeadAtoms = new Atom[length][];
pointer = new int[length];
if (length > 0) l = length - 1;
else length = 0;
int index = 0, offset = 0;
Collection<DLClause> datalogRules;
DLClause newClause;
for (Atom headAtom: clause.getHeadAtoms()) {
pointer[index] = 0;
datalogRules = overApprox(headAtom, bodyAtoms, originalClause, offset);
if (datalogRules.isEmpty()) {
l = -1;
auxiliaryClauses.clear();
return ;
}
for (Iterator<DLClause> iter = datalogRules.iterator(); iter.hasNext(); ) {
newClause = iter.next();
if (!DLClauseHelper.hasSubsetBodyAtoms(newClause, clause)) {
auxiliaryClauses.add(newClause);
iter.remove();
}
}
disjunctHeadAtoms[index] = new Atom[datalogRules.size()];
int j = 0;
for (DLClause disjunct: datalogRules) {
disjunctHeadAtoms[index][j++] = disjunct.getHeadAtom(0);
}
++index;
if (headAtom.getDLPredicate() instanceof AtLeast)
offset += ((AtLeast) headAtom.getDLPredicate()).getNumber();
}
}
@Override
public boolean hasNext() {
return l != -1 || !auxiliaryClauses.isEmpty();
}
@Override
public DLClause next() {
if (l == -1)
return auxiliaryClauses.removeFirst();
if (length > 0) {
Atom[] headAtoms = new Atom[length];
for (int i = 0; i < length; ++i)
headAtoms[i] = disjunctHeadAtoms[i][pointer[i]];
++pointer[l];
while (l >= 0 && pointer[l] >= disjunctHeadAtoms[l].length) {
pointer[l] = 0;
--l;
if (l >= 0)
++pointer[l];
}
if (l >= 0) l = length - 1;
return DLClauseHelper.simplified(DLClause.create(headAtoms, bodyAtoms));
// return DLClause.create(headAtoms, bodyAtoms);
}
else {
--l;
return DLClauseHelper.simplified(DLClause.create(new Atom[0], bodyAtoms));
// return DLClause.create(new Atom[0], bodyAtoms);
}
}
@Override
public void remove() { }
}
}
|
