aboutsummaryrefslogtreecommitdiff
path: root/src/uk/ac/ox/cs
diff options
context:
space:
mode:
authorRncLsn <rnc.lsn@gmail.com>2015-05-19 19:06:04 +0100
committerRncLsn <rnc.lsn@gmail.com>2015-05-19 19:06:04 +0100
commit7a68441a541b12b22587fb53072193e1130049ff (patch)
treee05f826da89e73a7f961c505359f4135cca646a8 /src/uk/ac/ox/cs
parent612729386b645b120f8397a007cd8421986af0ad (diff)
downloadACQuA-7a68441a541b12b22587fb53072193e1130049ff.tar.gz
ACQuA-7a68441a541b12b22587fb53072193e1130049ff.zip
Deleted unused classes.
Diffstat (limited to 'src/uk/ac/ox/cs')
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication2.java51
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java69
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/RestrictedApplication2.java177
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java238
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java107
-rw-r--r--src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager2.java78
-rw-r--r--src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java3
-rw-r--r--src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java2
-rw-r--r--src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java37
-rw-r--r--src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java2
-rw-r--r--src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java15
-rw-r--r--src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java26
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java9
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java77
-rw-r--r--src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java247
15 files changed, 196 insertions, 942 deletions
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication2.java b/src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication2.java
deleted file mode 100644
index 8212733..0000000
--- a/src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication2.java
+++ /dev/null
@@ -1,51 +0,0 @@
1package uk.ac.ox.cs.pagoda.multistage;
2
3import java.util.Collection;
4
5import org.semanticweb.HermiT.model.AtLeastConcept;
6import org.semanticweb.HermiT.model.Atom;
7import org.semanticweb.HermiT.model.DLClause;
8
9import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
10import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
11import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
12import uk.ac.ox.cs.pagoda.rules.Program;
13
14public class FoldedApplication2 extends TwoStageApplication {
15
16 public FoldedApplication2(TwoStageQueryEngine engine, DatalogProgram program, GapByStore4ID gap) {
17 super(engine, program, gap);
18 }
19
20 @Override
21 protected void addAuxiliaryRules() {
22 Collection<DLClause> overClauses;
23 DLClause disjunct;
24 Atom[] bodyAtoms;
25 int i;
26 for (DLClause constraint: constraints)
27 for (Atom headAtom: constraint.getHeadAtoms())
28 if (headAtom.getDLPredicate() instanceof AtLeastConcept) {
29 disjunct = DLClause.create(new Atom[] {headAtom}, constraint.getBodyAtoms());
30 overClauses = overExist.convert(disjunct, getOriginalClause(constraint));
31 bodyAtoms = new Atom[constraint.getBodyLength() + 1];
32 bodyAtoms[0] = getNAFAtom(headAtom);
33 i = 0;
34 for (Atom bodyAtom: constraint.getBodyAtoms())
35 bodyAtoms[++i] = bodyAtom;
36 for (DLClause overClause: overClauses)
37 if (DLClauseHelper.hasSubsetBodyAtoms(disjunct, constraint))
38 addDatalogRule(DLClause.create(new Atom[] {overClause.getHeadAtom(0)}, bodyAtoms));
39 }
40 else
41 addDatalogRule(DLClause.create(new Atom[] {headAtom}, constraint.getBodyAtoms()));
42 }
43
44 @Override
45 protected Collection<DLClause> getInitialClauses(Program program) {
46 return program.getClauses();
47 }
48
49
50
51}
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java b/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java
deleted file mode 100644
index a9c127b..0000000
--- a/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java
+++ /dev/null
@@ -1,69 +0,0 @@
1package uk.ac.ox.cs.pagoda.multistage;
2
3import org.openrdf.model.Resource;
4import org.openrdf.model.Statement;
5import org.openrdf.model.Value;
6import org.openrdf.model.impl.URIImpl;
7import org.openrdf.rio.RDFHandler;
8import org.openrdf.rio.RDFHandlerException;
9import uk.ac.ox.cs.JRDFox.model.Individual;
10import uk.ac.ox.cs.pagoda.rules.approximators.SkolemTermsManager;
11import uk.ac.ox.cs.pagoda.util.Namespace;
12
13import java.util.Collection;
14import java.util.HashSet;
15import java.util.Set;
16
17public class IndividualCollector implements RDFHandler {
18
19 boolean addedSkolemised = false;
20 Set<Individual> individuals = new HashSet<Individual>();
21
22 @Override
23 public void startRDF() throws RDFHandlerException {
24 // TODO Auto-generated method stub
25
26 }
27
28 @Override
29 public void endRDF() throws RDFHandlerException {
30 // TODO Auto-generated method stub
31
32 }
33
34 @Override
35 public void handleNamespace(String prefix, String uri)
36 throws RDFHandlerException {
37 // TODO Auto-generated method stub
38
39 }
40
41 @Override
42 public void handleStatement(Statement st) throws RDFHandlerException {
43 Resource sub = st.getSubject();
44 if (sub instanceof URIImpl)
45 individuals.add(Individual.create(sub.toString()));
46 if (!st.getPredicate().toString().equals(Namespace.RDF_TYPE)) {
47 Value obj = st.getObject();
48 if (obj instanceof URIImpl)
49 individuals.add(Individual.create(sub.toString()));
50 }
51 }
52
53 @Override
54 public void handleComment(String comment) throws RDFHandlerException {
55 // TODO Auto-generated method stub
56
57 }
58
59 public Collection<Individual> getAllIndividuals() {
60 if (!addedSkolemised) {
61 int number = SkolemTermsManager.getInstance().getNumberOfSkolemisedIndividual();
62 for (int i = 0; i < number; ++i)
63 individuals.add(Individual.create(SkolemTermsManager.skolemisedIndividualPrefix + i));
64 addedSkolemised = true;
65 }
66 return individuals;
67 }
68
69}
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/RestrictedApplication2.java b/src/uk/ac/ox/cs/pagoda/multistage/RestrictedApplication2.java
deleted file mode 100644
index 66e8a17..0000000
--- a/src/uk/ac/ox/cs/pagoda/multistage/RestrictedApplication2.java
+++ /dev/null
@@ -1,177 +0,0 @@
1package uk.ac.ox.cs.pagoda.multistage;
2
3import java.util.Arrays;
4import java.util.Collection;
5import java.util.Comparator;
6import java.util.LinkedList;
7
8import org.semanticweb.HermiT.model.AtLeastConcept;
9import org.semanticweb.HermiT.model.Atom;
10import org.semanticweb.HermiT.model.AtomicConcept;
11import org.semanticweb.HermiT.model.DLClause;
12import org.semanticweb.HermiT.model.DLPredicate;
13
14import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
15import uk.ac.ox.cs.pagoda.multistage.treatement.SimpleComparator;
16import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
17import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
18import uk.ac.ox.cs.pagoda.rules.Program;
19
20public class RestrictedApplication2 extends TwoStageApplication {
21
22 private Normalisation norm;
23 private boolean hasDisjunctions;
24 private Comparator<Atom> disjunctComparator;
25
26 public RestrictedApplication2(TwoStageQueryEngine engine, DatalogProgram program, GapByStore4ID gap) {
27 super(engine, program, gap);
28 if (hasDisjunctions) {
29 addNegativeDatalogRules();
30 disjunctComparator = new SimpleComparator();
31 }
32 }
33
34 private void addNegativeDatalogRules() {
35 Collection<DLClause> allRules = new LinkedList<DLClause>(rules);
36 allRules.addAll(constraints);
37 for (DLClause clause: allRules) {
38 addAddtionalDatalogRules(clause);
39 }
40 allRules.clear();
41 }
42
43 private void addAddtionalDatalogRules(DLClause clause) {
44 Atom[] headAtoms = clause.getHeadAtoms();
45 Atom[] bodyAtoms = clause.getBodyAtoms();
46 int headLength = headAtoms.length;
47 int bodyLength = bodyAtoms.length;
48 DLClause tClause;
49 if (m_bottom.isBottomRule(clause)) {
50 if (clause.getBodyLength() == 1) return ;
51 for (int i = 0; i < bodyLength; ++i)
52 if (bodyAtoms[i].getDLPredicate() instanceof AtomicConcept) {
53 Atom[] newBodyAtoms = new Atom[bodyLength - 1];
54 for (int j = 0; j < bodyLength - 1; ++j)
55 newBodyAtoms[j] = j < i ? bodyAtoms[j] : bodyAtoms[j + 1];
56
57 Atom negativeAtom = MultiStageUpperProgram.getNegativeAtom(bodyAtoms[i]);
58 tClause = DLClause.create(new Atom[] { negativeAtom }, newBodyAtoms);
59 addDatalogRule(tClause);
60 }
61 }
62 else if (headLength > 1) {
63 for (int i = 0; i < headLength; ++i) {
64 DLPredicate p = headAtoms[i].getDLPredicate();
65 if (!(p instanceof AtomicConcept)) {
66 return ;
67 }
68 }
69
70 for (int i = 0; i < headLength; ++i) {
71 Atom[] newBodyAtoms = new Atom[headLength + bodyLength - 1];
72 for (int j = 0; j < headLength + bodyLength - 1; ++j)
73 newBodyAtoms[j] = j < bodyLength ? bodyAtoms[j] :
74 j < bodyLength + i ? MultiStageUpperProgram.getNegativeAtom(headAtoms[j - bodyLength]) :
75 MultiStageUpperProgram.getNegativeAtom(headAtoms[j - bodyLength + 1]);
76
77 tClause = DLClause.create(new Atom[] { headAtoms[i] }, newBodyAtoms);
78 addDatalogRule(tClause);
79 }
80 }
81 else if (headLength == 1) {
82 DLPredicate p = clause.getHeadAtom(0).getDLPredicate();
83 if (p instanceof AtomicConcept) {
84 Atom negativeHeadAtom = MultiStageUpperProgram.getNegativeAtom(clause.getHeadAtom(0));
85 for (int i = 0; i < bodyLength; ++i)
86 if (bodyAtoms[i].getDLPredicate() instanceof AtomicConcept) {
87 Atom[] newBodyAtoms = new Atom[clause.getBodyLength()];
88 newBodyAtoms[0] = negativeHeadAtom;
89 for (int j = 1; j < bodyLength; ++j)
90 newBodyAtoms[j] = j <= i ? bodyAtoms[j - 1] : bodyAtoms[j];
91
92 tClause = DLClause.create(new Atom[] {MultiStageUpperProgram.getNegativeAtom(bodyAtoms[i])}, newBodyAtoms);
93 addDatalogRule(tClause);
94 }
95 }
96 else if (p instanceof AtLeastConcept && clause.getBodyLength() == 1 && clause.getBodyAtom(0).getDLPredicate() instanceof AtomicConcept) {
97 AtLeastConcept alc = (AtLeastConcept) p;
98 AtomicConcept ac = norm.getLeftAuxiliaryConcept(alc, true);
99 if (ac != null) {
100 Atom bodyAtom = clause.getBodyAtom(0);
101 addDatalogRule(DLClause.create(new Atom[] {MultiStageUpperProgram.getNegativeAtom(bodyAtom)},
102 new Atom[] {MultiStageUpperProgram.getNegativeAtom(Atom.create(ac, bodyAtom.getArgument(0)))} ));
103 }
104 }
105 }
106 }
107
108 @Override
109 protected void addAuxiliaryRules() {
110 for (DLClause constraint: constraints)
111 if (constraint.getHeadLength() <= 1)
112 processExistentialRule(constraint);
113 else
114 processDisjunctiveRule(constraint);
115 }
116
117 private static final Atom[] empty = new Atom[0];
118
119 private void processDisjunctiveRule(DLClause constraint) {
120 int headLength = constraint.getHeadLength();
121 Atom[] orderedAtoms = new Atom[headLength];
122 for (int i = 0; i < headLength; ++i)
123 orderedAtoms[i] = constraint.getHeadAtom(i);
124
125 Arrays.sort(orderedAtoms, disjunctComparator);
126
127 Collection<Atom> bodyAtoms = new LinkedList<Atom>();
128 for (int i = 0; i < headLength; ++i) {
129 bodyAtoms.add(getNAFAtom(orderedAtoms[i]));
130 }
131 for (Atom atom: constraint.getBodyAtoms())
132 bodyAtoms.add(atom);
133
134 Atom negAtom;
135 for (Atom atom: constraint.getHeadAtoms()) {
136 negAtom = MultiStageUpperProgram.getNegativeAtom(atom);
137 bodyAtoms.add(getNAFAtom(negAtom));
138 addDatalogRule(DLClause.create(new Atom[] {atom}, bodyAtoms.toArray(empty)));
139 }
140 }
141
142 private void processExistentialRule(DLClause constraint) {
143 Atom[] bodyAtoms = new Atom[constraint.getBodyLength() + 1];
144 bodyAtoms[0] = getNAFAtom(constraint.getHeadAtom(0));
145 int i = 0;
146 for (Atom atom: constraint.getBodyAtoms())
147 bodyAtoms[++i] = atom;
148
149 Collection<DLClause> overClauses = overExist.convert(constraint, getOriginalClause(constraint));
150 for (DLClause clause: overClauses)
151 if (DLClauseHelper.hasSubsetBodyAtoms(clause, constraint))
152 addDatalogRule(DLClause.create(new Atom[] {clause.getHeadAtom(0)}, bodyAtoms));
153 }
154
155 @Override
156 protected Collection<DLClause> getInitialClauses(Program program) {
157 Collection<DLClause> clauses = program.getClauses();
158 hasDisjunctions = false;
159 for (DLClause clause: clauses)
160 if (clause.getHeadLength() > 1) {
161 hasDisjunctions = true;
162 break;
163 }
164
165 if (hasDisjunctions) {
166 norm = new Normalisation(clauses, program.getOntology(), m_bottom);
167 norm.process();
168 clauses = norm.m_normClauses;
169 }
170 return clauses;
171 }
172
173 protected DLClause getOriginalClause(DLClause clause) {
174 DLClause original = super.getOriginalClause(clause);
175 return norm.getOriginalClause(original);
176 }
177}
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java b/src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java
deleted file mode 100644
index 79627d9..0000000
--- a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java
+++ /dev/null
@@ -1,238 +0,0 @@
1package uk.ac.ox.cs.pagoda.multistage;
2
3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.JRDFox.JRDFStoreException;
5import uk.ac.ox.cs.JRDFox.store.TupleIterator;
6import uk.ac.ox.cs.pagoda.MyPrefixes;
7import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
8import uk.ac.ox.cs.pagoda.hermit.RuleHelper;
9import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
10import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager;
11import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
12import uk.ac.ox.cs.pagoda.rules.Program;
13import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
14import uk.ac.ox.cs.pagoda.util.Namespace;
15import uk.ac.ox.cs.pagoda.util.SparqlHelper;
16import uk.ac.ox.cs.pagoda.util.Utility;
17
18import java.util.*;
19
20abstract class TwoStageApplication {
21
22 private static final String NAF_suffix = "_NAF";
23 protected TwoStageQueryEngine engine;
24 protected MyPrefixes prefixes = MyPrefixes.PAGOdAPrefixes;
25 protected Set<DLClause> rules = new HashSet<DLClause>();
26 protected Collection<DLClause> constraints = new LinkedList<DLClause>();
27 protected BottomStrategy m_bottom;
28 protected Set<Atom> toGenerateNAFFacts = new HashSet<Atom>();
29 protected OverApproxExist overExist = new OverApproxExist();
30 Program lowerProgram;
31 boolean m_incrementally = true;
32 Set<Integer> allIndividuals = new HashSet<Integer>();
33 RDFoxTripleManager tripleManager;
34 private GapByStore4ID gap;
35 private StringBuilder datalogRuleText = new StringBuilder();
36 private Map<DLClause, DLClause> map = new HashMap<DLClause, DLClause>();
37
38 public TwoStageApplication(TwoStageQueryEngine engine, DatalogProgram program, GapByStore4ID gap) {
39 this.engine = engine;
40 tripleManager = new RDFoxTripleManager(engine.getDataStore(), m_incrementally);
41 this.gap = gap;
42 m_bottom = program.getUpperBottomStrategy();
43 lowerProgram = program.getLower();
44
45 Variable X = Variable.create("X");
46 Collection<DLClause> clauses = getInitialClauses(program.getGeneral());
47 Collection<DLClause> introducedConstraints = new LinkedList<DLClause>();
48 LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>();
49 for (DLClause clause : m_bottom.process(clauses)) {
50 if (m_bottom.isBottomRule(clause)
51 || clause.getHeadLength() == 1
52 && !(clause.getHeadAtom(0).getDLPredicate() instanceof AtLeast))
53 addDatalogRule(clause);
54 else {
55 newHeadAtoms.clear();
56 boolean changed = false;
57 for (Atom atom : clause.getHeadAtoms()) {
58 if (atom.getDLPredicate() instanceof AtLeastConcept) {
59 AtLeastConcept atLeast = (AtLeastConcept) atom
60 .getDLPredicate();
61 if (atLeast.getToConcept() instanceof AtomicNegationConcept) {
62 AtomicConcept positive = ((AtomicNegationConcept) atLeast
63 .getToConcept()).getNegatedAtomicConcept();
64 AtomicConcept negative = OverApproxExist
65 .getNegationConcept(positive);
66 Atom atom1 = Atom.create(positive, X);
67 Atom atom2 = Atom.create(negative, X);
68 introducedConstraints.add(DLClause.create(
69 new Atom[0], new Atom[] { atom1, atom2 }));
70 newHeadAtoms.add(Atom.create(AtLeastConcept.create(
71 atLeast.getArity(), atLeast.getOnRole(),
72 negative), atom.getArgument(0)));
73 changed = true;
74 continue;
75 }
76 } else if (atom.getDLPredicate() instanceof AtLeastDataRange)
77 changed = true;
78 else
79 newHeadAtoms.add(atom);
80
81 }
82 if (!changed)
83 constraints.add(clause);
84 else if (!newHeadAtoms.isEmpty()) {
85 DLClause newClause = DLClause.create(
86 newHeadAtoms.toArray(new Atom[0]),
87 clause.getBodyAtoms());
88 map.put(newClause, clause);
89 constraints.add(newClause);
90 }
91 }
92 }
93
94 for (DLClause clause : m_bottom.process(introducedConstraints))
95 addDatalogRule(clause);
96
97 }
98
99 int materialise() {
100 StringBuilder builder = new StringBuilder(getDatalogRuleText());
101 for (DLClause clause: lowerProgram.getClauses())
102 if (!rules.contains(clause))
103 builder.append(RuleHelper.getText(clause));
104
105 engine.materialise(builder.toString(), null, false);
106 addAuxiliaryRules();
107 addAuxiliaryNAFFacts();
108 engine.materialise(getDatalogRuleText(), gap, m_incrementally);
109 return engine.isValid() ? 1 : 0;
110 }
111
112 void checkNAFFacts() {
113 int counter = 0;
114 TupleIterator tuples = null;
115 for (Atom atom : toGenerateNAFFacts) {
116 try {
117 counter = 0;
118 atom = getNAFAtom(atom);
119 tuples = engine.internal_evaluate(SparqlHelper.getSPARQLQuery(
120 new Atom[] { atom }, atom.getArgumentVariable(0)
121 .getName()));
122 for (long multi = tuples.open(); multi != 0; multi = tuples.getNext()) {
123 ++counter;
124 }
125 Utility.logDebug(atom + " " + counter);
126 } catch (JRDFStoreException e) {
127 // TODO Auto-generated catch block
128 e.printStackTrace();
129 } finally {
130 if (tuples != null) tuples.dispose();
131 tuples = null;
132 }
133 }
134 }
135
136 protected void addDatalogRule(DLClause clause) {
137 if (clause.getBodyAtom(0).equals(clause.getHeadAtom(0)))
138 return;
139 rules.add(clause);
140 datalogRuleText.append(RuleHelper.getText(clause)).append('\n');
141 }
142
143 public String getDatalogRuleText() {
144 StringBuilder program = new StringBuilder();
145 program.append(prefixes.prefixesText());
146 program.append(datalogRuleText.toString());
147 return program.toString();
148 }
149
150 protected abstract void addAuxiliaryRules();
151
152 private void addAuxiliaryNAFFacts() {
153
154 for (int id : tripleManager.getResourceIDs(engine.getAllIndividuals()))
155 allIndividuals.add(id);
156
157 DLPredicate naf;
158 DLPredicate p;
159 for (Atom atom: toGenerateNAFFacts) {
160 naf = getNAFAtom(atom, false).getDLPredicate();
161 p = atom.getDLPredicate();
162
163 int typeID = tripleManager.getResourceID(Namespace.RDF_TYPE);
164 int conceptID = tripleManager.getResourceID(((AtomicConcept) naf)
165 .getIRI());
166 for (int answer : generateNAFFacts(p)) {
167 tripleManager.addTripleByID(new int[] { answer, typeID,
168 conceptID });
169 }
170 }
171 }
172
173 private Collection<Integer> generateNAFFacts(DLPredicate p) {
174 Variable X = Variable.create("X");
175 TupleIterator tuples = null;
176 Set<Integer> ret = new HashSet<Integer>(allIndividuals);
177 try {
178 tuples = engine.internal_evaluate(SparqlHelper.getSPARQLQuery(
179 new Atom[] { Atom.create(p, X) }, "X"));
180 for (long multi = tuples.open(); multi != 0; multi = tuples.getNext()) {
181 ret.remove(tuples.getResourceID(0));
182 }
183 } catch (JRDFStoreException e) {
184 // TODO Auto-generated catch block
185 e.printStackTrace();
186 } finally {
187 if (tuples != null) tuples.dispose();
188 }
189 return ret;
190 }
191
192 protected abstract Collection<DLClause> getInitialClauses(Program program);
193
194 protected Atom getNAFAtom(Atom atom) {
195 return getNAFAtom(atom, true);
196 }
197
198 private Atom getNAFAtom(Atom atom, boolean update) {
199 DLPredicate p = atom.getDLPredicate();
200 if (update) {
201 toGenerateNAFFacts.add(atom);
202 }
203 if (p instanceof AtomicConcept) {
204 AtomicConcept nc = AtomicConcept.create(((AtomicConcept) p)
205 .getIRI() + "_NAF");
206 return Atom.create(nc, atom.getArgument(0));
207 }
208 if (p instanceof Equality || p instanceof AnnotatedEquality)
209 return Atom.create(
210 AtomicRole.create(Namespace.EQUALITY + NAF_suffix),
211 atom.getArgument(0), atom.getArgument(1));
212 if (p instanceof Inequality)
213 atom = Atom.create(
214 AtomicRole.create(Namespace.INEQUALITY + NAF_suffix),
215 atom.getArgument(0), atom.getArgument(1));
216 // if (p instanceof AtomicRole) {
217 // AtomicRole nr = AtomicRole.create(((AtomicRole) p).getIRI() +
218 // NAF_suffix);
219 // return Atom.create(nr, atom.getArgument(0), atom.getArgument(1));
220 // }
221 if (p instanceof AtLeastConcept) {
222 AtomicConcept nc = AtomicConcept.create(Normalisation
223 .getAuxiliaryConcept4Disjunct((AtLeastConcept) p)
224 + NAF_suffix);
225 return Atom.create(nc, atom.getArgument(0));
226 }
227 Utility.logError("Unknown DLPredicate in an atom: " + atom);
228 return null;
229 }
230
231 protected DLClause getOriginalClause(DLClause clause) {
232 DLClause original = map.get(clause);
233 if (original == null)
234 return clause;
235 return original;
236 }
237
238} \ No newline at end of file
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java
deleted file mode 100644
index 29cf23a..0000000
--- a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java
+++ /dev/null
@@ -1,107 +0,0 @@
1package uk.ac.ox.cs.pagoda.multistage;
2
3import org.openrdf.rio.RDFHandlerException;
4import org.openrdf.rio.RDFParseException;
5import org.openrdf.rio.turtle.TurtleParser;
6import uk.ac.ox.cs.JRDFox.JRDFStoreException;
7import uk.ac.ox.cs.JRDFox.model.Individual;
8import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
9import uk.ac.ox.cs.pagoda.reasoner.QueryReasoner;
10import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
11import uk.ac.ox.cs.pagoda.util.Timer;
12import uk.ac.ox.cs.pagoda.util.Utility;
13
14import java.io.FileInputStream;
15import java.io.FileNotFoundException;
16import java.io.IOException;
17import java.util.Collection;
18
19public class TwoStageQueryEngine extends StageQueryEngine {
20
21 IndividualCollector m_collector = new IndividualCollector();
22
23 public TwoStageQueryEngine(String name, boolean checkValidity) {
24 super(name, checkValidity);
25 }
26
27 @Override
28 public void materialiseFoldedly(DatalogProgram dProgram, GapByStore4ID gap) {
29 TwoStageApplication program = new FoldedApplication2(this, dProgram, gap);
30 program.materialise();
31 }
32
33 @Override
34 public void importRDFData(String fileName, String importedFile) {
35 super.importRDFData(fileName, importedFile);
36 TurtleParser parser = new TurtleParser();
37 parser.setRDFHandler(m_collector);
38 for (String file: importedFile.split(QueryReasoner.ImportDataFileSeparator)) {
39 FileInputStream inputStream;
40 try {
41 inputStream = new FileInputStream(file);
42 parser.parse(inputStream, "");
43 inputStream.close();
44 } catch (FileNotFoundException e) {
45 // TODO Auto-generated catch block
46 e.printStackTrace();
47 } catch (RDFParseException e) {
48 // TODO Auto-generated catch block
49 e.printStackTrace();
50 } catch (RDFHandlerException e) {
51 // TODO Auto-generated catch block
52 e.printStackTrace();
53 } catch (IOException e) {
54 // TODO Auto-generated catch block
55 e.printStackTrace();
56 }
57 }
58 }
59
60 @Override
61 public int materialiseRestrictedly(DatalogProgram dProgram, GapByStore4ID gap) {
62 TwoStageApplication program = new RestrictedApplication2(this, dProgram, gap);
63 return program.materialise();
64 }
65
66 @Override
67 public int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap) {
68 throw new UnsupportedOperationException("This method is not available in " + getClass());
69 }
70
71 public void materialise(String programText, GapByStore4ID gap, boolean incrementally) {
72 try {
73 if (gap != null) {
74 try {
75 gap.compile(incrementally ? null : programText);
76 gap.addBackTo();
77 } finally {
78 gap.clear();
79 }
80 } else {
81 long oldTripleCount = store.getTriplesCount();
82 Timer t = new Timer();
83
84 if (!incrementally)
85// store.addRules(new String[] {programText});
86 store.importRules(programText);
87 store.applyReasoning(incrementally);
88
89 long tripleCount = store.getTriplesCount();
90
91 Utility.logDebug("current store after materialising upper related rules: " + tripleCount + " (" + (tripleCount - oldTripleCount) + " new)");
92 Utility.logDebug("current store finished the materialisation of upper related rules in " + t.duration() + " seconds.");
93 }
94 store.clearRulesAndMakeFactsExplicit();
95 } catch (JRDFStoreException e) {
96 e.printStackTrace();
97 }
98
99 }
100
101 public Collection<Individual> getAllIndividuals() {
102 return m_collector.getAllIndividuals();
103 }
104
105}
106
107
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager2.java b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager2.java
deleted file mode 100644
index 9191067..0000000
--- a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager2.java
+++ /dev/null
@@ -1,78 +0,0 @@
1package uk.ac.ox.cs.pagoda.reasoner;
2
3import org.semanticweb.owlapi.model.OWLOntologyCreationException;
4import org.semanticweb.owlapi.model.OWLOntologyManager;
5import uk.ac.ox.cs.pagoda.query.AnswerTuples;
6import uk.ac.ox.cs.pagoda.query.QueryRecord;
7import uk.ac.ox.cs.pagoda.reasoner.full.Checker;
8import uk.ac.ox.cs.pagoda.summary.HermitSummaryFilter;
9import uk.ac.ox.cs.pagoda.tracking.QueryTracker;
10import uk.ac.ox.cs.pagoda.util.Utility;
11
12@Deprecated
13public class ConsistencyManager2 extends ConsistencyManager {
14
15 public ConsistencyManager2(MyQueryReasoner reasoner) {
16 super(reasoner);
17 fragmentExtracted = true;
18 }
19
20 protected boolean unsatisfiability(double duration) {
21 Utility.logDebug("The ontology and dataset is unsatisfiable.");
22 return false;
23 }
24
25 protected boolean satisfiability(double duration) {
26 Utility.logDebug("The ontology and dataset is satisfiable.");
27 return true;
28 }
29
30 @Override
31 boolean check() {
32// if (!checkRLLowerBound()) return false;
33// if (!checkELLowerBound()) return false;
34 // TODO test
35 if (checkUpper(m_reasoner.lazyUpperStore) && checkUpper(m_reasoner.limitedSkolemUpperStore)) return true;
36 AnswerTuples iter = null;
37
38 try {
39 iter = m_reasoner.trackingStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables());
40 fullQueryRecord.updateUpperBoundAnswers(iter);
41 } finally {
42 if (iter != null) iter.dispose();
43 }
44
45 if (fullQueryRecord.getNoOfCompleteAnswers() == 0)
46 return satisfiability(t.duration());
47
48 try {
49 extractAxioms();
50 } catch (OWLOntologyCreationException e) {
51 e.printStackTrace();
52 }
53
54 Checker checker = new HermitSummaryFilter(fullQueryRecord, true); // m_reasoner.factory.getSummarisedReasoner(fullQueryRecord);
55// fullQueryRecord.saveRelevantOntology("fragment_bottom.owl");
56 boolean satisfiable = checker.isConsistent();
57 checker.dispose();
58 if (!satisfiable) return unsatisfiability(t.duration());
59
60 return satisfiability(t.duration());
61 }
62
63 private void extractAxioms() throws OWLOntologyCreationException {
64 OWLOntologyManager manager = m_reasoner.encoder.getProgram().getOntology().getOWLOntologyManager();
65 fullQueryRecord.setRelevantOntology(manager.createOntology());
66 QueryTracker tracker = new QueryTracker(m_reasoner.encoder, m_reasoner.rlLowerStore, fullQueryRecord);
67 m_reasoner.encoder.setCurrentQuery(fullQueryRecord);
68 tracker.extract(m_reasoner.trackingStore, null, true);
69 }
70
71 @Override
72 public QueryRecord[] getQueryRecords() {
73 if (botQueryRecords == null)
74 botQueryRecords = new QueryRecord[] {fullQueryRecord};
75 return botQueryRecords;
76 }
77
78}
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java
index ab57ccf..2285b5f 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java
@@ -2,7 +2,6 @@ package uk.ac.ox.cs.pagoda.reasoner;
2 2
3import org.semanticweb.karma2.profile.ELHOProfile; 3import org.semanticweb.karma2.profile.ELHOProfile;
4import org.semanticweb.owlapi.model.OWLOntology; 4import org.semanticweb.owlapi.model.OWLOntology;
5
6import uk.ac.ox.cs.pagoda.constraints.UnaryBottom; 5import uk.ac.ox.cs.pagoda.constraints.UnaryBottom;
7import uk.ac.ox.cs.pagoda.query.AnswerTuples; 6import uk.ac.ox.cs.pagoda.query.AnswerTuples;
8import uk.ac.ox.cs.pagoda.query.QueryRecord; 7import uk.ac.ox.cs.pagoda.query.QueryRecord;
@@ -12,7 +11,7 @@ import uk.ac.ox.cs.pagoda.rules.LowerDatalogProgram;
12import uk.ac.ox.cs.pagoda.util.Timer; 11import uk.ac.ox.cs.pagoda.util.Timer;
13import uk.ac.ox.cs.pagoda.util.Utility; 12import uk.ac.ox.cs.pagoda.util.Utility;
14 13
15public class ELHOQueryReasoner extends QueryReasoner { 14class ELHOQueryReasoner extends QueryReasoner {
16 15
17 LowerDatalogProgram program; 16 LowerDatalogProgram program;
18 17
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java
index 6da86ac..a4fa7c3 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java
@@ -14,7 +14,7 @@ import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
14import uk.ac.ox.cs.pagoda.util.Timer; 14import uk.ac.ox.cs.pagoda.util.Timer;
15import uk.ac.ox.cs.pagoda.util.Utility; 15import uk.ac.ox.cs.pagoda.util.Utility;
16 16
17public class ELHOUQueryReasoner extends QueryReasoner { 17class ELHOUQueryReasoner extends QueryReasoner {
18 18
19 DatalogProgram program; 19 DatalogProgram program;
20 20
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java
index 5511691..d1856c9 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java
@@ -1,32 +1,22 @@
1package uk.ac.ox.cs.pagoda.reasoner; 1package uk.ac.ox.cs.pagoda.reasoner;
2 2
3import java.io.File;
4import java.io.IOException;
5import java.util.HashSet;
6import java.util.Set;
7
8import org.semanticweb.HermiT.Reasoner; 3import org.semanticweb.HermiT.Reasoner;
9import org.semanticweb.owlapi.model.OWLClassExpression; 4import org.semanticweb.owlapi.model.*;
10import org.semanticweb.owlapi.model.OWLDataFactory;
11import org.semanticweb.owlapi.model.OWLNamedIndividual;
12import org.semanticweb.owlapi.model.OWLOntology;
13import org.semanticweb.owlapi.model.OWLOntologyCreationException;
14import org.semanticweb.owlapi.model.OWLOntologyStorageException;
15
16import uk.ac.ox.cs.JRDFox.model.Individual; 5import uk.ac.ox.cs.JRDFox.model.Individual;
17import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine; 6import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine;
18import uk.ac.ox.cs.pagoda.owl.OWLHelper; 7import uk.ac.ox.cs.pagoda.owl.OWLHelper;
19import uk.ac.ox.cs.pagoda.owl.QueryRoller; 8import uk.ac.ox.cs.pagoda.owl.QueryRoller;
20import uk.ac.ox.cs.pagoda.query.AnswerTuple; 9import uk.ac.ox.cs.pagoda.query.*;
21import uk.ac.ox.cs.pagoda.query.AnswerTuples;
22import uk.ac.ox.cs.pagoda.query.AnswerTuplesImp;
23import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
24import uk.ac.ox.cs.pagoda.query.QueryRecord;
25import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; 10import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
26import uk.ac.ox.cs.pagoda.rules.DatalogProgram; 11import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
27import uk.ac.ox.cs.pagoda.util.Utility; 12import uk.ac.ox.cs.pagoda.util.Utility;
28 13
29public class HermiTReasoner extends QueryReasoner { 14import java.io.File;
15import java.io.IOException;
16import java.util.HashSet;
17import java.util.Set;
18
19class HermiTReasoner extends QueryReasoner {
30 20
31 Reasoner hermit; 21 Reasoner hermit;
32 22
@@ -54,15 +44,8 @@ public class HermiTReasoner extends QueryReasoner {
54 OWLOntology tbox = onto; 44 OWLOntology tbox = onto;
55 try { 45 try {
56 onto = OWLHelper.getImportedOntology(tbox, importedData.toString().split(ImportDataFileSeparator)); 46 onto = OWLHelper.getImportedOntology(tbox, importedData.toString().split(ImportDataFileSeparator));
57 importedOntologyPath = OWLHelper.getOntologyPath(onto); 47 importedOntologyPath = OWLHelper.getOntologyPath(onto);
58 } catch (OWLOntologyCreationException e) { 48 } catch(OWLOntologyCreationException | OWLOntologyStorageException | IOException e) {
59 // TODO Auto-generated catch block
60 e.printStackTrace();
61 } catch (OWLOntologyStorageException e) {
62 // TODO Auto-generated catch block
63 e.printStackTrace();
64 } catch (IOException e) {
65 // TODO Auto-generated catch block
66 e.printStackTrace(); 49 e.printStackTrace();
67 } 50 }
68 51
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
index b10e2d1..6adbd37 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -25,7 +25,7 @@ import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
25import java.util.Collection; 25import java.util.Collection;
26import java.util.HashMap; 26import java.util.HashMap;
27 27
28public class MyQueryReasoner extends QueryReasoner { 28class MyQueryReasoner extends QueryReasoner {
29 29
30 OWLOntology ontology; 30 OWLOntology ontology;
31 DatalogProgram program; 31 DatalogProgram program;
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java
index 3894874..60f34c6 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java
@@ -10,18 +10,17 @@ import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxQueryEngine;
10import uk.ac.ox.cs.pagoda.rules.LowerDatalogProgram; 10import uk.ac.ox.cs.pagoda.rules.LowerDatalogProgram;
11import uk.ac.ox.cs.pagoda.util.Timer; 11import uk.ac.ox.cs.pagoda.util.Timer;
12 12
13public class RLQueryReasoner extends QueryReasoner { 13class RLQueryReasoner extends QueryReasoner {
14 14
15 RDFoxQueryEngine rlLowerStore = null; 15 RDFoxQueryEngine rlLowerStore = null;
16 16
17 LowerDatalogProgram program; 17 LowerDatalogProgram program;
18 Timer t = new Timer();
18 19
19 public RLQueryReasoner() { 20 public RLQueryReasoner() {
20 rlLowerStore = new BasicQueryEngine("rl"); 21 rlLowerStore = new BasicQueryEngine("rl");
21 } 22 }
22 23
23 Timer t = new Timer();
24
25 @Override 24 @Override
26 public void evaluate(QueryRecord queryRecord) { 25 public void evaluate(QueryRecord queryRecord) {
27 AnswerTuples rlAnswer = null; 26 AnswerTuples rlAnswer = null;
@@ -56,10 +55,8 @@ public class RLQueryReasoner extends QueryReasoner {
56 public boolean preprocess() { 55 public boolean preprocess() {
57 rlLowerStore.importRDFData("data", importedData.toString()); 56 rlLowerStore.importRDFData("data", importedData.toString());
58 rlLowerStore.materialise("lower program", program.toString()); 57 rlLowerStore.materialise("lower program", program.toString());
59 58
60 if (!isConsistent()) 59 return isConsistent();
61 return false;
62 return true;
63 } 60 }
64 61
65 @Override 62 @Override
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java
index fe4022d..e5564d9 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java
@@ -1,7 +1,6 @@
1package uk.ac.ox.cs.pagoda.reasoner; 1package uk.ac.ox.cs.pagoda.reasoner;
2 2
3import org.semanticweb.owlapi.model.OWLOntology; 3import org.semanticweb.owlapi.model.OWLOntology;
4
5import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine; 4import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine;
6import uk.ac.ox.cs.pagoda.owl.EqualitiesEliminator; 5import uk.ac.ox.cs.pagoda.owl.EqualitiesEliminator;
7import uk.ac.ox.cs.pagoda.query.AnswerTuples; 6import uk.ac.ox.cs.pagoda.query.AnswerTuples;
@@ -12,26 +11,25 @@ import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
12import uk.ac.ox.cs.pagoda.util.Timer; 11import uk.ac.ox.cs.pagoda.util.Timer;
13import uk.ac.ox.cs.pagoda.util.Utility; 12import uk.ac.ox.cs.pagoda.util.Utility;
14 13
15public class RLUQueryReasoner extends QueryReasoner { 14class RLUQueryReasoner extends QueryReasoner {
16 15
17 DatalogProgram program; 16 DatalogProgram program;
18 17
19 BasicQueryEngine rlLowerStore, rlUpperStore; 18 BasicQueryEngine rlLowerStore, rlUpperStore;
20 19
21 boolean multiStageTag, equalityTag; 20 boolean multiStageTag, equalityTag;
21 Timer t = new Timer();
22 22
23 public RLUQueryReasoner(boolean multiStageTag, boolean considerEqualities) { 23 public RLUQueryReasoner(boolean multiStageTag, boolean considerEqualities) {
24 this.multiStageTag = multiStageTag; 24 this.multiStageTag = multiStageTag;
25 this.equalityTag = considerEqualities; 25 this.equalityTag = considerEqualities;
26 rlLowerStore = new BasicQueryEngine("rl-lower-bound"); 26 rlLowerStore = new BasicQueryEngine("rl-lower-bound");
27 if (!multiStageTag) 27 if(!multiStageTag)
28 rlUpperStore = new BasicQueryEngine("rl-upper-bound"); 28 rlUpperStore = new BasicQueryEngine("rl-upper-bound");
29 else 29 else
30 rlUpperStore = new MultiStageQueryEngine("rl-upper-bound", false); 30 rlUpperStore = new MultiStageQueryEngine("rl-upper-bound", false);
31 } 31 }
32 32
33 Timer t = new Timer();
34
35 @Override 33 @Override
36 public void evaluate(QueryRecord queryRecord) { 34 public void evaluate(QueryRecord queryRecord) {
37 AnswerTuples ans = null; 35 AnswerTuples ans = null;
@@ -100,11 +98,9 @@ public class RLUQueryReasoner extends QueryReasoner {
100 98
101 rlUpperStore.importRDFData("data", datafile); 99 rlUpperStore.importRDFData("data", datafile);
102 rlUpperStore.materialiseRestrictedly(program, null); 100 rlUpperStore.materialiseRestrictedly(program, null);
103
104 if (!isConsistent())
105 return false;
106 101
107 return true; 102 return isConsistent();
103
108 } 104 }
109 105
110 @Override 106 @Override
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
index 20ae53b..3f1ed7e 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -1,13 +1,14 @@
1package uk.ac.ox.cs.pagoda.rules.approximators; 1package uk.ac.ox.cs.pagoda.rules.approximators;
2 2
3import org.semanticweb.HermiT.model.*; 3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
5import uk.ac.ox.cs.pagoda.multistage.MultiStageUpperProgram; 4import uk.ac.ox.cs.pagoda.multistage.MultiStageUpperProgram;
6import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; 5import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
7import uk.ac.ox.cs.pagoda.util.tuples.Tuple; 6import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
8import uk.ac.ox.cs.pagoda.util.tuples.TupleBuilder; 7import uk.ac.ox.cs.pagoda.util.tuples.TupleBuilder;
9 8
10import java.util.*; 9import java.util.ArrayList;
10import java.util.Arrays;
11import java.util.Collection;
11 12
12/** 13/**
13 * Approximates existential rules through a limited form of Skolemisation. 14 * Approximates existential rules through a limited form of Skolemisation.
@@ -24,7 +25,6 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
24 private final int maxTermDepth; 25 private final int maxTermDepth;
25 private final TupleDependentApproximator alternativeApproximator; 26 private final TupleDependentApproximator alternativeApproximator;
26 private final SkolemTermsManager skolemTermsManager; 27 private final SkolemTermsManager skolemTermsManager;
27 private Map<AnswerTupleID, Integer> mapIndividualsToDepth;
28 28
29 public LimitedSkolemisationApproximator(int maxTermDepth) { 29 public LimitedSkolemisationApproximator(int maxTermDepth) {
30 this(maxTermDepth, new ExistConstantApproximator()); 30 this(maxTermDepth, new ExistConstantApproximator());
@@ -33,7 +33,6 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
33 public LimitedSkolemisationApproximator(int maxTermDepth, TupleDependentApproximator alternativeApproximator) { 33 public LimitedSkolemisationApproximator(int maxTermDepth, TupleDependentApproximator alternativeApproximator) {
34 this.maxTermDepth = maxTermDepth; 34 this.maxTermDepth = maxTermDepth;
35 this.alternativeApproximator = alternativeApproximator; 35 this.alternativeApproximator = alternativeApproximator;
36 this.mapIndividualsToDepth = new HashMap<>();
37 this.skolemTermsManager = SkolemTermsManager.getInstance(); 36 this.skolemTermsManager = SkolemTermsManager.getInstance();
38 } 37 }
39 38
@@ -144,7 +143,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
144 public int getMaxDepth(Tuple<Individual> violationTuple) { 143 public int getMaxDepth(Tuple<Individual> violationTuple) {
145 int maxDepth = 0; 144 int maxDepth = 0;
146 for (Individual individual : violationTuple) 145 for (Individual individual : violationTuple)
147 maxDepth = Integer.max(maxDepth, skolemTermsManager.getDepth(individual)); 146 maxDepth = Integer.max(maxDepth, skolemTermsManager.getDepthOf(individual));
148 147
149 return maxDepth; 148 return maxDepth;
150 } 149 }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
index 0c12a27..368c014 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
@@ -12,38 +12,56 @@ import java.util.Map;
12 */ 12 */
13public class SkolemTermsManager { 13public class SkolemTermsManager {
14 14
15 public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; 15 public static final String SKOLEMISED_INDIVIDUAL_PREFIX = Namespace.PAGODA_ANONY + "individual";
16 16
17 private static SkolemTermsManager skolemTermsManager; 17 private static SkolemTermsManager skolemTermsManager;
18 18
19 private int individualCounter = 0; 19 private int termsCounter = 0;
20 private Map<DLClause, Integer> termNumber = new HashMap<>(); 20 private Map<DLClause, Integer> mapClauseToId = new HashMap<>();
21 private Map<Individual, Integer> mapIndividualToDepth = new HashMap<>(); 21 private Map<Individual, Integer> mapTermToDepth = new HashMap<>();
22 private int dependenciesCounter = 0; 22 private int dependenciesCounter = 0;
23 23
24 // replace with hashcode. in case of collision you get only a different upper bound model. 24 // TODO replace with hashcode. in case of collision you get only a different upper bound model.
25 // or, better, use perfect hashing (i.e. devise an ad-hoc hash function without collisions) 25 // TODO you can use a cash.
26 private Map<Tuple<Individual>, Integer> mapDependencyToId = new HashMap<>(); 26 private Map<Tuple<Individual>, Integer> mapDependencyToId = new HashMap<>();
27 27
28 private SkolemTermsManager() {
29 }
30
31 public static int indexOfSkolemisedIndividual(Atom atom) {
32 Term t;
33 for(int index = 0; index < atom.getArity(); ++index) {
34 t = atom.getArgument(index);
35 if(t instanceof Individual && ((Individual) t).getIRI().contains(SKOLEMISED_INDIVIDUAL_PREFIX))
36 return index;
37 }
38 return -1;
39 }
40
41 public static SkolemTermsManager getInstance() {
42 if(skolemTermsManager == null) skolemTermsManager = new SkolemTermsManager();
43 return skolemTermsManager;
44 }
45
28 /** 46 /**
29 * Get a fresh Individual, unique for the clause, the offset and the dependency. 47 * Get a fresh Individual, unique for the clause, the offset and the dependency.
30 * */ 48 * */
31 public Individual getFreshIndividual(DLClause originalClause, int offset, Tuple<Individual> dependency) { 49 public Individual getFreshIndividual(DLClause originalClause, int offset, Tuple<Individual> dependency) {
32 if (!termNumber.containsKey(originalClause)) { 50 if(!mapClauseToId.containsKey(originalClause)) {
33 termNumber.put(originalClause, individualCounter); 51 mapClauseToId.put(originalClause, termsCounter);
34 individualCounter += noOfExistential(originalClause); 52 termsCounter += noOfExistential(originalClause);
35 } 53 }
36 if (!mapDependencyToId.containsKey(dependency)) { 54 if (!mapDependencyToId.containsKey(dependency)) {
37 mapDependencyToId.put(dependency, dependenciesCounter++); 55 mapDependencyToId.put(dependency, dependenciesCounter++);
38 } 56 }
39 57
40 String termId = termNumber.get(originalClause) + offset + "_" + mapDependencyToId(dependency); 58 String termId = mapClauseToId.get(originalClause) + offset + "_" + mapDependencyToId(dependency);
41 Individual newIndividual = Individual.create(skolemisedIndividualPrefix + termId); 59 Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId);
42 60
43 int depth = 0; 61 int depth = 0;
44 for (Individual individual : dependency) 62 for (Individual individual : dependency)
45 depth = Integer.max(depth, mapIndividualToDepth(individual)); 63 depth = Integer.max(depth, mapIndividualToDepth(individual));
46 mapIndividualToDepth.put(newIndividual, depth); 64 mapTermToDepth.put(newIndividual, depth);
47 65
48 return newIndividual; 66 return newIndividual;
49 } 67 }
@@ -52,14 +70,14 @@ public class SkolemTermsManager {
52 * Get a fresh Individual, unique for the clause and the offset. 70 * Get a fresh Individual, unique for the clause and the offset.
53 * */ 71 * */
54 public Individual getFreshIndividual(DLClause originalClause, int offset) { 72 public Individual getFreshIndividual(DLClause originalClause, int offset) {
55 if (!termNumber.containsKey(originalClause)) { 73 if(!mapClauseToId.containsKey(originalClause)) {
56 termNumber.put(originalClause, individualCounter); 74 mapClauseToId.put(originalClause, termsCounter);
57 individualCounter += noOfExistential(originalClause); 75 termsCounter += noOfExistential(originalClause);
58 } 76 }
59 77
60 String termId = "" + termNumber.get(originalClause) + offset; 78 String termId = "" + mapClauseToId.get(originalClause) + offset;
61 Individual newIndividual = Individual.create(skolemisedIndividualPrefix + termId); 79 Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId);
62 mapIndividualToDepth.put(newIndividual, 0); 80 mapTermToDepth.put(newIndividual, 0);
63 81
64 return newIndividual; 82 return newIndividual;
65 } 83 }
@@ -69,7 +87,7 @@ public class SkolemTermsManager {
69 * <p> 87 * <p>
70 * The term must have been generated by this manager. 88 * The term must have been generated by this manager.
71 * */ 89 * */
72 public int getDepth(Individual individual) { 90 public int getDepthOf(Individual individual) {
73 return mapIndividualToDepth(individual); 91 return mapIndividualToDepth(individual);
74 } 92 }
75 93
@@ -77,24 +95,7 @@ public class SkolemTermsManager {
77 * Get the number of individuals generated by this manager. 95 * Get the number of individuals generated by this manager.
78 * */ 96 * */
79 public int getNumberOfSkolemisedIndividual() { 97 public int getNumberOfSkolemisedIndividual() {
80 return mapIndividualToDepth.keySet().size(); 98 return mapTermToDepth.keySet().size();
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 private SkolemTermsManager() {
93 }
94
95 public static SkolemTermsManager getInstance() {
96 if (skolemTermsManager == null) skolemTermsManager = new SkolemTermsManager();
97 return skolemTermsManager;
98 } 99 }
99 100
100 private int mapDependencyToId(Tuple<Individual> dependency) { 101 private int mapDependencyToId(Tuple<Individual> dependency) {
@@ -103,7 +104,7 @@ public class SkolemTermsManager {
103 } 104 }
104 105
105 private int mapIndividualToDepth(Individual dependency) { 106 private int mapIndividualToDepth(Individual dependency) {
106 if (mapIndividualToDepth.containsKey(dependency)) return mapIndividualToDepth.get(dependency); 107 if(mapTermToDepth.containsKey(dependency)) return mapTermToDepth.get(dependency);
107 else return 0; 108 else return 0;
108 } 109 }
109 110
diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
index 2143b03..d96c747 100644
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
+++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
@@ -17,95 +17,98 @@ import java.util.Set;
17 17
18public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap { 18public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
19 19
20 private Set<DLClause> disjunctiveRules = new HashSet<DLClause>();
21 private Variable X = Variable.create("X"), Y = Variable.create("Y");
22 private String bottomTrackingProgram = null;
23
20 public TrackingRuleEncoderDisjVar1(UpperDatalogProgram program, BasicQueryEngine store) { 24 public TrackingRuleEncoderDisjVar1(UpperDatalogProgram program, BasicQueryEngine store) {
21 super(program, store); 25 super(program, store);
22 } 26 }
23 27
24 private Set<DLClause> disjunctiveRules = new HashSet<DLClause>();
25
26 @Override 28 @Override
27 public boolean encodingRules() { 29 public boolean encodingRules() {
28 if (super.encodingRules()) { 30 if (super.encodingRules()) {
29 processDisjunctiveRules(); 31 processDisjunctiveRules();
30 return true; 32 return true;
31 } 33 }
32 return false; 34 return false;
33 } 35 }
34 36
35 @Override 37 @Override
36 protected void encodingRule(DLClause clause) { 38 protected void encodingRule(DLClause clause) {
37 if (currentQuery.isBottom()) { 39 if (currentQuery.isBottom()) {
38// super.encodingRule(clause); 40// super.encodingRule(clause);
39 encodingBottomQueryClause(clause); 41 encodingBottomQueryClause(clause);
40 return ; 42 return;
41 } 43 }
42 44
43 DLClause original = program.getCorrespondingClause(clause); 45 DLClause original = program.getCorrespondingClause(clause);
44 if (original.getHeadLength() <= 1) { 46 if (original.getHeadLength() <= 1) {
45 super.encodingRule(clause); 47 super.encodingRule(clause);
46 } 48 }
47 else { 49 else {
48 if (!DLClauseHelper.hasSubsetBodyAtoms(clause, original)) 50 if (!DLClauseHelper.hasSubsetBodyAtoms(clause, original))
49 super.encodingRule(clause); 51 super.encodingRule(clause);
50 addDisjunctiveRule(original); 52 addDisjunctiveRule(original);
51 } 53 }
52 54
53 } 55 }
54
55 56
56 private void processDisjunctiveRules() { 57 private void processDisjunctiveRules() {
57 for (DLClause clause: disjunctiveRules) 58 for (DLClause clause: disjunctiveRules)
58 encodingDisjunctiveRule(clause); 59 encodingDisjunctiveRule(clause);
59 } 60 }
60 61
61 private Atom getAuxiliaryAtom(Atom headAtom) { 62 private Atom getAuxiliaryAtom(Atom headAtom) {
62 DLPredicate p = headAtom.getDLPredicate(); 63 DLPredicate p = headAtom.getDLPredicate();
63 if (p instanceof AtLeast || p instanceof AtLeast) { 64 if (p instanceof AtLeast || p instanceof AtLeast) {
64 return Atom.create(generateAuxiliaryRule((AtLeast) p, true), headAtom.getArgument(0)); 65 return Atom.create(generateAuxiliaryRule((AtLeast) p, true), headAtom.getArgument(0));
65 } 66 }
66 if (p instanceof AtomicConcept) 67 if(p instanceof AtomicConcept)
67 return Atom.create(generateAuxiliaryRule((AtomicConcept) p), headAtom.getArgument(0)); 68 return Atom.create(generateAuxiliaryRule((AtomicConcept) p), headAtom.getArgument(0));
68 if (p instanceof AtomicRole) 69 if(p instanceof AtomicRole)
69 return Atom.create(generateAuxiliaryRule((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1)); 70 return Atom.create(generateAuxiliaryRule((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1));
70 if (p instanceof Equality || p instanceof AnnotatedEquality) 71 if(p instanceof Equality || p instanceof AnnotatedEquality)
71 return Atom.create(generateAuxiliaryRule(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 72 return Atom.create(generateAuxiliaryRule(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
72 if (p instanceof Inequality) 73 if(p instanceof Inequality)
73 return Atom.create(generateAuxiliaryRule((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); 74 return Atom.create(generateAuxiliaryRule((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1));
74 75
75 return null; 76 return null;
76 } 77 }
77 78
78 private Atom getTrackingAtom(Atom headAtom) { 79 private Atom getTrackingAtom(Atom headAtom) {
79 DLPredicate p = headAtom.getDLPredicate(); 80 DLPredicate p = headAtom.getDLPredicate();
80 if (p instanceof AtLeast) { 81 if (p instanceof AtLeast) {
81 p = Normalisation.toAtLeastConcept((AtLeast) p); 82 p = Normalisation.toAtLeastConcept((AtLeast) p);
82 return Atom.create(getTrackingDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); 83 return Atom.create(getTrackingDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom
84 .getArgument(0));
83 } 85 }
84 if (p instanceof AtomicConcept) 86 if(p instanceof AtomicConcept)
85 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0)); 87 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0));
86 if (p instanceof AtomicRole) 88 if(p instanceof AtomicRole)
87 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); 89 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
88 if (p instanceof Equality || p instanceof AnnotatedEquality) 90 if(p instanceof Equality || p instanceof AnnotatedEquality)
89 return Atom.create(getTrackingDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 91 return Atom.create(getTrackingDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
90 if (p instanceof Inequality) 92 if(p instanceof Inequality)
91 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); 93 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
92 94
93 return null; 95 return null;
94 } 96 }
95 97
96 private Atom getGapAtom(Atom headAtom) { 98 private Atom getGapAtom(Atom headAtom) {
97 DLPredicate p = headAtom.getDLPredicate(); 99 DLPredicate p = headAtom.getDLPredicate();
98 if (p instanceof AtLeast) { 100 if (p instanceof AtLeast) {
99 p = Normalisation.toAtLeastConcept((AtLeast) p); 101 p = Normalisation.toAtLeastConcept((AtLeast) p);
100 return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); 102 return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom
103 .getArgument(0));
101 } 104 }
102 if (p instanceof AtomicConcept) 105 if(p instanceof AtomicConcept)
103 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0)); 106 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
104 if (p instanceof AtomicRole) 107 if(p instanceof AtomicRole)
105 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); 108 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
106 if (p instanceof Equality || p instanceof AnnotatedEquality) 109 if(p instanceof Equality || p instanceof AnnotatedEquality)
107 return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 110 return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
108 if (p instanceof Inequality) 111 if(p instanceof Inequality)
109 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); 112 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
110 if (p instanceof DatatypeRestriction) 113 if (p instanceof DatatypeRestriction)
111 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0)); 114 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
@@ -115,71 +118,71 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
115 118
116 private void encodingDisjunctiveRule(DLClause clause) { 119 private void encodingDisjunctiveRule(DLClause clause) {
117 int headLength = clause.getHeadLength(); 120 int headLength = clause.getHeadLength();
118 121
119 Atom[] auxAtoms = new Atom[headLength]; 122 Atom[] auxAtoms = new Atom[headLength];
120 for (int i = 0; i < headLength; ++i) 123 for (int i = 0; i < headLength; ++i)
121 auxAtoms[i] = getAuxiliaryAtom(clause.getHeadAtom(i)); 124 auxAtoms[i] = getAuxiliaryAtom(clause.getHeadAtom(i));
122 125
123 Atom[] trackingAtoms = new Atom[headLength]; 126 Atom[] trackingAtoms = new Atom[headLength];
124 for (int i = 0; i < headLength; ++i) 127 for (int i = 0; i < headLength; ++i)
125 trackingAtoms[i] = getTrackingAtom(clause.getHeadAtom(i)); 128 trackingAtoms[i] = getTrackingAtom(clause.getHeadAtom(i));
126 129
127 Atom[] gapAtoms = new Atom[headLength]; 130 Atom[] gapAtoms = new Atom[headLength];
128 for (int i = 0; i < headLength; ++i) 131 for (int i = 0; i < headLength; ++i)
129 gapAtoms[i] = getGapAtom(clause.getHeadAtom(i)); 132 gapAtoms[i] = getGapAtom(clause.getHeadAtom(i));
130 133
131 Atom[] bodyAtoms = clause.getBodyAtoms(); 134 Atom[] bodyAtoms = clause.getBodyAtoms();
132 135
133 LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>(); 136 LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>();
134 DLPredicate selected = AtomicConcept.create(getSelectedPredicate()); 137 DLPredicate selected = AtomicConcept.create(getSelectedPredicate());
135 newHeadAtoms.add(Atom.create(selected, getIndividual4GeneralRule(clause))); 138 newHeadAtoms.add(Atom.create(selected, getIndividual4GeneralRule(clause)));
136 139
137 for (Atom atom: bodyAtoms) { 140 for (Atom atom: bodyAtoms) {
138 Atom newAtom = Atom.create( 141 Atom newAtom = Atom.create(
139 getTrackingDLPredicate(atom.getDLPredicate()), 142 getTrackingDLPredicate(atom.getDLPredicate()),
140 DLClauseHelper.getArguments(atom)); 143 DLClauseHelper.getArguments(atom));
141 newHeadAtoms.add(newAtom); 144 newHeadAtoms.add(newAtom);
142 } 145 }
143 146
144 DLClause newClause; 147 DLClause newClause;
145 int index; 148 int index;
146 for (int j = 0; j < headLength; ++j) { 149 for (int j = 0; j < headLength; ++j) {
147 Atom[] newBodyAtoms = new Atom[headLength * 2 + bodyAtoms.length]; 150 Atom[] newBodyAtoms = new Atom[headLength * 2 + bodyAtoms.length];
148 index = 0; 151 index = 0;
149 for (int i = 0; i < headLength; ++i, ++index) 152 for (int i = 0; i < headLength; ++i, ++index)
150 newBodyAtoms[index] = gapAtoms[i]; 153 newBodyAtoms[index] = gapAtoms[i];
151 for (int i = 0; i < headLength; ++i, ++index) 154 for (int i = 0; i < headLength; ++i, ++index)
152 if (i != j) 155 if (i != j)
153 newBodyAtoms[index] = auxAtoms[i]; 156 newBodyAtoms[index] = auxAtoms[i];
154 else 157 else
155 newBodyAtoms[index] = trackingAtoms[i]; 158 newBodyAtoms[index] = trackingAtoms[i];
156 159
157 for (int i = 0; i < bodyAtoms.length; ++i, ++index) 160 for (int i = 0; i < bodyAtoms.length; ++i, ++index)
158 newBodyAtoms[index] = bodyAtoms[i]; 161 newBodyAtoms[index] = bodyAtoms[i];
159 162
160 for (Atom atom: newHeadAtoms) { 163 for (Atom atom: newHeadAtoms) {
161 newClause = DLClause.create(new Atom[] {atom}, newBodyAtoms); 164 newClause = DLClause.create(new Atom[]{atom}, newBodyAtoms);
162 addTrackingClause(newClause); 165 addTrackingClause(newClause);
163 } 166 }
164 } 167 }
165 } 168 }
166 169
167 private void addTrackingClause(DLClause clause) { 170 private void addTrackingClause(DLClause clause) {
168 trackingClauses.add(clause); 171 trackingClauses.add(clause);
169 } 172 }
170 173
171 private void addDisjunctiveRule(DLClause clause) { 174 private void addDisjunctiveRule(DLClause clause) {
172 disjunctiveRules.add(clause); 175 disjunctiveRules.add(clause);
173 } 176 }
174 177
175 private DLPredicate getAuxPredicate(DLPredicate p) { 178 private DLPredicate getAuxPredicate(DLPredicate p) {
176 if (p instanceof AtLeastConcept) { 179 if (p instanceof AtLeastConcept) {
177 StringBuilder builder = new StringBuilder( 180 StringBuilder builder = new StringBuilder(
178 Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p)); 181 Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p));
179 builder.append("_AUXa").append(currentQuery.getQueryID()); 182 builder.append("_AUXa").append(currentQuery.getQueryID());
180 return AtomicConcept.create(builder.toString()); 183 return AtomicConcept.create(builder.toString());
181 } 184 }
182 185
183 return getDLPredicate(p, "_AUXa" + currentQuery.getQueryID()); 186 return getDLPredicate(p, "_AUXa" + currentQuery.getQueryID());
184 } 187 }
185 188
@@ -188,120 +191,118 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
188 } 191 }
189 192
190 private DLPredicate generateAuxiliaryRule(AtLeast p1, boolean withAux) { 193 private DLPredicate generateAuxiliaryRule(AtLeast p1, boolean withAux) {
191 AtLeastConcept p = Normalisation.toAtLeastConcept(p1); 194 AtLeastConcept p = Normalisation.toAtLeastConcept(p1);
192 195
193 int num = p.getNumber(); 196 int num = p.getNumber();
194 Variable[] Ys = new Variable[num]; 197 Variable[] Ys = new Variable[num];
195 if (num > 1) 198 if (num > 1)
196 for (int i = 0; i < num; ++i) 199 for(int i = 0; i < num; ++i)
197 Ys[i] = Variable.create("Y" + (i + 1)); 200 Ys[i] = Variable.create("Y" + (i + 1));
198 else 201 else
199 Ys[0] = Y; 202 Ys[0] = Y;
200 203
201 Collection<Atom> expandedAtom = new LinkedList<Atom>(); 204 Collection<Atom> expandedAtom = new LinkedList<Atom>();
202 Collection<Atom> representativeAtom = new LinkedList<Atom>(); 205 Collection<Atom> representativeAtom = new LinkedList<Atom>();
203 if (p.getOnRole() instanceof AtomicRole) { 206 if (p.getOnRole() instanceof AtomicRole) {
204 AtomicRole r = (AtomicRole) p.getOnRole(); 207 AtomicRole r = (AtomicRole) p.getOnRole();
205 for (int i = 0; i < num; ++i) 208 for(int i = 0; i < num; ++i)
206 expandedAtom.add(Atom.create(r, X, Ys[i])); 209 expandedAtom.add(Atom.create(r, X, Ys[i]));
207 representativeAtom.add(Atom.create(r, X, Ys[0])); 210 representativeAtom.add(Atom.create(r, X, Ys[0]));
208 } 211 }
209 else { 212 else {
210 AtomicRole r = ((InverseRole) p.getOnRole()).getInverseOf(); 213 AtomicRole r = ((InverseRole) p.getOnRole()).getInverseOf();
211 for (int i = 0; i < num; ++i) 214 for(int i = 0; i < num; ++i)
212 expandedAtom.add(Atom.create(r, Ys[i], X)); 215 expandedAtom.add(Atom.create(r, Ys[i], X));
213 representativeAtom.add(Atom.create(r, Ys[0], X)); 216 representativeAtom.add(Atom.create(r, Ys[0], X));
214 } 217 }
215 218
216 if (num > 1) { 219 if (num > 1) {
217 representativeAtom.add(Atom.create(Inequality.INSTANCE, Ys[0], Ys[1])); 220 representativeAtom.add(Atom.create(Inequality.INSTANCE, Ys[0], Ys[1]));
218 } 221 }
219 for (int i = 0; i < num; ++i) 222 for (int i = 0; i < num; ++i)
220 for (int j = i + 1; j < num; ++j) 223 for (int j = i + 1; j < num; ++j)
221 expandedAtom.add(Atom.create(Inequality.INSTANCE, Ys[i], Ys[j])); 224 expandedAtom.add(Atom.create(Inequality.INSTANCE, Ys[i], Ys[j]));
222 225
223 if (!p.getToConcept().equals(AtomicConcept.THING)) { 226 if (!p.getToConcept().equals(AtomicConcept.THING)) {
224 AtomicConcept c; 227 AtomicConcept c;
225 if (p.getToConcept() instanceof AtomicConcept) 228 if(p.getToConcept() instanceof AtomicConcept)
226 c = (AtomicConcept) p.getToConcept(); 229 c = (AtomicConcept) p.getToConcept();
227 else { 230 else {
228 c = OverApproxExist.getNegationConcept(((AtomicNegationConcept) p.getToConcept()).getNegatedAtomicConcept()); 231 c = OverApproxExist.getNegationConcept(((AtomicNegationConcept) p.getToConcept()).getNegatedAtomicConcept());
229 } 232 }
230 for (int i = 0; i < num; ++i) 233 for (int i = 0; i < num; ++i)
231 expandedAtom.add(Atom.create(c, Ys[i])); 234 expandedAtom.add(Atom.create(c, Ys[i]));
232 representativeAtom.add(Atom.create(c, Ys[0])); 235 representativeAtom.add(Atom.create(c, Ys[0]));
233 } 236 }
234 237
235 AtomicConcept ac = AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct(p)); 238 AtomicConcept ac = AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct(p));
236 DLPredicate trackingPredicate = getTrackingDLPredicate(ac); 239 DLPredicate trackingPredicate = getTrackingDLPredicate(ac);
237 DLPredicate gapPredicate = getGapDLPredicate(ac); 240 DLPredicate gapPredicate = getGapDLPredicate(ac);
238 DLPredicate auxPredicate = withAux ? getAuxPredicate(p) : null; 241 DLPredicate auxPredicate = withAux ? getAuxPredicate(p) : null;
239 242
240 for (Atom atom: representativeAtom) { 243 for (Atom atom: representativeAtom) {
241 Atom[] bodyAtoms = new Atom[expandedAtom.size() + 1]; 244 Atom[] bodyAtoms = new Atom[expandedAtom.size() + 1];
242 if (atom.getArity() == 1) 245 if (atom.getArity() == 1)
243 bodyAtoms[0] = Atom.create(getTrackingDLPredicate(atom.getDLPredicate()), atom.getArgument(0)); 246 bodyAtoms[0] = Atom.create(getTrackingDLPredicate(atom.getDLPredicate()), atom.getArgument(0));
244 else 247 else
245 bodyAtoms[0] = Atom.create(getTrackingDLPredicate(atom.getDLPredicate()), atom.getArgument(0), atom.getArgument(1)); 248 bodyAtoms[0] = Atom.create(getTrackingDLPredicate(atom.getDLPredicate()), atom.getArgument(0), atom.getArgument(1));
246 int i = 0; 249 int i = 0;
247 for (Atom bodyAtom: expandedAtom) 250 for (Atom bodyAtom: expandedAtom)
248 bodyAtoms[++i] = bodyAtom; 251 bodyAtoms[++i] = bodyAtom;
249 addTrackingClause(DLClause.create(new Atom[] {Atom.create(trackingPredicate, X)}, bodyAtoms)); 252 addTrackingClause(DLClause.create(new Atom[] {Atom.create(trackingPredicate, X)}, bodyAtoms));
250 253
251 bodyAtoms = new Atom[expandedAtom.size() + 1]; 254 bodyAtoms = new Atom[expandedAtom.size() + 1];
252 if (atom.getArity() == 1) 255 if (atom.getArity() == 1)
253 bodyAtoms[0] = Atom.create(getGapDLPredicate(atom.getDLPredicate()), atom.getArgument(0)); 256 bodyAtoms[0] = Atom.create(getGapDLPredicate(atom.getDLPredicate()), atom.getArgument(0));
254 else 257 else
255 bodyAtoms[0] = Atom.create(getGapDLPredicate(atom.getDLPredicate()), atom.getArgument(0), atom.getArgument(1)); 258 bodyAtoms[0] = Atom.create(getGapDLPredicate(atom.getDLPredicate()), atom.getArgument(0), atom.getArgument(1));
256 i = 0; 259 i = 0;
257 for (Atom bodyAtom: expandedAtom) 260 for (Atom bodyAtom: expandedAtom)
258 bodyAtoms[++i] = bodyAtom; 261 bodyAtoms[++i] = bodyAtom;
259 addTrackingClause(DLClause.create(new Atom[] {Atom.create(gapPredicate, X)}, bodyAtoms)); 262 addTrackingClause(DLClause.create(new Atom[] {Atom.create(gapPredicate, X)}, bodyAtoms));
260 263
261 if (withAux) { 264 if (withAux) {
262 bodyAtoms = new Atom[expandedAtom.size() + 1]; 265 bodyAtoms = new Atom[expandedAtom.size() + 1];
263 bodyAtoms[0] = getAuxiliaryAtom(atom); 266 bodyAtoms[0] = getAuxiliaryAtom(atom);
264 i = 0; 267 i = 0;
265 for (Atom bodyAtom: expandedAtom) 268 for (Atom bodyAtom: expandedAtom)
266 bodyAtoms[++i] = bodyAtom; 269 bodyAtoms[++i] = bodyAtom;
267 addTrackingClause(DLClause.create(new Atom[] {Atom.create(auxPredicate, X)}, bodyAtoms)); 270 addTrackingClause(DLClause.create(new Atom[] {Atom.create(auxPredicate, X)}, bodyAtoms));
268 } 271 }
269 } 272 }
270 273
271 return withAux ? auxPredicate : trackingPredicate; 274 return withAux ? auxPredicate : trackingPredicate;
272 } 275 }
273 276
274 private DLPredicate generateAuxiliaryRule(AtomicRole p) { 277 private DLPredicate generateAuxiliaryRule(AtomicRole p) {
275 if (currentQuery.isBottom()) 278 if(currentQuery.isBottom())
276 return getTrackingDLPredicate(p); 279 return getTrackingDLPredicate(p);
277 280
278 DLPredicate ret = getAuxPredicate(p); 281 DLPredicate ret = getAuxPredicate(p);
279 Atom[] headAtom = new Atom[] {Atom.create(ret, X, Y)}; 282 Atom[] headAtom = new Atom[] {Atom.create(ret, X, Y)};
280 283
281 addTrackingClause( 284 addTrackingClause(
282 DLClause.create(headAtom, new Atom[] {Atom.create(getTrackingDLPredicate(p), X, Y)})); 285 DLClause.create(headAtom, new Atom[]{Atom.create(getTrackingDLPredicate(p), X, Y)}));
283 addTrackingClause( 286 addTrackingClause(
284 DLClause.create(headAtom, new Atom[] {Atom.create(getTrackingBottomDLPredicate(p), X, Y)})); 287 DLClause.create(headAtom, new Atom[]{Atom.create(getTrackingBottomDLPredicate(p), X, Y)}));
285 288
286 return ret; 289 return ret;
287 } 290 }
288
289 private Variable X = Variable.create("X"), Y = Variable.create("Y");
290 291
291 private DLPredicate generateAuxiliaryRule(AtomicConcept p) { 292 private DLPredicate generateAuxiliaryRule(AtomicConcept p) {
292 if (currentQuery.isBottom()) 293 if (currentQuery.isBottom())
293 return getTrackingDLPredicate(p); 294 return getTrackingDLPredicate(p);
294 295
295 DLPredicate ret = getAuxPredicate(p); 296 DLPredicate ret = getAuxPredicate(p);
296 Atom[] headAtom = new Atom[] {Atom.create(ret, X)}; 297 Atom[] headAtom = new Atom[]{Atom.create(ret, X)};
297 addTrackingClause( 298 addTrackingClause(
298 DLClause.create(headAtom, 299 DLClause.create(headAtom,
299 new Atom[] { Atom.create(getTrackingDLPredicate(p), X)})); 300 new Atom[]{Atom.create(getTrackingDLPredicate(p), X)}));
300 addTrackingClause( 301 addTrackingClause(
301 DLClause.create(headAtom, 302 DLClause.create(headAtom,
302 new Atom[] { Atom.create(getTrackingBottomDLPredicate(p), X)})); 303 new Atom[] { Atom.create(getTrackingBottomDLPredicate(p), X)}));
303 304
304 return ret; 305 return ret;
305 } 306 }
306 307
307 private DLPredicate generateAuxiliaryRule(Equality instance) { 308 private DLPredicate generateAuxiliaryRule(Equality instance) {
@@ -309,20 +310,18 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
309 } 310 }
310 311
311 private DLPredicate generateAuxiliaryRule(Inequality instance) { 312 private DLPredicate generateAuxiliaryRule(Inequality instance) {
312 return generateAuxiliaryRule(AtomicRole.create(Namespace.INEQUALITY)); 313 return generateAuxiliaryRule(AtomicRole.create(Namespace.INEQUALITY));
313 } 314 }
314 315
315 @Override 316 @Override
316 public String getTrackingProgram() { 317 public String getTrackingProgram() {
317 StringBuilder sb = getTrackingProgramBody(); 318 StringBuilder sb = getTrackingProgramBody();
318 if (currentQuery.isBottom()) 319 if (currentQuery.isBottom())
319 sb.append(getBottomTrackingProgram()); 320 sb.append(getBottomTrackingProgram());
320 sb.insert(0, MyPrefixes.PAGOdAPrefixes.prefixesText()); 321 sb.insert(0, MyPrefixes.PAGOdAPrefixes.prefixesText());
321 return sb.toString(); 322 return sb.toString();
322 } 323 }
323 324
324 private String bottomTrackingProgram = null;
325
326 private String getBottomTrackingProgram() { 325 private String getBottomTrackingProgram() {
327 if (bottomTrackingProgram != null) return bottomTrackingProgram.replace("_tn", getTrackingPredicate("")); 326 if (bottomTrackingProgram != null) return bottomTrackingProgram.replace("_tn", getTrackingPredicate(""));
328 327
@@ -350,7 +349,7 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
350// for (Atom tAtom: clause.getHeadAtoms()) { 349// for (Atom tAtom: clause.getHeadAtoms()) {
351// for (int i = 0; i < tAtom.getArity(); ++i) 350// for (int i = 0; i < tAtom.getArity(); ++i)
352// if ((t = tAtom.getArgument(i)) instanceof Individual) 351// if ((t = tAtom.getArgument(i)) instanceof Individual)
353// if (((Individual) t).getIRI().startsWith(OverApproxExist.skolemisedIndividualPrefix)) 352// if (((Individual) t).getIRI().startsWith(OverApproxExist.SKOLEMISED_INDIVIDUAL_PREFIX))
354// clause = program.getCorrespondingClause(clause); 353// clause = program.getCorrespondingClause(clause);
355// } 354// }
356 355