Implementing Limited Skolemisation, in particular SkolemTermsDispenser.

1 files changed, 59 insertions, 79 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java b/src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java
index b201918..70f841f 100644
--- a/src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java
+++ b/src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java
@@ -1,155 +1,135 @@
 package uk.ac.ox.cs.pagoda.constraints;
 
-import java.util.Collection;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.LinkedList;
-import java.util.Map;
-import java.util.Queue;
-import java.util.Set;
-
-import org.semanticweb.HermiT.model.AnnotatedEquality;
-import org.semanticweb.HermiT.model.AtLeastConcept;
-import org.semanticweb.HermiT.model.AtLeastDataRange;
-import org.semanticweb.HermiT.model.Atom;
-import org.semanticweb.HermiT.model.AtomicConcept;
-import org.semanticweb.HermiT.model.AtomicNegationConcept;
-import org.semanticweb.HermiT.model.AtomicRole;
-import org.semanticweb.HermiT.model.DLClause;
-import org.semanticweb.HermiT.model.DLPredicate;
-import org.semanticweb.HermiT.model.Equality;
-import org.semanticweb.HermiT.model.Inequality;
-import org.semanticweb.HermiT.model.InverseRole;
-
-import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
+import org.semanticweb.HermiT.model.*;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 import uk.ac.ox.cs.pagoda.util.Utility;
 
