aboutsummaryrefslogtreecommitdiff
path: root/src/uk/ac/ox/cs/pagoda/rules/approximators
diff options
context:
space:
mode:
authorFederico Igne <federico.igne@cs.ox.ac.uk>2022-05-10 18:17:06 +0100
committerFederico Igne <federico.igne@cs.ox.ac.uk>2022-05-11 12:34:47 +0100
commit17bd9beaf7f358a44e5bf36a5855fe6727d506dc (patch)
tree47e9310a0cff869d9ec017dcb2c81876407782c8 /src/uk/ac/ox/cs/pagoda/rules/approximators
parent8651164cd632a5db310b457ce32d4fbc97bdc41c (diff)
downloadACQuA-17bd9beaf7f358a44e5bf36a5855fe6727d506dc.tar.gz
ACQuA-17bd9beaf7f358a44e5bf36a5855fe6727d506dc.zip
[pagoda] Move project to Scala
This commit includes a few changes: - The repository still uses Maven to manage dependency but it is now a Scala project. - The code has been ported from OWLAPI 3.4.10 to 5.1.20 - A proof of concept program using both RSAComb and PAGOdA has been added.
Diffstat (limited to 'src/uk/ac/ox/cs/pagoda/rules/approximators')
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java42
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java146
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java24
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java100
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java224
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java139
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java19
7 files changed, 0 insertions, 694 deletions
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java
deleted file mode 100644
index f910c64..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java
+++ /dev/null
@@ -1,42 +0,0 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.DLClause;
4
5import java.util.Collection;
6
7public interface Approximator {
8
9 Collection<DLClause> convert(DLClause clause, DLClause originalClause);
10
11}
12
13// TODO remove
14//class IgnoreExist implements Approximator {
15//
16// @Override
17// public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
18// Collection<DLClause> ret = new LinkedList<DLClause>();
19// DLPredicate p;
20// for (Atom headAtom: clause.getHeadAtoms()) {
21// p = headAtom.getDLPredicate();
22// if (p instanceof AtLeast) return ret;
23// }
24//
25// ret.add(clause);
26// return ret;
27// }
28//
29//}
30//
31//
32//
33//class IgnoreDisj implements Approximator {
34//
35// @Override
36// public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
37// Collection<DLClause> ret = new LinkedList<DLClause>();
38// if (clause.getHeadLength() > 1) return ret;
39// ret.add(clause);
40// return ret;
41// }
42//}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
deleted file mode 100644
index a140225..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ /dev/null
@@ -1,146 +0,0 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.pagoda.multistage.MultiStageUpperProgram;
5import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
6import uk.ac.ox.cs.pagoda.util.tuples.TupleBuilder;
7
8import java.util.ArrayList;
9import java.util.Collection;
10import java.util.Collections;
11
12/***
13 * Approximates existential rules through a limited form of Skolemisation.
14 * <p>
15 * Given a rule and a ground substitution,
16 * it Skolemises the rule
17 * if all the terms in the substitution have depth less than a given depth,
18 * otherwise it approximates using an alternative <tt>TupleDependentApproximator</tt>.
19 */
20public class LimitedSkolemisationApproximator implements TupleDependentApproximator {
21
22 private static final Atom[] EMPTY_BODY = new Atom[0];
23 private static final Variable X = Variable.create("X");
24 private final int maxTermDepth;
25 private final SkolemTermsManager skolemTermsManager;
26
27 public LimitedSkolemisationApproximator(int maxTermDepth) {
28 this.maxTermDepth = maxTermDepth;
29 this.skolemTermsManager = SkolemTermsManager.getInstance();
30 }
31
32 @Override
33 public Collection<DLClause> convert(DLClause clause,
34 DLClause originalClause,
35 Collection<Tuple<Individual>> violationTuples) {
36 switch(clause.getHeadLength()) {
37 case 1:
38 return overApprox(clause, originalClause, violationTuples);
39 case 0:
40 return Collections.singletonList(clause);
41 default:
42 throw new IllegalArgumentException(
43 "Expected clause with head length < 1, but it is " + clause.getHeadLength());
44 }
45
46
47 }
48
49 public int getMaxDepth(Tuple<Individual> violationTuple) {
50 int maxDepth = 0;
51 for(Individual individual : violationTuple)
52 maxDepth = Integer.max(maxDepth, skolemTermsManager.getDepthOf(individual));
53
54 return maxDepth;
55 }
56
57 private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
58 ArrayList<DLClause> result = new ArrayList<>();
59 for(Tuple<Individual> violationTuple : violationTuples) {
60 result.addAll(getGroundSkolemisation(clause,
61 originalClause, violationTuple, getMaxDepth(violationTuple) >= maxTermDepth));
62 }
63
64 return result;
65 }
66
67 private Collection<DLClause> getGroundSkolemisation(DLClause clause,
68 DLClause originalClause,
69 Tuple<Individual> violationTuple,
70 boolean useClauseUniqueIndividual) {
71
72 String[] commonVars = MultiStageUpperProgram.getCommonVars(clause);
73
74 // TODO check: strong assumption, the first tuples are the common ones
75 TupleBuilder<Individual> commonIndividualsBuilder = new TupleBuilder<>();
76 for(int i = 0; i < commonVars.length; i++)
77 commonIndividualsBuilder.append(violationTuple.get(i));
78 Tuple<Individual> commonIndividuals = commonIndividualsBuilder.build();
79
80 Atom headAtom = clause.getHeadAtom(0);
81
82// Atom[] bodyAtoms = clause.getBodyAtoms();
83 int offset = OverApproxExist.indexOfExistential(headAtom, originalClause);
84
85 // BEGIN: copy and paste
86 ArrayList<DLClause> ret = new ArrayList<>();
87 DLPredicate predicate = headAtom.getDLPredicate();
88 if(predicate instanceof AtLeastConcept) {
89 AtLeastConcept atLeastConcept = (AtLeastConcept) predicate;
90 LiteralConcept concept = atLeastConcept.getToConcept();
91 Role role = atLeastConcept.getOnRole();
92 AtomicConcept atomicConcept;
93
94 if(concept instanceof AtomicNegationConcept) {
95 Atom atom1 =
96 Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
97 Atom atom2 = Atom.create(atomicConcept = OverApproxExist.getNegationConcept(atomicConcept), X);
98 ret.add(DLClause.create(new Atom[0], new Atom[]{atom1, atom2}));
99 }
100 else {
101 atomicConcept = (AtomicConcept) concept;
102 if(atomicConcept.equals(AtomicConcept.THING))
103 atomicConcept = null;
104 }
105
106 int card = atLeastConcept.getNumber();
107 Individual[] individuals = new Individual[card];
108 SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
109 for(int i = 0; i < card; ++i)
110 if(useClauseUniqueIndividual)
111 individuals[i] = termsManager.getFreshIndividual(originalClause,
112 offset + i,
113 maxTermDepth + 1);
114 else
115 individuals[i] = termsManager.getFreshIndividual(originalClause,
116 offset + i,
117 commonIndividuals);
118
119 for(int i = 0; i < card; ++i) {
120 if(atomicConcept != null)
121 ret.add(DLClause.create(new Atom[]{Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY));
122
123 Atom atom = role instanceof AtomicRole ?
124 Atom.create((AtomicRole) role, commonIndividuals.get(0), individuals[i]) :
125 Atom.create(((InverseRole) role).getInverseOf(), individuals[i], commonIndividuals.get(0));
126
127 ret.add(DLClause.create(new Atom[]{atom}, EMPTY_BODY));
128 }
129
130 for(int i = 0; i < card; ++i)
131 for(int j = i + 1; j < card; ++j)
132 // TODO to be checked ... different as
133 ret.add(DLClause.create(new Atom[]{Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, EMPTY_BODY));
134
135 }
136 else if(predicate instanceof AtLeastDataRange) {
137 // TODO to be implemented ...
138 }
139 else
140 ret.add(DLClause.create(new Atom[]{headAtom}, EMPTY_BODY));
141
142 return ret;
143
144 // END: copy and paste
145 }
146}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java
deleted file mode 100644
index ae2a2cf..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java
+++ /dev/null
@@ -1,24 +0,0 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.AtLeastDataRange;
4import org.semanticweb.HermiT.model.DLClause;
5
6import java.util.Collection;
7import java.util.LinkedList;
8
9public class OverApproxBoth implements Approximator {
10
11 Approximator approxDist = new OverApproxDisj(), approxExist = new OverApproxExist();
12
13 @Override
14 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
15 Collection<DLClause> ret = new LinkedList<DLClause>();
16 for (DLClause tClause: approxDist.convert(clause, originalClause)) {
17 if (tClause.getHeadLength() > 0 && tClause.getHeadAtom(0).getDLPredicate() instanceof AtLeastDataRange)
18 continue;
19 ret.addAll(approxExist.convert(tClause, originalClause));
20 }
21 return ret;
22 }
23
24}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java
deleted file mode 100644
index 05d9442..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java
+++ /dev/null
@@ -1,100 +0,0 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
5
6import java.util.*;
7
8public class OverApproxDisj implements Approximator {
9
10 /**
11 * Splits a disjunctive rule into a bunch of rules.
12 * <p>
13 * It returns a collection containing a rule for each atom in the head of the input rule.
14 * Each rule has the same body of the input rule,
15 * and the relative head atom as head.
16 * */
17 @Override
18 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
19 LinkedList<DLClause> distincts = new LinkedList<DLClause>();
20 Atom[] headAtoms = clause.getHeadAtoms(), bodyAtoms = clause.getBodyAtoms();
21 LinkedList<DLClause> newClauses = new LinkedList<DLClause>();
22 DLClause newClause;
23 if (headAtoms.length > 1) {
24 for (Atom headAtom: headAtoms) {
25 newClause = DLClause.create(new Atom[] {headAtom}, bodyAtoms);
26 newClauses.add(newClause);
27// distincts.add(newClause);
28 }
29
30 for (DLClause cls: newClauses) {
31 newClause = DLClauseHelper.simplified(cls);
32 if (!isSubsumedBy(newClause, distincts))
33 distincts.add(newClause);
34 }
35 }
36 else distincts.add(clause);
37
38 return distincts;
39 }
40
41 public static boolean isSubsumedBy(DLClause newClause, Collection<DLClause> distinctClauses) {
42 Map<Variable, Term> unifier;
43 Set<Atom> bodyAtoms = new HashSet<Atom>();
44 for (DLClause clause: distinctClauses) {
45 if (newClause.getHeadLength() > 0 && clause.getHeadLength() > 0 &&
46 (unifier = isSubsumedBy(newClause.getHeadAtom(0), clause.getHeadAtom(0))) == null)
47 continue;
48 else
49 unifier = new HashMap<Variable, Term>();
50
51 for (Atom atom: clause.getBodyAtoms())
52 bodyAtoms.add(rename(atom, unifier));
53 unifier.clear();
54
55 for (Atom atom: newClause.getBodyAtoms())
56 if (!bodyAtoms.contains(atom))
57 continue;
58
59 return true;
60 }
61
62 return false;
63 }
64
65 public static Map<Variable, Term> isSubsumedBy(Atom atom1, Atom atom2) {
66 DLPredicate predicate = atom1.getDLPredicate();
67 if (!predicate.equals(atom2.getDLPredicate()))
68 return null;
69
70 Map<Variable, Term> unifier = new HashMap<Variable, Term>();
71 Term term1, term2;
72 for (int index = 0; index < predicate.getArity(); ++index) {
73 term1 = rename(atom1.getArgument(index), unifier);
74 term2 = rename(atom2.getArgument(index), unifier);
75
76 if (term1.equals(term2));
77 else if (term1 instanceof Variable)
78 unifier.put((Variable) term1, term2);
79 else
80 return null;
81 }
82 return unifier;
83 }
84
85 public static Atom rename(Atom atom, Map<Variable, Term> unifier) {
86 Term[] arguments = new Term[atom.getArity()];
87 for (int i = 0; i < atom.getArity(); ++i)
88 arguments[i] = rename(atom.getArgument(i), unifier);
89 return Atom.create(atom.getDLPredicate(), arguments);
90 }
91
92 public static Term rename(Term argument, Map<Variable, Term> unifier) {
93 Term newArg;
94 while ((newArg = unifier.get(argument)) != null)
95 return newArg;
96 return argument;
97 }
98
99
100}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
deleted file mode 100644
index 028568c..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
+++ /dev/null
@@ -1,224 +0,0 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
5
6import java.util.Collection;
7import java.util.Iterator;
8import java.util.LinkedList;
9
10public class OverApproxExist implements Approximator {
11
12 public static final String negativeSuffix = "_neg";
13 private static final Variable X = Variable.create("X");
14
15 static int indexOfExistential(Atom headAtom, DLClause originalClause) {
16 if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1;
17 AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
18 if (alc.getToConcept() instanceof AtomicConcept) {
19 AtomicConcept ac = (AtomicConcept) alc.getToConcept();
20 if (ac.getIRI().endsWith(negativeSuffix)) {
21 alc = AtLeastConcept.create(alc.getNumber(), alc.getOnRole(), AtomicNegationConcept.create(getNegationConcept(ac)));
22 headAtom = Atom.create(alc, headAtom.getArgument(0));
23 }
24 }
25
26 int index = 0;
27 for (Atom atom: originalClause.getHeadAtoms()) {
28 if (atom.equals(headAtom))
29 return index;
30 if (atom.getDLPredicate() instanceof AtLeast)
31 index += ((AtLeast) atom.getDLPredicate()).getNumber();
32 }
33 return -1;
34 }
35
36 public static AtomicConcept getNegationConcept(DLPredicate p) {
37 if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING;
38 if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING;
39
40 if (p instanceof AtomicConcept) {
41 String iri = ((AtomicConcept) p).getIRI();
42 if (iri.endsWith(negativeSuffix))
43 iri = iri.substring(0, iri.length() - 4);
44 else
45 iri += negativeSuffix;
46
47 return AtomicConcept.create(iri);
48 }
49 if (p instanceof AtLeastConcept) {
50 // FIXME !!! here
51 return null;
52 }
53 return null;
54 }
55
56 @Override
57 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
58 Collection<DLClause> ret;
59 switch (clause.getHeadLength()) {
60 case 1:
61 return overApprox(clause.getHeadAtom(0), clause.getBodyAtoms(), originalClause);
62 case 0:
63 ret = new LinkedList<DLClause>();
64 ret.add(clause);
65 return ret;
66 default:
67 ret = new LinkedList<DLClause>();
68 for (Iterator<DLClause> iter = new DisjunctiveHeads(clause, originalClause); iter.hasNext(); )
69 ret.add(iter.next());
70 return ret;
71 }
72 }
73
74 public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause) {
75 return overApprox(headAtom, bodyAtoms, originalClause, indexOfExistential(headAtom, originalClause));
76 }
77
78 public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause, int offset) {
79 Collection<DLClause> ret = new LinkedList<DLClause>();
80 DLPredicate predicate = headAtom.getDLPredicate();
81 if (predicate instanceof AtLeastConcept) {
82 AtLeastConcept atLeastConcept = (AtLeastConcept) predicate;
83 LiteralConcept concept = atLeastConcept.getToConcept();
84 Role role = atLeastConcept.getOnRole();
85 AtomicConcept atomicConcept = null;
86
87 if (concept instanceof AtomicNegationConcept) {
88 // TODO CHECK: is this already in MultiStageUpperProgram?
89 Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
90 Atom atom2 = Atom.create(atomicConcept = getNegationConcept(atomicConcept), X);
91 ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2}));
92 }
93 else {
94 atomicConcept = (AtomicConcept) concept;
95 if (atomicConcept.equals(AtomicConcept.THING))
96 atomicConcept = null;
97 }
98
99 int card = atLeastConcept.getNumber();
100 Individual[] individuals = new Individual[card];
101 SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
102 for (int i = 0; i < card; ++i) individuals[i] = termsManager.getFreshIndividual(originalClause, offset + i);
103
104 for (int i = 0; i < card; ++i) {
105 if (atomicConcept != null)
106 ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, bodyAtoms));
107
108 Atom atom = role instanceof AtomicRole ?
109 Atom.create((AtomicRole) role, X, individuals[i]) :
110 Atom.create(((InverseRole) role).getInverseOf(), individuals[i], X);
111
112 ret.add(DLClause.create(new Atom[] {atom}, bodyAtoms));
113 }
114
115 for (int i = 0; i < card; ++i)
116 for (int j = i + 1; j < card; ++j)
117 // TODO to be checked ... different as
118 ret.add(DLClause.create(new Atom[] {Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, bodyAtoms));
119 //DLClauseHelper.contructor_differentAs(individuals[i], individuals[j]));
120
121 }
122 else if (predicate instanceof AtLeastDataRange) {
123 // TODO to be implemented ...
124 }
125 else
126 ret.add(DLClause.create(new Atom[] {headAtom}, bodyAtoms));
127
128 return ret;
129 }
130
131 class DisjunctiveHeads implements Iterator<DLClause> {
132
133 Atom[] bodyAtoms;
134 Atom[][] disjunctHeadAtoms;
135 int[] pointer;
136 int length, l;
137 LinkedList<DLClause> auxiliaryClauses = new LinkedList<DLClause>();
138
139 public DisjunctiveHeads(DLClause clause, DLClause originalClause) {
140 length = clause.getHeadLength();
141
142 bodyAtoms = clause.getBodyAtoms();
143 disjunctHeadAtoms = new Atom[length][];
144 pointer = new int[length];
145 if (length > 0) l = length - 1;
146 else length = 0;
147
148 int index = 0, offset = 0;
149 Collection<DLClause> datalogRules;
150 DLClause newClause;
151 for (Atom headAtom: clause.getHeadAtoms()) {
152 pointer[index] = 0;
153
154 datalogRules = overApprox(headAtom, bodyAtoms, originalClause, offset);
155
156 if (datalogRules.isEmpty()) {
157 l = -1;
158 auxiliaryClauses.clear();
159 return ;
160 }
161
162 for (Iterator<DLClause> iter = datalogRules.iterator(); iter.hasNext(); ) {
163 newClause = iter.next();
164 if (!DLClauseHelper.hasSubsetBodyAtoms(newClause, clause)) {
165 auxiliaryClauses.add(newClause);
166 iter.remove();
167 }
168 }
169
170 disjunctHeadAtoms[index] = new Atom[datalogRules.size()];
171
172 int j = 0;
173 for (DLClause disjunct: datalogRules) {
174 disjunctHeadAtoms[index][j++] = disjunct.getHeadAtom(0);
175 }
176
177 ++index;
178 if (headAtom.getDLPredicate() instanceof AtLeast)
179 offset += ((AtLeast) headAtom.getDLPredicate()).getNumber();
180
181 }
182
183 }
184
185 @Override
186 public boolean hasNext() {
187 return l != -1 || !auxiliaryClauses.isEmpty();
188 }
189
190 @Override
191 public DLClause next() {
192 if (l == -1)
193 return auxiliaryClauses.removeFirst();
194
195 if (length > 0) {
196 Atom[] headAtoms = new Atom[length];
197 for (int i = 0; i < length; ++i)
198 headAtoms[i] = disjunctHeadAtoms[i][pointer[i]];
199
200 ++pointer[l];
201 while (l >= 0 && pointer[l] >= disjunctHeadAtoms[l].length) {
202 pointer[l] = 0;
203 --l;
204 if (l >= 0)
205 ++pointer[l];
206 }
207
208 if (l >= 0) l = length - 1;
209
210 return DLClauseHelper.simplified(DLClause.create(headAtoms, bodyAtoms));
211// return DLClause.create(headAtoms, bodyAtoms);
212 }
213 else {
214 --l;
215 return DLClauseHelper.simplified(DLClause.create(new Atom[0], bodyAtoms));
216// return DLClause.create(new Atom[0], bodyAtoms);
217 }
218 }
219
220 @Override
221 public void remove() { }
222
223 }
224}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
deleted file mode 100644
index ed93d0e..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
+++ /dev/null
@@ -1,139 +0,0 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.pagoda.util.Namespace;
5import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
6
7import java.util.HashMap;
8import java.util.Map;
9
10/**
11 * If you need a Skolem term (i.e. fresh individual), ask this class.
12 */
13public class SkolemTermsManager {
14
15 public static final String SKOLEMISED_INDIVIDUAL_PREFIX = Namespace.PAGODA_ANONY + "individual";
16 public static final String RULE_UNIQUE_SKOLEMISED_INDIVIDUAL_PREFIX = SKOLEMISED_INDIVIDUAL_PREFIX + "_unique";
17
18 private static SkolemTermsManager skolemTermsManager;
19
20 private int termsCounter = 0;
21 private Map<DLClause, Integer> clauseToId_map = new HashMap<>();
22 private Map<Individual, Integer> individualToDepth_map = new HashMap<>();
23 private int dependenciesCounter = 0;
24
25 private Map<Tuple<Individual>, Integer> dependencyToId_map = new HashMap<>();
26
27 private SkolemTermsManager() {
28 }
29
30 public static int indexOfSkolemisedIndividual(Atom atom) {
31 Term t;
32 for(int index = 0; index < atom.getArity(); ++index) {
33 t = atom.getArgument(index);
34 if(t instanceof Individual && ((Individual) t).getIRI().contains(SKOLEMISED_INDIVIDUAL_PREFIX))
35 return index;
36 }
37 return -1;
38 }
39
40 /**
41 * Returns the existing unique <tt>SkolemTermsManager</tt> or a new one.
42 * <p>
43 * Indeed the <tt>SkolemTermsManager</tt> is a singleton.
44 */
45 public static SkolemTermsManager getInstance() {
46 if(skolemTermsManager == null) skolemTermsManager = new SkolemTermsManager();
47 return skolemTermsManager;
48 }
49
50 /**
51 * Get a fresh Individual, unique for the clause, the offset and the dependency.
52 */
53 public Individual getFreshIndividual(DLClause originalClause, int offset, Tuple<Individual> dependency) {
54 String termId = Integer.toString(mapClauseToId(originalClause) + offset)
55 + "_" + mapDependencyToId(dependency);
56 Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId);
57
58 if(!individualToDepth_map.containsKey(newIndividual)) {
59 int depth = 0;
60 for (Individual individual : dependency)
61 depth = Integer.max(depth, getDepthOf(individual));
62 individualToDepth_map.put(newIndividual, depth + 1);
63 }
64
65 return newIndividual;
66 }
67
68 /***
69 * Create a term of a given depth, unique for the clause and the depth.
70 *
71 * @param originalClause
72 * @param offset
73 * @param depth
74 * @return
75 */
76 public Individual getFreshIndividual(DLClause originalClause, int offset, int depth) {
77 String termId = Integer.toString(mapClauseToId(originalClause) + offset) + "_depth_" + depth;
78 Individual newIndividual = Individual.create(RULE_UNIQUE_SKOLEMISED_INDIVIDUAL_PREFIX + termId);
79
80 individualToDepth_map.putIfAbsent(newIndividual, depth);
81
82 return newIndividual;
83 }
84
85 /**
86 * Get a fresh Individual, unique for the clause and the offset.
87 */
88 public Individual getFreshIndividual(DLClause originalClause, int offset) {
89 String termId = Integer.toString(mapClauseToId(originalClause) + offset);
90 return Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId);
91 }
92
93 /**
94 * Get the depth of a term.
95 * <p>
96 * The term must have been generated by this manager.
97 */
98 public int getDepthOf(Individual individual) {
99 if(individualToDepth_map.containsKey(individual)) return individualToDepth_map.get(individual);
100 else return 0;
101 }
102
103 /**
104 * Get the number of individuals generated by this manager.
105 */
106 public int getSkolemIndividualsCount() {
107 return individualToDepth_map.keySet().size();
108 }
109
110 /**
111 * Just for reading the clause id from <tt>LimitedSkolemisationApproximator</tt>.
112 */
113 int getClauseId(DLClause clause) {
114 return clauseToId_map.get(clause);
115 }
116
117 private int mapClauseToId(DLClause clause) {
118 if(!clauseToId_map.containsKey(clause)) {
119 clauseToId_map.put(clause, termsCounter);
120 termsCounter += noOfExistential(clause);
121 }
122 return clauseToId_map.get(clause);
123 }
124
125 private int mapDependencyToId(Tuple<Individual> dependency) {
126 if(!dependencyToId_map.containsKey(dependency))
127 dependencyToId_map.put(dependency, dependenciesCounter++);
128 return dependencyToId_map.get(dependency);
129 }
130
131 private int noOfExistential(DLClause originalClause) {
132 int no = 0;
133 for(Atom atom : originalClause.getHeadAtoms())
134 if(atom.getDLPredicate() instanceof AtLeast)
135 no += ((AtLeast) atom.getDLPredicate()).getNumber();
136 return no;
137 }
138
139}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
deleted file mode 100644
index c99a1ad..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
+++ /dev/null
@@ -1,19 +0,0 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.DLClause;
4import org.semanticweb.HermiT.model.Individual;
5import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
6
7import java.util.Collection;
8
9/**
10 * It can approximate clauses according to a collection of tuples of individuals.
11 * <p>
12 * In particular it can be used to approximate rules given some body instantiations.
13 */
14public interface TupleDependentApproximator {
15
16 Collection<DLClause> convert(DLClause clause,
17 DLClause originalClause,
18 Collection<Tuple<Individual>> individualsTuples);
19}
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-06 23:45:13 +0000