1 files changed, 103 insertions, 0 deletions

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 @@
+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;
+        }
+
+
+}