11 files changed, 301 insertions, 211 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
index 453b5ca..3fd2fbd 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
@@ -23,6 +23,7 @@ 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.pagoda.util.disposable.Disposable;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
 
 import java.util.LinkedList;
 
@@ -49,6 +50,8 @@ public class ConsistencyManager extends Disposable {
         }
 
         public void extractBottomFragment() {
+                if(isDisposed()) throw new DisposedException();
+
                 if(fragmentExtracted) return;
                 fragmentExtracted = true;
 
@@ -141,10 +144,14 @@ public class ConsistencyManager extends Disposable {
         }
 
         public QueryRecord[] getQueryRecords() {
+                if(isDisposed()) throw new DisposedException();
+
                 return botQueryRecords;
         }
 
         boolean checkRLLowerBound() {
+                if(isDisposed()) throw new DisposedException();
+
                 fullQueryRecord = m_queryManager.create(QueryRecord.botQueryText, 0);
                 AnswerTuples iter = null;
 
@@ -175,6 +182,8 @@ public class ConsistencyManager extends Disposable {
 //      }
 
         boolean checkELLowerBound() {
+                if(isDisposed()) throw new DisposedException();
+
                 fullQueryRecord.updateLowerBoundAnswers(m_reasoner.elLowerStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord
                                 .getAnswerVariables()));
                 if(fullQueryRecord.getNoOfSoundAnswers() > 0) {
@@ -185,6 +194,8 @@ public class ConsistencyManager extends Disposable {
         }
 
         boolean checkUpper(BasicQueryEngine upperStore) {
+                if(isDisposed()) throw new DisposedException();
+
                 if(upperStore != null) {
                         AnswerTuples tuples = null;
                         try {
@@ -202,6 +213,8 @@ public class ConsistencyManager extends Disposable {
         }
 
         boolean check() {
+                if(isDisposed()) throw new DisposedException();
+
 //              if (!checkRLLowerBound()) return false;
 //              if (!checkELLowerBound()) return false;
 //              if (checkLazyUpper()) return true;
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java
index 0a151bc..cc2c4c0 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java
@@ -70,7 +70,7 @@ class ELHOQueryReasoner extends QueryReasoner {
     @Override
     public boolean preprocess() {
         if(isDisposed()) throw new DisposedException();
-        elLowerStore.importRDFData("data", importedData.toString());
+        elLowerStore.importRDFData("data", getImportedData());
         String rlLowerProgramText = program.toString();
 //              program.save();
         elLowerStore.materialise("lower program", rlLowerProgramText);
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java
index 771190e..a56a793 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java
@@ -129,7 +129,7 @@ class ELHOUQueryReasoner extends QueryReasoner {
     @Override
     public boolean preprocess() {
         if(isDisposed()) throw new DisposedException();
-        String name = "data", datafile = importedData.toString();
+        String name = "data", datafile = getImportedData();
 
         String lowername = "lower program";
         String rlLowerProgramText = program.getLower().toString();
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java
index 78b9a0b..15eb9e8 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java
@@ -46,7 +46,7 @@ class HermiTReasoner extends QueryReasoner {
         if(isDisposed()) throw new DisposedException();
         OWLOntology tbox = onto;
         try {
-            onto = OWLHelper.getImportedOntology(tbox, importedData.toString().split(ImportDataFileSeparator));
+            onto = OWLHelper.getImportedOntology(tbox, getImportedData().split(ImportDataFileSeparator));
             importedOntologyPath = OWLHelper.getOntologyPath(onto);
         } catch(OWLOntologyCreationException | OWLOntologyStorageException | IOException e) {
             e.printStackTrace();
@@ -55,7 +55,7 @@ class HermiTReasoner extends QueryReasoner {
         DatalogProgram datalogProgram = new DatalogProgram(tbox, false);
         importData(datalogProgram.getAdditionalDataFile());
         upperStore = new MultiStageQueryEngine("rl-upper", false);
-        upperStore.importRDFData("data", importedData.toString());
+        upperStore.importRDFData("data", getImportedData());
         GapByStore4ID gap = new GapByStore4ID(upperStore);
         upperStore.materialiseFoldedly(datalogProgram, gap);
         gap.clear();
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
index acdb8a3..b4e2f5a 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -29,20 +29,22 @@ import java.util.Collection;
 class MyQueryReasoner extends QueryReasoner {
 
     OWLOntology ontology;
+    OWLOntology elho_ontology;
     DatalogProgram program;
 
     BasicQueryEngine rlLowerStore = null;
-    BasicQueryEngine lazyUpperStore = null;
-    //    MultiStageQueryEngine limitedSkolemUpperStore;
-    OWLOntology elho_ontology;
     KarmaQueryEngine elLowerStore = null;
-    BasicQueryEngine trackingStore = null;
+    MultiStageQueryEngine lazyUpperStore = null;
+    MultiStageQueryEngine trackingStore = null;
     TrackingRuleEncoder encoder;
+
     private boolean equalityTag;
     private Timer t = new Timer();
+
     private Collection<String> predicatesWithGap = null;
-    private SatisfiabilityStatus satisfiable;
+    private ConsistencyStatus isConsistent;
     private ConsistencyManager consistency = new ConsistencyManager(this);
+    private boolean useSkolemisation = false; // now only debugging
 
     public MyQueryReasoner() {
         setup(true);
@@ -92,11 +94,15 @@ class MyQueryReasoner extends QueryReasoner {
         t.reset();
         Utility.logInfo("Preprocessing (and checking satisfiability)...");
 
-        String name = "data", datafile = importedData.toString();
+        String name = "data", datafile = getImportedData();
         rlLowerStore.importRDFData(name, datafile);
         rlLowerStore.materialise("lower program", program.getLower().toString());
 //              program.getLower().save();
-        if(!consistency.checkRLLowerBound()) return false;
+        if(!consistency.checkRLLowerBound()) {
+            Utility.logDebug("time for satisfiability checking: " + t.duration());
+            isConsistent = ConsistencyStatus.INCONSISTENT;
+            return false;
+        }
         Utility.logDebug("The number of sameAs assertions in RL lower store: " + rlLowerStore.getSameAsNumber());
 
         String originalMarkProgram = OWLHelper.getOriginalMarkProgram(ontology);
@@ -105,20 +111,28 @@ class MyQueryReasoner extends QueryReasoner {
         elLowerStore.materialise("saturate named individuals", originalMarkProgram);
         elLowerStore.materialise("lower program", program.getLower().toString());
         elLowerStore.initialiseKarma();
-        if(!consistency.checkELLowerBound()) return false;
+        if(!consistency.checkELLowerBound()) {
+            Utility.logDebug("time for satisfiability checking: " + t.duration());
+            isConsistent = ConsistencyStatus.INCONSISTENT;
+            return false;
+        }
 
         if(lazyUpperStore != null) {
             lazyUpperStore.importRDFData(name, datafile);
             lazyUpperStore.materialise("saturate named individuals", originalMarkProgram);
             int tag = lazyUpperStore.materialiseRestrictedly(program, null);
-            if(tag != 1) {
+            if(tag == -1) {
+                Utility.logDebug("time for satisfiability checking: " + t.duration());
+                isConsistent = ConsistencyStatus.INCONSISTENT;
+                return false;
+            }
+            else if(tag != 1) {
                 lazyUpperStore.dispose();
                 lazyUpperStore = null;
             }
-            if(tag == -1) return false;
         }
         if(consistency.checkUpper(lazyUpperStore)) {
-            satisfiable = SatisfiabilityStatus.SATISFIABLE;
+            isConsistent = ConsistencyStatus.CONSISTENT;
             Utility.logDebug("time for satisfiability checking: " + t.duration());
         }
 
@@ -140,13 +154,12 @@ class MyQueryReasoner extends QueryReasoner {
 //                      encoder = new TrackingRuleEncoderDisjVar2(program.getUpper(), trackingStore);
 //                      encoder = new TrackingRuleEncoderDisj2(program.getUpper(), trackingStore);
 
+        // TODO add consistency check by Skolem-upper-bound
+
         if(!isConsistent())
             return false;
 
         consistency.extractBottomFragment();
-        consistency.dispose();
-
-        program.dispose();
 
         return true;
     }
@@ -154,11 +167,19 @@ class MyQueryReasoner extends QueryReasoner {
     @Override
     public boolean isConsistent() {
         if(isDisposed()) throw new DisposedException();
-        if(satisfiable == SatisfiabilityStatus.UNCHECKED) {
-            satisfiable = consistency.check() ? SatisfiabilityStatus.SATISFIABLE : SatisfiabilityStatus.UNSATISFIABLE;
-            Utility.logInfo("time for satisfiability checking: " + t.duration());
+
+        if(isConsistent == ConsistencyStatus.UNCHECKED) {
+            isConsistent = consistency.check() ? ConsistencyStatus.CONSISTENT : ConsistencyStatus.INCONSISTENT;
+            Utility.logDebug("time for satisfiability checking: " + t.duration());
+        }
+        if(isConsistent == ConsistencyStatus.CONSISTENT) {
+            Utility.logInfo("The ontology is consistent!");
+            return true;
+        }
+        else {
+            Utility.logInfo("The ontology is inconsistent!");
+            return false;
         }
-        return satisfiable == SatisfiabilityStatus.SATISFIABLE;
     }
 
     @Override
@@ -169,9 +190,9 @@ class MyQueryReasoner extends QueryReasoner {
             return;
 
         OWLOntology relevantOntologySubset = extractRelevantOntologySubset(queryRecord);
-//              queryRecord.saveRelevantOntology("fragment_query" + queryRecord.getQueryID() + ".owl");
+        queryRecord.saveRelevantOntology("/home/alessandro/Desktop/fragment_query" + queryRecord.getQueryID() + ".owl");
 
-        if(querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord))
+        if(useSkolemisation && querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord))
             return;
 
         Timer t = new Timer();
@@ -207,12 +228,14 @@ class MyQueryReasoner extends QueryReasoner {
         if(lazyUpperStore != null) lazyUpperStore.dispose();
         if(elLowerStore != null) elLowerStore.dispose();
         if(trackingStore != null) trackingStore.dispose();
-//        if(limitedSkolemUpperStore != null) limitedSkolemUpperStore.dispose();
+        if(consistency != null) consistency.dispose();
+        if(program != null) program.dispose();
     }
 
     private void setup(boolean considerEqualities) {
         if(isDisposed()) throw new DisposedException();
-        satisfiable = SatisfiabilityStatus.UNCHECKED;
+
+        isConsistent = ConsistencyStatus.UNCHECKED;
         this.equalityTag = considerEqualities;
 
         rlLowerStore = new BasicQueryEngine("rl-lower-bound");
@@ -239,7 +262,7 @@ class MyQueryReasoner extends QueryReasoner {
      */
     private boolean queryUpperStore(BasicQueryEngine upperStore, QueryRecord queryRecord,
                                     Tuple<String> extendedQuery, Step step) {
-
+        t.reset();
         if(queryRecord.hasNonAnsDistinguishedVariables())
             queryUpperBound(upperStore, queryRecord, extendedQuery.get(0), queryRecord.getAnswerVariables());
         else
@@ -254,6 +277,7 @@ class MyQueryReasoner extends QueryReasoner {
     }
 
     private boolean checkGapAnswers(BasicQueryEngine relevantStore, QueryRecord queryRecord) {
+        t.reset();
         Tuple<String> extendedQueries = queryRecord.getExtendedQueryText();
         if(queryRecord.hasNonAnsDistinguishedVariables())
             checkGapAnswers(relevantStore, queryRecord, extendedQueries.get(0), queryRecord.getAnswerVariables());
@@ -296,8 +320,6 @@ class MyQueryReasoner extends QueryReasoner {
         }
         queryRecord.addProcessingTime(Step.LOWER_BOUND, t.duration());
 
-        t.reset();
-
         Tuple<String> extendedQueryTexts = queryRecord.getExtendedQueryText();
 
         Utility.logDebug("Tracking store");
@@ -343,8 +365,6 @@ class MyQueryReasoner extends QueryReasoner {
         // just statistics
         int numOfABoxAxioms = relevantOntologySubset.getABoxAxioms(true).size();
         int numOfTBoxAxioms = relevantOntologySubset.getAxiomCount() - numOfABoxAxioms;
-        int originalNumOfABoxAxioms = ontology.getABoxAxioms(true).size();
-        int originalNumOfTBoxAxioms = ontology.getAxiomCount() - originalNumOfABoxAxioms;
         Utility.logInfo("Relevant ontology-subset has been extracted: |ABox|="
                                 + numOfABoxAxioms + ", |TBox|=" + numOfTBoxAxioms);
 
@@ -365,6 +385,7 @@ class MyQueryReasoner extends QueryReasoner {
 
     private boolean querySkolemisedRelevantSubset(OWLOntology relevantSubset, QueryRecord queryRecord) {
         Utility.logInfo("Evaluating semi-Skolemised relevant upper store...");
+        t.reset();
 
         DatalogProgram relevantProgram = new DatalogProgram(relevantSubset, false); // toClassify is false
 
@@ -373,16 +394,24 @@ class MyQueryReasoner extends QueryReasoner {
 
         relevantStore.importDataFromABoxOf(relevantSubset);
 
-        int materialisationResult = relevantStore.materialiseSkolemly(relevantProgram, null);
-        if(materialisationResult != 1)
-            throw new RuntimeException("Skolemised materialisation error"); // TODO check consistency
+        int queryDependentMaxTermDepth = 1; // TODO make it dynamic
+        int materialisationTag = relevantStore.materialiseSkolemly(relevantProgram, null,
+                                                                   queryDependentMaxTermDepth);
+        queryRecord.addProcessingTime(Step.L_SKOLEM_UPPER_BOUND, t.duration());
+        if(materialisationTag == -1) {
+            throw new Error("A consistent ontology has turned out to be " +
+                                    "inconsistent in the Skolemises-relevant-upper-store");
+        }
+        else if(materialisationTag != 1) {
+            Utility.logInfo("Semi-Skolemised relevant upper store cannot be employed");
+            return false;
+        }
 
         boolean isFullyProcessed = checkGapAnswers(relevantStore, queryRecord);
-
         Utility.logInfo("Semi-Skolemised relevant upper store has been evaluated");
         return isFullyProcessed;
     }
 
-    enum SatisfiabilityStatus {SATISFIABLE, UNSATISFIABLE, UNCHECKED}
+    private enum ConsistencyStatus {CONSISTENT, INCONSISTENT, UNCHECKED}
 
 }
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java
index 962a78f..eab6a1b 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java
@@ -26,10 +26,10 @@ public abstract class QueryReasoner extends Disposable {
     private static final boolean DEFAULT_MULTI_STAGES = true;
     private static final boolean DEFAULT_EQUALITIES = true;
     public boolean fullReasoner = this instanceof MyQueryReasoner;
-    protected StringBuilder importedData = new StringBuilder();
     //  protected boolean forSemFacet = false;
     PagodaProperties properties;
     BufferedWriter answerWriter = null;
+    private StringBuilder importedData = new StringBuilder();
     private QueryManager m_queryManager = new QueryManager();
 
     public static QueryReasoner getInstance(PagodaProperties p) {
@@ -208,10 +208,6 @@ public abstract class QueryReasoner extends Disposable {
         queryRecords.stream().forEach(record -> record.dispose());
     }
 
-//      public void evaluate(Collection<QueryRecord> queryRecords) {
-//              evaluate(queryRecords);
-//      }
-
     @Override
     public void dispose() {
         super.dispose();
@@ -225,11 +221,19 @@ public abstract class QueryReasoner extends Disposable {
 //              Utility.cleanup();
     }
 
+//      public void evaluate(Collection<QueryRecord> queryRecords) {
+//              evaluate(queryRecords);
+//      }
+
     public QueryManager getQueryManager() {
         if(isDisposed()) throw new DisposedException();
         return m_queryManager;
     }
 
+    protected String getImportedData() {
+        return importedData.toString();
+    }
+
     private void importDataDirectory(File file) {
         for(File child : file.listFiles())
             if(child.isFile()) importDataFile(child);
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java
index 16e2627..3934498 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java
@@ -57,7 +57,7 @@ class RLQueryReasoner extends QueryReasoner {
         @Override
         public boolean preprocess() {
                 if(isDisposed()) throw new DisposedException();
-                rlLowerStore.importRDFData("data", importedData.toString());
+                rlLowerStore.importRDFData("data", getImportedData());
                 rlLowerStore.materialise("lower program", program.toString());
 
                 return isConsistent();
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java
index d0712e1..368fbb2 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java
@@ -97,7 +97,7 @@ class RLUQueryReasoner extends QueryReasoner {
         @Override
         public boolean preprocess() {
                 if(isDisposed()) throw new DisposedException();
-                String datafile = importedData.toString(); 
+                String datafile = getImportedData();
                 rlLowerStore.importRDFData("data", datafile);
                 rlLowerStore.materialise("lower program", program.getLower().toString());
                 
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java b/src/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java
index 849b971..fd620a5 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java
@@ -2,14 +2,14 @@ package uk.ac.ox.cs.pagoda.reasoner.full;
 
 import uk.ac.ox.cs.pagoda.query.AnswerTuple;
 import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.util.disposable.Disposable;
 
-public interface Checker {
+public abstract class Checker extends Disposable {
 
-        public int check(AnswerTuples answers);
-        
-        public boolean check(AnswerTuple answer);
+        public abstract int check(AnswerTuples answers);
 
-        public boolean isConsistent();
+        public abstract boolean check(AnswerTuple answer);
+
+        public abstract boolean isConsistent();
 
-        public void dispose(); 
 }
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java b/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
index 5dcf0f8..35db0f2 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
@@ -1,24 +1,10 @@
 package uk.ac.ox.cs.pagoda.reasoner.full;
 
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Map;
-import java.util.Set;
-
 import org.semanticweb.HermiT.Reasoner;
 import org.semanticweb.HermiT.model.DLClause;
 import org.semanticweb.HermiT.model.Term;
 import org.semanticweb.HermiT.model.Variable;
-import org.semanticweb.owlapi.model.IRI;
-import org.semanticweb.owlapi.model.OWLAxiom;
-import org.semanticweb.owlapi.model.OWLClassAssertionAxiom;
-import org.semanticweb.owlapi.model.OWLDataFactory;
-import org.semanticweb.owlapi.model.OWLDataPropertyAssertionAxiom;
-import org.semanticweb.owlapi.model.OWLIndividual;
-import org.semanticweb.owlapi.model.OWLObjectPropertyAssertionAxiom;
-import org.semanticweb.owlapi.model.OWLOntology;
-import org.semanticweb.owlapi.model.OWLOntologyManager;
-
+import org.semanticweb.owlapi.model.*;
 import uk.ac.ox.cs.pagoda.endomorph.Clique;
 import uk.ac.ox.cs.pagoda.endomorph.DependencyGraph;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
@@ -30,216 +16,236 @@ import uk.ac.ox.cs.pagoda.util.ConjunctiveQueryHelper;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
 
-public class HermitChecker implements Checker {
-        
-        protected OWLDataFactory factory;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
 
-        private String queryText; 
-        private DLClause queryClause; 
+public class HermitChecker extends Checker {
         
-        private Reasoner hermit;
+        protected OWLDataFactory factory;
         protected String[][] answerVariable;
         protected OWLOntology ontology;
-        protected QueryRecord record; 
-        protected QueryGraph qGraph = null; 
+        protected QueryRecord record;
+        protected QueryGraph qGraph = null;
         boolean toCheck = true;
-        
+        AnswerTuple topAnswerTuple = null, botAnswerTuple = null;
+        private String queryText;
+        private DLClause queryClause;
+        private Reasoner hermit;
+        private int tag = 0;
+        private int counter = 0;
+        private DependencyGraph dGraph = null;
         public HermitChecker(Checker checker) {
                 if (checker instanceof HermitChecker) {
                         HermitChecker other = (HermitChecker) checker;
-                        factory = other.factory; 
+                        factory = other.factory;
                         queryText = other.queryText;
-                        queryClause = other.queryClause; 
+                        queryClause = other.queryClause;
                         answerVariable = other.answerVariable;
                         ontology = other.ontology;
-//                      record = other.record; 
+//                      record = other.record;
                 }
-                
+
                 hermit = new Reasoner(ontology);
         }
-        
+
         public HermitChecker(OWLOntology ontology, QueryRecord record, boolean toCheck) {
                 this.ontology = ontology;
-                queryText = record.getQueryText(); 
+                queryText = record.getQueryText();
                 answerVariable = record.getVariables();
-                queryClause = record.getClause(); 
-//              this.record = record;  
-                this.toCheck = toCheck; 
+                queryClause = record.getClause();
+//              this.record = record;
+                this.toCheck = toCheck;
         }
-        
+
         public HermitChecker(OWLOntology ontology, String queryText) {
                 this.ontology = ontology;
-                this.queryText = queryText; 
+                this.queryText = queryText;
                 answerVariable = queryText == null ? null : ConjunctiveQueryHelper.getAnswerVariables(queryText);
-                queryClause = DLClauseHelper.getQuery(queryText, null); 
-//              this.record = null; 
+                queryClause = DLClauseHelper.getQuery(queryText, null);
+//              this.record = null;
+        }
+
+        @Override
+        public int check(AnswerTuples answers) {
+                if(isDisposed()) throw new DisposedException();
+
+                if(hermit == null) initialiseReasoner();
+                int answerCounter = 0, counter = 0;
+                for(; answers.isValid(); answers.moveNext()) {
+                        ++counter;
+                        if(check(answers.getTuple())) ++answerCounter;
+                }
+                answers.dispose();
+
+                Utility.logDebug("The number of individuals to be checked by HermiT: " + counter,
+                                                 "The number of correct answers: " + answerCounter);
+                return answerCounter;
+        }
+
+        @Override
+        public boolean check(AnswerTuple answerTuple) {
+                if(isDisposed()) throw new DisposedException();
+
+                if(!toCheck) return false;
+
+                if(hermit == null) initialiseReasoner();
+                if(tag != 0) return tag == 1;
+                ++counter;
+                Timer t = new Timer();
+                Map<Variable, Term> sub = answerTuple.getAssignment(answerVariable[1]);
+                Set<OWLAxiom> toCheckAxioms = qGraph.getAssertions(sub);
+
+//              for (OWLAxiom axiom: toCheckAxioms)     System.out.println(axiom.toString());
+
+                if(hermit.isEntailed(toCheckAxioms)) {
+                        Utility.logDebug("@TIME to check one tuple: " + t.duration());
+                        return true;
+                }
+                Utility.logDebug("@TIME to check one tuple: " + t.duration());
+                return false;
         }
         
-        private int tag = 0;
-        AnswerTuple topAnswerTuple = null, botAnswerTuple = null; 
-        
+        @Override
+        public boolean isConsistent() {
+                if(isDisposed()) throw new DisposedException();
+
+                if(hermit == null) initialiseReasoner();
+                return hermit.isConsistent();
+        }
+
+        public void dispose() {
+                super.dispose();
+
+                Utility.logInfo("Hermit was called " + counter + " times.");
+                if(hermit != null) hermit.dispose();
+                hermit = null;
+        }
+
+        public void setDependencyGraph(DependencyGraph dGraph) {
+                if(isDisposed()) throw new DisposedException();
+
+                this.dGraph = dGraph;
+        }
+
         private void initialiseReasoner() {
-                qGraph = new QueryGraph(queryClause.getBodyAtoms(), answerVariable[1], ontology); 
-                OWLOntologyManager manager = ontology.getOWLOntologyManager(); 
+                qGraph = new QueryGraph(queryClause.getBodyAtoms(), answerVariable[1], ontology);
+                OWLOntologyManager manager = ontology.getOWLOntologyManager();
                 factory = manager.getOWLDataFactory();
-                
-                if (hermit != null)     hermit.dispose();
-                
-                if (dGraph != null && answerVariable[1].length == 1 && (dGraph.getExits().size() > 1 || dGraph.getEntrances().size() > 1)) {
-                        Set<OWLAxiom> topAxioms = new HashSet<OWLAxiom>(); 
-                        Set<OWLAxiom> botAxioms = new HashSet<OWLAxiom>(); 
+
+                if(hermit != null) hermit.dispose();
+
+                if(dGraph != null && answerVariable[1].length == 1 && (dGraph.getExits().size() > 1 || dGraph.getEntrances()
+                                                                                                                                                                                                         .size() > 1)) {
+                        Set<OWLAxiom> topAxioms = new HashSet<OWLAxiom>();
+                        Set<OWLAxiom> botAxioms = new HashSet<OWLAxiom>();
                         addTopAndBotTuple(topAxioms, botAxioms);
-                        manager.addAxioms(ontology, topAxioms); 
-                        manager.addAxioms(ontology, botAxioms); 
+                        manager.addAxioms(ontology, topAxioms);
+                        manager.addAxioms(ontology, botAxioms);
                         hermit = new Reasoner(ontology);
-                        boolean topValid = true; 
-                        if (!hermit.isConsistent() || topAnswerTuple != null && (topValid = check(topAnswerTuple))) {
+                        boolean topValid = true;
+                        if(!hermit.isConsistent() || topAnswerTuple != null && (topValid = check(topAnswerTuple))) {
                                 hermit.dispose();
-                                manager.removeAxioms(ontology, topAxioms); 
-                                hermit = new Reasoner(ontology); 
-                        } else {
-                                if (!topValid) tag = -1; 
-                                else 
-                                        if (botAnswerTuple != null && check(botAnswerTuple)) tag = 1; 
+                                manager.removeAxioms(ontology, topAxioms);
+                                hermit = new Reasoner(ontology);
+                        }
+                        else {
+                                if(!topValid) tag = -1;
+                                else if(botAnswerTuple != null && check(botAnswerTuple)) tag = 1;
                         }
                 }
-                else 
+                else
                         hermit = new Reasoner(ontology);
         }
-        
+
         private void addTopAndBotTuple(Set<OWLAxiom> topAxioms, Set<OWLAxiom> botAxioms) {
                 String top_str = Namespace.PAGODA_ANONY + "top", bot_str = Namespace.PAGODA_ANONY + "bot";
-                topAnswerTuple = new AnswerTuple(new uk.ac.ox.cs.JRDFox.model.Individual[] { uk.ac.ox.cs.JRDFox.model.Individual.create(top_str) } ); 
-                botAnswerTuple = new AnswerTuple(new uk.ac.ox.cs.JRDFox.model.Individual[] { uk.ac.ox.cs.JRDFox.model.Individual.create(bot_str) } );  
-                OWLIndividual top_ind = factory.getOWLNamedIndividual(IRI.create(top_str)), bot_ind = factory.getOWLNamedIndividual(IRI.create(bot_str));
-                Map<OWLAxiom, Integer> counter = new HashMap<OWLAxiom, Integer>(); 
-                
+                topAnswerTuple =
+                                new AnswerTuple(new uk.ac.ox.cs.JRDFox.model.Individual[]{uk.ac.ox.cs.JRDFox.model.Individual.create(top_str)});
+                botAnswerTuple =
+                                new AnswerTuple(new uk.ac.ox.cs.JRDFox.model.Individual[]{uk.ac.ox.cs.JRDFox.model.Individual.create(bot_str)});
+                OWLIndividual top_ind = factory.getOWLNamedIndividual(IRI.create(top_str)), bot_ind =
+                                factory.getOWLNamedIndividual(IRI.create(bot_str));
+                Map<OWLAxiom, Integer> counter = new HashMap<OWLAxiom, Integer>();
+
                 Set<String> topAnswers = new HashSet<String>(), botAnswers = new HashSet<String>();
-                OWLIndividual sub, obj; 
-                if (dGraph.getExits().size() > 1) {
-                        for (Clique answerClique: dGraph.getExits())  
-                                topAnswers.add(((uk.ac.ox.cs.JRDFox.model.Individual) answerClique.getRepresentative().getAnswerTuple().getGroundTerm(0)).getIRI());
+                OWLIndividual sub, obj;
+                if(dGraph.getExits().size() > 1) {
+                        for(Clique answerClique : dGraph.getExits())
+                                topAnswers.add(((uk.ac.ox.cs.JRDFox.model.Individual) answerClique.getRepresentative()
+                                                                                                                                                                  .getAnswerTuple()
+                                                                                                                                                                  .getGroundTerm(0)).getIRI());
                 }
-                else topAnswerTuple = null; 
-                
-                if (dGraph.getEntrances().size() > 1) {
-                        for (Clique answerClique: dGraph.getEntrances()) 
-                                botAnswers.add(((uk.ac.ox.cs.JRDFox.model.Individual) answerClique.getRepresentative().getAnswerTuple().getGroundTerm(0)).getIRI()); 
+                else topAnswerTuple = null;
+
+                if(dGraph.getEntrances().size() > 1) {
+                        for(Clique answerClique : dGraph.getEntrances())
+                                botAnswers.add(((uk.ac.ox.cs.JRDFox.model.Individual) answerClique.getRepresentative()
+                                                                                                                                                                  .getAnswerTuple()
+                                                                                                                                                                  .getGroundTerm(0)).getIRI());
                 }
-                else botAnswerTuple = null; 
-                
-                for (OWLAxiom axiom: ontology.getABoxAxioms(true)) 
-                        if (axiom instanceof OWLClassAssertionAxiom) {
+                else botAnswerTuple = null;
+
+                for(OWLAxiom axiom : ontology.getABoxAxioms(true))
+                        if(axiom instanceof OWLClassAssertionAxiom) {
                                 OWLClassAssertionAxiom ca = (OWLClassAssertionAxiom) axiom;
                                 sub = ca.getIndividual();
-                                if (topAnswers.contains(sub.toStringID())) 
+                                if(topAnswers.contains(sub.toStringID()))
                                         topAxioms.add(factory.getOWLClassAssertionAxiom(ca.getClassExpression(), top_ind));
-                                if (botAnswers.contains(sub.toStringID())) 
+                                if(botAnswers.contains(sub.toStringID()))
                                         inc(counter, factory.getOWLClassAssertionAxiom(ca.getClassExpression(), bot_ind));
                         }
-                        else if (axiom instanceof OWLObjectPropertyAssertionAxiom) {
-                                OWLObjectPropertyAssertionAxiom oa = (OWLObjectPropertyAssertionAxiom) axiom; 
-                                sub = oa.getSubject(); obj = oa.getObject(); 
-                                if (topAnswers.contains(sub.toStringID()))
-                                        if (topAnswers.contains(obj.toStringID()))
+                        else if(axiom instanceof OWLObjectPropertyAssertionAxiom) {
+                                OWLObjectPropertyAssertionAxiom oa = (OWLObjectPropertyAssertionAxiom) axiom;
+                                sub = oa.getSubject();
+                                obj = oa.getObject();
+                                if(topAnswers.contains(sub.toStringID()))
+                                        if(topAnswers.contains(obj.toStringID()))
                                                 topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), top_ind, top_ind));
-                                        else 
+                                        else
                                                 topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), top_ind, obj));
                                 else {
-                                        if (topAnswers.contains(obj.toStringID()))
+                                        if(topAnswers.contains(obj.toStringID()))
                                                 topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), sub, top_ind));
                                 }
-                                
-                                if (botAnswers.contains(sub.toStringID()))
-                                        if (botAnswers.contains(obj.toStringID()))
+
+                                if(botAnswers.contains(sub.toStringID()))
+                                        if(botAnswers.contains(obj.toStringID()))
                                                 inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), bot_ind, bot_ind));
-                                        else 
+                                        else
                                                 inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), bot_ind, obj));
                                 else {
-                                        if (botAnswers.contains(obj.toStringID()))
+                                        if(botAnswers.contains(obj.toStringID()))
                                                 inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), sub, bot_ind));
                                 }
-                                
+
                         }
-                        else if (axiom instanceof OWLDataPropertyAssertionAxiom) {
-                                OWLDataPropertyAssertionAxiom da = (OWLDataPropertyAssertionAxiom) axiom; 
-                                sub = da.getSubject(); 
-                                if (topAnswers.contains(sub.toStringID())) 
+                        else if(axiom instanceof OWLDataPropertyAssertionAxiom) {
+                                OWLDataPropertyAssertionAxiom da = (OWLDataPropertyAssertionAxiom) axiom;
+                                sub = da.getSubject();
+                                if(topAnswers.contains(sub.toStringID()))
                                         topAxioms.add(factory.getOWLDataPropertyAssertionAxiom(da.getProperty(), top_ind, da.getObject()));
-                                
-                                if (botAnswers.contains(sub.toStringID())) 
+
+                                if(botAnswers.contains(sub.toStringID()))
                                         inc(counter, factory.getOWLDataPropertyAssertionAxiom(da.getProperty(), bot_ind, da.getObject()));
                         }
-                
-                int number = botAnswers.size(); 
-                for (Map.Entry<OWLAxiom, Integer> entry: counter.entrySet()) {
-                        if (entry.getValue() == number) 
+
+                int number = botAnswers.size();
+                for(Map.Entry<OWLAxiom, Integer> entry : counter.entrySet()) {
+                        if(entry.getValue() == number)
                                 botAxioms.add(entry.getKey());
                 }
         }
 
         private void inc(Map<OWLAxiom, Integer> counter, OWLAxiom newAxiom) {
-                Integer number = counter.get(newAxiom);  
-                if (number == null) counter.put(newAxiom, 1);
-                else counter.put(newAxiom, number + 1); 
-        }
+                if(isDisposed()) throw new DisposedException();
 
-        @Override
-        public int check(AnswerTuples answers) {
-                if (hermit == null) initialiseReasoner();
-                int answerCounter = 0, counter = 0; 
-                for (; answers.isValid(); answers.moveNext()) {
-                        ++counter; 
-                        if (check(answers.getTuple())) ++answerCounter;
-                }
-                answers.dispose();
-                
-                Utility.logDebug("The number of individuals to be checked by HermiT: " + counter, 
-                                "The number of correct answers: " + answerCounter);
-                return answerCounter; 
-        }
-        
-        private int counter = 0;
-        
-        @Override
-        public boolean check(AnswerTuple answerTuple) {
-                if (!toCheck) return false; 
-                
-                if (hermit == null) initialiseReasoner();
-                if (tag != 0) return tag == 1; 
-                ++counter; 
-                Timer t = new Timer(); 
-                Map<Variable, Term> sub = answerTuple.getAssignment(answerVariable[1]); 
-                Set<OWLAxiom> toCheckAxioms = qGraph.getAssertions(sub);
-                
-//              for (OWLAxiom axiom: toCheckAxioms)     System.out.println(axiom.toString());
-                
-                if (hermit.isEntailed(toCheckAxioms)) {
-                        Utility.logDebug("@TIME to check one tuple: " + t.duration()); 
-                        return true; 
-                }
-                Utility.logDebug("@TIME to check one tuple: " + t.duration()); 
-                return false; 
-        }
-
-        @Override
-        public boolean isConsistent() {
-                if (hermit == null) initialiseReasoner();                       
-                return hermit.isConsistent();
-        }
-        
-
-        public void dispose() {
-                Utility.logInfo("Hermit was called " + counter + " times.");
-                if (hermit != null) hermit.dispose(); 
-                hermit = null; 
-        }
-
-        private DependencyGraph dGraph = null; 
-        
-        public void setDependencyGraph(DependencyGraph dGraph) {
-                this.dGraph = dGraph; 
+                Integer number = counter.get(newAxiom);
+                if(number == null) counter.put(newAxiom, 1);
+                else counter.put(newAxiom, number + 1);
         }
 
 }
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 fe43e09..107d3ca 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java
@@ -104,16 +104,22 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public void outputInstance4BinaryPredicate(String iri, String filename) {
+        if(isDisposed()) throw new DisposedException();
+
         Utility.redirectCurrentOut(filename);
         outputInstance4BinaryPredicate(iri);
         Utility.closeCurrentOut();
     }
 
     public void outputInstance4BinaryPredicate(String iri) {
+        if(isDisposed()) throw new DisposedException();
+
         outputAnswers("select ?x ?y where { ?x <" + iri + "> ?y . }");
     }
 
     public void outputInstanceNumbers(String filename) {
+        if(isDisposed()) throw new DisposedException();
+
         TupleIterator predicateTuples = null;
         TupleIterator instanceTuples;
         Set<String> number = new HashSet<String>();
@@ -177,6 +183,8 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public TupleIterator internal_evaluateAgainstIDBs(String queryText) throws JRDFStoreException {
+        if(isDisposed()) throw new DisposedException();
+
         TupleIterator iter =
                 store.compileQuery(queryText, prefixes, parameters, TripleStatus.TUPLE_STATUS_IDB.union(TripleStatus.TUPLE_STATUS_EDB), TripleStatus.TUPLE_STATUS_IDB);
 //              iter.open();
@@ -184,16 +192,22 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public TupleIterator internal_evaluate(String queryText) throws JRDFStoreException {
+        if(isDisposed()) throw new DisposedException();
+
         TupleIterator iter = store.compileQuery(queryText, prefixes, parameters);
 //              iter.open();
         return iter;
     }
 
     public void setExpandEquality(boolean flag) {
+        if(isDisposed()) throw new DisposedException();
+
         parameters.m_expandEquality = flag;
     }
 
     public TupleIterator internal_evaluateNotExpanded(String queryText) throws JRDFStoreException {
+        if(isDisposed()) throw new DisposedException();
+
         parameters.m_expandEquality = false;
         TupleIterator iter = store.compileQuery(queryText, prefixes, parameters);
 //              iter.open();
@@ -202,10 +216,14 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public TupleIterator internal_evaluate(String queryText, boolean incrementally) throws JRDFStoreException {
+        if(isDisposed()) throw new DisposedException();
+
         return incrementally ? internal_evaluateAgainstIDBs(queryText) : internal_evaluate(queryText);
     }
 
     public String getUnusedRules(Collection<DLClause> clauses, boolean toUpdate) {
+        if(isDisposed()) throw new DisposedException();
+
         DLClause clause;
         for(Iterator<DLClause> iter = clauses.iterator(); iter.hasNext(); ) {
             if(materialisedRules.contains(clause = iter.next()))
@@ -219,10 +237,14 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public void outputMaterialisedRules() {
+        if(isDisposed()) throw new DisposedException();
+
         System.out.println(DLClauseHelper.toString(materialisedRules));
     }
 
     public void outputAnswers(String query) {
+        if(isDisposed()) throw new DisposedException();
+
         TupleIterator iter = null;
         try {
             iter = internal_evaluate(query);
@@ -241,6 +263,8 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public void outputInstance4UnaryPredicate(String iri) {
+        if(isDisposed()) throw new DisposedException();
+
         outputAnswers("select ?x where { ?x "
                               + "<http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <"
                               + iri
@@ -248,14 +272,20 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public void outputSubjects(String p, String o) {
+        if(isDisposed()) throw new DisposedException();
+
         outputAnswers("select x where { ?x <" + p + "> <" + o + "> . }");
     }
 
     public void outputObjects(String s, String p) {
+        if(isDisposed()) throw new DisposedException();
+
         outputAnswers("select ?x where { <" + s + "> <" + p + "> ?x . }");
     }
 
     public void outputIDBFacts() {
+        if(isDisposed()) throw new DisposedException();
+
         TupleIterator iter = null;
         try {
             iter = internal_evaluateAgainstIDBs("select distict ?x ?y ?z where { ?x ?y ?z }");
@@ -274,10 +304,14 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public void outputType4Individual(String iri) {
+        if(isDisposed()) throw new DisposedException();
+
         outputAnswers("select ?z where { <" + iri + "> " + Namespace.RDF_TYPE_QUOTED + " ?z }");
     }
 
     public int getSameAsNumber() {
+        if(isDisposed()) throw new DisposedException();
+
         TupleIterator iter = null;
         int counter = 0;
         try {
@@ -294,6 +328,8 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public UFS<String> getEqualityGroups(boolean reuse) {
+        if(isDisposed()) throw new DisposedException();
+
         if(reuse && equalityGroups != null) return equalityGroups;
 
         equalityGroups = new UFS<String>();
@@ -317,6 +353,8 @@ public class BasicQueryEngine extends RDFoxQueryEngine {
     }
 
     public void clearRulesAndIDBFacts(Collection<int[]> collection) {
+        if(isDisposed()) throw new DisposedException();
+
 //              performDeletion(collection);
         collection.clear();
         try {