1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
package uk.ac.ox.cs.pagoda.rules;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Set;
import org.semanticweb.HermiT.model.Atom;
import org.semanticweb.HermiT.model.DLClause;
import org.semanticweb.HermiT.model.DLPredicate;
import org.semanticweb.HermiT.model.Term;
import org.semanticweb.HermiT.model.Variable;
import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
public class OverApproxDisj implements Approximator {
@Override
public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
LinkedList<DLClause> distincts = new LinkedList<DLClause>();
Atom[] headAtoms = clause.getHeadAtoms(), bodyAtoms = clause.getBodyAtoms();
LinkedList<DLClause> newClauses = new LinkedList<DLClause>();
DLClause newClause;
if (headAtoms.length > 1) {
for (Atom headAtom: headAtoms) {
newClause = DLClause.create(new Atom[] {headAtom}, bodyAtoms);
newClauses.add(newClause);
// distincts.add(newClause);
}
for (DLClause cls: newClauses) {
newClause = DLClauseHelper.simplified(cls);
if (!isSubsumedBy(newClause, distincts))
distincts.add(newClause);
}
}
else distincts.add(clause);
return distincts;
}
public static boolean isSubsumedBy(DLClause newClause, Collection<DLClause> distinctClauses) {
Map<Variable, Term> unifier;
Set<Atom> bodyAtoms = new HashSet<Atom>();
for (DLClause clause: distinctClauses) {
if (newClause.getHeadLength() > 0 && clause.getHeadLength() > 0 &&
(unifier = isSubsumedBy(newClause.getHeadAtom(0), clause.getHeadAtom(0))) == null)
continue;
else
unifier = new HashMap<Variable, Term>();
for (Atom atom: clause.getBodyAtoms())
bodyAtoms.add(rename(atom, unifier));
unifier.clear();
for (Atom atom: newClause.getBodyAtoms())
if (!bodyAtoms.contains(atom))
continue;
return true;
}
return false;
}
public static Map<Variable, Term> isSubsumedBy(Atom atom1, Atom atom2) {
DLPredicate predicate = atom1.getDLPredicate();
if (!predicate.equals(atom2.getDLPredicate()))
return null;
Map<Variable, Term> unifier = new HashMap<Variable, Term>();
Term term1, term2;
for (int index = 0; index < predicate.getArity(); ++index) {
term1 = rename(atom1.getArgument(index), unifier);
term2 = rename(atom2.getArgument(index), unifier);
if (term1.equals(term2));
else if (term1 instanceof Variable)
unifier.put((Variable) term1, term2);
else
return null;
}
return unifier;
}
public static Atom rename(Atom atom, Map<Variable, Term> unifier) {
Term[] arguments = new Term[atom.getArity()];
for (int i = 0; i < atom.getArity(); ++i)
arguments[i] = rename(atom.getArgument(i), unifier);
return Atom.create(atom.getDLPredicate(), arguments);
}
public static Term rename(Term argument, Map<Variable, Term> unifier) {
Term newArg;
while ((newArg = unifier.get(argument)) != null)
return newArg;
return argument;
}
}
|
