aboutsummaryrefslogtreecommitdiff
path: root/src/main/java/uk/ac/ox/cs/pagoda/rules
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/main/java/uk/ac/ox/cs/pagoda/rules
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/main/java/uk/ac/ox/cs/pagoda/rules')
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java106
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/DatalogProgram.java81
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java20
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/EqualityAxiomatiser.java91
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java26
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java20
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java75
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/GeneralProgram.java50
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/IncrementalProgram.java14
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java238
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/Program.java384
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java47
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/UpperProgram.java12
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java42
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java146
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java24
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java100
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java224
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java139
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java19
-rw-r--r--src/main/java/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java100
21 files changed, 1958 insertions, 0 deletions
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java
new file mode 100644
index 0000000..acbf354
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java
@@ -0,0 +1,106 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.semanticweb.HermiT.model.DLClause;
4import org.semanticweb.owlapi.model.OWLAxiom;
5import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom;
6import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom;
7import uk.ac.ox.cs.pagoda.owl.OWLHelper;
8import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
9
10import java.util.*;
11
12public abstract class ApproxProgram extends Program {
13
14 protected Approximator m_approx = null;
15 /**
16 * mapping from over-approximated DLClauses to DLClauses from the original ontology
17 */
18 Map<DLClause, Object> correspondence = new HashMap<DLClause, Object>();
19
20 protected ApproxProgram() { initApproximator(); }
21
22 protected abstract void initApproximator();
23
24 @Override
25 public void transform() {
26 super.transform();
27 Iterator<DLClause> iterClause = transitiveClauses.iterator();
28 for (Iterator<OWLTransitiveObjectPropertyAxiom> iterAxiom = transitiveAxioms.iterator(); iterAxiom.hasNext(); )
29 addCorrespondence(iterClause.next(), iterAxiom.next());
30
31 iterClause = subPropChainClauses.iterator();
32 for (Iterator<OWLSubPropertyChainOfAxiom> iterAxiom = subPropChainAxioms.iterator(); iterAxiom.hasNext(); )
33 addCorrespondence(iterClause.next(), iterAxiom.next());
34 }
35
36 @Override
37 public Collection<DLClause> convert2Clauses(DLClause clause) {
38 Collection<DLClause> ret = botStrategy.process(m_approx.convert(clause, clause));
39// OWLAxiom correspondingAxiom = OWLHelper.getOWLAxiom(ontology, clause);
40 for (DLClause newClause: ret) {
41 addCorrespondence(newClause, clause);
42// addCorrespondence(newClause, correspondingAxiom);
43 }
44 return ret;
45 }
46
47 private void addCorrespondence(DLClause newClause, Object corresponding) {
48 Object object;
49 if ((object = correspondence.get(newClause)) != null) {
50 if (object.equals(corresponding))
51 return ;
52
53 if (object instanceof DLClause) {
54 DLClause c1 = (DLClause) object;
55 if (c1.getHeadLength() == 1) return ;
56 DLClause c2 = (DLClause) corresponding;
57 if (c2.getHeadLength() == 1) {
58 correspondence.put(newClause, c2);
59 return ;
60 }
61 ClauseSet list = new ClauseSet(c1, c2);
62 correspondence.put(newClause, list);
63 }
64 else if (object instanceof ClauseSet){
65 ClauseSet list = (ClauseSet) object;
66 list.add((DLClause) corresponding);
67 }
68 }
69 correspondence.put(newClause, corresponding);
70 }
71
72 public OWLAxiom getEquivalentAxiom(DLClause clause) {
73 Object obj = correspondence.get(clause);
74 while (obj != null && obj instanceof DLClause && !obj.equals(clause) && correspondence.containsKey(obj))
75 obj = correspondence.get(clause);
76 if (obj instanceof OWLAxiom)
77 return (OWLAxiom) obj;
78 else if (obj != null)
79 return OWLHelper.getOWLAxiom(ontology, (DLClause) obj);
80 else {
81 return OWLHelper.getOWLAxiom(ontology, clause);
82 }
83 }
84
85 public DLClause getCorrespondingClause(DLClause clause) {
86 Object obj = correspondence.get(clause);
87 if (obj instanceof DLClause)
88 return (DLClause) obj;
89 else
90 return clause;
91 }
92}
93
94class ClauseSet extends HashSet<DLClause> {
95
96 /**
97 *
98 */
99 private static final long serialVersionUID = 1L;
100
101 public ClauseSet(DLClause first, DLClause second) {
102 add(first);
103 add(second);
104 }
105
106} \ No newline at end of file
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/DatalogProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/DatalogProgram.java
new file mode 100644
index 0000000..e2a171d
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/DatalogProgram.java
@@ -0,0 +1,81 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.semanticweb.owlapi.model.OWLOntology;
4import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
5import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom;
6import uk.ac.ox.cs.pagoda.util.disposable.Disposable;
7import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
8
9import java.io.InputStream;
10
11public class DatalogProgram extends Disposable {
12
13 UpperDatalogProgram upperProgram = new UpperDatalogProgram();
14 LowerDatalogProgram lowerProgram;
15 GeneralProgram program = new GeneralProgram();
16
17 BottomStrategy upperBottom;
18
19 public DatalogProgram(InputStream inputStream) {
20 lowerProgram = new LowerDatalogProgram();
21
22 upperProgram.load(inputStream, upperBottom = new UpperUnaryBottom());
23 lowerProgram.clone(upperProgram);
24 program.clone(upperProgram);
25
26 upperProgram.transform();
27 lowerProgram.transform();
28 program.transform();
29
30 program.buildDependencyGraph();
31 lowerProgram.dependencyGraph = upperProgram.buildDependencyGraph();
32 }
33
34 public DatalogProgram(OWLOntology o) {
35 lowerProgram = new LowerDatalogProgram();
36
37 upperProgram.load(o, upperBottom = new UpperUnaryBottom());
38// upperProgram.load(o, upperBottom = new UnaryBottom());
39 lowerProgram.clone(upperProgram);
40 program.clone(upperProgram);
41// program.botStrategy = new UnaryBottom();
42
43 upperProgram.transform();
44 lowerProgram.transform();
45 program.transform();
46
47 program.buildDependencyGraph();
48 lowerProgram.dependencyGraph = upperProgram.buildDependencyGraph();
49 }
50
51 public LowerDatalogProgram getLower() {
52 if(isDisposed()) throw new DisposedException();
53 return lowerProgram;
54 }
55
56 public UpperDatalogProgram getUpper() {
57 if(isDisposed()) throw new DisposedException();
58 return upperProgram;
59 }
60
61 public GeneralProgram getGeneral() {
62 if(isDisposed()) throw new DisposedException();
63 return program;
64 }
65
66 public String getAdditionalDataFile() {
67 if(isDisposed()) throw new DisposedException();
68 return upperProgram.getAdditionalDataFile();
69 }
70
71 public BottomStrategy getUpperBottomStrategy() {
72 if(isDisposed()) throw new DisposedException();
73 return upperBottom;
74 }
75
76 @Override
77 public void dispose() {
78 super.dispose();
79 if(upperProgram != null) upperProgram.deleteABoxTurtleFile();
80 }
81}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java
new file mode 100644
index 0000000..d50c2d4
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java
@@ -0,0 +1,20 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
4
5public class DisjunctiveProgram extends UpperProgram {
6
7 @Override
8 protected void initApproximator() {
9 m_approx = new OverApproxExist();
10 }
11
12// @Override
13// public String getDirectory() {
14// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "disjunctiveRules");
15// if (!dir.exists())
16// dir.mkdirs();
17// return dir.getPath();
18// }
19
20}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/EqualityAxiomatiser.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/EqualityAxiomatiser.java
new file mode 100644
index 0000000..81b8a01
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/EqualityAxiomatiser.java
@@ -0,0 +1,91 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.io.BufferedWriter;
4import java.io.FileOutputStream;
5import java.io.IOException;
6import java.io.OutputStreamWriter;
7
8import org.semanticweb.owlapi.apibinding.OWLManager;
9import org.semanticweb.owlapi.model.OWLClass;
10import org.semanticweb.owlapi.model.OWLObjectProperty;
11import org.semanticweb.owlapi.model.OWLOntology;
12import uk.ac.ox.cs.pagoda.owl.OWLHelper;
13import uk.ac.ox.cs.pagoda.util.Namespace;
14import uk.ac.ox.cs.pagoda.util.Utility;
15
16public class EqualityAxiomatiser {
17
18 OWLOntology ontology;
19
20 public EqualityAxiomatiser(String fileName) {
21 ontology = OWLHelper.loadOntology(OWLManager.createOWLOntologyManager(), fileName);
22 }
23
24 public EqualityAxiomatiser(OWLOntology ontology) {
25 this.ontology = ontology;
26 }
27
28 public static void main(String[] args) throws IOException {
29 if (args.length == 0) {
30 args = new String[1];
31 args[0] = "../uobmGenerator/ontologies/2rl/univ-bench-dl-TBox.owl";
32 }
33
34 EqualityAxiomatiser axiomatiser;
35 for (String fileName: args) {
36 axiomatiser = new EqualityAxiomatiser(fileName);
37 String outputFileName = fileName.replace(".owl", "-axiomatised.rule");
38 BufferedWriter writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(outputFileName)));
39 writer.write(axiomatiser.getRuleTexts());
40 writer.close();
41 }
42 }
43
44 public String getRuleTexts() {
45 StringBuffer buf = new StringBuffer();
46// buf.append(reflexivity()).append(Utility.LINE_SEPARATOR);
47 buf.append(symmetry()).append(Utility.LINE_SEPARATOR);
48 buf.append(transitivity()).append(Utility.LINE_SEPARATOR);
49
50 for (OWLObjectProperty p: ontology.getObjectPropertiesInSignature(true))
51 buf.append(addingEqualities4Properties(OWLHelper.addAngles(p.getIRI().toString()))).append(Utility.LINE_SEPARATOR);
52
53 for (OWLClass c: ontology.getClassesInSignature(true))
54 buf.append(addingEqualities4Class(OWLHelper.addAngles(c.getIRI().toString()))).append(Utility.LINE_SEPARATOR);
55
56 return buf.toString();
57 }
58
59 private static String transitivity() {
60 StringBuffer buffer = new StringBuffer();
61 buffer.append(Namespace.EQUALITY_QUOTED).append("(?Y0,?Y2) :- ").append(Namespace.EQUALITY_QUOTED ).append("(?Y0,?Y1), ").append(Namespace.EQUALITY_QUOTED ).append("(?Y1,?Y2) .");
62 return buffer.toString();
63 }
64
65 private static String symmetry() {
66 StringBuffer buffer = new StringBuffer();
67 buffer.append(Namespace.EQUALITY_QUOTED ).append("(?Y1,?Y0) :- ").append(Namespace.EQUALITY_QUOTED ).append("(?Y0,?Y1) .");
68 return buffer.toString();
69 }
70
71 @SuppressWarnings("unused")
72 private static String reflexivity() {
73 StringBuffer buffer = new StringBuffer();
74 buffer.append(Namespace.EQUALITY_QUOTED ).append("(?Y0,?Y0) :- .");
75 return buffer.toString();
76 }
77
78 private static String addingEqualities4Properties(String property) {
79 StringBuffer buffer = new StringBuffer();
80 buffer.append(property).append("(?Y2,?Y1) :- ").append(property).append("(?Y0,?Y1), ").append(Namespace.EQUALITY_QUOTED ).append("(?Y0,?Y2) .\n");
81 buffer.append(property).append("(?Y0,?Y2) :- ").append(property).append("(?Y0,?Y1), ").append(Namespace.EQUALITY_QUOTED ).append("(?Y1,?Y2) .");
82 return buffer.toString();
83 }
84
85 private static String addingEqualities4Class(String clazz) {
86 StringBuffer buffer = new StringBuffer();
87 buffer.append(clazz).append("(?Y1) :- ").append(clazz).append("(?Y0), ").append(Namespace.EQUALITY_QUOTED ).append("(?Y0,?Y1) .");
88 return buffer.toString();
89 }
90
91}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
new file mode 100644
index 0000000..a7afa2e
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
@@ -0,0 +1,26 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.semanticweb.HermiT.model.DLClause;
4import org.semanticweb.HermiT.model.Individual;
5import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
6import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator;
7import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
8
9import java.util.Collection;
10
11/**
12 * A wrapper for <tt>OverApproxExist</tt>.
13 * */
14public class ExistConstantApproximator implements TupleDependentApproximator {
15
16 private final OverApproxExist overApproxExist;
17
18 public ExistConstantApproximator() {
19 overApproxExist = new OverApproxExist();
20 }
21
22 @Override
23 public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
24 return overApproxExist.convert(clause, originalClause);
25 }
26}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java
new file mode 100644
index 0000000..e825917
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java
@@ -0,0 +1,20 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxDisj;
4
5public class ExistentialProgram extends UpperProgram {
6
7// @Override
8// public String getDirectory() {
9// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "existential");
10// if (!dir.exists())
11// dir.mkdirs();
12// return dir.getPath();
13// }
14
15 @Override
16 protected void initApproximator() {
17 m_approx = new OverApproxDisj();
18 }
19
20}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java
new file mode 100644
index 0000000..2098f73
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java
@@ -0,0 +1,75 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.semanticweb.HermiT.model.*;
4import org.semanticweb.owlapi.model.OWLObjectProperty;
5import org.semanticweb.owlapi.model.OWLOntology;
6import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
7import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
8import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
9
10import java.util.Collection;
11import java.util.HashSet;
12import java.util.LinkedList;
13import java.util.Set;
14
15public class ExistentialToDisjunctive extends UpperProgram {
16
17 Set<String> inverseFuncProperties = new HashSet<String>();
18
19 @Override
20 public void load(OWLOntology o, BottomStrategy bottomStrategy) {
21 super.load(o, bottomStrategy);
22 for (OWLObjectProperty prop: ontology.getObjectPropertiesInSignature(true))
23 if (!(ontology.getInverseFunctionalObjectPropertyAxioms(prop).isEmpty()))
24 inverseFuncProperties.add(prop.getIRI().toString());
25 ((RefinedOverApproxExist) m_approx).setInverseFuncProps(inverseFuncProperties);
26 }
27
28 @Override
29 protected void initApproximator() {
30 m_approx = new RefinedOverApproxExist();
31 }
32
33}
34
35class RefinedOverApproxExist implements Approximator {
36
37 Approximator approxExist = new OverApproxExist();
38 Set<String> inverseFuncProperties;
39
40 public void setInverseFuncProps(Set<String> set) {
41 inverseFuncProperties = set;
42 }
43
44 @Override
45 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
46 DLPredicate p;
47 Collection<Atom> newHeadAtoms = new LinkedList<Atom>();
48 for (Atom headAtom: clause.getHeadAtoms())
49 newHeadAtoms.add(headAtom);
50
51 for (Atom headAtom: clause.getHeadAtoms()) {
52 p = headAtom.getDLPredicate();
53 if (isAtLeastOneOnInverseFuncProperties(p))
54 newHeadAtoms.add(headAtom);
55 }
56
57 if (newHeadAtoms.size() > clause.getHeadLength())
58 clause = DLClause.create(newHeadAtoms.toArray(new Atom[0]), clause.getBodyAtoms());
59
60 return approxExist.convert(clause, clause);
61 }
62
63 private boolean isAtLeastOneOnInverseFuncProperties(DLPredicate predicate) {
64 if (!(predicate instanceof AtLeastConcept))
65 return false;
66 AtLeastConcept atLeast = (AtLeastConcept) predicate;
67 if (!(atLeast.getOnRole() instanceof AtomicRole))
68 return false;
69
70 return atLeast.getNumber() == 1 && inverseFuncProperties.contains(((AtomicRole) atLeast.getOnRole()).getIRI());
71 }
72
73
74}
75
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/GeneralProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/GeneralProgram.java
new file mode 100644
index 0000000..e390a29
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/GeneralProgram.java
@@ -0,0 +1,50 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.apache.commons.io.FilenameUtils;
4import org.semanticweb.HermiT.model.DLClause;
5import org.semanticweb.owlapi.model.OWLOntology;
6import uk.ac.ox.cs.pagoda.constraints.UnaryBottom;
7
8import java.util.Collection;
9import java.util.Collections;
10import java.util.Set;
11
12public class GeneralProgram extends Program {
13
14 public GeneralProgram(Set<DLClause> relevantClauses, OWLOntology relevantOntology) {
15 ontology = relevantOntology;
16
17 ontologyDirectory = null;
18// dlOntology = null;
19 botStrategy = new UnaryBottom();
20
21 clauses = botStrategy.process(relevantClauses);
22 }
23
24 public GeneralProgram() {}
25
26 public Collection<DLClause> convert2Clauses(DLClause clause) {
27 return botStrategy.process(Collections.singleton(clause));
28 }
29
30 @Override
31 public String getOutputPath() {
32 return FilenameUtils.concat(getDirectory(), "rules.dlog");
33 }
34
35// @Override
36// public String getDirectory() {
37// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "general");
38// if (!dir.exists())
39// dir.mkdirs();
40// return dir.getPath();
41// }
42
43 public boolean isHorn() {
44 for (DLClause clause: clauses)
45 if (clause.getHeadLength() > 1)
46 return false;
47 return true;
48 }
49
50}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/IncrementalProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/IncrementalProgram.java
new file mode 100644
index 0000000..339738a
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/IncrementalProgram.java
@@ -0,0 +1,14 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4
5import org.semanticweb.HermiT.model.DLClause;
6import org.semanticweb.owlapi.model.OWLOntology;
7
8public interface IncrementalProgram {
9
10 public OWLOntology getOntology();
11
12 public void enrich(Collection<DLClause> delta);
13
14}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java
new file mode 100644
index 0000000..a2676e8
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java
@@ -0,0 +1,238 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.apache.commons.io.FilenameUtils;
4import org.semanticweb.HermiT.Reasoner;
5import org.semanticweb.HermiT.model.*;
6import org.semanticweb.owlapi.model.*;
7import org.semanticweb.owlapi.reasoner.Node;
8import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
9import uk.ac.ox.cs.pagoda.constraints.NullaryBottom;
10import uk.ac.ox.cs.pagoda.constraints.UnaryBottom;
11import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom;
12import uk.ac.ox.cs.pagoda.multistage.Normalisation;
13import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication;
14import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
15import uk.ac.ox.cs.pagoda.util.Timer;
16import uk.ac.ox.cs.pagoda.util.Utility;
17
18import java.util.Collection;
19import java.util.Iterator;
20import java.util.LinkedList;
21import java.util.Set;
22
23public class LowerDatalogProgram extends ApproxProgram implements IncrementalProgram {
24
25 boolean m_toClassify;
26
27 public LowerDatalogProgram() {
28 m_toClassify = true;
29 }
30
31 public LowerDatalogProgram(boolean toClassify) {
32 m_toClassify = toClassify; // false; //
33 }
34
35 void clone(Program program) {
36 super.clone(program);
37 if (botStrategy instanceof UpperUnaryBottom)
38 botStrategy = new UnaryBottom();
39 }
40
41
42 // TODO -RULE- filter out unsafe rules
43 @Override
44 public void transform() {
45 if (m_toClassify) {
46 ClassifyThread thread = new ClassifyThread(this);
47 thread.start();
48 super.transform();
49 try {
50 thread.join(5000);
51 } catch (InterruptedException e) {
52 return ;
53 }
54 if (!thread.isAlive()) thread.dispose();
55 else thread.interrupt();
56 }
57 else
58 super.transform();
59
60 Normalisation norm = new Normalisation(dlClauses, ontology, new NullaryBottom());
61 BottomStrategy tBottom = new NullaryBottom();
62 norm.process();
63 for (DLClause nClause: norm.getNormlisedClauses()) {
64 if (nClause.getHeadLength() != 1)
65 for (DLClause newClause: RestrictedApplication.addAdditionalDatalogRules(nClause, tBottom, norm)) {
66// System.out.println(newClause);
67 if (newClause.getHeadAtom(0).getDLPredicate() instanceof AtomicConcept || newClause.getHeadAtom(0).getDLPredicate() instanceof AtomicRole) {
68// System.out.println(newClause);
69 clauses.add(newClause);
70 }
71 }
72
73 if (nClause.getHeadLength() == 1 && (nClause.getHeadAtom(0).getDLPredicate() instanceof AtomicConcept || nClause.getHeadAtom(0).getDLPredicate() instanceof AtomicRole) && clauses.add(nClause)) {
74// System.out.println(nClause);
75 }
76 }
77 }
78
79 @Override
80 public String getOutputPath() {
81 return FilenameUtils.concat(getDirectory(), "lower.dlog");
82 }
83
84// @Override
85// public String getDirectory() {
86// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "datalog");
87// if (!dir.exists())
88// dir.mkdirs();
89// return dir.getPath();
90// }
91
92 @Override
93 public void enrich(Collection<DLClause> delta) {
94 synchronized (clauses) {
95 Iterator<DLClause> iter = delta.iterator();
96 while (iter.hasNext())
97 clauses.add(iter.next());
98 }
99 }
100
101 @Override
102 public String toString() {
103 String text;
104 synchronized (clauses) {
105 text = super.toString();
106 }
107 return text;
108 }
109
110 @Override
111 protected void initApproximator() {
112 m_approx = new IgnoreBoth();
113 }
114
115 private class IgnoreBoth implements Approximator {
116
117 @Override
118 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
119 Collection<DLClause> ret = new LinkedList<DLClause>();
120
121 if (clause.getHeadLength() > 1) return ret;
122
123 if (clause.getHeadLength() > 0) {
124 DLPredicate predicate = clause.getHeadAtom(0).getDLPredicate();
125
126 if (predicate instanceof AtLeast) return ret;
127 }
128
129 ret.add(clause);
130 return ret;
131 }
132 }
133
134}
135
136class ClassifyThread extends Thread {
137
138 IncrementalProgram m_program;
139 Collection<DLClause> clauses = new LinkedList<DLClause>();
140
141 Variable X = Variable.create("X"), Y = Variable.create("Y");
142 Reasoner hermitReasoner;
143 OWLOntology ontology;
144 ClassifyThread(IncrementalProgram program) {
145 m_program = program;
146 }
147
148 @Override
149 public void run() {
150 ontology = m_program.getOntology();
151 try {
152 hermitReasoner = new Reasoner(ontology);
153 Timer t = new Timer();
154 hermitReasoner.classifyClasses();
155 Utility.logInfo("HermiT classification done: " + t.duration());
156 } catch (Exception e) {
157// e.printStackTrace();
158 Utility.logInfo("HermiT cannot classify the ontology.");
159 hermitReasoner = null;
160 }
161 }
162
163 public void dispose() {
164 if (hermitReasoner == null)
165 return ;
166 Set<OWLClass> classes;
167 OWLClass lastClass = null, currentClass;
168 for (OWLClass subClass: ontology.getClassesInSignature()) {
169 Node<OWLClass> node = hermitReasoner.getEquivalentClasses(subClass);
170 if (!subClass.equals(node.getRepresentativeElement())) continue;
171
172 classes = node.getEntities();
173 lastClass = subClass;
174 for (Iterator<OWLClass> iter = classes.iterator(); iter.hasNext(); ) {
175 currentClass = iter.next();
176 if (currentClass.equals(subClass)) continue;
177 addClause(lastClass, currentClass);
178 lastClass = currentClass;
179 }
180 addClause(lastClass, subClass);
181
182 for (Node<OWLClass> tNode: hermitReasoner.getSuperClasses(subClass, true)) {
183 OWLClass superClass = tNode.getRepresentativeElement();
184 addClause(subClass, superClass);
185 }
186 }
187
188 Set<OWLObjectPropertyExpression> properties;
189 OWLObjectPropertyExpression lastProperty, currentProperty;
190 for (OWLObjectProperty subProperty: ontology.getObjectPropertiesInSignature()) {
191 Node<OWLObjectPropertyExpression> node = hermitReasoner.getEquivalentObjectProperties(subProperty);
192 if (!subProperty.equals(node.getRepresentativeElement())) continue;
193
194 properties = node.getEntities();
195 lastProperty = subProperty;
196 for (Iterator<OWLObjectPropertyExpression> iter = properties.iterator(); iter.hasNext(); ) {
197 currentProperty = iter.next();
198 if (currentProperty.equals(subProperty)) continue;
199 addClause(lastProperty, currentProperty);
200 lastProperty = currentProperty;
201 }
202 addClause(lastProperty, subProperty);
203
204 for (Node<OWLObjectPropertyExpression> tNode: hermitReasoner.getSuperObjectProperties(subProperty, true)) {
205 OWLObjectPropertyExpression superProperty = tNode.getRepresentativeElement();
206 addClause(subProperty, superProperty);
207 }
208 }
209
210 m_program.enrich(clauses);
211 Utility.logInfo("classification done and enriched lower bound rules.");
212 }
213
214
215 private void addClause(OWLObjectPropertyExpression subProperty, OWLObjectPropertyExpression superProperty) {
216 if (subProperty.equals(superProperty)) return ;
217 if (superProperty.toString().equals("owl:topObjectProperty")) return ;
218 clauses.add(DLClause.create(new Atom[] { getAtom(superProperty) }, new Atom[] { getAtom(subProperty) }));
219 }
220
221 private Atom getAtom(OWLObjectPropertyExpression p) {
222 if (p instanceof OWLObjectInverseOf)
223 return Atom.create(AtomicRole.create(((OWLObjectProperty) ((OWLObjectInverseOf) p).getInverse()).toStringID()), Y, X);
224
225 return Atom.create(AtomicRole.create(((OWLObjectProperty) p).toStringID()), X, Y);
226 }
227
228 private void addClause(OWLClass subClass, OWLClass superClass) {
229 if (subClass.equals(superClass)) return ;
230 if (subClass.toString().equals("owl:Nothing")) return ;
231 if (superClass.toString().equals("owl:Thing")) return ;
232 clauses.add(DLClause.create(new Atom[] { getAtom(superClass) }, new Atom[] { getAtom(subClass) }));
233 }
234
235 private Atom getAtom(OWLClass c) {
236 return Atom.create(AtomicConcept.create(c.toStringID()), X);
237 }
238} \ No newline at end of file
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/Program.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/Program.java
new file mode 100644
index 0000000..de06f52
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/Program.java
@@ -0,0 +1,384 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.apache.commons.io.FilenameUtils;
4import org.semanticweb.HermiT.Configuration;
5import org.semanticweb.HermiT.model.*;
6import org.semanticweb.HermiT.structural.OWLClausification;
7import org.semanticweb.owlapi.apibinding.OWLManager;
8import org.semanticweb.owlapi.model.*;
9import org.semanticweb.simpleETL.SimpleETL;
10import uk.ac.ox.cs.pagoda.MyPrefixes;
11import uk.ac.ox.cs.pagoda.approx.KnowledgeBase;
12import uk.ac.ox.cs.pagoda.approx.RLPlusOntology;
13import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
14import uk.ac.ox.cs.pagoda.constraints.NullaryBottom;
15import uk.ac.ox.cs.pagoda.constraints.PredicateDependency;
16import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
17import uk.ac.ox.cs.pagoda.hermit.RuleHelper;
18import uk.ac.ox.cs.pagoda.owl.OWLHelper;
19import uk.ac.ox.cs.pagoda.util.Utility;
20
21import java.io.*;
22import java.util.*;
23
24public abstract class Program implements KnowledgeBase {
25
26 protected String ontologyDirectory = null;
27 protected OWLOntology ontology;
28// protected DLOntology dlOntology;
29 protected Set<DLClause> dlClauses = new HashSet<>();
30 protected Set<Atom> positiveFacts = new HashSet<>();
31 protected BottomStrategy botStrategy;
32 protected Collection<DLClause> clauses = new HashSet<DLClause>();
33// protected Set<DLClause> used = new HashSet<DLClause>();
34protected PredicateDependency dependencyGraph;
35 protected LinkedList<OWLTransitiveObjectPropertyAxiom> transitiveAxioms;
36 protected LinkedList<DLClause> transitiveClauses;
37 protected LinkedList<OWLSubPropertyChainOfAxiom> subPropChainAxioms;
38 protected LinkedList<DLClause> subPropChainClauses;
39 private String additionalDataFile = null;
40
41 public static String toString(Collection<DLClause> clauses) {
42 StringBuilder sb = new StringBuilder(DLClauseHelper.toString(clauses));
43 sb.insert(0, MyPrefixes.PAGOdAPrefixes.prefixesText());
44 return sb.toString();
45 }
46
47 public void load(InputStream rules, BottomStrategy botStrategy) {
48// this.botStrategy = botStrategy;
49// // fake instantiation
50 try {
51 load(OWLManager.createOWLOntologyManager().createOntology(), botStrategy);
52 } catch (OWLOntologyCreationException e) {
53 e.printStackTrace();
54 }
55
56 try(BufferedReader br = new BufferedReader(new InputStreamReader(rules))) {
57 String line;
58 while((line = br.readLine()) != null)
59 dlClauses.add(RuleHelper.parseClause(line));
60 } catch (IOException e) {
61 e.printStackTrace();
62 }
63 }
64
65 public void load(OWLOntology o, BottomStrategy botStrategy) {
66 this.botStrategy = botStrategy;
67 RLPlusOntology owlOntology = new RLPlusOntology();
68 owlOntology.load(o, new NullaryBottom());
69 owlOntology.simplify();
70
71 ontology = owlOntology.getTBox();
72// String ontologyPath = OWLHelper.getOntologyPath(ontology);
73// ontologyDirectory = ontologyPath.substring(0, ontologyPath.lastIndexOf(Utility.JAVA_FILE_SEPARATOR));
74 String ontologyPath = ontology.getOWLOntologyManager().getOntologyDocumentIRI(ontology).toURI().getPath();
75 ontologyDirectory = FilenameUtils.getFullPath(ontologyPath);
76 clausify();
77
78 String aboxOWLFile = owlOntology.getABoxPath();
79 OWLOntology abox = OWLHelper.loadOntology(aboxOWLFile);
80 OWLOntologyManager manager = abox.getOWLOntologyManager();
81 OWLAxiom axiom;
82 for (Atom atom: positiveFacts) {
83 if ((axiom = OWLHelper.getABoxAssertion(manager.getOWLDataFactory(), atom)) != null)
84 manager.addAxiom(abox, axiom);
85 }
86
87 try {
88 FileOutputStream out = new FileOutputStream(aboxOWLFile);
89 manager.saveOntology(abox, out);
90 out.close();
91 } catch(IOException | OWLOntologyStorageException e) {
92 e.printStackTrace();
93 System.exit(1);
94 }
95
96 if (!abox.isEmpty()) {
97 SimpleETL rewriter = new SimpleETL(owlOntology.getOntologyIRI(), aboxOWLFile);
98 try {
99 rewriter.rewrite();
100 } catch (Exception e) {
101 e.printStackTrace();
102 }
103 additionalDataFile = rewriter.getExportedFile();
104 new File(aboxOWLFile).delete();
105 }
106
107 }
108
109 public String getAdditionalDataFile() {
110 return additionalDataFile;
111 }
112
113 @Override
114 public void transform() {
115 for(DLClause dlClause : dlClauses) {
116 DLClause simplifiedDLClause = DLClauseHelper.removeNominalConcept(dlClause);
117 simplifiedDLClause = removeAuxiliaryBodyAtoms(simplifiedDLClause);
118 simplifiedDLClause = DLClauseHelper.replaceWithDataValue(simplifiedDLClause);
119 convert(simplifiedDLClause);
120 }
121
122 addingTransitiveAxioms();
123 addingSubPropertyChainAxioms();
124
125 Collection<DLClause> botRelated = new LinkedList<DLClause>();
126 Variable X = Variable.create("X");
127 botRelated.add(DLClause.create(new Atom[0], new Atom[]{Atom.create(Inequality.INSTANCE, X, X)}));
128 clauses.addAll(botStrategy.process(botRelated));
129
130 if(this instanceof GeneralProgram)
131 Utility.logDebug("The number of rules: " + (clauses.size() - 1));
132 }
133
134 @Override
135 public void save() {
136 try {
137 BufferedWriter ruleWriter = new BufferedWriter(new OutputStreamWriter(
138 new FileOutputStream(getOutputPath())));
139 ruleWriter.write(toString());
140 ruleWriter.close();
141 } catch(IOException e) {
142 e.printStackTrace();
143 }
144 Utility.logInfo("The rules are saved in " + getOutputPath() + ".");
145 }
146
147 @Override
148 public String toString() {
149 return toString(clauses);
150 }
151
152 public final void convert(DLClause clause) {
153 Collection<DLClause> tempClauses = convert2Clauses(clause);
154 clauses.addAll(tempClauses);
155 }
156
157 public abstract Collection<DLClause> convert2Clauses(DLClause clause);
158
159 public abstract String getOutputPath();
160
161 public OWLOntology getOntology() {
162 return ontology;
163 }
164
165 public Collection<DLClause> getClauses() {
166 return clauses;
167 }
168
169 public Collection<DLClause> getClauses(DLClause queryClause) {
170// if (true) return new HashSet<DLClause>(clauses);
171 Set<DLPredicate> predicates = new HashSet<DLPredicate>();
172 predicates.addAll(dependencyGraph.collectPredicate(queryClause.getBodyAtoms()));
173
174 Set<DLPredicate> dependence = new HashSet<DLPredicate>();
175 for(DLPredicate predicate : predicates)
176 dependence.addAll(dependencyGraph.getAncesters(predicate));
177
178 Collection<DLClause> relevantClauses = new LinkedList<DLClause>();
179 for(DLClause clause : clauses) {
180 if(relevant(clause, dependence))
181 relevantClauses.add(clause);
182
183 }
184 return relevantClauses;
185 }
186
187 public PredicateDependency buildDependencyGraph() {
188 if(dependencyGraph == null)
189 return dependencyGraph = new PredicateDependency(clauses);
190 else
191 return dependencyGraph;
192 }
193
194 public void getDependencyGraph(PredicateDependency g) {
195 dependencyGraph = g;
196 }
197
198 public final String getDirectory() {
199 return Utility.getGlobalTempDirAbsolutePath();
200 }
201
202 public void deleteABoxTurtleFile() {
203 if(additionalDataFile != null)
204 new File(additionalDataFile).delete();
205 }
206
207 /**
208 * clone all information of another program after load()
209 *
210 * @param program
211 */
212 void clone(Program program) {
213 this.ontologyDirectory = program.ontologyDirectory;
214 this.ontology = program.ontology;
215// this.dlOntology = program.dlOntology;
216 this.dlClauses = program.dlClauses;
217 this.positiveFacts = program.positiveFacts;
218 this.botStrategy = program.botStrategy;
219 this.additionalDataFile = program.additionalDataFile;
220 this.transitiveAxioms = program.transitiveAxioms;
221 this.transitiveClauses = program.transitiveClauses;
222 this.subPropChainAxioms = program.subPropChainAxioms;
223 this.subPropChainClauses = program.subPropChainClauses;
224 }
225
226 private void clausify() {
227 Configuration conf = new Configuration();
228 OWLClausification clausifier = new OWLClausification(conf);
229 OWLOntology filteredOntology = null;
230 OWLOntologyManager manager = ontology.getOWLOntologyManager();
231 try {
232 filteredOntology = manager.createOntology();
233 } catch(OWLOntologyCreationException e) {
234 e.printStackTrace();
235 }
236
237 transitiveAxioms = new LinkedList<OWLTransitiveObjectPropertyAxiom>();
238 subPropChainAxioms = new LinkedList<OWLSubPropertyChainOfAxiom>();
239
240 OWLDatatype date = ontology.getOWLOntologyManager()
241 .getOWLDataFactory()
242 .getOWLDatatype(IRI.create("http://www.w3.org/2001/XMLSchema#date"));
243 int noOfDataPropertyRangeAxioms = 0, noOfAxioms = 0;
244 for(OWLOntology onto : ontology.getImportsClosure())
245 for(OWLAxiom axiom : onto.getAxioms()) {
246 if(axiom instanceof OWLTransitiveObjectPropertyAxiom)
247 transitiveAxioms.add((OWLTransitiveObjectPropertyAxiom) axiom);
248 else if(axiom instanceof OWLSubPropertyChainOfAxiom)
249 subPropChainAxioms.add((OWLSubPropertyChainOfAxiom) axiom);
250 // TODO to filter out datatype axioms
251 else if(axiom instanceof OWLDataPropertyRangeAxiom) {
252 ++noOfDataPropertyRangeAxioms;
253 Utility.logInfo("The axiom: " + axiom + " is being ignored.");
254 }
255 else {
256 if(axiom.getDatatypesInSignature().contains(date)) {
257 Utility.logInfo("The axiom: " + axiom + " is being ignored.");
258 }
259 else manager.addAxiom(filteredOntology, axiom);
260 }
261
262 if(axiom instanceof OWLAnnotationAssertionAxiom ||
263 axiom instanceof OWLSubAnnotationPropertyOfAxiom ||
264 axiom instanceof OWLDeclarationAxiom ||
265 axiom instanceof OWLDataPropertyRangeAxiom) {
266 }
267 else {
268// System.out.println(axiom);
269 ++noOfAxioms;
270 }
271
272 }
273 Utility.logInfo("The number of data property range axioms that are ignored: " + noOfDataPropertyRangeAxioms + "(" + noOfAxioms + ")");
274
275 DLOntology dlOntology = (DLOntology) clausifier.preprocessAndClausify(filteredOntology, null)[1];
276 dlClauses = dlOntology.getDLClauses();
277 positiveFacts = dlOntology.getPositiveFacts();
278 }
279
280 private DLClause removeAuxiliaryBodyAtoms(DLClause dlClause) {
281 Collection<Atom> newBodyAtoms = new LinkedList<Atom>();
282 DLPredicate p;
283 for(Atom bodyAtom : dlClause.getBodyAtoms()) {
284 p = bodyAtom.getDLPredicate();
285 if(p instanceof AtomicConcept ||
286 p instanceof AtomicRole || p instanceof InverseRole ||
287 p instanceof Equality || p instanceof AnnotatedEquality || p instanceof Inequality)
288 newBodyAtoms.add(bodyAtom);
289 }
290 LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>();
291 Map<Variable, Term> assign = new HashMap<Variable, Term>();
292 for(Atom headAtom : dlClause.getHeadAtoms()) {
293 p = headAtom.getDLPredicate();
294 if(p instanceof AtomicNegationDataRange) {
295 AtomicDataRange positive = ((AtomicNegationDataRange) p).getNegatedDataRange();
296 if(!(positive instanceof ConstantEnumeration))
297 newBodyAtoms.add(Atom.create(positive, headAtom.getArgument(0)));
298 else if(((ConstantEnumeration) positive).getNumberOfConstants() == 1) {
299 assign.put((Variable) headAtom.getArgument(0), ((ConstantEnumeration) positive).getConstant(0));
300// newBodyAtoms.add(Atom.create(Equality.INSTANCE, headAtom.getArgument(0), ((ConstantEnumeration) positive).getConstant(0)));
301 }
302 else newHeadAtoms.add(headAtom);
303 }
304 else
305 newHeadAtoms.add(headAtom);
306 }
307
308 if(assign.isEmpty() && newHeadAtoms.isEmpty() && newBodyAtoms.size() == dlClause.getBodyLength())
309 return dlClause;
310
311 Atom[] headArray =
312 newHeadAtoms.size() == dlClause.getHeadLength() ? dlClause.getHeadAtoms() : newHeadAtoms.toArray(new Atom[0]);
313 Atom[] bodyArray =
314 newBodyAtoms.size() == dlClause.getBodyLength() ? dlClause.getBodyAtoms() : newBodyAtoms.toArray(new Atom[0]);
315 if(!assign.isEmpty()) {
316 for(int i = 0; i < headArray.length; ++i)
317 headArray[i] = DLClauseHelper.getInstance(headArray[i], assign);
318 for(int i = 0; i < bodyArray.length; ++i)
319 bodyArray[i] = DLClauseHelper.getInstance(bodyArray[i], assign);
320 }
321 return DLClause.create(headArray, bodyArray);
322 }
323
324 private void addingTransitiveAxioms() {
325 DLClause transitiveClause;
326 Atom headAtom;
327 Variable X = Variable.create("X"), Y = Variable.create("Y"), Z = Variable.create("Z");
328 transitiveClauses = new LinkedList<DLClause>();
329 for(OWLTransitiveObjectPropertyAxiom axiom : transitiveAxioms) {
330 OWLObjectPropertyExpression objExp = axiom.getProperty();
331 headAtom = getAtom(objExp, X, Z);
332 Atom[] bodyAtoms = new Atom[2];
333 bodyAtoms[0] = getAtom(objExp, X, Y);
334 bodyAtoms[1] = getAtom(objExp, Y, Z);
335 transitiveClause = DLClause.create(new Atom[]{headAtom}, bodyAtoms);
336 clauses.add(transitiveClause);
337 transitiveClauses.add(transitiveClause);
338 }
339 }
340
341 private Atom getAtom(OWLObjectPropertyExpression exp, Variable x, Variable y) {
342 if(exp instanceof OWLObjectProperty)
343 return Atom.create(AtomicRole.create(((OWLObjectProperty) exp).toStringID()), x, y);
344 // TODO fixed, test it
345 OWLObjectPropertyExpression inverseOf;
346 if(exp instanceof OWLObjectInverseOf && (inverseOf = (
347 (OWLObjectInverseOf) exp).getInverse()) instanceof OWLObjectProperty)
348 return Atom.create(AtomicRole.create(((OWLObjectProperty) inverseOf).toStringID()), x, y);
349 return null;
350 }
351
352 private void addingSubPropertyChainAxioms() {
353 DLClause dlClause;
354 subPropChainClauses = new LinkedList<DLClause>();
355 Atom headAtom;
356 Iterator<OWLObjectPropertyExpression> iterExp;
357 OWLObjectPropertyExpression objExp;
358 for(OWLSubPropertyChainOfAxiom axiom : subPropChainAxioms) {
359 objExp = axiom.getSuperProperty();
360 List<OWLObjectPropertyExpression> objs = axiom.getPropertyChain();
361 headAtom = getAtom(objExp, Variable.create("X"), Variable.create("X" + objs.size()));
362 iterExp = objs.iterator();
363 int index = 1;
364 Atom[] bodyAtoms = new Atom[objs.size()];
365 bodyAtoms[0] = getAtom(iterExp.next(), Variable.create("X"), Variable.create("X1"));
366 while(index < objs.size()) {
367 bodyAtoms[index] =
368 getAtom(iterExp.next(), Variable.create("X" + index), Variable.create("X" + (index + 1)));
369 ++index;
370 }
371 dlClause = DLClause.create(new Atom[]{headAtom}, bodyAtoms);
372 clauses.add(dlClause);
373 subPropChainClauses.add(dlClause);
374 }
375 }
376
377 private boolean relevant(DLClause clause, Set<DLPredicate> set) {
378 for(DLPredicate p : dependencyGraph.collectPredicate(clause.getHeadAtoms()))
379 if(set.contains(p))
380 return true;
381 return false;
382 }
383
384}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java
new file mode 100644
index 0000000..611e183
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java
@@ -0,0 +1,47 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.semanticweb.HermiT.model.DLClause;
4import org.semanticweb.HermiT.model.DLPredicate;
5import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxBoth;
6
7import java.util.Collection;
8import java.util.HashMap;
9import java.util.Map;
10
11
12public class UpperDatalogProgram extends UpperProgram {
13
14 public UpperDatalogProgram() {}
15
16// @Override
17// public String getDirectory() {
18// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "datalog");
19// if (!dir.exists())
20// dir.mkdirs();
21// return dir.getPath();
22// }
23
24 @Override
25 protected void initApproximator() {
26 m_approx = new OverApproxBoth();
27 }
28
29 public int getBottomNumber() {
30 return botStrategy.getBottomNumber();
31 }
32
33 public void updateDependencyGraph(Collection<DLClause> delta) {
34 Map<DLPredicate, DLClause> map = new HashMap<DLPredicate, DLClause>();
35 for (DLClause clause: clauses)
36 if (botStrategy.isBottomRule(clause))
37 map.put(clause.getHeadAtom(0).getDLPredicate(), getCorrespondingClause(clause));
38
39 for (DLClause clause: delta) {
40 clauses.add(clause);
41 correspondence.put(clause, map.get(clause.getBodyAtom(0).getDLPredicate()));
42 }
43
44 dependencyGraph.update(delta);
45 }
46
47}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/UpperProgram.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/UpperProgram.java
new file mode 100644
index 0000000..52d60b7
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/UpperProgram.java
@@ -0,0 +1,12 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.apache.commons.io.FilenameUtils;
4
5public abstract class UpperProgram extends ApproxProgram {
6
7 @Override
8 public String getOutputPath() {
9 return FilenameUtils.concat(getDirectory(), "upper.dlog");
10 }
11
12}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java
new file mode 100644
index 0000000..f910c64
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java
@@ -0,0 +1,42 @@
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/main/java/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
new file mode 100644
index 0000000..a140225
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -0,0 +1,146 @@
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/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java
new file mode 100644
index 0000000..ae2a2cf
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java
@@ -0,0 +1,24 @@
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/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java
new file mode 100644
index 0000000..05d9442
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java
@@ -0,0 +1,100 @@
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/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
new file mode 100644
index 0000000..028568c
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
@@ -0,0 +1,224 @@
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/main/java/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
new file mode 100644
index 0000000..ed93d0e
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
@@ -0,0 +1,139 @@
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/main/java/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
new file mode 100644
index 0000000..c99a1ad
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
@@ -0,0 +1,19 @@
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}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java b/src/main/java/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java
new file mode 100644
index 0000000..2adb66b
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java
@@ -0,0 +1,100 @@
1package uk.ac.ox.cs.pagoda.rules.clauses;
2
3public class Clause {
4
5// public static final String IF = ":-";
6// public static final String OR = "|";
7// public static final String AND = ",";
8//
9// protected final List<List<Atom>> head;
10// protected final List<Atom> body;
11//
12// protected Clause(Atom[] headAtoms, Atom[] bodyAtoms) {
13// this.head = Collections.singletonList(Arrays.asList(headAtoms));
14// this.body= Arrays.asList(bodyAtoms);
15// }
16//
17// protected Clause(String s) {
18// this.headAtoms = null;
19// this.bodyAtoms = null;
20// }
21//
22// public int getHeadLength() {
23// return headAtoms.length;
24// }
25//
26// public Atom getHeadAtom(int atomIndex) {
27// return headAtoms[atomIndex];
28// }
29//
30// public Atom[] getHeadAtoms() {
31// return headAtoms.clone();
32// }
33//
34// public int getBodyLength() {
35// return bodyAtoms.length;
36// }
37//
38// public Atom getBodyAtom(int atomIndex) {
39// return bodyAtoms[atomIndex];
40// }
41//
42// public Atom[] getBodyAtoms() {
43// return bodyAtoms.clone();
44// }
45//
46// public String toString(Prefixes prefixes) {
47// StringBuilder buffer = new StringBuilder();
48// for(int headIndex = 0; headIndex < headAtoms.length; headIndex++) {
49// if(headIndex != 0)
50// buffer.append(" ").append(OR).append(" ");
51// buffer.append(headAtoms[headIndex].toString(prefixes));
52// }
53// buffer.append(" ").append(IF).append(" ");
54// for(int bodyIndex = 0; bodyIndex < bodyAtoms.length; bodyIndex++) {
55// if(bodyIndex != 0)
56// buffer.append(AND).append(" ");
57// buffer.append(bodyAtoms[bodyIndex].toString(prefixes));
58// }
59// return buffer.toString();
60// }
61//
62// public String toString() {
63// return toString(Prefixes.STANDARD_PREFIXES);
64// }
65//
66// protected static InterningManager<? extends Clause> s_interningManager = new InterningManager<Clause>() {
67// protected boolean equal(Clause object1, Clause object2) {
68// if(object1.head.length != object2.headAtoms.length
69// || object1.bodyAtoms.length != object2.bodyAtoms.length)
70// return false;
71// for(int index = object1.headAtoms.length - 1; index >= 0; --index)
72// if(object1.headAtoms[index] != object2.headAtoms[index])
73// return false;
74// for(int index = object1.bodyAtoms.length - 1; index >= 0; --index)
75// if(object1.bodyAtoms[index] != object2.bodyAtoms[index])
76// return false;
77// return true;
78// }
79//
80// protected int getHashCode(Clause object) {
81// int hashCode = 0;
82// for(int index = object.bodyAtoms.length - 1; index >= 0; --index)
83// hashCode += object.bodyAtoms[index].hashCode();
84// for(int index = object.headAtoms.length - 1; index >= 0; --index)
85// hashCode += object.headAtoms[index].hashCode();
86// return hashCode;
87// }
88// };
89//
90// /**
91// * Creates a clause from a string.
92// *
93// * @param s
94// * @return
95// */
96// public static Clause create(String s) {
97// return s_interningManager.intern(new Clause(s));
98// }
99
100}
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-05 21:02:14 +0000