From 9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8 Mon Sep 17 00:00:00 2001
From: yzhou <yujiao.zhou@gmail.com>
Date: Tue, 21 Apr 2015 10:34:27 +0100
Subject: initial version

---
 src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java | 103 +++++++++++++++++++++++
 1 file changed, 103 insertions(+)
 create mode 100644 src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java

(limited to 'src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java')

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;
+	}
+
+
+}
-- 
cgit v1.2.3