aboutsummaryrefslogtreecommitdiff
path: root/src/uk/ac/ox/cs/pagoda/rules
diff options
context:
space:
mode:
authoryzhou <yujiao.zhou@gmail.com>2015-04-21 10:34:27 +0100
committeryzhou <yujiao.zhou@gmail.com>2015-04-21 10:34:27 +0100
commit9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8 (patch)
tree47511c0fb89dccff0db4b5990522e04f294d795b /src/uk/ac/ox/cs/pagoda/rules
parentb1ac207612ee8b045244253fb94b866104bc34f2 (diff)
downloadACQuA-9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8.tar.gz
ACQuA-9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8.zip
initial version
Diffstat (limited to 'src/uk/ac/ox/cs/pagoda/rules')
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java111
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/Approximator.java62
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/DatalogProgram.java64
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java18
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/EqualityAxiomatiser.java91
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java18
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java77
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/GeneralProgram.java49
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/IncrementalProgram.java14
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java228
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java24
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java103
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java279
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/Program.java388
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java46
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/UpperProgram.java10
16 files changed, 1582 insertions, 0 deletions
diff --git a/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java b/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java
new file mode 100644
index 0000000..3b9d6fc
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java
@@ -0,0 +1,111 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.HashMap;
5import java.util.HashSet;
6import java.util.Iterator;
7import java.util.Map;
8
9import org.semanticweb.HermiT.model.DLClause;
10import org.semanticweb.owlapi.model.OWLAxiom;
11import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom;
12import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom;
13
14import uk.ac.ox.cs.pagoda.owl.OWLHelper;
15
16public abstract class ApproxProgram extends Program {
17
18 /**
19 * mapping from over-approximated DLClauses to DLClauses from the original ontology
20 */
21 Map<DLClause, Object> correspondence = new HashMap<DLClause, Object>();
22
23 protected Approximator m_approx = null;
24
25 protected ApproxProgram() { initApproximator(); }
26
27 protected abstract void initApproximator();
28
29 @Override
30 public void transform() {
31 super.transform();
32 Iterator<DLClause> iterClause = transitiveClauses.iterator();
33 for (Iterator<OWLTransitiveObjectPropertyAxiom> iterAxiom = transitiveAxioms.iterator(); iterAxiom.hasNext(); )
34 addCorrespondence(iterClause.next(), iterAxiom.next());
35
36 iterClause = subPropChainClauses.iterator();
37 for (Iterator<OWLSubPropertyChainOfAxiom> iterAxiom = subPropChainAxioms.iterator(); iterAxiom.hasNext(); )
38 addCorrespondence(iterClause.next(), iterAxiom.next());
39 }
40
41 @Override
42 public Collection<DLClause> convert2Clauses(DLClause clause) {
43 Collection<DLClause> ret = botStrategy.process(m_approx.convert(clause, clause));
44// OWLAxiom correspondingAxiom = OWLHelper.getOWLAxiom(ontology, clause);
45 for (DLClause newClause: ret) {
46 addCorrespondence(newClause, clause);
47// addCorrespondence(newClause, correspondingAxiom);
48 }
49 return ret;
50 }
51
52 private void addCorrespondence(DLClause newClause, Object corresponding) {
53 Object object;
54 if ((object = correspondence.get(newClause)) != null) {
55 if (object.equals(corresponding))
56 return ;
57
58 if (object instanceof DLClause) {
59 DLClause c1 = (DLClause) object;
60 if (c1.getHeadLength() == 1) return ;
61 DLClause c2 = (DLClause) corresponding;
62 if (c2.getHeadLength() == 1) {
63 correspondence.put(newClause, c2);
64 return ;
65 }
66 ClauseSet list = new ClauseSet(c1, c2);
67 correspondence.put(newClause, list);
68 }
69 else if (object instanceof ClauseSet){
70 ClauseSet list = (ClauseSet) object;
71 list.add((DLClause) corresponding);
72 }
73 }
74 correspondence.put(newClause, corresponding);
75 }
76
77 public OWLAxiom getEquivalentAxiom(DLClause clause) {
78 Object obj = correspondence.get(clause);
79 while (obj != null && obj instanceof DLClause && !obj.equals(clause) && correspondence.containsKey((DLClause) obj))
80 obj = correspondence.get(clause);
81 if (obj instanceof OWLAxiom)
82 return (OWLAxiom) obj;
83 else if (obj != null)
84 return OWLHelper.getOWLAxiom(ontology, (DLClause) obj);
85 else {
86 return OWLHelper.getOWLAxiom(ontology, clause);
87 }
88 }
89
90 public DLClause getCorrespondingClause(DLClause clause) {
91 Object obj = correspondence.get(clause);
92 if (obj instanceof DLClause)
93 return (DLClause) obj;
94 else
95 return clause;
96 }
97}
98
99class ClauseSet extends HashSet<DLClause> {
100
101 public ClauseSet(DLClause first, DLClause second) {
102 add(first);
103 add(second);
104 }
105
106 /**
107 *
108 */
109 private static final long serialVersionUID = 1L;
110
111} \ No newline at end of file
diff --git a/src/uk/ac/ox/cs/pagoda/rules/Approximator.java b/src/uk/ac/ox/cs/pagoda/rules/Approximator.java
new file mode 100644
index 0000000..b2edd56
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/Approximator.java
@@ -0,0 +1,62 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.LinkedList;
5
6import org.semanticweb.HermiT.model.AtLeast;
7import org.semanticweb.HermiT.model.Atom;
8import org.semanticweb.HermiT.model.DLClause;
9import org.semanticweb.HermiT.model.DLPredicate;
10
11public interface Approximator {
12
13 public Collection<DLClause> convert(DLClause clause, DLClause originalClause);
14
15}
16
17class IgnoreExist implements Approximator {
18
19 @Override
20 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
21 Collection<DLClause> ret = new LinkedList<DLClause>();
22 DLPredicate p;
23 for (Atom headAtom: clause.getHeadAtoms()) {
24 p = headAtom.getDLPredicate();
25 if (p instanceof AtLeast) return ret;
26 }
27
28 ret.add(clause);
29 return ret;
30 }
31
32}
33
34class IgnoreBoth implements Approximator {
35
36 @Override
37 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
38 Collection<DLClause> ret = new LinkedList<DLClause>();
39
40 if (clause.getHeadLength() > 1) return ret;
41
42 if (clause.getHeadLength() > 0) {
43 DLPredicate predicate = clause.getHeadAtom(0).getDLPredicate();
44
45 if (predicate instanceof AtLeast) return ret;
46 }
47
48 ret.add(clause);
49 return ret;
50 }
51}
52
53class IgnoreDisj implements Approximator {
54
55 @Override
56 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
57 Collection<DLClause> ret = new LinkedList<DLClause>();
58 if (clause.getHeadLength() > 1) return ret;
59 ret.add(clause);
60 return ret;
61 }
62}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/DatalogProgram.java b/src/uk/ac/ox/cs/pagoda/rules/DatalogProgram.java
new file mode 100644
index 0000000..1f7148c
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/DatalogProgram.java
@@ -0,0 +1,64 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.semanticweb.owlapi.model.OWLOntology;
4
5import uk.ac.ox.cs.pagoda.constraints.*;
6
7public class DatalogProgram {
8
9 UpperDatalogProgram upperProgram = new UpperDatalogProgram();
10 LowerDatalogProgram lowerProgram;
11 GeneralProgram program = new GeneralProgram();
12
13 BottomStrategy upperBottom;
14
15 public DatalogProgram(OWLOntology o) {
16 lowerProgram = new LowerDatalogProgram();
17 init(o, false);
18 }
19
20 public DatalogProgram(OWLOntology o, boolean toClassify) {
21 lowerProgram = new LowerDatalogProgram(toClassify);
22 init(o, toClassify);
23 }
24
25 private void init(OWLOntology o, boolean forSemFacet) {
26 upperProgram.load(o, upperBottom = new UpperUnaryBottom());
27// upperProgram.load(o, upperBottom = new UnaryBottom());
28 lowerProgram.clone(upperProgram);
29 program.clone(upperProgram);
30// program.botStrategy = new UnaryBottom();
31
32 upperProgram.transform();
33 lowerProgram.transform();
34 program.transform();
35
36 program.buildDependencyGraph();
37 PredicateDependency graph = upperProgram.buildDependencyGraph();
38 lowerProgram.dependencyGraph = graph;
39 }
40
41 public LowerDatalogProgram getLower() {
42 return lowerProgram;
43 }
44
45 public UpperDatalogProgram getUpper() {
46 return upperProgram;
47 }
48
49 public GeneralProgram getGeneral() {
50 return program;
51 }
52
53 public String getAdditionalDataFile() {
54 return upperProgram.getAdditionalDataFile();
55 }
56
57 public BottomStrategy getUpperBottomStrategy() {
58 return upperBottom;
59 }
60
61 public void deleteABoxTurtleFile() {
62 if (upperProgram != null) upperProgram.deleteABoxTurtleFile();
63 }
64}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java b/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java
new file mode 100644
index 0000000..6ebe666
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java
@@ -0,0 +1,18 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3public class DisjunctiveProgram extends UpperProgram {
4
5 @Override
6 protected void initApproximator() {
7 m_approx = new OverApproxExist();
8 }
9
10// @Override
11// public String getDirectory() {
12// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "disjunctiveRules");
13// if (!dir.exists())
14// dir.mkdirs();
15// return dir.getPath();
16// }
17
18}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/EqualityAxiomatiser.java b/src/uk/ac/ox/cs/pagoda/rules/EqualityAxiomatiser.java
new file mode 100644
index 0000000..81b8a01
--- /dev/null
+++ b/src/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/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java b/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java
new file mode 100644
index 0000000..64d018f
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java
@@ -0,0 +1,18 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3public class ExistentialProgram extends UpperProgram {
4
5// @Override
6// public String getDirectory() {
7// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "existential");
8// if (!dir.exists())
9// dir.mkdirs();
10// return dir.getPath();
11// }
12
13 @Override
14 protected void initApproximator() {
15 m_approx = new OverApproxDisj();
16 }
17
18}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java b/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java
new file mode 100644
index 0000000..ebe0b7d
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java
@@ -0,0 +1,77 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.HashSet;
5import java.util.LinkedList;
6import java.util.Set;
7
8import org.semanticweb.HermiT.model.AtLeastConcept;
9import org.semanticweb.HermiT.model.Atom;
10import org.semanticweb.HermiT.model.AtomicRole;
11import org.semanticweb.HermiT.model.DLClause;
12import org.semanticweb.HermiT.model.DLPredicate;
13import org.semanticweb.owlapi.model.OWLObjectProperty;
14import org.semanticweb.owlapi.model.OWLOntology;
15import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
16
17public class ExistentialToDisjunctive extends UpperProgram {
18
19 Set<String> inverseFuncProperties = new HashSet<String>();
20
21 @Override
22 public void load(OWLOntology o, BottomStrategy bottomStrategy) {
23 super.load(o, bottomStrategy);
24 for (OWLObjectProperty prop: ontology.getObjectPropertiesInSignature(true))
25 if (!(ontology.getInverseFunctionalObjectPropertyAxioms(prop).isEmpty()))
26 inverseFuncProperties.add(prop.getIRI().toString());
27 ((RefinedOverApproxExist) m_approx).setInverseFuncProps(inverseFuncProperties);
28 }
29
30 @Override
31 protected void initApproximator() {
32 m_approx = new RefinedOverApproxExist();
33 }
34
35}
36
37class RefinedOverApproxExist implements Approximator {
38
39 Approximator approxExist = new OverApproxExist();
40 Set<String> inverseFuncProperties;
41
42 public void setInverseFuncProps(Set<String> set) {
43 inverseFuncProperties = set;
44 }
45
46 @Override
47 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
48 DLPredicate p;
49 Collection<Atom> newHeadAtoms = new LinkedList<Atom>();
50 for (Atom headAtom: clause.getHeadAtoms())
51 newHeadAtoms.add(headAtom);
52
53 for (Atom headAtom: clause.getHeadAtoms()) {
54 p = headAtom.getDLPredicate();
55 if (isAtLeastOneOnInverseFuncProperties(p))
56 newHeadAtoms.add(headAtom);
57 }
58
59 if (newHeadAtoms.size() > clause.getHeadLength())
60 clause = DLClause.create(newHeadAtoms.toArray(new Atom[0]), clause.getBodyAtoms());
61
62 return approxExist.convert(clause, clause);
63 }
64
65 private boolean isAtLeastOneOnInverseFuncProperties(DLPredicate predicate) {
66 if (!(predicate instanceof AtLeastConcept))
67 return false;
68 AtLeastConcept atLeast = (AtLeastConcept) predicate;
69 if (!(atLeast.getOnRole() instanceof AtomicRole))
70 return false;
71
72 return atLeast.getNumber() == 1 && inverseFuncProperties.contains(((AtomicRole) atLeast.getOnRole()).getIRI());
73 }
74
75
76}
77
diff --git a/src/uk/ac/ox/cs/pagoda/rules/GeneralProgram.java b/src/uk/ac/ox/cs/pagoda/rules/GeneralProgram.java
new file mode 100644
index 0000000..38fa494
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/GeneralProgram.java
@@ -0,0 +1,49 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.Collections;
5import java.util.Set;
6
7import org.semanticweb.HermiT.model.DLClause;
8import org.semanticweb.owlapi.model.OWLOntology;
9import uk.ac.ox.cs.pagoda.constraints.UnaryBottom;
10
11public class GeneralProgram extends Program {
12
13 public GeneralProgram(Set<DLClause> relevantClauses, OWLOntology relevantOntology) {
14 ontology = relevantOntology;
15
16 ontologyDirectory = null;
17 dlOntology = null;
18 botStrategy = new UnaryBottom();
19
20 clauses = botStrategy.process(relevantClauses);
21 }
22
23 public GeneralProgram() {}
24
25 public Collection<DLClause> convert2Clauses(DLClause clause) {
26 return botStrategy.process(Collections.singleton(clause));
27 }
28
29 @Override
30 public String getOutputPath() {
31 return getDirectory() + "rules.dlog";
32 }
33
34// @Override
35// public String getDirectory() {
36// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "general");
37// if (!dir.exists())
38// dir.mkdirs();
39// return dir.getPath();
40// }
41
42 public boolean isHorn() {
43 for (DLClause clause: clauses)
44 if (clause.getHeadLength() > 1)
45 return false;
46 return true;
47 }
48
49}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/IncrementalProgram.java b/src/uk/ac/ox/cs/pagoda/rules/IncrementalProgram.java
new file mode 100644
index 0000000..339738a
--- /dev/null
+++ b/src/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/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java b/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java
new file mode 100644
index 0000000..6e17f02
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java
@@ -0,0 +1,228 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.Iterator;
5import java.util.LinkedList;
6import java.util.Set;
7
8import org.semanticweb.HermiT.Reasoner;
9import org.semanticweb.HermiT.model.Atom;
10import org.semanticweb.HermiT.model.AtomicConcept;
11import org.semanticweb.HermiT.model.AtomicRole;
12import org.semanticweb.HermiT.model.DLClause;
13import org.semanticweb.HermiT.model.Variable;
14import org.semanticweb.owlapi.model.OWLClass;
15import org.semanticweb.owlapi.model.OWLObjectInverseOf;
16import org.semanticweb.owlapi.model.OWLObjectProperty;
17import org.semanticweb.owlapi.model.OWLObjectPropertyExpression;
18import org.semanticweb.owlapi.model.OWLOntology;
19import org.semanticweb.owlapi.reasoner.Node;
20
21import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
22import uk.ac.ox.cs.pagoda.constraints.NullaryBottom;
23import uk.ac.ox.cs.pagoda.constraints.UnaryBottom;
24import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom;
25import uk.ac.ox.cs.pagoda.multistage.Normalisation;
26import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication;
27import uk.ac.ox.cs.pagoda.util.Timer;
28import uk.ac.ox.cs.pagoda.util.Utility;
29
30public class LowerDatalogProgram extends ApproxProgram implements IncrementalProgram {
31
32 boolean m_toClassify;
33
34 public LowerDatalogProgram() {
35 m_toClassify = true;
36 }
37
38 public LowerDatalogProgram(boolean toClassify) {
39 m_toClassify = toClassify; // false; //
40 }
41
42 void clone(Program program) {
43 super.clone(program);
44 if (botStrategy instanceof UpperUnaryBottom)
45 botStrategy = new UnaryBottom();
46 }
47
48
49 @Override
50 public void transform() {
51 if (m_toClassify) {
52 ClassifyThread thread = new ClassifyThread(this);
53 thread.start();
54 super.transform();
55 try {
56 thread.join(5000);
57 } catch (InterruptedException e) {
58 return ;
59 }
60 if (!thread.isAlive()) thread.dispose();
61 else thread.interrupt();
62 }
63 else
64 super.transform();
65
66 Normalisation norm = new Normalisation(dlOntology.getDLClauses(), ontology, new NullaryBottom());
67 BottomStrategy tBottom = new NullaryBottom();
68 norm.process();
69 for (DLClause nClause: norm.getNormlisedClauses()) {
70 if (nClause.getHeadLength() != 1)
71 for (DLClause newClause: RestrictedApplication.addAddtionalDatalogRules(nClause, tBottom, norm)) {
72// System.out.println(newClause);
73 if (newClause.getHeadAtom(0).getDLPredicate() instanceof AtomicConcept || newClause.getHeadAtom(0).getDLPredicate() instanceof AtomicRole) {
74// System.out.println(newClause);
75 clauses.add(newClause);
76 }
77 }
78
79 if (nClause.getHeadLength() == 1 && (nClause.getHeadAtom(0).getDLPredicate() instanceof AtomicConcept || nClause.getHeadAtom(0).getDLPredicate() instanceof AtomicRole) && clauses.add(nClause)) {
80// System.out.println(nClause);
81 }
82 }
83 }
84
85 @Override
86 public String getOutputPath() {
87 return getDirectory() + "lower.dlog";
88 }
89
90// @Override
91// public String getDirectory() {
92// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "datalog");
93// if (!dir.exists())
94// dir.mkdirs();
95// return dir.getPath();
96// }
97
98 @Override
99 public void enrich(Collection<DLClause> delta) {
100 synchronized (clauses) {
101 Iterator<DLClause> iter = delta.iterator();
102 while (iter.hasNext())
103 clauses.add(iter.next());
104 }
105 }
106
107 @Override
108 public String toString() {
109 String text;
110 synchronized (clauses) {
111 text = super.toString();
112 }
113 return text;
114 }
115
116 @Override
117 protected void initApproximator() {
118 m_approx = new IgnoreBoth();
119 }
120
121}
122
123class ClassifyThread extends Thread {
124
125 IncrementalProgram m_program;
126 Collection<DLClause> clauses = new LinkedList<DLClause>();
127
128 Variable X = Variable.create("X"), Y = Variable.create("Y");
129
130 ClassifyThread(IncrementalProgram program) {
131 m_program = program;
132 }
133
134 Reasoner hermitReasoner;
135 OWLOntology ontology;
136
137 @Override
138 public void run() {
139 ontology = m_program.getOntology();
140 try {
141 hermitReasoner = new Reasoner(ontology);
142 Timer t = new Timer();
143 hermitReasoner.classifyClasses();
144 Utility.logInfo("HermiT classification done: " + t.duration());
145 } catch (Exception e) {
146// e.printStackTrace();
147 Utility.logInfo("HermiT cannot classify the ontology.");
148 hermitReasoner = null;
149 }
150 }
151
152 public void dispose() {
153 if (hermitReasoner == null)
154 return ;
155 Set<OWLClass> classes;
156 OWLClass lastClass = null, currentClass;
157 for (OWLClass subClass: ontology.getClassesInSignature()) {
158 Node<OWLClass> node = hermitReasoner.getEquivalentClasses(subClass);
159 if (!subClass.equals(node.getRepresentativeElement())) continue;
160
161 classes = node.getEntities();
162 lastClass = subClass;
163 for (Iterator<OWLClass> iter = classes.iterator(); iter.hasNext(); ) {
164 currentClass = iter.next();
165 if (currentClass.equals(subClass)) continue;
166 addClause(lastClass, currentClass);
167 lastClass = currentClass;
168 }
169 addClause(lastClass, subClass);
170
171 for (Node<OWLClass> tNode: hermitReasoner.getSuperClasses(subClass, true)) {
172 OWLClass superClass = tNode.getRepresentativeElement();
173 addClause(subClass, superClass);
174 }
175 }
176
177 Set<OWLObjectPropertyExpression> properties;
178 OWLObjectPropertyExpression lastProperty, currentProperty;
179 for (OWLObjectProperty subProperty: ontology.getObjectPropertiesInSignature()) {
180 Node<OWLObjectPropertyExpression> node = hermitReasoner.getEquivalentObjectProperties(subProperty);
181 if (!subProperty.equals(node.getRepresentativeElement())) continue;
182
183 properties = node.getEntities();
184 lastProperty = subProperty;
185 for (Iterator<OWLObjectPropertyExpression> iter = properties.iterator(); iter.hasNext(); ) {
186 currentProperty = iter.next();
187 if (currentProperty.equals(subProperty)) continue;
188 addClause(lastProperty, currentProperty);
189 lastProperty = currentProperty;
190 }
191 addClause(lastProperty, subProperty);
192
193 for (Node<OWLObjectPropertyExpression> tNode: hermitReasoner.getSuperObjectProperties(subProperty, true)) {
194 OWLObjectPropertyExpression superProperty = tNode.getRepresentativeElement();
195 addClause(subProperty, superProperty);
196 }
197 }
198
199 m_program.enrich(clauses);
200 Utility.logInfo("classification done and enriched lower bound rules.");
201 }
202
203
204 private void addClause(OWLObjectPropertyExpression subProperty, OWLObjectPropertyExpression superProperty) {
205 if (subProperty.equals(superProperty)) return ;
206 if (superProperty.toString().equals("owl:topObjectProperty")) return ;
207 clauses.add(DLClause.create(new Atom[] { getAtom(superProperty) }, new Atom[] { getAtom(subProperty) }));
208 }
209
210 private Atom getAtom(OWLObjectPropertyExpression p) {
211 if (p instanceof OWLObjectInverseOf)
212 return Atom.create(AtomicRole.create(((OWLObjectProperty) ((OWLObjectInverseOf) p).getInverse()).toStringID()), Y, X);
213
214 return Atom.create(AtomicRole.create(((OWLObjectProperty) p).toStringID()), X, Y);
215 }
216
217 private void addClause(OWLClass subClass, OWLClass superClass) {
218 if (subClass.equals(superClass)) return ;
219 if (subClass.toString().equals("owl:Nothing")) return ;
220 if (superClass.toString().equals("owl:Thing")) return ;
221 clauses.add(DLClause.create(new Atom[] { getAtom(superClass) }, new Atom[] { getAtom(subClass) }));
222 }
223
224 private Atom getAtom(OWLClass c) {
225 return Atom.create(AtomicConcept.create(c.toStringID()), X);
226 }
227
228} \ No newline at end of file
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java
new file mode 100644
index 0000000..3cc2aba
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java
@@ -0,0 +1,24 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.LinkedList;
5
6import org.semanticweb.HermiT.model.AtLeastDataRange;
7import org.semanticweb.HermiT.model.DLClause;
8
9public class OverApproxBoth implements Approximator {
10
11 Approximator approxDist = new OverApproxDisj(), approxExist = new OverApproxExist();
12
13 @Override
14 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
15 Collection<DLClause> ret = new LinkedList<DLClause>();
16 for (DLClause tClause: approxDist.convert(clause, originalClause)) {
17 if (tClause.getHeadLength() > 0 && tClause.getHeadAtom(0).getDLPredicate() instanceof AtLeastDataRange)
18 continue;
19 ret.addAll(approxExist.convert(tClause, originalClause));
20 }
21 return ret;
22 }
23
24}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java
new file mode 100644
index 0000000..5edb08e
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java
@@ -0,0 +1,103 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.HashMap;
5import java.util.HashSet;
6import java.util.LinkedList;
7import java.util.Map;
8import java.util.Set;
9
10import org.semanticweb.HermiT.model.Atom;
11import org.semanticweb.HermiT.model.DLClause;
12import org.semanticweb.HermiT.model.DLPredicate;
13import org.semanticweb.HermiT.model.Term;
14import org.semanticweb.HermiT.model.Variable;
15
16import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
17
18public class OverApproxDisj implements Approximator {
19
20 @Override
21 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
22 LinkedList<DLClause> distincts = new LinkedList<DLClause>();
23 Atom[] headAtoms = clause.getHeadAtoms(), bodyAtoms = clause.getBodyAtoms();
24 LinkedList<DLClause> newClauses = new LinkedList<DLClause>();
25 DLClause newClause;
26 if (headAtoms.length > 1) {
27 for (Atom headAtom: headAtoms) {
28 newClause = DLClause.create(new Atom[] {headAtom}, bodyAtoms);
29 newClauses.add(newClause);
30// distincts.add(newClause);
31 }
32
33 for (DLClause cls: newClauses) {
34 newClause = DLClauseHelper.simplified(cls);
35 if (!isSubsumedBy(newClause, distincts))
36 distincts.add(newClause);
37 }
38 }
39 else distincts.add(clause);
40
41 return distincts;
42 }
43
44 public static boolean isSubsumedBy(DLClause newClause, Collection<DLClause> distinctClauses) {
45 Map<Variable, Term> unifier;
46 Set<Atom> bodyAtoms = new HashSet<Atom>();
47 for (DLClause clause: distinctClauses) {
48 if (newClause.getHeadLength() > 0 && clause.getHeadLength() > 0 &&
49 (unifier = isSubsumedBy(newClause.getHeadAtom(0), clause.getHeadAtom(0))) == null)
50 continue;
51 else
52 unifier = new HashMap<Variable, Term>();
53
54 for (Atom atom: clause.getBodyAtoms())
55 bodyAtoms.add(rename(atom, unifier));
56 unifier.clear();
57
58 for (Atom atom: newClause.getBodyAtoms())
59 if (!bodyAtoms.contains(atom))
60 continue;
61
62 return true;
63 }
64
65 return false;
66 }
67
68 public static Map<Variable, Term> isSubsumedBy(Atom atom1, Atom atom2) {
69 DLPredicate predicate = atom1.getDLPredicate();
70 if (!predicate.equals(atom2.getDLPredicate()))
71 return null;
72
73 Map<Variable, Term> unifier = new HashMap<Variable, Term>();
74 Term term1, term2;
75 for (int index = 0; index < predicate.getArity(); ++index) {
76 term1 = rename(atom1.getArgument(index), unifier);
77 term2 = rename(atom2.getArgument(index), unifier);
78
79 if (term1.equals(term2));
80 else if (term1 instanceof Variable)
81 unifier.put((Variable) term1, term2);
82 else
83 return null;
84 }
85 return unifier;
86 }
87
88 public static Atom rename(Atom atom, Map<Variable, Term> unifier) {
89 Term[] arguments = new Term[atom.getArity()];
90 for (int i = 0; i < atom.getArity(); ++i)
91 arguments[i] = rename(atom.getArgument(i), unifier);
92 return Atom.create(atom.getDLPredicate(), arguments);
93 }
94
95 public static Term rename(Term argument, Map<Variable, Term> unifier) {
96 Term newArg;
97 while ((newArg = unifier.get(argument)) != null)
98 return newArg;
99 return argument;
100 }
101
102
103}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java
new file mode 100644
index 0000000..7e66411
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java
@@ -0,0 +1,279 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.HashMap;
5import java.util.Iterator;
6import java.util.LinkedList;
7import java.util.Map;
8
9import org.semanticweb.HermiT.model.AtLeast;
10import org.semanticweb.HermiT.model.AtLeastConcept;
11import org.semanticweb.HermiT.model.AtLeastDataRange;
12import org.semanticweb.HermiT.model.Atom;
13import org.semanticweb.HermiT.model.AtomicConcept;
14import org.semanticweb.HermiT.model.AtomicNegationConcept;
15import org.semanticweb.HermiT.model.AtomicRole;
16import org.semanticweb.HermiT.model.DLClause;
17import org.semanticweb.HermiT.model.DLPredicate;
18import org.semanticweb.HermiT.model.Individual;
19import org.semanticweb.HermiT.model.Inequality;
20import org.semanticweb.HermiT.model.InverseRole;
21import org.semanticweb.HermiT.model.LiteralConcept;
22import org.semanticweb.HermiT.model.Role;
23import org.semanticweb.HermiT.model.Term;
24import org.semanticweb.HermiT.model.Variable;
25import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
26import uk.ac.ox.cs.pagoda.util.Namespace;
27
28public class OverApproxExist implements Approximator {
29
30 @Override
31 public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
32 Collection<DLClause> ret;
33 switch (clause.getHeadLength()) {
34 case 1:
35 return overApprox(clause.getHeadAtom(0), clause.getBodyAtoms(), originalClause);
36 case 0:
37 ret = new LinkedList<DLClause>();
38 ret.add(clause);
39 return ret;
40 default:
41 ret = new LinkedList<DLClause>();
42 for (Iterator<DLClause> iter = new DisjunctiveHeads(clause, originalClause); iter.hasNext(); )
43 ret.add(iter.next());
44 return ret;
45 }
46 }
47
48 private static int noOfExistential(DLClause originalClause) {
49 int no = 0;
50 for (Atom atom: originalClause.getHeadAtoms())
51 if (atom.getDLPredicate() instanceof AtLeast)
52 no += ((AtLeast) atom.getDLPredicate()).getNumber();
53 return no;
54 }
55
56 private static int indexOfExistential(Atom headAtom, DLClause originalClause) {
57 if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1;
58 AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
59 if (alc.getToConcept() instanceof AtomicConcept) {
60 AtomicConcept ac = (AtomicConcept) alc.getToConcept();
61 if (ac.getIRI().endsWith(negativeSuffix)) {
62 alc = AtLeastConcept.create(alc.getNumber(), alc.getOnRole(), AtomicNegationConcept.create(getNegationConcept(ac)));
63 headAtom = Atom.create(alc, headAtom.getArgument(0));
64 }
65 }
66
67 int index = 0;
68 for (Atom atom: originalClause.getHeadAtoms()) {
69 if (atom.equals(headAtom))
70 return index;
71 if (atom.getDLPredicate() instanceof AtLeast)
72 index += ((AtLeast) atom.getDLPredicate()).getNumber();
73 }
74 return -1;
75 }
76
77 private static final Variable X = Variable.create("X");
78 public static final String negativeSuffix = "_neg";
79
80 public static AtomicConcept getNegationConcept(DLPredicate p) {
81 if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING;
82 if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING;
83
84 if (p instanceof AtomicConcept) {
85 String iri = ((AtomicConcept) p).getIRI();
86 if (iri.endsWith(negativeSuffix))
87 iri = iri.substring(0, iri.length() - 4);
88 else
89 iri += negativeSuffix;
90
91 return AtomicConcept.create(iri);
92 }
93 if (p instanceof AtLeastConcept) {
94 // FIXME !!! here
95 return null;
96 }
97 return null;
98 }
99
100 public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
101
102 private static int individualCounter = 0;
103 private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>();
104
105 public static int getNumberOfSkolemisedIndividual() {
106 return individualCounter;
107 }
108
109 public static Individual getNewIndividual(DLClause originalClause, int offset) {
110 Individual ret;
111 if (individualNumber.containsKey(originalClause)) {
112 ret = Individual.create(skolemisedIndividualPrefix + (individualNumber.get(originalClause) + offset));
113 }
114 else {
115 individualNumber.put(originalClause, individualCounter);
116 ret = Individual.create(skolemisedIndividualPrefix + (individualCounter + offset));
117 individualCounter += noOfExistential(originalClause);
118 }
119 return ret;
120 }
121
122 public static int indexOfSkolemisedIndividual(Atom atom) {
123 Term t;
124 for (int index = 0; index < atom.getArity(); ++index) {
125 t = atom.getArgument(index);
126 if (t instanceof Individual && ((Individual) t).getIRI().contains(skolemisedIndividualPrefix)) return index;
127 }
128 return -1;
129 }
130
131 public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause) {
132 return overApprox(headAtom, bodyAtoms, originalClause, indexOfExistential(headAtom, originalClause));
133 }
134
135 public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause, int offset) {
136 Collection<DLClause> ret = new LinkedList<DLClause>();
137 DLPredicate predicate = headAtom.getDLPredicate();
138 if (predicate instanceof AtLeastConcept) {
139 AtLeastConcept atLeastConcept = (AtLeastConcept) predicate;
140 LiteralConcept concept = atLeastConcept.getToConcept();
141 Role role = atLeastConcept.getOnRole();
142 AtomicConcept atomicConcept = null;
143
144 if (concept instanceof AtomicNegationConcept) {
145 Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
146 Atom atom2 = Atom.create(atomicConcept = getNegationConcept(atomicConcept), X);
147 ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2}));
148 }
149 else {
150 atomicConcept = (AtomicConcept) concept;
151 if (atomicConcept.equals(AtomicConcept.THING))
152 atomicConcept = null;
153 }
154
155 int card = atLeastConcept.getNumber();
156 Individual[] individuals = new Individual[card];
157 for (int i = 0; i < card; ++i) individuals[i] = getNewIndividual(originalClause, offset + i);
158
159 for (int i = 0; i < card; ++i) {
160 if (atomicConcept != null)
161 ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, bodyAtoms));
162
163 Atom atom = role instanceof AtomicRole ?
164 Atom.create((AtomicRole) role, X, individuals[i]) :
165 Atom.create(((InverseRole) role).getInverseOf(), individuals[i], X);
166
167 ret.add(DLClause.create(new Atom[] {atom}, bodyAtoms));
168 }
169
170 for (int i = 0; i < card; ++i)
171 for (int j = i + 1; j < card; ++j)
172 // TODO to be checked ... different as
173 ret.add(DLClause.create(new Atom[] {Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, bodyAtoms));
174 //DLClauseHelper.contructor_differentAs(individuals[i], individuals[j]));
175
176 }
177 else if (predicate instanceof AtLeastDataRange) {
178 // TODO to be implemented ...
179 }
180 else
181 ret.add(DLClause.create(new Atom[] {headAtom}, bodyAtoms));
182
183 return ret;
184 }
185
186 class DisjunctiveHeads implements Iterator<DLClause> {
187
188 Atom[] bodyAtoms;
189 Atom[][] disjunctHeadAtoms;
190 int[] pointer;
191 int length, l;
192 LinkedList<DLClause> auxiliaryClauses = new LinkedList<DLClause>();
193
194 public DisjunctiveHeads(DLClause clause, DLClause originalClause) {
195 length = clause.getHeadLength();
196
197 bodyAtoms = clause.getBodyAtoms();
198 disjunctHeadAtoms = new Atom[length][];
199 pointer = new int[length];
200 if (length > 0) l = length - 1;
201 else length = 0;
202
203 int index = 0, offset = 0;
204 Collection<DLClause> datalogRules;
205 DLClause newClause;
206 for (Atom headAtom: clause.getHeadAtoms()) {
207 pointer[index] = 0;
208
209 datalogRules = overApprox(headAtom, bodyAtoms, originalClause, offset);
210
211 if (datalogRules.isEmpty()) {
212 l = -1;
213 auxiliaryClauses.clear();
214 return ;
215 }
216
217 for (Iterator<DLClause> iter = datalogRules.iterator(); iter.hasNext(); ) {
218 newClause = iter.next();
219 if (!DLClauseHelper.hasSubsetBodyAtoms(newClause, clause)) {
220 auxiliaryClauses.add(newClause);
221 iter.remove();
222 }
223 }
224
225 disjunctHeadAtoms[index] = new Atom[datalogRules.size()];
226
227 int j = 0;
228 for (DLClause disjunct: datalogRules) {
229 disjunctHeadAtoms[index][j++] = disjunct.getHeadAtom(0);
230 }
231
232 ++index;
233 if (headAtom.getDLPredicate() instanceof AtLeast)
234 offset += ((AtLeast) headAtom.getDLPredicate()).getNumber();
235
236 }
237
238 }
239
240 @Override
241 public boolean hasNext() {
242 return l != -1 || !auxiliaryClauses.isEmpty();
243 }
244
245 @Override
246 public DLClause next() {
247 if (l == -1)
248 return auxiliaryClauses.removeFirst();
249
250 if (length > 0) {
251 Atom[] headAtoms = new Atom[length];
252 for (int i = 0; i < length; ++i)
253 headAtoms[i] = disjunctHeadAtoms[i][pointer[i]];
254
255 ++pointer[l];
256 while (l >= 0 && pointer[l] >= disjunctHeadAtoms[l].length) {
257 pointer[l] = 0;
258 --l;
259 if (l >= 0)
260 ++pointer[l];
261 }
262
263 if (l >= 0) l = length - 1;
264
265 return DLClauseHelper.simplified(DLClause.create(headAtoms, bodyAtoms));
266// return DLClause.create(headAtoms, bodyAtoms);
267 }
268 else {
269 --l;
270 return DLClauseHelper.simplified(DLClause.create(new Atom[0], bodyAtoms));
271// return DLClause.create(new Atom[0], bodyAtoms);
272 }
273 }
274
275 @Override
276 public void remove() { }
277
278 }
279}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/Program.java b/src/uk/ac/ox/cs/pagoda/rules/Program.java
new file mode 100644
index 0000000..b533e50
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/Program.java
@@ -0,0 +1,388 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.io.BufferedWriter;
4import java.io.File;
5import java.io.FileNotFoundException;
6import java.io.FileOutputStream;
7import java.io.IOException;
8import java.io.OutputStreamWriter;
9import java.util.Collection;
10import java.util.HashMap;
11import java.util.HashSet;
12import java.util.Iterator;
13import java.util.LinkedList;
14import java.util.List;
15import java.util.Map;
16import java.util.Set;
17
18import org.semanticweb.HermiT.Configuration;
19import org.semanticweb.HermiT.model.AnnotatedEquality;
20import org.semanticweb.HermiT.model.Atom;
21import org.semanticweb.HermiT.model.AtomicConcept;
22import org.semanticweb.HermiT.model.AtomicDataRange;
23import org.semanticweb.HermiT.model.AtomicNegationDataRange;
24import org.semanticweb.HermiT.model.AtomicRole;
25import org.semanticweb.HermiT.model.ConstantEnumeration;
26import org.semanticweb.HermiT.model.DLClause;
27import org.semanticweb.HermiT.model.DLOntology;
28import org.semanticweb.HermiT.model.DLPredicate;
29import org.semanticweb.HermiT.model.Equality;
30import org.semanticweb.HermiT.model.Inequality;
31import org.semanticweb.HermiT.model.InverseRole;
32import org.semanticweb.HermiT.model.Term;
33import org.semanticweb.HermiT.model.Variable;
34import org.semanticweb.HermiT.structural.OWLClausification;
35import org.semanticweb.owlapi.model.*;
36
37import uk.ac.ox.cs.pagoda.MyPrefixes;
38import uk.ac.ox.cs.pagoda.approx.KnowledgeBase;
39import uk.ac.ox.cs.pagoda.approx.RLPlusOntology;
40import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
41import uk.ac.ox.cs.pagoda.constraints.NullaryBottom;
42import uk.ac.ox.cs.pagoda.constraints.PredicateDependency;
43import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
44import uk.ac.ox.cs.pagoda.owl.OWLHelper;
45import uk.ac.ox.cs.pagoda.util.Utility;
46
47import org.semanticweb.simpleETL.SimpleETL;
48
49public abstract class Program implements KnowledgeBase {
50
51 protected String ontologyDirectory = null;
52 protected OWLOntology ontology;
53 protected DLOntology dlOntology;
54 protected BottomStrategy botStrategy;
55
56 private String additionalDataFile = null;
57
58 protected Collection<DLClause> clauses = new HashSet<DLClause>();
59// protected Set<DLClause> used = new HashSet<DLClause>();
60 protected PredicateDependency dependencyGraph;
61
62 /**
63 * clone all information of another program after load()
64 *
65 * @param program
66 */
67 void clone(Program program) {
68 this.ontologyDirectory = program.ontologyDirectory;
69 this.ontology = program.ontology;
70 this.dlOntology = program.dlOntology;
71 this.botStrategy = program.botStrategy;
72 this.additionalDataFile = program.additionalDataFile;
73 this.transitiveAxioms = program.transitiveAxioms;
74 this.transitiveClauses = program.transitiveClauses;
75 this.subPropChainAxioms = program.subPropChainAxioms;
76 this.subPropChainClauses = program.subPropChainClauses;
77 }
78
79 public void load(OWLOntology o, BottomStrategy botStrategy) {
80 this.botStrategy = botStrategy;
81 RLPlusOntology owlOntology = new RLPlusOntology();
82 owlOntology.load(o, new NullaryBottom());
83 owlOntology.simplify();
84
85 ontology = owlOntology.getTBox();
86 String ontologyPath = OWLHelper.getOntologyPath(ontology);
87 ontologyDirectory = ontologyPath.substring(0, ontologyPath.lastIndexOf(Utility.JAVA_FILE_SEPARATOR));
88 clausify();
89
90 String aboxOWLFile = owlOntology.getABoxPath();
91 OWLOntology abox = OWLHelper.loadOntology(aboxOWLFile);
92 OWLOntologyManager manager = abox.getOWLOntologyManager();
93 OWLAxiom axiom;
94 for (Atom atom: dlOntology.getPositiveFacts()) {
95 if ((axiom = OWLHelper.getABoxAssertion(manager.getOWLDataFactory(), atom)) != null)
96 manager.addAxiom(abox, axiom);
97 }
98
99 try {
100 FileOutputStream out = new FileOutputStream(aboxOWLFile);
101 manager.saveOntology(abox, out);
102 out.close();
103 } catch (OWLOntologyStorageException e) {
104 // TODO Auto-generated catch block
105 e.printStackTrace();
106 } catch (FileNotFoundException e) {
107 // TODO Auto-generated catch block
108 e.printStackTrace();
109 } catch (IOException e) {
110 // TODO Auto-generated catch block
111 e.printStackTrace();
112 }
113
114 if (!abox.isEmpty()) {
115 SimpleETL rewriter = new SimpleETL(owlOntology.getOntologyIRI(), aboxOWLFile);
116 try {
117 rewriter.rewrite();
118 } catch (Exception e) {
119 e.printStackTrace();
120 }
121 additionalDataFile = rewriter.getExportedFile();
122 new File(aboxOWLFile).delete();
123 }
124
125 }
126
127 private void clausify() {
128 Configuration conf = new Configuration();
129 OWLClausification clausifier = new OWLClausification(conf);
130 OWLOntology filteredOntology = null;
131 OWLOntologyManager manager = ontology.getOWLOntologyManager();
132 try {
133 filteredOntology = manager.createOntology();
134 } catch (OWLOntologyCreationException e) {
135 e.printStackTrace();
136 }
137
138 transitiveAxioms = new LinkedList<OWLTransitiveObjectPropertyAxiom>();
139 subPropChainAxioms = new LinkedList<OWLSubPropertyChainOfAxiom>();
140
141 OWLEntity date = ontology.getOWLOntologyManager().getOWLDataFactory().getOWLDatatype(IRI.create("http://www.w3.org/2001/XMLSchema#date"));
142 int noOfDataPropertyRangeAxioms = 0, noOfAxioms = 0;
143 for (OWLOntology onto: ontology.getImportsClosure())
144 for (OWLAxiom axiom: onto.getAxioms()) {
145 if (axiom instanceof OWLTransitiveObjectPropertyAxiom)
146 transitiveAxioms.add((OWLTransitiveObjectPropertyAxiom) axiom);
147 else if (axiom instanceof OWLSubPropertyChainOfAxiom)
148 subPropChainAxioms.add((OWLSubPropertyChainOfAxiom) axiom);
149 // TODO to filter out datatype axioms
150 else if (axiom instanceof OWLDataPropertyRangeAxiom) {
151 ++noOfDataPropertyRangeAxioms;
152 Utility.logInfo("The axiom: " + axiom + " is being ignored.");
153 }
154 else {
155 if (axiom.containsEntityInSignature(date)) {
156 Utility.logInfo("The axiom: " + axiom + " is being ignored.");
157 }
158 else manager.addAxiom(filteredOntology, axiom);
159 }
160
161 if (axiom instanceof OWLAnnotationAssertionAxiom ||
162 axiom instanceof OWLSubAnnotationPropertyOfAxiom ||
163 axiom instanceof OWLDeclarationAxiom ||
164 axiom instanceof OWLDataPropertyRangeAxiom) {
165 }
166 else {
167// System.out.println(axiom);
168 ++noOfAxioms;
169 }
170
171 }
172 Utility.logInfo("The number of data property range axioms that are ignored: " + noOfDataPropertyRangeAxioms + "(" + noOfAxioms + ")");
173
174 dlOntology = (DLOntology)clausifier.preprocessAndClausify(filteredOntology, null)[1];
175 clausifier = null;
176 }
177
178 public String getAdditionalDataFile() {
179 return additionalDataFile;
180 }
181
182 protected LinkedList<OWLTransitiveObjectPropertyAxiom> transitiveAxioms;
183 protected LinkedList<DLClause> transitiveClauses;
184
185 protected LinkedList<OWLSubPropertyChainOfAxiom> subPropChainAxioms;
186 protected LinkedList<DLClause> subPropChainClauses;
187
188 @Override
189 public void transform() {
190 for (DLClause dlClause: dlOntology.getDLClauses()) {
191 DLClause simplifiedDLClause = DLClauseHelper.removeNominalConcept(dlClause);
192 simplifiedDLClause = removeAuxiliaryBodyAtoms(simplifiedDLClause);
193 simplifiedDLClause = DLClauseHelper.replaceWithDataValue(simplifiedDLClause);
194 convert(simplifiedDLClause);
195 }
196
197 addingTransitiveAxioms();
198 addingSubPropertyChainAxioms();
199
200 Collection<DLClause> botRelated = new LinkedList<DLClause>();
201 Variable X = Variable.create("X");
202 botRelated.add(DLClause.create(new Atom[0], new Atom[] {Atom.create(Inequality.INSTANCE, X, X)}));
203 clauses.addAll(botStrategy.process(botRelated));
204
205 if (this instanceof GeneralProgram)
206 Utility.logInfo("The number of rules: " + (clauses.size() - 1));
207 }
208
209 private DLClause removeAuxiliaryBodyAtoms(DLClause dlClause) {
210 Collection<Atom> newBodyAtoms = new LinkedList<Atom>();
211 DLPredicate p;
212 for (Atom bodyAtom: dlClause.getBodyAtoms()) {
213 p = bodyAtom.getDLPredicate();
214 if (p instanceof AtomicConcept ||
215 p instanceof AtomicRole || p instanceof InverseRole ||
216 p instanceof Equality || p instanceof AnnotatedEquality || p instanceof Inequality)
217 newBodyAtoms.add(bodyAtom);
218 }
219 LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>();
220 Map<Variable, Term> assign = new HashMap<Variable, Term>();
221 for (Atom headAtom: dlClause.getHeadAtoms()) {
222 p = headAtom.getDLPredicate();
223 if (p instanceof AtomicNegationDataRange) {
224 AtomicDataRange positive = ((AtomicNegationDataRange) p).getNegatedDataRange();
225 if (!(positive instanceof ConstantEnumeration))
226 newBodyAtoms.add(Atom.create(positive, headAtom.getArgument(0)));
227 else if (((ConstantEnumeration) positive).getNumberOfConstants() == 1) {
228 assign.put((Variable) headAtom.getArgument(0), ((ConstantEnumeration) positive).getConstant(0));
229// newBodyAtoms.add(Atom.create(Equality.INSTANCE, headAtom.getArgument(0), ((ConstantEnumeration) positive).getConstant(0)));
230 }
231 else newHeadAtoms.add(headAtom);
232 }
233 else
234 newHeadAtoms.add(headAtom);
235 }
236
237 if (assign.isEmpty() && newHeadAtoms.isEmpty() && newBodyAtoms.size() == dlClause.getBodyLength())
238 return dlClause;
239
240 Atom[] headArray = newHeadAtoms.size() == dlClause.getHeadLength() ? dlClause.getHeadAtoms() : newHeadAtoms.toArray(new Atom[0]);
241 Atom[] bodyArray = newBodyAtoms.size() == dlClause.getBodyLength() ? dlClause.getBodyAtoms() : newBodyAtoms.toArray(new Atom[0]);
242 if (!assign.isEmpty()) {
243 for (int i = 0; i < headArray.length; ++i)
244 headArray[i] = DLClauseHelper.getInstance(headArray[i], assign);
245 for (int i = 0; i < bodyArray.length; ++i)
246 bodyArray[i] = DLClauseHelper.getInstance(bodyArray[i], assign);
247 }
248 return DLClause.create(headArray, bodyArray);
249 }
250
251 private void addingTransitiveAxioms() {
252 DLClause transitiveClause;
253 Atom headAtom;
254 Variable X = Variable.create("X"), Y = Variable.create("Y"), Z = Variable.create("Z");
255 transitiveClauses = new LinkedList<DLClause>();
256 for (OWLTransitiveObjectPropertyAxiom axiom: transitiveAxioms) {
257 OWLObjectPropertyExpression objExp = axiom.getProperty();
258 headAtom = getAtom(objExp, X, Z);
259 Atom[] bodyAtoms = new Atom[2];
260 bodyAtoms[0] = getAtom(objExp, X, Y);
261 bodyAtoms[1] = getAtom(objExp, Y, Z);
262 transitiveClause = DLClause.create(new Atom[] {headAtom}, bodyAtoms);
263 clauses.add(transitiveClause);
264 transitiveClauses.add(transitiveClause);
265 }
266 }
267
268 private Atom getAtom(OWLObjectPropertyExpression exp, Variable x, Variable y) {
269 if (exp instanceof OWLObjectProperty)
270 return Atom.create(AtomicRole.create(((OWLObjectProperty) exp).toStringID()), x, y);
271 OWLObjectInverseOf inverseOf;
272 if (exp instanceof OWLObjectInverseOf && (inverseOf = (OWLObjectInverseOf) exp).getInverse() instanceof OWLObjectProperty)
273 return Atom.create(AtomicRole.create(((OWLObjectProperty) inverseOf).toStringID()), x, y);
274 return null;
275 }
276
277 private void addingSubPropertyChainAxioms() {
278 DLClause dlClause;
279 subPropChainClauses = new LinkedList<DLClause>();
280 Atom headAtom;
281 Iterator<OWLObjectPropertyExpression> iterExp;
282 OWLObjectPropertyExpression objExp;
283 for (OWLSubPropertyChainOfAxiom axiom: subPropChainAxioms) {
284 objExp = axiom.getSuperProperty();
285 List<OWLObjectPropertyExpression> objs = axiom.getPropertyChain();
286 headAtom = getAtom(objExp, Variable.create("X"), Variable.create("X" + objs.size()));
287 iterExp = objs.iterator();
288 int index = 1;
289 Atom[] bodyAtoms = new Atom[objs.size()];
290 bodyAtoms[0] = getAtom(iterExp.next(), Variable.create("X"), Variable.create("X1"));
291 while (index < objs.size()) {
292 bodyAtoms[index] = getAtom(iterExp.next(), Variable.create("X" + index), Variable.create("X" + (index + 1)));
293 ++index;
294 }
295 dlClause = DLClause.create(new Atom[] {headAtom}, bodyAtoms);
296 clauses.add(dlClause);
297 subPropChainClauses.add(dlClause);
298 }
299 }
300
301 @Override
302 public void save() {
303 try {
304 BufferedWriter ruleWriter = new BufferedWriter(new OutputStreamWriter(
305 new FileOutputStream(getOutputPath())));
306 ruleWriter.write(toString());
307 ruleWriter.close();
308 } catch (IOException e) {
309 e.printStackTrace();
310 }
311 Utility.logDebug("The rules are saved in " + getOutputPath() + ".");
312 }
313
314 @Override
315 public String toString() {
316 return toString(clauses);
317 }
318
319 public static String toString(Collection<DLClause> clauses) {
320 StringBuilder sb = new StringBuilder(DLClauseHelper.toString(clauses));
321 sb.insert(0, MyPrefixes.PAGOdAPrefixes.prefixesText());
322 return sb.toString();
323 }
324
325 public final void convert(DLClause clause) {
326 Collection<DLClause> tempClauses = convert2Clauses(clause);
327 clauses.addAll(tempClauses);
328 }
329
330 public abstract Collection<DLClause> convert2Clauses(DLClause clause);
331
332 public abstract String getOutputPath();
333
334
335 public OWLOntology getOntology() {
336 return ontology;
337 }
338
339 public Collection<DLClause> getClauses() {
340 return clauses;
341 }
342
343 public Collection<DLClause> getClauses(DLClause queryClause) {
344// if (true) return new HashSet<DLClause>(clauses);
345 Set<DLPredicate> predicates = new HashSet<DLPredicate>();
346 predicates.addAll(dependencyGraph.collectPredicate(queryClause.getBodyAtoms()));
347
348 Set<DLPredicate> dependence = new HashSet<DLPredicate>();
349 for (DLPredicate predicate: predicates)
350 dependence.addAll(dependencyGraph.getAncesters(predicate));
351
352 Collection<DLClause> relevantClauses = new LinkedList<DLClause>();
353 for (DLClause clause: clauses) {
354 if (relevant(clause, dependence))
355 relevantClauses.add(clause);
356
357 }
358 return relevantClauses;
359 }
360
361 private boolean relevant(DLClause clause, Set<DLPredicate> set) {
362 for (DLPredicate p: dependencyGraph.collectPredicate(clause.getHeadAtoms()))
363 if (set.contains(p))
364 return true;
365 return false;
366 }
367
368 public PredicateDependency buildDependencyGraph() {
369 if (dependencyGraph == null)
370 return dependencyGraph = new PredicateDependency(clauses);
371 else
372 return dependencyGraph;
373 }
374
375 public void getDependencyGraph(PredicateDependency g) {
376 dependencyGraph = g;
377 }
378
379 public final String getDirectory() {
380 return Utility.TempDirectory;
381 }
382
383 public void deleteABoxTurtleFile() {
384 if (additionalDataFile != null)
385 new File(additionalDataFile).delete();
386 }
387
388}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java b/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java
new file mode 100644
index 0000000..a4cd790
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java
@@ -0,0 +1,46 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import java.util.Collection;
4import java.util.HashMap;
5import java.util.Map;
6
7import org.semanticweb.HermiT.model.DLClause;
8import org.semanticweb.HermiT.model.DLPredicate;
9
10
11public class UpperDatalogProgram extends UpperProgram {
12
13 public UpperDatalogProgram() {}
14
15// @Override
16// public String getDirectory() {
17// File dir = new File(ontologyDirectory + Utility.FILE_SEPARATOR + "datalog");
18// if (!dir.exists())
19// dir.mkdirs();
20// return dir.getPath();
21// }
22
23 @Override
24 protected void initApproximator() {
25 m_approx = new OverApproxBoth();
26 }
27
28 public int getBottomNumber() {
29 return botStrategy.getBottomNumber();
30 }
31
32 public void updateDependencyGraph(Collection<DLClause> delta) {
33 Map<DLPredicate, DLClause> map = new HashMap<DLPredicate, DLClause>();
34 for (DLClause clause: clauses)
35 if (botStrategy.isBottomRule(clause))
36 map.put(clause.getHeadAtom(0).getDLPredicate(), getCorrespondingClause(clause));
37
38 for (DLClause clause: delta) {
39 clauses.add(clause);
40 correspondence.put(clause, map.get(clause.getBodyAtom(0).getDLPredicate()));
41 }
42
43 dependencyGraph.update(delta);
44 }
45
46}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/UpperProgram.java b/src/uk/ac/ox/cs/pagoda/rules/UpperProgram.java
new file mode 100644
index 0000000..46f22e3
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/UpperProgram.java
@@ -0,0 +1,10 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3public abstract class UpperProgram extends ApproxProgram {
4
5 @Override
6 public String getOutputPath() {
7 return getDirectory() + "upper.dlog";
8 }
9
10}
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-06 09:39:39 +0000