It executes. Matching bounds for query 18 of UOBM.

It is not stable: several critical fixes to do!

6 files changed, 44 insertions, 40 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
index f80da5f..4ba2715 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
@@ -143,6 +143,10 @@ public class MultiStageQueryEngine extends StageQueryEngine {
                                 subTimer.reset(); 
                                 oldTripleCount = store.getTriplesCount(); 
                                 for (Violation v : violations) {
+
+                                        Utility.logDebug("Dealing with violation: " + v.constraint);
+                                        Utility.logDebug("Number of violation tuples: " + v.size());
+
                                         Timer localTimer = new Timer(); 
                                         int number = v.size(); 
                                         long vOldCounter = store.getTriplesCount();  
@@ -151,8 +155,8 @@ public class MultiStageQueryEngine extends StageQueryEngine {
                                                 Utility.logInfo(name + " store FAILED for multi-stage materialisation in " + t.duration() + " seconds."); 
                                                 return 0; 
                                         }
-                                        Utility.logDebug("Time to make the constraint being satisfied: " + localTimer.duration() + " " + number + " tuples for " + v.constraint); 
-                                        Utility.logDebug("tuple number: " + v.size() + " before: " + vOldCounter + " after: " + store.getTriplesCount() + " (" + (store.getTriplesCount() - vOldCounter) + " new) ." ); 
+                                        Utility.logDebug("Time to make the constraint being satisfied: " + localTimer.duration());
+                                        Utility.logDebug("Triples in the store: before=" + vOldCounter + ", after=" + store.getTriplesCount() + ", new=" + (store.getTriplesCount() - vOldCounter));
                                 }
                                 Utility.logDebug(name + " store after adding facts for violations: " + (tripleCount = store.getTriplesCount()) + " (" + (tripleCount - oldTripleCount) + " new)");
                                 Utility.logDebug("Time to add triples for violations: " + subTimer.duration()); 
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/Violation.java b/src/uk/ac/ox/cs/pagoda/multistage/Violation.java
index b872f00..2f98784 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/Violation.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/Violation.java
@@ -1,9 +1,9 @@
 package uk.ac.ox.cs.pagoda.multistage;
 
-import java.util.LinkedList;
-
 import org.semanticweb.HermiT.model.DLClause;
 
+import java.util.LinkedList;
+
 public class Violation {
 
         DLClause clause = null; 
@@ -41,6 +41,13 @@ public class Violation {
         public String[] getVariables() {
                 return vars; 
         }
-        
-        
+
+        @Override
+        public String toString() {
+                return "Violation{" +
+                                "constraint=" + constraint +
+                                ", clause=" + clause +
+                                ", tuples=" + tuples +
+                                '}';
+        }
 }
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
index d179d14..b7a3667 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
@@ -73,6 +73,9 @@ public class ConsistencyManager {
                         AnswerTuples tuples = null; 
                         try {
                                 tuples = m_reasoner.lazyUpperStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables());
+
+                                Utility.logDebug("CheckLazyUpperBound: answerVars=" + fullQueryRecord.getAnswerVariables());
+
                                 if (!tuples.isValid()) {
                                         Utility.logInfo("There are no contradictions derived in the lazy upper bound materialisation."); 
                                         return satisfiability(t.duration()); 
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
index 233963e..36ea7de 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -33,7 +33,8 @@ public class MyQueryReasoner extends QueryReasoner {
         DatalogProgram program; 
 
         BasicQueryEngine rlLowerStore = null;
-        BasicQueryEngine lazyUpperStore = null;  
+        BasicQueryEngine lazyUpperStore = null;
+        BasicQueryEngine limitedSkolemUpperStore;
 //      boolean[] namedIndividuals_lazyUpper; 
         
         OWLOntology elho_ontology; 
@@ -49,7 +50,6 @@ 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);
@@ -163,10 +163,11 @@ public class MyQueryReasoner extends QueryReasoner {
                         }
                         if (tag == -1) return false;
                 }
-                if (consistency.checkSkolemUpper()) {
-                        satisfiable = true;
-                        Utility.logInfo("time for satisfiability checking: " + t.duration());
-                }
+                // FIXME nullPointerException
+//              if (consistency.checkSkolemUpper()) {
+//                      satisfiable = true;
+//                      Utility.logInfo("time for satisfiability checking: " + t.duration());
+//              }
 
                 trackingStore.importRDFData(name, datafile);
                 trackingStore.materialise("saturate named individuals", originalMarkProgram);
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxTripleManager.java b/src/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxTripleManager.java
index c2065dc..232bc31 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxTripleManager.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxTripleManager.java
@@ -1,31 +1,17 @@
 package uk.ac.ox.cs.pagoda.reasoner.light;
 
-import java.util.Collection;
-import java.util.HashMap;
-import java.util.LinkedList;
-import java.util.Map;
-import java.util.Queue;
-import org.semanticweb.HermiT.model.AnnotatedEquality;
-import org.semanticweb.HermiT.model.Atom;
-import org.semanticweb.HermiT.model.AtomicConcept;
-import org.semanticweb.HermiT.model.AtomicRole;
-import org.semanticweb.HermiT.model.Constant;
-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.Term;
-import org.semanticweb.HermiT.model.Variable;
-
-import uk.ac.ox.cs.pagoda.owl.OWLHelper;
-import uk.ac.ox.cs.pagoda.util.Namespace;
+import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.model.Datatype;
 import uk.ac.ox.cs.JRDFox.model.GroundTerm;
 import uk.ac.ox.cs.JRDFox.store.DataStore;
-import uk.ac.ox.cs.JRDFox.model.Datatype;
-import uk.ac.ox.cs.JRDFox.store.Dictionary;
 import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType;
+import uk.ac.ox.cs.JRDFox.store.Dictionary;
 import uk.ac.ox.cs.JRDFox.store.Resource;
+import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+
+import java.util.*;
 
 public class RDFoxTripleManager {
         
@@ -183,10 +169,11 @@ public class RDFoxTripleManager {
         int sizeLimit = 10000; 
 
         private int getResourceID(Term arg, Map<Variable, Integer> assignment) {
-                while (termCache.size() > sizeLimit) 
-                        termCache.remove(termList.poll()); 
+                // FIXME infinite loop
+//              while (termCache.size() > sizeLimit)
+//                      termCache.remove(termList.poll());
                 
-                if (arg instanceof Variable) return assignment.get((Variable) arg); 
+                if (arg instanceof Variable) return assignment.get(arg);
                 Integer id = null; 
                 if ((id = termCache.get(arg)) != null)
                         return id; 
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 4444c00..ba58e23 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -79,9 +79,11 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
         TupleBuilder<Individual> commonIndividualsBuilder = new TupleBuilder<>();
         for (int i = 0; i < commonVars.length; i++)
             commonIndividualsBuilder.add(violationTuple.get(i));
+        Tuple<Individual> commonIndividuals = commonIndividualsBuilder.create();
 
         Atom headAtom = clause.getHeadAtom(0);
-        Atom[] bodyAtoms = clause.getBodyAtoms();
+
+//        Atom[] bodyAtoms = clause.getBodyAtoms();
         int offset = OverApproxExist.indexOfExistential(headAtom, originalClause);
 
         // BEGIN: copy and paste
@@ -111,15 +113,15 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
             for (int i = 0; i < card; ++i)
                 individuals[i] = termsManager.getFreshIndividual(originalClause,
                                                                  offset + i,
-                                                                 commonIndividualsBuilder.create());
+                                                                 commonIndividuals);
 
             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);
+                        Atom.create((AtomicRole) role, commonIndividuals.get(0), individuals[i]) :
+                        Atom.create(((InverseRole) role).getInverseOf(), individuals[i], commonIndividuals.get(0));
 
                 ret.add(DLClause.create(new Atom[] {atom}, EMPTY_BODY));
             }