Fast implementation of all the other things to get something working, but it doesn't.

9 files changed, 184 insertions, 61 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java b/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java
index f729158..b548d39 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java
@@ -2,7 +2,6 @@ package uk.ac.ox.cs.pagoda.multistage;
 
 
 import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
-import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
 import uk.ac.ox.cs.pagoda.rules.Program;
 import uk.ac.ox.cs.pagoda.rules.approximators.LimitedSkolemisationApproximator;
 
@@ -12,6 +11,6 @@ public class LimitedSkolemisationApplication extends RestrictedApplication {
 
     public LimitedSkolemisationApplication(Program program, BottomStrategy upperBottom) {
         super(program, upperBottom);
-        m_approxExist = new LimitedSkolemisationApproximator(MAX_DEPTH, new ExistConstantApproximator());
+        m_approxExist = new LimitedSkolemisationApproximator(MAX_DEPTH);
     }
 }
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
index f0f631a..f80da5f 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
@@ -55,6 +55,18 @@ public class MultiStageQueryEngine extends StageQueryEngine {
                 treatment.dispose();
                 return ret; 
         }
+
+        /**
+         * delta-chase
+         */
+        @Override
+        public int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap) {
+                materialise("lower program", dProgram.getLower().toString());
+                Program generalProgram = dProgram.getGeneral();
+                LimitedSkolemisationApplication program = new LimitedSkolemisationApplication(generalProgram, dProgram.getUpperBottomStrategy());
+                Treatment treatment = new Pick4NegativeConceptNaive(this, program);
+                return materialise(program, treatment, gap);
+        }
         
         private int materialise(MultiStageUpperProgram program, Treatment treatment, GapByStore4ID gap) {
                 if (gap != null) 
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java
index 5d2e0d1..84798ce 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java
@@ -18,8 +18,10 @@ public abstract class StageQueryEngine extends BasicQueryEngine {
 
         public abstract void materialiseFoldedly(DatalogProgram dProgram, GapByStore4ID gap); 
         
-        public abstract int materialiseRestrictedly(DatalogProgram dProgram, GapByStore4ID gap); 
-        
+        public abstract int materialiseRestrictedly(DatalogProgram dProgram, GapByStore4ID gap);
+
+        public abstract int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap);
+
         public void dispose() {
                 super.dispose();
         }
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java
index b7f989f..29cf23a 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java
@@ -1,14 +1,8 @@
 package uk.ac.ox.cs.pagoda.multistage;
 
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.IOException;
-import java.util.Collection;
-
 import org.openrdf.rio.RDFHandlerException;
 import org.openrdf.rio.RDFParseException;
 import org.openrdf.rio.turtle.TurtleParser;
-
 import uk.ac.ox.cs.JRDFox.JRDFStoreException;
 import uk.ac.ox.cs.JRDFox.model.Individual;
 import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
@@ -17,6 +11,11 @@ import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
 
+import java.io.FileInputStream;
+import java.io.FileNotFoundException;
+import java.io.IOException;
+import java.util.Collection;
+
 public class TwoStageQueryEngine extends StageQueryEngine {
         
         IndividualCollector m_collector = new IndividualCollector();
@@ -64,6 +63,11 @@ public class TwoStageQueryEngine extends StageQueryEngine {
                 return program.materialise();
         }
 
+        @Override
+        public int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap) {
+                throw new UnsupportedOperationException("This method is not available in " + getClass());
+        }
+
         public void materialise(String programText,     GapByStore4ID gap, boolean incrementally) {
                 try {
                         if (gap != null) {
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
index 9b862ce..d179d14 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
@@ -1,7 +1,5 @@
 package uk.ac.ox.cs.pagoda.reasoner;
 
-import java.util.LinkedList;
-
 import org.semanticweb.HermiT.model.Atom;
 import org.semanticweb.HermiT.model.AtomicConcept;
 import org.semanticweb.HermiT.model.DLClause;
@@ -9,7 +7,9 @@ import org.semanticweb.HermiT.model.Variable;
 import org.semanticweb.owlapi.model.OWLOntology;
 import org.semanticweb.owlapi.model.OWLOntologyCreationException;
 import org.semanticweb.owlapi.model.OWLOntologyManager;
-
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.store.DataStore;
+import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
 import uk.ac.ox.cs.pagoda.query.AnswerTuples;
 import uk.ac.ox.cs.pagoda.query.QueryManager;
@@ -21,9 +21,8 @@ import uk.ac.ox.cs.pagoda.tracking.QueryTracker;
 import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoder;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
-import uk.ac.ox.cs.JRDFox.JRDFStoreException;
-import uk.ac.ox.cs.JRDFox.store.DataStore;
-import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType;
+
+import java.util.LinkedList;
 
 public class ConsistencyManager {
 
@@ -85,6 +84,23 @@ public class ConsistencyManager {
                 }
                 return false; 
         }
+
+        boolean checkSkolemUpper() {
+                if (m_reasoner.limitedSkolemUpperStore != null) {
+                        AnswerTuples tuples = null;
+                        try {
+                                tuples = m_reasoner.limitedSkolemUpperStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables());
+                                if (!tuples.isValid()) {
+                                        Utility.logInfo("There are no contradictions derived in the limited-skolem upper bound materialisation.");
+                                        return satisfiability(t.duration());
+                                }
+                        }
+                        finally {
+                                if (tuples != null) tuples.dispose();
+                        }
+                }
+                return false;
+        }
         
         boolean check() {
 //              if (!checkRLLowerBound()) return false; 
@@ -288,5 +304,6 @@ public class ConsistencyManager {
         public QueryRecord[] getQueryRecords() {
                 return botQueryRecords; 
         }
-        
+
+
 }
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
index 3c0a001..233963e 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -49,7 +49,8 @@ public class MyQueryReasoner extends QueryReasoner {
         private Collection<String> predicatesWithGap = null;
         private Boolean satisfiable;
         private ConsistencyManager consistency = new ConsistencyManager(this);
-        
+        BasicQueryEngine limitedSkolemUpperStore;
+
         public MyQueryReasoner() {
                 setup(true, true);
         }
@@ -102,10 +103,10 @@ public class MyQueryReasoner extends QueryReasoner {
 
                 if (multiStageTag && !program.getGeneral().isHorn()) {
                         lazyUpperStore =  getUpperStore("lazy-upper-bound", true); // new MultiStageQueryEngine("lazy-upper-bound", true); //
+                        // TODO CHECK
+                        limitedSkolemUpperStore =  getUpperStore("limited-skolem-upper-bound", true);
                 }
 
-                // TODO add new upper store creation
-
                 importData(program.getAdditionalDataFile());
 
                 elho_ontology = new ELHOProfile().getFragment(ontology);
@@ -151,7 +152,21 @@ public class MyQueryReasoner extends QueryReasoner {
                         Utility.logInfo("time for satisfiability checking: " + t.duration());
                 }
 
-                // TODO add new upper store preprocessing
+                // TODO check
+                if (limitedSkolemUpperStore != null) {
+                        limitedSkolemUpperStore.importRDFData(name, datafile);
+                        limitedSkolemUpperStore.materialise("saturate named individuals", originalMarkProgram);
+                        int tag = limitedSkolemUpperStore.materialiseSkolemly(program, null);
+                        if (tag != 1) {
+                                limitedSkolemUpperStore.dispose();
+                                limitedSkolemUpperStore = null;
+                        }
+                        if (tag == -1) return false;
+                }
+                if (consistency.checkSkolemUpper()) {
+                        satisfiable = true;
+                        Utility.logInfo("time for satisfiability checking: " + t.duration());
+                }
 
                 trackingStore.importRDFData(name, datafile);
                 trackingStore.materialise("saturate named individuals", originalMarkProgram);
@@ -223,6 +238,9 @@ public class MyQueryReasoner extends QueryReasoner {
                 if (!queryRecord.isBottom() && lazyUpperStore != null) {
                         queryUpperBound(trackingStore, queryRecord, queryRecord.getQueryText(), queryRecord.getAnswerVariables());
                 }
+                if (!queryRecord.isBottom() && limitedSkolemUpperStore != null) {
+                        queryUpperBound(limitedSkolemUpperStore, queryRecord, queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+                }
                 // END: trying to intersect
 
                 queryRecord.addProcessingTime(Step.UpperBound, t.duration());
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java b/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java
index 11588ce..5d2e411 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java
@@ -1,29 +1,21 @@
 package uk.ac.ox.cs.pagoda.reasoner.light;
 
-import java.util.Arrays;
-import java.util.Collection;
-import java.util.HashSet;
-import java.util.Iterator;
-import java.util.Set;
-
 import org.semanticweb.HermiT.model.DLClause;
-
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.store.DataStore;
+import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType;
+import uk.ac.ox.cs.JRDFox.store.Parameters;
+import uk.ac.ox.cs.JRDFox.store.TripleStatus;
+import uk.ac.ox.cs.JRDFox.store.TupleIterator;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
 import uk.ac.ox.cs.pagoda.query.AnswerTuples;
 import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
 import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
 import uk.ac.ox.cs.pagoda.rules.Program;
-import uk.ac.ox.cs.pagoda.util.ConjunctiveQueryHelper;
-import uk.ac.ox.cs.pagoda.util.Namespace;
+import uk.ac.ox.cs.pagoda.util.*;
 import uk.ac.ox.cs.pagoda.util.Timer;
-import uk.ac.ox.cs.pagoda.util.UFS;
-import uk.ac.ox.cs.pagoda.util.Utility;
-import uk.ac.ox.cs.JRDFox.JRDFStoreException;
-import uk.ac.ox.cs.JRDFox.store.DataStore;
-import uk.ac.ox.cs.JRDFox.store.Parameters;
-import uk.ac.ox.cs.JRDFox.store.TripleStatus;
-import uk.ac.ox.cs.JRDFox.store.TupleIterator;
-import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType;
+
+import java.util.*;
 
 public class BasicQueryEngine extends RDFoxQueryEngine {
 
@@ -74,6 +66,10 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
                 
                 return 1; 
         }
+
+        public int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap) {
+                throw new UnsupportedOperationException();
+        }
         
         @Override
         public AnswerTuples evaluate(String queryText) {
@@ -163,8 +159,7 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
                                 instanceTuples = null; 
                                 try {
                                         instanceTuples = getDataStore().compileQuery("SELECT ?X ?Z WHERE { ?X " + predicate + " ?Z }", prefixes, parameters);
-                                        ;
-                                        long totalCount = 0; 
+                                        long totalCount = 0;
                                         for (long multi1 = instanceTuples.open(); multi1 != 0; multi1 = instanceTuples.getNext())
                                                 totalCount += instanceTuples.getMultiplicity();
                                         number.add(predicate + " * " + totalCount); 
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
index e53ae49..4444c00 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -1,26 +1,29 @@
 package uk.ac.ox.cs.pagoda.rules.approximators;
 
-import org.semanticweb.HermiT.model.DLClause;
-import org.semanticweb.HermiT.model.Individual;
+import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+import uk.ac.ox.cs.pagoda.multistage.MultiStageUpperProgram;
 import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
 import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
+import uk.ac.ox.cs.pagoda.util.tuples.TupleBuilder;
 
 import java.util.*;
 
 /**
- * Approximates existential rules by a limited form of Skolemisation.
+ * Approximates existential rules through a limited form of Skolemisation.
  * <p>
- * Given a rule and a grounding substitution,
- * it Skolemises the rule if
- * all the terms in the substitution have depth less than a given depth,
+ * Given a rule and a ground substitution,
+ * it Skolemises the rule
+ * if all the terms in the substitution have depth less than a given depth,
  * otherwise it approximates using an alternative <tt>TupleDependentApproximator</tt>.
- *
  * */
 public class LimitedSkolemisationApproximator implements TupleDependentApproximator {
 
+    private static final Atom[] EMPTY_BODY = new Atom[0];
+
     private final int maxTermDepth;
     private final TupleDependentApproximator alternativeApproximator;
+    private final SkolemTermsManager skolemTermsManager;
 
     private Map<AnswerTupleID, Integer> mapIndividualsToDepth;
 
@@ -32,19 +35,21 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
         this.maxTermDepth = maxTermDepth;
         this.alternativeApproximator = alternativeApproximator;
         this.mapIndividualsToDepth = new HashMap<>();
+        this.skolemTermsManager = SkolemTermsManager.getInstance();
     }
 
     @Override
-    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
+    public Collection<DLClause> convert(DLClause clause,
+                                        DLClause originalClause,
+                                        Collection<Tuple<Individual>> violationTuples) {
         switch (clause.getHeadLength()) {
             case 1:
                 return overApprox(clause, originalClause, violationTuples);
             case 0:
                 return Arrays.asList(clause);
             default:
-                ArrayList<DLClause> result = new ArrayList<>();
-                // TODO implement
-                return result;
+                throw new IllegalArgumentException(
+                        "Expected clause with head length < 1, but it is " + clause.getHeadLength());
         }
 
 
@@ -54,23 +59,94 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
         ArrayList<DLClause> result = new ArrayList<>();
 
         for (Tuple<Individual> violationTuple : violationTuples)
-            if (getDepth(violationTuple) > maxTermDepth)
+            if (getMaxDepth(violationTuple) > maxTermDepth)
                 result.addAll(alternativeApproximator.convert(clause, originalClause, null));
             else
-                result.add(getGroundSkolemisation(clause, originalClause, violationTuple));
+                result.addAll(getGroundSkolemisation(clause, originalClause, violationTuple));
 
         return result;
     }
 
+    private static final Variable X = Variable.create("X");
+
+    private Collection<DLClause> getGroundSkolemisation(DLClause clause,
+                                                        DLClause originalClause,
+                                                        Tuple<Individual> violationTuple) {
+
+        String[] commonVars = MultiStageUpperProgram.getCommonVars(clause);
+
+        // TODO check: strong assumption, the first tuples are the common ones
+        TupleBuilder<Individual> commonIndividualsBuilder = new TupleBuilder<>();
+        for (int i = 0; i < commonVars.length; i++)
+            commonIndividualsBuilder.add(violationTuple.get(i));
+
+        Atom headAtom = clause.getHeadAtom(0);
+        Atom[] bodyAtoms = clause.getBodyAtoms();
+        int offset = OverApproxExist.indexOfExistential(headAtom, originalClause);
+
+        // BEGIN: copy and paste
+        ArrayList<DLClause> ret = new ArrayList<>();
+        DLPredicate predicate = headAtom.getDLPredicate();
+        if (predicate instanceof AtLeastConcept) {
+            AtLeastConcept atLeastConcept = (AtLeastConcept) predicate;
+            LiteralConcept concept = atLeastConcept.getToConcept();
+            Role role = atLeastConcept.getOnRole();
+            AtomicConcept atomicConcept;
+
+            if (concept instanceof AtomicNegationConcept) {
+                // TODO CHECK: is this already in MultiStageUpperProgram?
+                Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
+                Atom atom2 = Atom.create(atomicConcept = OverApproxExist.getNegationConcept(atomicConcept), X);
+                ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2}));
+            }
+            else {
+                atomicConcept = (AtomicConcept) concept;
+                if (atomicConcept.equals(AtomicConcept.THING))
+                    atomicConcept = null;
+            }
+
+            int card = atLeastConcept.getNumber();
+            Individual[] individuals = new Individual[card];
+            SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
+            for (int i = 0; i < card; ++i)
+                individuals[i] = termsManager.getFreshIndividual(originalClause,
+                                                                 offset + i,
+                                                                 commonIndividualsBuilder.create());
+
+            for (int i = 0; i < card; ++i) {
+                if (atomicConcept != null)
+                    ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY));
+
+                Atom atom = role instanceof AtomicRole ?
+                        Atom.create((AtomicRole) role, X, individuals[i]) :
+                        Atom.create(((InverseRole) role).getInverseOf(), individuals[i], X);
+
+                ret.add(DLClause.create(new Atom[] {atom}, EMPTY_BODY));
+            }
+
+            for (int i = 0; i < card; ++i)
+                for (int j = i + 1; j < card; ++j)
+                    // TODO to be checked ... different as
+                    ret.add(DLClause.create(new Atom[] {Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, EMPTY_BODY));
+
+        }
+        else if (predicate instanceof AtLeastDataRange) {
+            // TODO to be implemented ...
+        }
+        else
+            ret.add(DLClause.create(new Atom[] {headAtom}, EMPTY_BODY));
 
-    private DLClause getGroundSkolemisation(DLClause clause, DLClause originalClause, Tuple<Individual> violationTuple) {
-        // TODO implement
-        // filter the violation tuples appearing on both the sides of the rule
-        return null;
+        return ret;
+
+        // END: copy and paste
     }
 
-    private int getDepth(Tuple<Individual> violationTuple) {
-        if (!mapIndividualsToDepth.containsKey(violationTuple)) return 0;
-        return mapIndividualsToDepth.get(violationTuple);
+
+    public int getMaxDepth(Tuple<Individual> violationTuple) {
+        int maxDepth = 0;
+        for (Individual individual : violationTuple)
+            maxDepth = Integer.max(maxDepth, skolemTermsManager.getDepth(individual));
+
+        return maxDepth;
     }
 }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
index d71c472..028568c 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
@@ -12,7 +12,7 @@ public class OverApproxExist implements Approximator {
         public static final String negativeSuffix = "_neg";
         private static final Variable X = Variable.create("X");
 
-        private static int indexOfExistential(Atom headAtom, DLClause originalClause) {
+        static int indexOfExistential(Atom headAtom, DLClause originalClause) {
                 if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1;
                 AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
                 if (alc.getToConcept() instanceof AtomicConcept) {