Implementing Limited Skolemisation, in particular SkolemTermsDispenser.

5 files changed, 35 insertions, 101 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
index cee829f..331ad12 100644
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
+++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
@@ -1,30 +1,14 @@
 package uk.ac.ox.cs.pagoda.tracking;
 
-import java.util.Collection;
-import java.util.Collections;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Iterator;
-import java.util.LinkedList;
-import java.util.Map;
-
-import org.semanticweb.HermiT.model.AnnotatedEquality;
-import org.semanticweb.HermiT.model.AtLeastConcept;
-import org.semanticweb.HermiT.model.Atom;
-import org.semanticweb.HermiT.model.AtomicConcept;
-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.Individual;
-import org.semanticweb.HermiT.model.Inequality;
-
+import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
 import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
-import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
 import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 
+import java.util.*;
+
 public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap {
 
         public TrackingRuleEncoderDisj(UpperDatalogProgram program, BasicQueryEngine store) {
diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java
index e72ed96..d6b5e8b 100644
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java
+++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java
@@ -1,26 +1,14 @@
 package uk.ac.ox.cs.pagoda.tracking;
 
-import java.util.LinkedList;
-
-import org.semanticweb.HermiT.model.AtLeastConcept;
-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.Individual;
-import org.semanticweb.HermiT.model.Inequality;
-import org.semanticweb.HermiT.model.InverseRole;
-import org.semanticweb.HermiT.model.Term;
-import org.semanticweb.HermiT.model.Variable;
-
+import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.MyPrefixes;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
 import uk.ac.ox.cs.pagoda.multistage.Normalisation;
 import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
-import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
 import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+
+import java.util.LinkedList;
 
 public class TrackingRuleEncoderDisj1 extends TrackingRuleEncoderDisj {
 
diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java
index 6cf239f..8d79090 100644
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java
+++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java
@@ -1,24 +1,12 @@
 package uk.ac.ox.cs.pagoda.tracking;
 
-import org.semanticweb.HermiT.model.AtLeastConcept;
-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.Individual;
-import org.semanticweb.HermiT.model.Inequality;
-import org.semanticweb.HermiT.model.InverseRole;
-import org.semanticweb.HermiT.model.Term;
-import org.semanticweb.HermiT.model.Variable;
-
+import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.MyPrefixes;
 import uk.ac.ox.cs.pagoda.multistage.Normalisation;
 import uk.ac.ox.cs.pagoda.query.QueryRecord;
 import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
-import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
 import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
 
 public class TrackingRuleEncoderDisj2 extends TrackingRuleEncoderDisj {
 
@@ -56,7 +44,7 @@ public class TrackingRuleEncoderDisj2 extends TrackingRuleEncoderDisj {
         
         @Override
         protected DLPredicate generateAuxiliaryRule(AtLeastConcept p, DLClause original, Individual[] individuals) {
-                DLPredicate ret = AtomicConcept.create(getTrackingPredicate(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p, individuals))); 
+                DLPredicate ret = AtomicConcept.create(getTrackingPredicate(Normalisation.getAuxiliaryConcept4Disjunct(p, individuals)));
                 Atom[] headAtom = new Atom[] {Atom.create(ret, X)};
                 
                 AtomicRole role = p.getOnRole() instanceof AtomicRole ? 
diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
index 37116d4..2143b03 100644
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
+++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
@@ -1,34 +1,20 @@
 package uk.ac.ox.cs.pagoda.tracking;
 
-import java.util.Collection;
-import java.util.HashSet;
-import java.util.LinkedList;
-import java.util.Set;
-
-import org.semanticweb.HermiT.model.AnnotatedEquality;
-import org.semanticweb.HermiT.model.AtLeast;
-import org.semanticweb.HermiT.model.AtLeastConcept;
-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.DatatypeRestriction;
-import org.semanticweb.HermiT.model.Equality;
-import org.semanticweb.HermiT.model.Inequality;
-import org.semanticweb.HermiT.model.InverseRole;
-import org.semanticweb.HermiT.model.Variable;
-
+import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.MyPrefixes;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
 import uk.ac.ox.cs.pagoda.multistage.Normalisation;
 import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
-import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
 import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
+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.Collection;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.Set;
+
 public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
 
         public TrackingRuleEncoderDisjVar1(UpperDatalogProgram program, BasicQueryEngine store) {
@@ -96,13 +82,13 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
                         return Atom.create(getTrackingDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); 
                 }
                 if (p instanceof AtomicConcept) 
-                        return Atom.create(getTrackingDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); 
+                        return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0));
                 if (p instanceof AtomicRole) 
-                        return Atom.create(getTrackingDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1));
+                        return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
                 if (p instanceof Equality || p instanceof AnnotatedEquality) 
                         return Atom.create(getTrackingDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 
                 if (p instanceof Inequality) 
-                        return Atom.create(getTrackingDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); 
+                        return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
 
                 return null;
         }
@@ -114,15 +100,15 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
                         return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); 
                 }
                 if (p instanceof AtomicConcept) 
-                        return Atom.create(getGapDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); 
+                        return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
                 if (p instanceof AtomicRole) 
-                        return Atom.create(getGapDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1));
+                        return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
                 if (p instanceof Equality || p instanceof AnnotatedEquality) 
                         return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 
                 if (p instanceof Inequality) 
-                        return Atom.create(getGapDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); 
+                        return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
                 if (p instanceof DatatypeRestriction)
-                        return Atom.create(getGapDLPredicate((DatatypeRestriction) p), headAtom.getArgument(0)); 
+                        return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
                 Utility.logError(p + " is not recognised.");
                 return null;
         }
diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java
index d257de3..7311a86 100644
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java
+++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java
@@ -1,31 +1,19 @@
 package uk.ac.ox.cs.pagoda.tracking;
 
-import java.util.Collection;
-import java.util.HashSet;
-import java.util.LinkedList;
-import java.util.Set;
-
-import org.semanticweb.HermiT.model.AnnotatedEquality;
-import org.semanticweb.HermiT.model.AtLeastConcept;
-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 org.semanticweb.HermiT.model.Variable;
-
+import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
 import uk.ac.ox.cs.pagoda.multistage.Normalisation;
 import uk.ac.ox.cs.pagoda.query.QueryRecord;
 import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
-import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
 import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.Set;
+
 public class TrackingRuleEncoderDisjVar2 extends TrackingRuleEncoderWithGap {
 
         public TrackingRuleEncoderDisjVar2(UpperDatalogProgram program, BasicQueryEngine store) {
@@ -91,13 +79,13 @@ public class TrackingRuleEncoderDisjVar2 extends TrackingRuleEncoderWithGap {
                         return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); 
                 }
                 if (p instanceof AtomicConcept) 
-                        return Atom.create(getGapDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); 
+                        return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
                 if (p instanceof AtomicRole) 
-                        return Atom.create(getGapDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1));
+                        return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
                 if (p instanceof Equality || p instanceof AnnotatedEquality) 
                         return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 
                 if (p instanceof Inequality) 
-                        return Atom.create(getGapDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); 
+                        return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
 
                 return null;
         }