aboutsummaryrefslogtreecommitdiff
path: root/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java
diff options
context:
space:
mode:
Diffstat (limited to 'src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java')
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java100
1 files changed, 0 insertions, 100 deletions
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java
deleted file mode 100644
index 5b298e8..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java
+++ /dev/null
@@ -1,100 +0,0 @@
1package uk.ac.ox.cs.pagoda.rules;
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}