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