Finalise implementation of ACQuA query reasoner

2 files changed, 334 insertions, 275 deletions

diff --git a/src/main/scala/uk/ac/ox/cs/acqua/reasoner/AcquaQueryReasoner.scala b/src/main/scala/uk/ac/ox/cs/acqua/reasoner/AcquaQueryReasoner.scala
index 4fe32d8..0aa5ff2 100644
--- a/src/main/scala/uk/ac/ox/cs/acqua/reasoner/AcquaQueryReasoner.scala
+++ b/src/main/scala/uk/ac/ox/cs/acqua/reasoner/AcquaQueryReasoner.scala
@@ -16,13 +16,14 @@
 
 package uk.ac.ox.cs.acqua.reasoner
 
+import java.util.LinkedList;
+
 import scala.collection.JavaConverters._
 import org.semanticweb.karma2.profile.ELHOProfile
 import org.semanticweb.owlapi.model.OWLOntology
-// import org.semanticweb.owlapi.model.parameters.Imports;
-// import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import org.semanticweb.owlapi.model.parameters.Imports
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
 import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine
-// import uk.ac.ox.cs.pagoda.owl.EqualitiesEliminator;
 import uk.ac.ox.cs.pagoda.owl.OWLHelper
 import uk.ac.ox.cs.pagoda.query.{
   AnswerTuples,
@@ -30,7 +31,7 @@ import uk.ac.ox.cs.pagoda.query.{
   GapByStore4ID2,
   QueryRecord,
 }
-import uk.ac.ox.cs.pagoda.query.QueryRecord.Step;
+import uk.ac.ox.cs.pagoda.query.QueryRecord.Step
 import uk.ac.ox.cs.pagoda.reasoner.{
   ConsistencyManager,
   MyQueryReasoner,
@@ -38,28 +39,29 @@ import uk.ac.ox.cs.pagoda.reasoner.{
 }
 import uk.ac.ox.cs.pagoda.reasoner.light.{KarmaQueryEngine,BasicQueryEngine}
 import uk.ac.ox.cs.pagoda.rules.DatalogProgram
-// import uk.ac.ox.cs.pagoda.summary.HermitSummaryFilter;
-// import uk.ac.ox.cs.pagoda.tracking.QueryTracker;
+import uk.ac.ox.cs.pagoda.summary.HermitSummaryFilter;
 import uk.ac.ox.cs.pagoda.tracking.{
+  QueryTracker,
   TrackingRuleEncoder,
   TrackingRuleEncoderDisjVar1,
   TrackingRuleEncoderWithGap,
 }
-// import uk.ac.ox.cs.pagoda.util.ExponentialInterpolation;
-// import uk.ac.ox.cs.pagoda.util.PagodaProperties;
-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;
+import uk.ac.ox.cs.pagoda.util.{
+  ExponentialInterpolation,
+  PagodaProperties,
+  Timer,
+  Utility
+}
 import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
 import uk.ac.ox.cs.rsacomb.ontology.Ontology
 import uk.ac.ox.cs.rsacomb.approximation.{Lowerbound,Upperbound}
 
-// import java.util.Collection;
-// import java.util.LinkedList;
-
 class AcquaQueryReasoner(val ontology: Ontology)
   extends QueryReasoner {
 
+  /** Compatibility convertions between PAGOdA and RSAComb */
+  import uk.ac.ox.cs.acqua.implicits.PagodaConverters._
+
   private var encoder: Option[TrackingRuleEncoder] = None
   private var lazyUpperStore: Option[MultiStageQueryEngine] = None;
 
@@ -167,9 +169,11 @@ class AcquaQueryReasoner(val ontology: Ontology)
     if (!isConsistent()) return false
     consistencyManager.extractBottomFragment();
 
-    /* Force computation of lower/upper RSA approximations */
-    lowerRSAOntology//.computeCanonicalModel()
-    upperRSAOntology//.computeCanonicalModel()
+    /* Force computation of lower RSA approximations and its canonical
+     * model. We wait to process the upperbound since it might not be
+     * necessary after all. */
+    lowerRSAOntology.computeCanonicalModel()
+    //upperRSAOntology.computeCanonicalModel()
 
     true
   }
@@ -190,127 +194,152 @@ class AcquaQueryReasoner(val ontology: Ontology)
     return _isConsistent.asBoolean
   }
 
+  /** Evaluate a query against this reasoner.
+    *
+    * This is the main entry to compute the answers to a query.
+    * By the end of the computation, the query record passed as input
+    * will contain the answers found during the answering process.
+    * This behaves conservately and will try very hard not to perform
+    * unnecessary computation.
+    *
+    * @param query the query record to evaluate.
+    */
   def evaluate(query: QueryRecord): Unit = {
-    if(queryLowerAndUpperBounds(query))
-      return;
-
-//        OWLOntology relevantOntologySubset = extractRelevantOntologySubset(queryRecord);
-
-////        queryRecord.saveRelevantOntology("/home/alessandro/Desktop/test-relevant-ontology-"+relevantOntologiesCounter+".owl");
-////        relevantOntologiesCounter++;
-
-//        if(properties.getSkolemUpperBound() == PagodaProperties.SkolemUpperBoundOptions.BEFORE_SUMMARISATION
-//                && querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord)) {
-//            return;
-//        }
-
-//        Utility.logInfo(">> Summarisation <<");
-//        HermitSummaryFilter summarisedChecker = new HermitSummaryFilter(queryRecord, properties.getToCallHermiT());
-//        if(summarisedChecker.check(queryRecord.getGapAnswers()) == 0) {
-//            summarisedChecker.dispose();
-//            return;
-//        }
-
-//        if(properties.getSkolemUpperBound() == PagodaProperties.SkolemUpperBoundOptions.AFTER_SUMMARISATION
-//                && querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord)) {
-//            summarisedChecker.dispose();
-//            return;
-//        }
-
-//        Utility.logInfo(">> Full reasoning <<");
-//        Timer t = new Timer();
-//        summarisedChecker.checkByFullReasoner(queryRecord.getGapAnswers());
-//        Utility.logDebug("Total time for full reasoner: " + t.duration());
-
-//        if(properties.getToCallHermiT())
-//            queryRecord.markAsProcessed();
-//        summarisedChecker.dispose();
-    ???
+    val processed =
+      queryLowerAndUpperBounds(query) ||
+      queryRSALowerBound(query) ||
+      queryRSAUpperBound(query)
+    if (!processed) {
+      val relevantOntologySubset: OWLOntology =
+        extractRelevantOntologySubset(query)
+
+      if (properties.getSkolemUpperBound == PagodaProperties.SkolemUpperBoundOptions.BEFORE_SUMMARISATION &&
+          querySkolemisedRelevantSubset(relevantOntologySubset, query)
+      ) return;
+
+      Utility logInfo ">> Summarisation <<"
+      val summarisedChecker: HermitSummaryFilter =
+        new HermitSummaryFilter(query, properties.getToCallHermiT)
+      if(summarisedChecker.check(query.getGapAnswers) == 0) {
+        summarisedChecker.dispose()
+        return;
+      }
+
+      if (properties.getSkolemUpperBound == PagodaProperties.SkolemUpperBoundOptions.AFTER_SUMMARISATION &&
+          querySkolemisedRelevantSubset(relevantOntologySubset, query)
+      ) {
+        summarisedChecker.dispose()
+        return;
+      }
+
+      Utility logInfo ">> Full reasoning <<"
+      timer.reset()
+      summarisedChecker checkByFullReasoner query.getGapAnswers
+      Utility logDebug s"Total time for full reasoner: ${timer.duration()}"
+
+      if (properties.getToCallHermiT) query.markAsProcessed()
+
+      summarisedChecker.dispose()
+    }
+  }
+
+  /** Only compute the upperbound for a query.
+    *
+    * @note this is not supported at the moment. Look at
+    * [[uk.ac.ox.cs.pagoda.reasoner.MyQueryReasoner]] for an example
+    * implementation.
+    */
+  def evaluateUpper(record: QueryRecord): Unit = ???
+
+  /** Clean up the query reasoner */
+  override def dispose(): Unit = {
+    super.dispose()
+    if(encoder.isDefined) encoder.get.dispose()
+    if(rlLowerStore != null) rlLowerStore.dispose();
+    if(lazyUpperStore.isDefined) lazyUpperStore.get.dispose();
+    if(elLowerStore != null) elLowerStore.dispose();
+    if(trackingStore != null) trackingStore.dispose();
+    if(consistencyManager != null) consistencyManager.dispose();
+    if(datalog != null) datalog.dispose();
+  }
+
+  /** Perform CQ anwering for a specific upper bound engine.
+    *
+    * @param store upper bound engine to be used in the computation.
+    * @param query query record.
+    * @param queryText actual text of the query to be executed.
+    * @param answerVariables answer variables for the query.
+    */
+  private def queryUpperBound(
+    store: BasicQueryEngine,
+    query: QueryRecord,
+    queryText: String,
+    answerVariables: Array[String]
+  ): Unit = {
+    var rlAnswer: AnswerTuples = null
+    try {
+      Utility logDebug queryText
+      rlAnswer = store.evaluate(queryText, answerVariables)
+      Utility logDebug timer.duration()
+      query updateUpperBoundAnswers rlAnswer
+    } finally {
+        if (rlAnswer != null) rlAnswer.dispose()
+    }
   }
 
-  def evaluateUpper(record: QueryRecord): Unit= ???
-
-//    @Override
-//    public void evaluate(QueryRecord queryRecord) {
-//    }
-
-//    @Override
-//    public void evaluateUpper(QueryRecord queryRecord) {
-//        if(isDisposed()) throw new DisposedException();
-//        // TODO? add new upper store
-//        AnswerTuples rlAnswer = null;
-//        boolean useFull = queryRecord.isBottom() || lazyUpperStore == null;
-//        try {
-//            rlAnswer =
-//                    (useFull ? trackingStore : lazyUpperStore).evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
-//            queryRecord.updateUpperBoundAnswers(rlAnswer, true);
-//        } finally {
-//            if(rlAnswer != null) rlAnswer.dispose();
-//        }
-//    }
-
-//    @Override
-//    public void dispose() {
-//        super.dispose();
-
-//        if(encoder != null) encoder.dispose();
-//        if(rlLowerStore != null) rlLowerStore.dispose();
-//        if(lazyUpperStore != null) lazyUpperStore.dispose();
-//        if(elLowerStore != null) elLowerStore.dispose();
-//        if(trackingStore != null) trackingStore.dispose();
-//        if(consistency != null) consistency.dispose();
-//        if(program != null) program.dispose();
-//    }
-
-//    protected void internal_importDataFile(String name, String datafile) {
-////            addDataFile(datafile);
-//        rlLowerStore.importRDFData(name, datafile);
-//        if(lazyUpperStore != null)
-//            lazyUpperStore.importRDFData(name, datafile);
-//        elLowerStore.importRDFData(name, datafile);
-//        trackingStore.importRDFData(name, datafile);
-//    }
-
-//    /**
-//     * It deals with blanks nodes differently from variables
-//     * according to SPARQL semantics for OWL2 Entailment Regime.
-//     * <p>
-//     * In particular variables are matched only against named individuals,
-//     * and blank nodes against named and anonymous individuals.
-//     */
-//    private boolean queryUpperStore(BasicQueryEngine upperStore, QueryRecord queryRecord,
-//                                    Tuple<String> extendedQuery, Step step) {
-//        t.reset();
-
-//        Utility.logDebug("First query type");
-//        queryUpperBound(upperStore, queryRecord, queryRecord.getQueryText(), queryRecord.getAnswerVariables());
-//        if(!queryRecord.isProcessed() && !queryRecord.getQueryText().equals(extendedQuery.get(0))) {
-//            Utility.logDebug("Second query type");
-//            queryUpperBound(upperStore, queryRecord, extendedQuery.get(0), queryRecord.getAnswerVariables());
-//        }
-//        if(!queryRecord.isProcessed() && queryRecord.hasNonAnsDistinguishedVariables()) {
-//            Utility.logDebug("Third query type");
-//            queryUpperBound(upperStore, queryRecord, extendedQuery.get(1), queryRecord.getDistinguishedVariables());
-//        }
-
-//        queryRecord.addProcessingTime(step, t.duration());
-//        if(queryRecord.isProcessed()) {
-//            queryRecord.setDifficulty(step);
-//            return true;
-//        }
-//        return false;
-//    }
-
-  /**
-   * Returns the part of the ontology relevant for Hermit, while computing the bound answers.
-   */
+  /** Perform CQ anwering for a specific upper bound engine.
+    *
+    * @param store upper bound engine to be used in the computation.
+    * @param query query record.
+    * @param extendedQuery extended version of the query.
+    * @param step difficulty of the current step.
+    * @returns whether the query has been fully answered, i.e., the
+    *          bounds computed so far coincide.
+    *
+    * @note It deals with blanks nodes differently from variables
+    * according to SPARQL semantics for OWL2 Entailment Regime. In
+    * particular variables are matched only against named individuals,
+    * and blank nodes against named and anonymous individuals.
+    */
+  private def queryUpperStore(
+    upperStore: BasicQueryEngine,
+    query: QueryRecord,
+    extendedQuery: Tuple[String],
+    step: Step
+  ): Boolean = {
+    timer.reset();
+
+    Utility logDebug "First query type"
+    queryUpperBound(upperStore, query, query.getQueryText, query.getAnswerVariables)
+    if (!query.isProcessed() && !query.getQueryText().equals(extendedQuery.get(0))) {
+      Utility logDebug "Second query type"
+      queryUpperBound(upperStore, query, extendedQuery.get(0), query.getAnswerVariables)
+    }
+    if (!query.isProcessed() && query.hasNonAnsDistinguishedVariables()) {
+      Utility logDebug "Third query type"
+      queryUpperBound(upperStore, query, extendedQuery.get(1), query.getDistinguishedVariables)
+    }
+
+    query.addProcessingTime(step, timer.duration())
+    if (query.isProcessed()) query.setDifficulty(step)
+    query.isProcessed()
+  }
+
+  /** Computes the bounds to the answers for a query.
+    * 
+    * Both the lower (RL + ELHO) and upper bounds are computed here.
+    *
+    * @param query the query to be executed
+    * @returns whether the query has been fully answered, i.e., the
+    *          bounds computed so far coincide.
+    */
   private def queryLowerAndUpperBounds(query: QueryRecord): Boolean = {
     Utility logInfo ">> Base bounds <<"
     val extendedQueryTexts: Tuple[String] = query.getExtendedQueryText()
     var rlAnswer: AnswerTuples = null
     var elAnswer: AnswerTuples = null
 
-    /* Computing RL lower bound answers */
+    /* Compute RL lower bound answers */
     timer.reset();
     try {
       rlAnswer = rlLowerStore.evaluate(query.getQueryText, query.getAnswerVariables)
@@ -321,148 +350,182 @@ class AcquaQueryReasoner(val ontology: Ontology)
     }
     query.addProcessingTime(Step.LOWER_BOUND, timer.duration());
 
+    /* Compute upper bound answers */
     if(properties.getUseAlwaysSimpleUpperBound() || lazyUpperStore.isEmpty) {
-        Utility logDebug "Tracking store"
-        // if (queryUpperStore(trackingStore, query, extendedQueryTexts, Step.SIMPLE_UPPER_BOUND))
-        //     return true;
+      Utility logDebug "Tracking store"
+      if (queryUpperStore(trackingStore, query, extendedQueryTexts, Step.SIMPLE_UPPER_BOUND))
+        return true;
+    }
+    if (!query.isBottom) {
+      Utility logDebug "Lazy store"
+      if (lazyUpperStore.isDefined && queryUpperStore(lazyUpperStore.get, query, extendedQueryTexts, Step.LAZY_UPPER_BOUND))
+        return true
     }
 
-//        if(!queryRecord.isBottom()) {
-//            Utility.logDebug("Lazy store");
-//            if(lazyUpperStore != null && queryUpperStore(lazyUpperStore, queryRecord, extendedQueryTexts, Step.LAZY_UPPER_BOUND))
-//                return true;
-//        }
-
-//        t.reset();
-//        try {
-//            elAnswer = elLowerStore.evaluate(extendedQueryTexts.get(0),
-//                                             queryRecord.getAnswerVariables(),
-//                                             queryRecord.getLowerBoundAnswers());
-//            Utility.logDebug(t.duration());
-//            queryRecord.updateLowerBoundAnswers(elAnswer);
-//        } finally {
-//            if(elAnswer != null) elAnswer.dispose();
-//        }
-//        queryRecord.addProcessingTime(Step.EL_LOWER_BOUND, t.duration());
-
-//        if(queryRecord.isProcessed()) {
-//            queryRecord.setDifficulty(Step.EL_LOWER_BOUND);
-//            return true;
-//        }
-
-    return false;
+    timer.reset()
+    /* Compute ELHO lower bound answers */
+    try {
+      elAnswer = elLowerStore.evaluate(
+        extendedQueryTexts.get(0),
+        query.getAnswerVariables,
+        query.getLowerBoundAnswers
+      )
+      Utility logDebug timer.duration()
+      query updateLowerBoundAnswers elAnswer
+    } finally {
+      if (elAnswer != null) elAnswer.dispose()
+    }
+    query.addProcessingTime(Step.EL_LOWER_BOUND, timer.duration())
+
+    if (query.isProcessed()) query.setDifficulty(Step.EL_LOWER_BOUND)
+    query.isProcessed()
+  }
+
+  /** Compute lower bound using RSAComb.
+    *
+    * @param query query record to update.
+    * @returns true if the query is fully answered.
+    */
+  private def queryRSALowerBound(query: QueryRecord): Boolean = {
+    import uk.ac.ox.cs.acqua.implicits.RSACombAnswerTuples._
+    val answers = lowerRSAOntology ask query
+    query updateLowerBoundAnswers answers
+    query.isProcessed
   }
 
-//    private OWLOntology extractRelevantOntologySubset(QueryRecord queryRecord) {
-//        Utility.logInfo(">> Relevant ontology-subset extraction <<");
-
-//        t.reset();
-
-//        QueryTracker tracker = new QueryTracker(encoder, rlLowerStore, queryRecord);
-//        OWLOntology relevantOntologySubset = tracker.extract(trackingStore, consistency.getQueryRecords(), true);
-
-//        queryRecord.addProcessingTime(Step.FRAGMENT, t.duration());
-
-//        int numOfABoxAxioms = relevantOntologySubset.getABoxAxioms(Imports.INCLUDED).size();
-//        int numOfTBoxAxioms = relevantOntologySubset.getAxiomCount() - numOfABoxAxioms;
-//        Utility.logInfo("Relevant ontology-subset has been extracted: |ABox|="
-//                                + numOfABoxAxioms + ", |TBox|=" + numOfTBoxAxioms);
-
-//        return relevantOntologySubset;
-//    }
-
-//    private void queryUpperBound(BasicQueryEngine upperStore, QueryRecord queryRecord, String queryText, String[] answerVariables) {
-//        AnswerTuples rlAnswer = null;
-//        try {
-//            Utility.logDebug(queryText);
-//            rlAnswer = upperStore.evaluate(queryText, answerVariables);
-//            Utility.logDebug(t.duration());
-//            queryRecord.updateUpperBoundAnswers(rlAnswer);
-//        } finally {
-//            if(rlAnswer != null) rlAnswer.dispose();
-//        }
-//    }
-
-//    private boolean querySkolemisedRelevantSubset(OWLOntology relevantSubset, QueryRecord queryRecord) {
-//        Utility.logInfo(">> Semi-Skolemisation <<");
-//        t.reset();
-
-//        DatalogProgram relevantProgram = new DatalogProgram(relevantSubset);
-
-//        MultiStageQueryEngine relevantStore =
-//                new MultiStageQueryEngine("Relevant-store", true); // checkValidity is true
-
-//        relevantStore.importDataFromABoxOf(relevantSubset);
-//        String relevantOriginalMarkProgram = OWLHelper.getOriginalMarkProgram(relevantSubset);
-
-//        relevantStore.materialise("Mark original individuals", relevantOriginalMarkProgram);
-
-//        boolean isFullyProcessed = false;
-//        LinkedList<Tuple<Long>> lastTwoTriplesCounts = new LinkedList<>();
-//        for (int currentMaxTermDepth = 1; !isFullyProcessed; currentMaxTermDepth++) {
-
-//            if(currentMaxTermDepth > properties.getSkolemDepth()) {
-//                Utility.logInfo("Maximum term depth reached");
-//                break;
-//            }
-
-//            if(lastTwoTriplesCounts.size() == 2) {
-//                if(lastTwoTriplesCounts.get(0).get(1).equals(lastTwoTriplesCounts.get(1).get(1)))
-//                    break;
-
-//                ExponentialInterpolation interpolation = new ExponentialInterpolation(lastTwoTriplesCounts.get(0).get(0),
-//                        lastTwoTriplesCounts.get(0).get(1),
-//                        lastTwoTriplesCounts.get(1).get(0),
-//                        lastTwoTriplesCounts.get(1).get(1));
-//                double triplesEstimate = interpolation.computeValue(currentMaxTermDepth);
-
-//                Utility.logDebug("Estimate of the number of triples:" + triplesEstimate);
-
-//                // exit condition if the query is not fully answered
-//                if(triplesEstimate > properties.getMaxTriplesInSkolemStore()) {
-//                    Utility.logInfo("Interrupting Semi-Skolemisation because of triples count limit");
-//                    break;
-//                }
-//            }
-
-//            Utility.logInfo("Trying with maximum depth " + currentMaxTermDepth);
-
-//            int materialisationTag = relevantStore.materialiseSkolemly(relevantProgram, null,
-//                    currentMaxTermDepth);
-//            queryRecord.addProcessingTime(Step.SKOLEM_UPPER_BOUND, t.duration());
-//            if(materialisationTag == -1) {
-//                relevantStore.dispose();
-//                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");
-//                break;
-//            }
-
-//            Utility.logInfo("Querying semi-Skolemised upper store...");
-//            isFullyProcessed = queryUpperStore(relevantStore, queryRecord,
-//                    queryRecord.getExtendedQueryText(),
-//                    Step.SKOLEM_UPPER_BOUND);
-
-//            try {
-//                lastTwoTriplesCounts.add
-//                        (new Tuple<>((long) currentMaxTermDepth, relevantStore.getStoreSize()));
-//            } catch (JRDFStoreException e) {
-//                e.printStackTrace();
-//                break;
-//            }
-//            if(lastTwoTriplesCounts.size() > 2)
-//                lastTwoTriplesCounts.remove();
-
-//            Utility.logDebug("Last two triples counts:" + lastTwoTriplesCounts);
-//        }
-
-//        relevantStore.dispose();
-//        Utility.logInfo("Semi-Skolemised relevant upper store has been evaluated");
-//        return isFullyProcessed;
-//    }
+  /** Compute upper bound using RSAComb.
+    *
+    * @param query query record to update.
+    * @returns true if the query is fully answered.
+    */
+  private def queryRSAUpperBound(query: QueryRecord): Boolean = {
+    import uk.ac.ox.cs.acqua.implicits.RSACombAnswerTuples._
+    val answers = upperRSAOntology ask query
+    query updateUpperBoundAnswers answers
+    query.isProcessed
+  }
+
+  /** Extract a subset of the ontology relevant to the query.
+    *
+    * @param query query record for which the subset ontology is computed.
+    * @returns an [[OWLOntology]] subset of the input ontology.
+    */
+  private def extractRelevantOntologySubset(query: QueryRecord): OWLOntology = {
+      Utility logInfo ">> Relevant ontology-subset extraction <<"
+  
+      timer.reset()
+  
+      val tracker: QueryTracker =
+        new QueryTracker(encoder.get, rlLowerStore, query)
+      val relevantOntologySubset: OWLOntology =
+        tracker.extract( trackingStore, consistencyManager.getQueryRecords, true)
+
+      query.addProcessingTime(Step.FRAGMENT, timer.duration())
+  
+      val numOfABoxAxioms: Int = relevantOntologySubset.getABoxAxioms(Imports.INCLUDED).size
+      val numOfTBoxAxioms: Int = relevantOntologySubset.getAxiomCount() - numOfABoxAxioms
+      Utility logInfo s"Relevant ontology-subset has been extracted: |ABox|=$numOfABoxAxioms, |TBox|=$numOfTBoxAxioms"
+  
+      return relevantOntologySubset
+  }
+
+  /** Query the skolemized ontology subset relevant to a query record.
+    *
+    * @param relevantSubset the relevant ontology subset.
+    * @param query the query to be answered.
+    * @returns true if the query has been fully answered.
+    *
+    * TODO: the code has been adapted from [[uk.ac.ox.cs.pagoda.reasoner.MyQueryReasoner]]
+    * and ported to Scala. There are better, more Scala-esque ways of
+    * deal with the big `while` in this function, but this should work
+    * for now.
+    */
+  private def querySkolemisedRelevantSubset(
+    relevantSubset: OWLOntology,
+    query: QueryRecord
+  ): Boolean = {
+    Utility logInfo ">> Semi-Skolemisation <<"
+    timer.reset()
+
+    val relevantProgram: DatalogProgram = new DatalogProgram(relevantSubset)
+    val relevantStore: MultiStageQueryEngine =
+      new MultiStageQueryEngine("Relevant-store", true)
+    relevantStore importDataFromABoxOf relevantSubset
+    val relevantOriginalMarkProgram: String =
+      OWLHelper getOriginalMarkProgram relevantSubset
+    relevantStore.materialise("Mark original individuals", relevantOriginalMarkProgram)
+
+    var isFullyProcessed = false
+    val lastTwoTriplesCounts: LinkedList[Tuple[Long]] = new LinkedList()
+    var currentMaxTermDepth = 1
+    var keepGoing = true
+    while (!isFullyProcessed && keepGoing) {
+      if (currentMaxTermDepth > properties.getSkolemDepth) {
+        Utility logInfo "Maximum term depth reached"
+        keepGoing = false
+      } else if (
+        lastTwoTriplesCounts.size() == 2 && (
+          lastTwoTriplesCounts.get(0).get(1).equals(lastTwoTriplesCounts.get(1).get(1)) ||
+          {
+            val interpolation: ExponentialInterpolation  =
+              new ExponentialInterpolation(
+                lastTwoTriplesCounts.get(0).get(0),
+                lastTwoTriplesCounts.get(0).get(1),
+                lastTwoTriplesCounts.get(1).get(0),
+                lastTwoTriplesCounts.get(1).get(1)
+              )
+            val triplesEstimate: Double =
+              interpolation computeValue currentMaxTermDepth
+            Utility logDebug s"Estimate of the number of triples: $triplesEstimate"
+            if (triplesEstimate > properties.getMaxTriplesInSkolemStore)
+              Utility logInfo "Interrupting Semi-Skolemisation because of triples count limit"
+            triplesEstimate > properties.getMaxTriplesInSkolemStore
+          }
+        )
+      ) {
+        keepGoing = false
+      } else {
+        Utility logInfo s"Trying with maximum depth $currentMaxTermDepth"
+
+        val materialisationTag: Int =
+          relevantStore.materialiseSkolemly(relevantProgram, null, currentMaxTermDepth)
+        query.addProcessingTime(Step.SKOLEM_UPPER_BOUND, timer.duration())
+        if (materialisationTag == -1) {
+          relevantStore.dispose()
+          throw new Error("A consistent ontology has turned out to be inconsistent in the Skolemises-relevant-upper-store")
+        }
+
+        if (materialisationTag != 1) {
+          Utility logInfo "Semi-Skolemised relevant upper store cannot be employed"
+          keepGoing = false
+        } else {
+          Utility logInfo "Querying semi-Skolemised upper store..."
+          isFullyProcessed = queryUpperStore(
+            relevantStore, query, query.getExtendedQueryText(), Step.SKOLEM_UPPER_BOUND
+          )
+
+          try {
+            lastTwoTriplesCounts.add(new Tuple(currentMaxTermDepth, relevantStore.getStoreSize))
+            if (lastTwoTriplesCounts.size() > 2)
+              lastTwoTriplesCounts.remove()
+            Utility logDebug s"Last two triples counts: $lastTwoTriplesCounts"
+            currentMaxTermDepth += 1
+          } catch {
+            case e: JRDFStoreException => {
+              e.printStackTrace()
+              keepGoing = false
+            }
+          }
+        }
+      }
+    }
+
+    relevantStore.dispose()
+    Utility logInfo "Semi-Skolemised relevant upper store has been evaluated"
+    isFullyProcessed
+  }
 
+  /** Consistency status of the ontology */
   private sealed trait ConsistencyStatus {
     val asBoolean = false
   }
diff --git a/src/main/scala/uk/ac/ox/cs/acqua/reasoner/RSAQueryReasoner.scala b/src/main/scala/uk/ac/ox/cs/acqua/reasoner/RSACombQueryReasoner.scala
index a6c5276..6d89b7b 100644
--- a/src/main/scala/uk/ac/ox/cs/acqua/reasoner/RSAQueryReasoner.scala
+++ b/src/main/scala/uk/ac/ox/cs/acqua/reasoner/RSACombQueryReasoner.scala
@@ -20,24 +20,20 @@ import java.util.Collection;
 import scala.collection.JavaConverters._
 
 import org.semanticweb.owlapi.model.OWLOntology
-import uk.ac.ox.cs.rsacomb.ontology.RSAOntology
 import uk.ac.ox.cs.rsacomb.approximation.{Approximation,Lowerbound}
-import uk.ac.ox.cs.rsacomb.ontology.Ontology
+import uk.ac.ox.cs.rsacomb.ontology.{Ontology,RSAOntology}
 import uk.ac.ox.cs.pagoda.query.QueryRecord
 import uk.ac.ox.cs.pagoda.reasoner.QueryReasoner
+import uk.ac.ox.cs.acqua.approximation.Noop
 
-class RSAQueryReasoner(val origin: Ontology) extends QueryReasoner {
+class RSACombQueryReasoner(
+  val origin: Ontology,
+  val toRSA: Approximation[RSAOntology] = Noop
+) extends QueryReasoner {
 
   /* Implicit compatibility between PAGOdA and RSAComb types */
   import uk.ac.ox.cs.acqua.implicits.PagodaConverters._
 
-  /** This class is instantiated when the input ontology is RSA.
-    * Approximation (via any algorithm with RSAOntology as target)
-    * doesn't perform anything, but is useful to turn a generic
-    * [[uk.ac.ox.cs.rsacomb.ontology.Ontology]] into an
-    * [[uk.ac.ox.cs.rsacomb.RSAOntology]].
-    */
-  private val toRSA: Approximation[RSAOntology] = new Lowerbound
   val rsa: RSAOntology = origin approximate toRSA
 
   /** Doesn't perform any action.