+import java.util.*;
+
 
 public class PredicateDependency extends DependencyGraph<DLPredicate> {
-        
-        Collection<DLClause> m_clauses; 
-        Map<PredicatePair, LinkedList<DLClause>> edgeLabels = new HashMap<PredicatePair, LinkedList<DLClause>>();  
-                
+
+        private static final DLPredicate equality = AtomicRole.create(Namespace.EQUALITY);
+        private static final DLPredicate inequality = AtomicRole.create(Namespace.INEQUALITY);
+        Collection<DLClause> m_clauses;
+        Map<PredicatePair, LinkedList<DLClause>> edgeLabels = new HashMap<PredicatePair, LinkedList<DLClause>>();
+        Set<DLPredicate> reachableToBottom = null;
+
         public PredicateDependency(Collection<DLClause> clauses) {
                 m_clauses = clauses;
-                build(); 
+                build();
         }
 
         @Override
         protected void build() {
                 update(m_clauses);
-                
+
                 addLink(equality, AtomicConcept.NOTHING);
                 addLink(inequality, AtomicConcept.NOTHING);
         }
-        
+
         private void addEdgeLabel(DLPredicate body, DLPredicate head, DLClause clause) {
-                PredicatePair key = new PredicatePair(body, head); 
-                LinkedList<DLClause> value; 
-                if ((value = edgeLabels.get(key)) == null) 
-                        edgeLabels.put(key, value = new LinkedList<DLClause>()); 
+                PredicatePair key = new PredicatePair(body, head);
+                LinkedList<DLClause> value;
+                if ((value = edgeLabels.get(key)) == null)
+                        edgeLabels.put(key, value = new LinkedList<DLClause>());
                 value.add(clause);
         }
 
         private void addLinks4Negation(AtomicConcept c, DLClause clause) {
                 addLink(c, AtomicConcept.NOTHING);
                 addEdgeLabel(c, AtomicConcept.NOTHING, clause);
-                String iri = c.getIRI(); 
+                String iri = c.getIRI();
                 addLink(c = AtomicConcept.create(iri.substring(0, iri.length() - 4)), AtomicConcept.NOTHING);
                 addEdgeLabel(c, AtomicConcept.NOTHING, clause);
         }
 
         public Set<DLPredicate> collectPredicate(Atom[] atoms) {
                 Set<DLPredicate> predicates = new HashSet<DLPredicate>();
-                for (Atom atom: atoms) 
-                        predicates.addAll(getAtomicPredicates(atom.getDLPredicate())); 
+                for (Atom atom : atoms)
+                        predicates.addAll(getAtomicPredicates(atom.getDLPredicate()));
                 return predicates;
         }
-
-        private static final DLPredicate equality = AtomicRole.create(Namespace.EQUALITY); 
-        private static final DLPredicate inequality = AtomicRole.create(Namespace.INEQUALITY);
         
         private Set<DLPredicate> getAtomicPredicates(DLPredicate predicate) {
-                Set<DLPredicate> predicates = new HashSet<DLPredicate>(); 
+                Set<DLPredicate> predicates = new HashSet<DLPredicate>();
                 if (predicate instanceof AtLeastConcept)
                         predicates.addAll(getAtomicPredicates((AtLeastConcept) predicate));
                 else {
-                        if ((predicate = getAtomicPredicate(predicate)) != null) 
+                        if ((predicate = getAtomicPredicate(predicate)) != null)
                                 predicates.add(predicate);
                 }
-                return predicates; 
+                return predicates;
         }
         
         private Set<DLPredicate> getAtomicPredicates(AtLeastConcept alc) {
                 Set<DLPredicate> set = new HashSet<DLPredicate>();
-                if (alc.getOnRole() instanceof AtomicRole) 
-                        set.add((AtomicRole) alc.getOnRole()); 
-                else 
+                if (alc.getOnRole() instanceof AtomicRole)
+                        set.add((AtomicRole) alc.getOnRole());
+                else
                         set.add(((InverseRole) alc.getOnRole()).getInverseOf());
-                
-                if (alc.getToConcept() instanceof AtomicConcept) 
-                        if (alc.getToConcept().equals(AtomicConcept.THING)); 
-                        else set.add((AtomicConcept) alc.getToConcept()); 
-                else 
+
+                if (alc.getToConcept() instanceof AtomicConcept)
+                        if (alc.getToConcept().equals(AtomicConcept.THING)) ;
+                        else set.add((AtomicConcept) alc.getToConcept());
+                else
                         set.add(OverApproxExist.getNegationConcept(((AtomicNegationConcept) alc.getToConcept()).getNegatedAtomicConcept()));
-                return set; 
+                return set;
         }
         
         private DLPredicate getAtomicPredicate(DLPredicate p) {
                 if (p instanceof Equality || p instanceof AnnotatedEquality)
                         return equality;
                 if (p instanceof Inequality)
-                        return inequality; 
+                        return inequality;
                 if (p instanceof AtomicConcept)
-                        if (p.equals(AtomicConcept.THING)) 
+                        if (p.equals(AtomicConcept.THING))
                                 return null;
-                        else return p; 
+                        else return p;
                 if (p instanceof AtomicRole)
-                        return p; 
+                        return p;
                 if (p instanceof AtLeastDataRange) {
-                        AtLeastDataRange aldr = (AtLeastDataRange) p; 
-                        if (aldr.getOnRole() instanceof AtomicRole) 
-                                return (AtomicRole) aldr.getOnRole(); 
-                        else 
-                                return ((InverseRole) aldr.getOnRole()).getInverseOf(); 
+                        AtLeastDataRange aldr = (AtLeastDataRange) p;
+                        if (aldr.getOnRole() instanceof AtomicRole)
+                                return (AtomicRole) aldr.getOnRole();
+                        else
+                                return ((InverseRole) aldr.getOnRole()).getInverseOf();
                 }
                 Utility.logDebug("Unknown DLPredicate in PredicateDependency: " + p);
-                return null; 
+                return null;
         }
         
         public Set<DLClause> pathTo(DLPredicate p) {
-                Set<DLClause> rules = new HashSet<DLClause>(); 
-                Set<DLPredicate> visited = new HashSet<DLPredicate>(); 
-                
-                Queue<DLPredicate> queue = new LinkedList<DLPredicate>(); 
-                queue.add(p); 
+                Set<DLClause> rules = new HashSet<DLClause>();
+                Set<DLPredicate> visited = new HashSet<DLPredicate>();
+
+                Queue<DLPredicate> queue = new LinkedList<DLPredicate>();
+                queue.add(p);
                 visited.add(p);
-                
-                Set<DLPredicate> edge; 
-                Collection<DLClause> clauses; 
-                
+
+                Set<DLPredicate> edge;
+                Collection<DLClause> clauses;
+
                 while (!queue.isEmpty()) {
                         if ((edge = reverseEdges.get(p = queue.poll())) != null) {
                                 for (DLPredicate pred: edge) {
                                         if (!visited.contains(pred)) {
-                                                queue.add(pred); 
-                                                visited.add(pred); 
+                                                queue.add(pred);
+                                                visited.add(pred);
                                         }
-                                        clauses = edgeLabelsBetween(pred, p); 
-                                        if (clauses != null) rules.addAll(clauses); 
+                                        clauses = edgeLabelsBetween(pred, p);
+                                        if (clauses != null) rules.addAll(clauses);
                                 }
                         }
                 }
-                return rules; 
+                return rules;
         }
-        
+
         private LinkedList<DLClause> edgeLabelsBetween(DLPredicate p, DLPredicate q) {
                 PredicatePair pair = new PredicatePair(p, q);
-                return edgeLabels.get(pair); 
+                return edgeLabels.get(pair);
         }
-
-        Set<DLPredicate> reachableToBottom = null; 
         
         public Set<DLClause> pathToBottom(DLPredicate p) {
                 if (reachableToBottom == null) {