15 files changed, 195 insertions, 116 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java b/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java
index 3b9d6fc..acbf354 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java
@@ -1,27 +1,22 @@
 package uk.ac.ox.cs.pagoda.rules;
 
-import java.util.Collection;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Iterator;
-import java.util.Map;
-
 import org.semanticweb.HermiT.model.DLClause;
 import org.semanticweb.owlapi.model.OWLAxiom;
 import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom;
 import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom;
-
 import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
+
+import java.util.*;
 
 public abstract class ApproxProgram extends Program {
-        
+
+        protected Approximator m_approx = null;
         /**
          * mapping from over-approximated DLClauses to DLClauses from the original ontology
          */
         Map<DLClause, Object> correspondence = new HashMap<DLClause, Object>();
         
-        protected Approximator m_approx = null; 
-        
         protected ApproxProgram() { initApproximator(); }
         
         protected abstract void initApproximator(); 
@@ -76,7 +71,7 @@ public abstract class ApproxProgram extends Program {
 
         public OWLAxiom getEquivalentAxiom(DLClause clause) {
                 Object obj  = correspondence.get(clause);
-                while (obj != null && obj instanceof DLClause && !obj.equals(clause) && correspondence.containsKey((DLClause) obj))
+                while (obj != null && obj instanceof DLClause && !obj.equals(clause) && correspondence.containsKey(obj))
                         obj = correspondence.get(clause);
                 if (obj instanceof OWLAxiom) 
                         return (OWLAxiom) obj; 
@@ -98,14 +93,14 @@ public abstract class ApproxProgram extends Program {
 
 class ClauseSet extends HashSet<DLClause> {
 
-        public ClauseSet(DLClause first, DLClause second) {
-                add(first);  
-                add(second); 
-        }
-
         /**
-         * 
+         *
          */
         private static final long serialVersionUID = 1L;
-        
+
+        public ClauseSet(DLClause first, DLClause second) {
+                add(first);
+                add(second);
+        }
+
 }
\ No newline at end of file
diff --git a/src/uk/ac/ox/cs/pagoda/rules/Approximator.java b/src/uk/ac/ox/cs/pagoda/rules/Approximator.java
deleted file mode 100644
index 66e676b..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/Approximator.java
+++ /dev/null
@@ -1,62 +0,0 @@
-package uk.ac.ox.cs.pagoda.rules;
-
-import org.semanticweb.HermiT.model.AtLeast;
-import org.semanticweb.HermiT.model.Atom;
-import org.semanticweb.HermiT.model.DLClause;
-import org.semanticweb.HermiT.model.DLPredicate;
-
-import java.util.Collection;
-import java.util.LinkedList;
-
-public interface Approximator {
-
-        Collection<DLClause> convert(DLClause clause, DLClause originalClause);
-        
-}
-
-class IgnoreExist implements Approximator {
-                
-        @Override
-        public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
-                Collection<DLClause> ret = new LinkedList<DLClause>(); 
-                DLPredicate p; 
-                for (Atom headAtom: clause.getHeadAtoms()) {
-                        p = headAtom.getDLPredicate(); 
-                        if (p instanceof AtLeast) return ret; 
-                }
-                
-                ret.add(clause);
-                return ret; 
-        }
-        
-}
-
-class IgnoreBoth implements Approximator {
-        
-        @Override
-        public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
-                Collection<DLClause> ret = new LinkedList<DLClause>();
-                
-                if (clause.getHeadLength() > 1) return ret;
-                
-                if (clause.getHeadLength() > 0) {
-                        DLPredicate predicate = clause.getHeadAtom(0).getDLPredicate();
-                        
-                        if (predicate instanceof AtLeast) return ret; 
-                }
-                
-                ret.add(clause); 
-                return ret; 
-        }
-}
-
-class IgnoreDisj implements Approximator {
-        
-        @Override
-        public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
-                Collection<DLClause> ret = new LinkedList<DLClause>(); 
-                if (clause.getHeadLength() > 1) return ret;  
-                ret.add(clause); 
-                return ret; 
-        }
-}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java b/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java
index 6ebe666..d50c2d4 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java
@@ -1,10 +1,12 @@
 package uk.ac.ox.cs.pagoda.rules;
 
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+
 public class DisjunctiveProgram extends UpperProgram {
 
         @Override
         protected void initApproximator() {
-                m_approx = new OverApproxExist(); 
+                m_approx = new OverApproxExist();
         }
         
 //      @Override
diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
index 74c531f..7c9562f 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
@@ -2,6 +2,8 @@ package uk.ac.ox.cs.pagoda.rules;
 
 import org.semanticweb.HermiT.model.DLClause;
 import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator;
 
 import java.util.Collection;
 
diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java b/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java
index 64d018f..e825917 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java
@@ -1,5 +1,7 @@
 package uk.ac.ox.cs.pagoda.rules;
 
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxDisj;
+
 public class ExistentialProgram extends UpperProgram {
 
 //      @Override
@@ -12,7 +14,7 @@ public class ExistentialProgram extends UpperProgram {
 
         @Override
         protected void initApproximator() {
-                m_approx = new OverApproxDisj();                
+                m_approx = new OverApproxDisj();
         }
 
 }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java b/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java
index ebe0b7d..2098f73 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java
@@ -1,19 +1,17 @@
 package uk.ac.ox.cs.pagoda.rules;
 
+import org.semanticweb.HermiT.model.*;
+import org.semanticweb.owlapi.model.OWLObjectProperty;
+import org.semanticweb.owlapi.model.OWLOntology;
+import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
+import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+
 import java.util.Collection;
 import java.util.HashSet;
 import java.util.LinkedList;
 import java.util.Set;
 
-import org.semanticweb.HermiT.model.AtLeastConcept;
-import org.semanticweb.HermiT.model.Atom;
-import org.semanticweb.HermiT.model.AtomicRole;
-import org.semanticweb.HermiT.model.DLClause;
-import org.semanticweb.HermiT.model.DLPredicate;
-import org.semanticweb.owlapi.model.OWLObjectProperty;
-import org.semanticweb.owlapi.model.OWLOntology;
-import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
-
 public class ExistentialToDisjunctive extends UpperProgram {
         
         Set<String> inverseFuncProperties = new HashSet<String>(); 
diff --git a/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java b/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java
index a664ba1..199d167 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java
@@ -10,6 +10,7 @@ import uk.ac.ox.cs.pagoda.constraints.UnaryBottom;
 import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom;
 import uk.ac.ox.cs.pagoda.multistage.Normalisation;
 import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication;
+import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
 
@@ -106,7 +107,26 @@ public class LowerDatalogProgram extends ApproxProgram implements IncrementalPro
         
         @Override
         protected void initApproximator() {
-                m_approx = new IgnoreBoth(); 
+                m_approx = new IgnoreBoth();
+        }
+
+        private class IgnoreBoth implements Approximator {
+
+                @Override
+                public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+                        Collection<DLClause> ret = new LinkedList<DLClause>();
+
+                        if (clause.getHeadLength() > 1) return ret;
+
+                        if (clause.getHeadLength() > 0) {
+                                DLPredicate predicate = clause.getHeadAtom(0).getDLPredicate();
+
+                                if (predicate instanceof AtLeast) return ret;
+                        }
+
+                        ret.add(clause);
+                        return ret;
+                }
         }
 
 }
@@ -116,15 +136,13 @@ class ClassifyThread extends Thread {
         IncrementalProgram m_program; 
         Collection<DLClause> clauses = new LinkedList<DLClause>(); 
         
-        Variable X = Variable.create("X"), Y = Variable.create("Y"); 
-        
+        Variable X = Variable.create("X"), Y = Variable.create("Y");
+        Reasoner hermitReasoner;
+        OWLOntology ontology;
         ClassifyThread(IncrementalProgram program) {
                 m_program = program;
         }
         
-        Reasoner hermitReasoner;
-        OWLOntology ontology; 
-        
         @Override
         public void run() {
                 ontology = m_program.getOntology();
@@ -215,5 +233,4 @@ class ClassifyThread extends Thread {
         private Atom getAtom(OWLClass c) {
                 return Atom.create(AtomicConcept.create(c.toStringID()), X);
         }
-
 }
\ No newline at end of file
diff --git a/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java b/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java
index a4cd790..611e183 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java
@@ -1,12 +1,13 @@
 package uk.ac.ox.cs.pagoda.rules;
 
+import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.HermiT.model.DLPredicate;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxBoth;
+
 import java.util.Collection;
 import java.util.HashMap;
 import java.util.Map;
 
-import org.semanticweb.HermiT.model.DLClause;
-import org.semanticweb.HermiT.model.DLPredicate;
-
 
 public class UpperDatalogProgram extends UpperProgram {
         
@@ -22,7 +23,7 @@ public class UpperDatalogProgram extends UpperProgram {
 
         @Override
         protected void initApproximator() {
-                m_approx = new OverApproxBoth();                
+                m_approx = new OverApproxBoth();
         }
 
         public int getBottomNumber() {
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java
new file mode 100644
index 0000000..f910c64
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java
@@ -0,0 +1,42 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.DLClause;
+
+import java.util.Collection;
+
+public interface Approximator {
+
+    Collection<DLClause> convert(DLClause clause, DLClause originalClause);
+
+}
+
+// TODO remove
+//class IgnoreExist implements Approximator {
+//
+//      @Override
+//      public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+//              Collection<DLClause> ret = new LinkedList<DLClause>();
+//              DLPredicate p;
+//              for (Atom headAtom: clause.getHeadAtoms()) {
+//                      p = headAtom.getDLPredicate();
+//                      if (p instanceof AtLeast) return ret;
+//              }
+//
+//              ret.add(clause);
+//              return ret;
+//      }
+//
+//}
+//
+//
+//
+//class IgnoreDisj implements Approximator {
+//
+//      @Override
+//      public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+//              Collection<DLClause> ret = new LinkedList<DLClause>();
+//              if (clause.getHeadLength() > 1) return ret;
+//              ret.add(clause);
+//              return ret;
+//      }
+//}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
index 284edd2..8fc6b77 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -1,7 +1,8 @@
-package uk.ac.ox.cs.pagoda.rules;
+package uk.ac.ox.cs.pagoda.rules.approximators;
 
 import org.semanticweb.HermiT.model.DLClause;
 import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
 
 import java.util.*;
 
@@ -62,6 +63,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
 
     private DLClause getInstantiatedSkolemisation(DLClause clause, DLClause originalClause, AnswerTupleID violationTuple) {
         // TODO implement
+        // filter the violation tuples appearing on both the sides of the rule
         return null;
     }
 
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java
index 3cc2aba..ae2a2cf 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java
@@ -1,11 +1,11 @@
-package uk.ac.ox.cs.pagoda.rules;
-
-import java.util.Collection;
-import java.util.LinkedList;
+package uk.ac.ox.cs.pagoda.rules.approximators;
 
 import org.semanticweb.HermiT.model.AtLeastDataRange;
 import org.semanticweb.HermiT.model.DLClause;
 
+import java.util.Collection;
+import java.util.LinkedList;
+
 public class OverApproxBoth implements Approximator {
         
         Approximator approxDist = new OverApproxDisj(), approxExist = new OverApproxExist();
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java
index 5b298e8..05d9442 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java
@@ -1,4 +1,4 @@
-package uk.ac.ox.cs.pagoda.rules;
+package uk.ac.ox.cs.pagoda.rules.approximators;
 
 import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
@@ -88,7 +88,7 @@ public class OverApproxDisj implements Approximator {
                         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) 
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
index 1099acf..e0bafe0 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
@@ -1,4 +1,4 @@
-package uk.ac.ox.cs.pagoda.rules;
+package uk.ac.ox.cs.pagoda.rules.approximators;
 
 import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
@@ -11,9 +11,11 @@ public class OverApproxExist implements Approximator {
         public static final String negativeSuffix = "_neg";
         public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
         private static final Variable X = Variable.create("X");
+        //DEBUG
+        public static Collection<String> createdIndividualIRIs = new HashSet<>();
         private static int individualCounter = 0;
         private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>();
-        
+
         private static int noOfExistential(DLClause originalClause) {
                 int no = 0;
                 for (Atom atom: originalClause.getHeadAtoms())
@@ -42,7 +44,7 @@ public class OverApproxExist implements Approximator {
                 }
                 return -1;
         }
-        
+
         public static AtomicConcept getNegationConcept(DLPredicate p) {
                 if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING;
                 if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING;
@@ -66,15 +68,19 @@ public class OverApproxExist implements Approximator {
         public static int getNumberOfSkolemisedIndividual() {
                 return individualCounter;
         }
-        
+        //DEBUG
+
         public static Individual getNewIndividual(DLClause originalClause, int offset) {
                 Individual ret;
+                int individualID;
                 if (individualNumber.containsKey(originalClause)) {
-                        ret = Individual.create(skolemisedIndividualPrefix + (individualNumber.get(originalClause) + offset));
+                        individualID = individualNumber.get(originalClause) + offset;
+                        ret = Individual.create(skolemisedIndividualPrefix + individualID);
                 }
                 else {
                         individualNumber.put(originalClause, individualCounter);
-                        ret = Individual.create(skolemisedIndividualPrefix + (individualCounter + offset));
+                        individualID = individualCounter + offset;
+                        ret = Individual.create(skolemisedIndividualPrefix + individualID);
                         individualCounter += noOfExistential(originalClause);
                 }
                 return ret;
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java
new file mode 100644
index 0000000..a920ec5
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java
@@ -0,0 +1,74 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.AtLeast;
+import org.semanticweb.HermiT.model.Atom;
+import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.HermiT.model.Individual;
+import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * If you need a Skolem term (i.e. fresh individual), ask this class.
+ */
+public class SkolemTermsDispenser {
+
+    public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
+    private static SkolemTermsDispenser skolemTermsDispenser;
+    private int individualCounter = 0;
+    private Map<DLClause, Integer> termNumber = new HashMap<>();
+    private Map<SkolemTermId, Integer> mapTermToDepth = new HashMap<>();
+    private int dependenciesCounter = 0;
+    private Map<AnswerTupleID, Integer> mapDependencyToId = new HashMap<>();
+
+    private SkolemTermsDispenser() {
+    }
+
+    public static SkolemTermsDispenser getInstance() {
+        if (skolemTermsDispenser == null) skolemTermsDispenser = new SkolemTermsDispenser();
+        return skolemTermsDispenser;
+    }
+
+    private int getDependencyId(AnswerTupleID answerTupleID) {
+        if (mapDependencyToId.containsKey(answerTupleID)) return mapDependencyToId.get(answerTupleID);
+        else return mapDependencyToId.put(answerTupleID, dependenciesCounter++);
+    }
+
+    public Individual getNewIndividual(DLClause originalClause, int offset, AnswerTupleID dependency) {
+        if (!termNumber.containsKey(originalClause)) {
+            termNumber.put(originalClause, individualCounter);
+            individualCounter += noOfExistential(originalClause);
+        }
+        if (!mapDependencyToId.containsKey(dependency)) {
+            mapDependencyToId.put(dependency, dependenciesCounter++);
+        }
+
+        SkolemTermId termId = new SkolemTermId(termNumber.get(originalClause) + offset, getDependencyId(dependency));
+        return Individual.create(skolemisedIndividualPrefix + termId);
+    }
+
+    private int noOfExistential(DLClause originalClause) {
+        int no = 0;
+        for (Atom atom : originalClause.getHeadAtoms())
+            if (atom.getDLPredicate() instanceof AtLeast)
+                no += ((AtLeast) atom.getDLPredicate()).getNumber();
+        return no;
+    }
+
+    private class SkolemTermId {
+        private final int idBase;
+        private final int idOffset;
+
+        private SkolemTermId(int idBase, int idOffset) {
+            this.idBase = idBase;
+            this.idOffset = idOffset;
+        }
+
+        @Override
+        public String toString() {
+            return idBase + "_" + idOffset;
+        }
+    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
index 63057c4..1a729e5 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
@@ -1,4 +1,4 @@
-package uk.ac.ox.cs.pagoda.rules;
+package uk.ac.ox.cs.pagoda.rules.approximators;
 
 import org.semanticweb.HermiT.model.DLClause;
 import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;