Many little changes.

15 files changed, 298 insertions, 54 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/Pagoda.java b/src/uk/ac/ox/cs/pagoda/Pagoda.java
index f5dce15..7d2317d 100644
--- a/src/uk/ac/ox/cs/pagoda/Pagoda.java
+++ b/src/uk/ac/ox/cs/pagoda/Pagoda.java
@@ -1,12 +1,21 @@
 package uk.ac.ox.cs.pagoda;
 
 import org.apache.commons.cli.*;
+import org.apache.commons.io.FilenameUtils;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
 import uk.ac.ox.cs.pagoda.reasoner.QueryReasoner;
 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 java.io.BufferedWriter;
+import java.io.IOException;
+import java.nio.file.Files;
 import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.Map;
 
 /**
  * Executable command line user interface.
@@ -23,7 +32,7 @@ public class Pagoda implements Runnable {
 
     /**
      * Do not use it
-     * */
+     */
     private Pagoda() {
         properties = new PagodaProperties();
     }
@@ -85,7 +94,7 @@ public class Pagoda implements Runnable {
 
     /**
      * Get a builder.
-     * */
+     */
     public static PagodaBuilder builder() {
         return new PagodaBuilder();
     }
@@ -102,21 +111,48 @@ public class Pagoda implements Runnable {
         try {
             Timer t = new Timer();
             pagoda = QueryReasoner.getInstance(properties);
-            if (pagoda == null) return;
-
-            Utility.logInfo("Preprocessing Done in " + t.duration()     + " seconds.");
-
-            if (properties.getQueryPath() != null)
-                for (String queryFile: properties.getQueryPath().split(";"))
-                    pagoda.evaluate(pagoda.getQueryManager().collectQueryRecords(queryFile));
+            if(pagoda == null) return;
+
+            Utility.logInfo("Preprocessing Done in " + t.duration() + " seconds.");
+
+            if(properties.getQueryPath() != null) {
+                for(String queryFile : properties.getQueryPath().split(";")) {
+                    Collection<QueryRecord> queryRecords = pagoda.getQueryManager().collectQueryRecords(queryFile);
+                    pagoda.evaluate(queryRecords);
+
+                    if(PagodaProperties.isDebuggingMode()) {
+                        HashMap<String, Map<String, String>> statistics = new HashMap<>();
+                        for(QueryRecord queryRecord : queryRecords) {
+                            statistics.put(queryRecord.getQueryID(), queryRecord.getStatistics());
+                        }
+                        String statisticsFilename = getStatisticsFilename(properties, queryFile);
+                        try(BufferedWriter writer = Files.newBufferedWriter(Paths.get(statisticsFilename))) {
+                            QueryRecord.GsonCreator.getInstance().toJson(statistics, writer);
+                        } catch(IOException e) {
+                            Utility.logError("Unable to save statistics");
+                        }
+                    }
+                }
+            }
         } finally {
-            if (pagoda != null) pagoda.dispose();
+            if(pagoda != null) pagoda.dispose();
         }
     }
 
+    private String getStatisticsFilename(PagodaProperties properties, String queryFile) {
+        String statisticsFilename = "statistics_" +
+                FilenameUtils.removeExtension(FilenameUtils.getName(properties.getOntologyPath().replaceAll("_", "-")));
+        statisticsFilename += "_" + FilenameUtils.removeExtension(FilenameUtils.getName(queryFile).replaceAll("_", "-"));
+        statisticsFilename += "_" + ((properties.getUseSkolemUpperBound()) ? "skolem" : "");
+        statisticsFilename += ".json";
+        statisticsFilename = FilenameUtils.concat(properties.getStatisticsDir().toString(),
+                                                  statisticsFilename);
+        return statisticsFilename;
+    }
+
     /**
      * Allows to set the parameters before creating a Pagoda instance.
-     * */
+     */
     public static class PagodaBuilder {
 
         private Pagoda instance;
diff --git a/src/uk/ac/ox/cs/pagoda/endomorph/plan/OpenEndPlan.java b/src/uk/ac/ox/cs/pagoda/endomorph/plan/OpenEndPlan.java
index 73a27bf..a46da85 100644
--- a/src/uk/ac/ox/cs/pagoda/endomorph/plan/OpenEndPlan.java
+++ b/src/uk/ac/ox/cs/pagoda/endomorph/plan/OpenEndPlan.java
@@ -7,6 +7,7 @@ import uk.ac.ox.cs.pagoda.query.QueryRecord;
 import uk.ac.ox.cs.pagoda.query.QueryRecord.Step;
 import uk.ac.ox.cs.pagoda.reasoner.full.Checker;
 import uk.ac.ox.cs.pagoda.summary.NodeTuple;
+import uk.ac.ox.cs.pagoda.util.SimpleProgressBar;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
 
@@ -40,7 +41,11 @@ public class OpenEndPlan implements CheckPlan {
                 Timer t = new Timer(); 
                 
                 AnswerTuple answerTuple;
-                while (!topo.isEmpty()) { 
+                int initialTopoSize = topo.size();
+                // TODO test progress bar
+                SimpleProgressBar progressBar = new SimpleProgressBar("Checking", initialTopoSize);
+                while (!topo.isEmpty()) {
+                        progressBar.update(initialTopoSize - topo.size());
                         if (flag) {
                                 clique = topo.removeFirst();
                                 if (redundant(clique)) continue; 
@@ -70,6 +75,8 @@ public class OpenEndPlan implements CheckPlan {
                                 }
                         }
                 }
+                progressBar.update(initialTopoSize - topo.size());
+                progressBar.dispose();
                 
 //              Utility.logDebug("HermiT was called " + times + " times."); 
                 
diff --git a/src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java b/src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java
index 530b97f..81c99a4 100644
--- a/src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java
+++ b/src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java
@@ -37,7 +37,7 @@ public class RuleHelper {
                 boolean lastSpace = true;
                 for (Atom headAtom: clause.getHeadAtoms()) {
                         if ((atomText = getText(headAtom)) == null) continue; 
-                        if (!lastSpace) buf.append(" | ");
+                        if (!lastSpace) buf.append(" v ");
                         buf.append(atomText);
                         lastSpace = false;
                 }
diff --git a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
index 291af27..d88376f 100644
--- a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
+++ b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
@@ -171,14 +171,10 @@ public class QueryRecord extends Disposable {
     }
 
     public String getQueryText() {
-        if(isDisposed()) throw new DisposedException();
-
         return queryText;
     }
 
     public String getQueryID() {
-        if(isDisposed()) throw new DisposedException();
-
         return stringQueryID;
     }
 
@@ -193,8 +189,6 @@ public class QueryRecord extends Disposable {
     }
 
     public String toString() {
-        if(isDisposed()) throw new DisposedException();
-
         return queryText;
     }
 
@@ -281,6 +275,20 @@ public class QueryRecord extends Disposable {
         }
     }
 
+    public Map<String, String> getStatistics() {
+        HashMap<String, String> result = new HashMap<>();
+
+        double totalTime = 0.0;
+        for(Step step : Step.values()) {
+            result.put(step.toString(), Double.toString(timer[step.ordinal()]));
+            totalTime += timer[step.ordinal()];
+        }
+        result.put("totalTime", Double.toString(totalTime));
+        result.put("difficulty", difficulty.toString());
+
+        return result;
+    }
+
     public String outputSoundAnswerTuple() {
         if(isDisposed()) throw new DisposedException();
 
@@ -359,6 +367,8 @@ public class QueryRecord extends Disposable {
                 Utility.logError("The answer (" + answer + ") cannot be removed, because it is not in the upper bound.");
             gapAnswerTuples.remove(answer);
         }
+        int numOfUpperBoundAnswers = soundAnswerTuples.size() + gapAnswerTuples.size();
+        Utility.logInfo("Upper bound answers updated: " + numOfUpperBoundAnswers);
     }
 
     public void addLowerBoundAnswers(Collection<AnswerTuple> answers) {
@@ -722,7 +732,9 @@ public class QueryRecord extends Disposable {
 
         @Override
         public String toString() {
-            return WordUtils.capitalizeFully(super.toString(), new char[]{'_'}).replace("_", "");
+            String s = super.toString();
+            if(s == null) return null;
+            return WordUtils.capitalizeFully(s, new char[]{'_'}).replace("_", "");
         }
     }
 
diff --git a/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java b/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java
index a09cf5b..116e724 100644
--- a/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java
+++ b/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java
@@ -102,16 +102,17 @@ public class QueryGraph {
 //              return axioms;
 //      }
 
-        public Set<OWLAxiom> getExistentialAxioms() {
+        public Set<OWLAxiom> getExistentialAxioms(Map<Variable, Term> assignment) {
                 if(!rollable_edges.isEmpty()) return null;
 
+                Visitor visitor = new Visitor(factory, assignment);
                 Set<OWLAxiom> axioms = new HashSet<>();
                 for(Map.Entry<Term, Set<OWLClassExpression>> entry : concepts.map.entrySet()) {
                         if(existVars.contains(entry.getKey())) {
                                 OWLClassExpression conjunction =
                                                 factory.getOWLObjectIntersectionOf(factory.getOWLThing());
                                 for(OWLClassExpression owlClassExpression : entry.getValue()) {
-                                        conjunction = factory.getOWLObjectIntersectionOf(conjunction, owlClassExpression);
+                                        conjunction = factory.getOWLObjectIntersectionOf(conjunction, owlClassExpression.accept(visitor));
                                 }
                                 axioms.add(factory.getOWLSubClassOfAxiom(conjunction, factory.getOWLNothing()));
                         }
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
index e5074d5..b419289 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -68,9 +68,9 @@ class MyQueryReasoner extends QueryReasoner {
 
         ontology = o;
         program = new DatalogProgram(ontology, properties.getToClassify());
-                program.getLower().save();
-                program.getUpper().save();
-                program.getGeneral().save();
+//              program.getLower().save();
+//              program.getUpper().save();
+//              program.getGeneral().save();
 
         if(!program.getGeneral().isHorn())
             lazyUpperStore = new MultiStageQueryEngine("lazy-upper-bound", true);
@@ -195,19 +195,24 @@ class MyQueryReasoner extends QueryReasoner {
 
         Utility.logInfo("Summarisation...");
         HermitSummaryFilter summarisedChecker = new HermitSummaryFilter(queryRecord, properties.getToCallHermiT());
-        if(summarisedChecker.check(queryRecord.getGapAnswers()) == 0)
+        if(summarisedChecker.check(queryRecord.getGapAnswers()) == 0) {
+            summarisedChecker.dispose();
             return;
+        }
 
         if(properties.getUseSkolemUpperBound() &&
-                querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord))
+                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());
 
-        queryRecord.markAsProcessed();
+        if(properties.getToCallHermiT())
+            queryRecord.markAsProcessed();
         summarisedChecker.dispose();
     }
 
@@ -377,7 +382,7 @@ class MyQueryReasoner extends QueryReasoner {
         relevantStore.importDataFromABoxOf(relevantSubset);
         String relevantOriginalMarkProgram = OWLHelper.getOriginalMarkProgram(relevantSubset);
 
-        int queryDependentMaxTermDepth = 5; // TODO make it dynamic
+        int queryDependentMaxTermDepth = 1; // TODO make it dynamic
         relevantStore.materialise("Mark original individuals", relevantOriginalMarkProgram);
         int materialisationTag = relevantStore.materialiseSkolemly(relevantProgram, null,
                                                                    queryDependentMaxTermDepth);
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 cfae88b..9574845 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
@@ -99,7 +99,6 @@ public class HermitChecker extends Checker {
 
         if(!toCheck) return false;
         ++noOfCalls;
-
         if(tag != 0) return tag == 1;
         if(hermit == null) initialiseReasoner();
 
@@ -107,19 +106,19 @@ public class HermitChecker extends Checker {
         Map<Variable, Term> sub = answerTuple.getAssignment(answerVariable[1]);
         Set<OWLAxiom> toCheckAxioms = qGraph.getAssertions(sub);
 
-        // TODO complete
-        Set<OWLAxiom> toCheckExistentialAxioms = qGraph.getExistentialAxioms();
-
-        // TODO possibly inefficient
-        for(OWLAxiom subclassAxiom : toCheckExistentialAxioms) {
-            Utility.logDebug("Checking consistency of ontology union " + subclassAxiom);
-            ontology.getOWLOntologyManager().addAxiom(ontology, subclassAxiom);
-            if(hermit.isConsistent()) {
-                Utility.logDebug("@TIME to check one tuple: " + t.duration());
-                return false;
-            }
-            ontology.getOWLOntologyManager().removeAxiom(ontology, subclassAxiom);
-        }
+//        // TODO complete
+//        Set<OWLAxiom> toCheckExistentialAxioms = qGraph.getExistentialAxioms(sub);
+//
+//        // TODO possibly inefficient
+//        for(OWLAxiom subclassAxiom : toCheckExistentialAxioms) {
+//            Utility.logInfo("Checking consistency of ontology union " + subclassAxiom);
+//            ontology.getOWLOntologyManager().addAxiom(ontology, subclassAxiom);
+//            if(hermit.isConsistent()) {
+//                Utility.logDebug("@TIME to check one tuple: " + t.duration());
+//                return false;
+//            }
+//            ontology.getOWLOntologyManager().removeAxiom(ontology, subclassAxiom);
+//        }
 
 
 //              for (OWLAxiom axiom: toCheckAxioms)     System.out.println(axiom.toString());
diff --git a/src/uk/ac/ox/cs/pagoda/rules/Program.java b/src/uk/ac/ox/cs/pagoda/rules/Program.java
index 85000e3..a0edf85 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/Program.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/Program.java
@@ -316,9 +316,10 @@ protected PredicateDependency dependencyGraph;
         private Atom getAtom(OWLObjectPropertyExpression exp, Variable x, Variable y) {
                 if(exp instanceof OWLObjectProperty)
                         return Atom.create(AtomicRole.create(((OWLObjectProperty) exp).toStringID()), x, y);
-                OWLObjectInverseOf inverseOf;
-                if(exp instanceof OWLObjectInverseOf && (inverseOf =
-                                (OWLObjectInverseOf) exp).getInverse() instanceof OWLObjectProperty)
+                // TODO fixed, test it
+                OWLObjectPropertyExpression inverseOf;
+                if(exp instanceof OWLObjectInverseOf && (inverseOf = (
+                                (OWLObjectInverseOf) exp).getInverse()) instanceof OWLObjectProperty)
                         return Atom.create(AtomicRole.create(((OWLObjectProperty) inverseOf).toStringID()), x, y);
                 return null;
         }
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 dfe1e59..d694b61 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -64,14 +64,14 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
 
     private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
         ArrayList<DLClause> result = new ArrayList<>();
-        for(Tuple<Individual> violationTuple : violationTuples)
+        for(Tuple<Individual> violationTuple : violationTuples) {
             if(getMaxDepth(violationTuple) < maxTermDepth) {
                 result.addAll(getGroundSkolemisation(clause, originalClause, violationTuple));
                 Utility.logDebug("Approximating maximal individual by a constant in rule:" + originalClause);
             }
             else
                 result.addAll(alternativeApproximator.convert(clause, originalClause, null));
-
+        }
 
         return result;
     }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java b/src/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java
new file mode 100644
index 0000000..2adb66b
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java
@@ -0,0 +1,100 @@
+package uk.ac.ox.cs.pagoda.rules.clauses;
+
+public class Clause {
+
+//    public static final String IF = ":-";
+//    public static final String OR = "|";
+//    public static final String AND = ",";
+//
+//    protected final List<List<Atom>> head;
+//    protected final List<Atom> body;
+//
+//    protected Clause(Atom[] headAtoms, Atom[] bodyAtoms) {
+//        this.head = Collections.singletonList(Arrays.asList(headAtoms));
+//        this.body= Arrays.asList(bodyAtoms);
+//    }
+//
+//    protected Clause(String s) {
+//        this.headAtoms = null;
+//        this.bodyAtoms = null;
+//    }
+//
+//    public int getHeadLength() {
+//        return headAtoms.length;
+//    }
+//
+//    public Atom getHeadAtom(int atomIndex) {
+//        return headAtoms[atomIndex];
+//    }
+//
+//    public Atom[] getHeadAtoms() {
+//        return headAtoms.clone();
+//    }
+//
+//    public int getBodyLength() {
+//        return bodyAtoms.length;
+//    }
+//
+//    public Atom getBodyAtom(int atomIndex) {
+//        return bodyAtoms[atomIndex];
+//    }
+//
+//    public Atom[] getBodyAtoms() {
+//        return bodyAtoms.clone();
+//    }
+//
+//    public String toString(Prefixes prefixes) {
+//        StringBuilder buffer = new StringBuilder();
+//        for(int headIndex = 0; headIndex < headAtoms.length; headIndex++) {
+//            if(headIndex != 0)
+//                buffer.append(" ").append(OR).append(" ");
+//            buffer.append(headAtoms[headIndex].toString(prefixes));
+//        }
+//        buffer.append(" ").append(IF).append(" ");
+//        for(int bodyIndex = 0; bodyIndex < bodyAtoms.length; bodyIndex++) {
+//            if(bodyIndex != 0)
+//                buffer.append(AND).append(" ");
+//            buffer.append(bodyAtoms[bodyIndex].toString(prefixes));
+//        }
+//        return buffer.toString();
+//    }
+//
+//    public String toString() {
+//        return toString(Prefixes.STANDARD_PREFIXES);
+//    }
+//
+//    protected static InterningManager<? extends Clause> s_interningManager = new InterningManager<Clause>() {
+//        protected boolean equal(Clause object1, Clause object2) {
+//            if(object1.head.length != object2.headAtoms.length
+//                    || object1.bodyAtoms.length != object2.bodyAtoms.length)
+//                return false;
+//            for(int index = object1.headAtoms.length - 1; index >= 0; --index)
+//                if(object1.headAtoms[index] != object2.headAtoms[index])
+//                    return false;
+//            for(int index = object1.bodyAtoms.length - 1; index >= 0; --index)
+//                if(object1.bodyAtoms[index] != object2.bodyAtoms[index])
+//                    return false;
+//            return true;
+//        }
+//
+//        protected int getHashCode(Clause object) {
+//            int hashCode = 0;
+//            for(int index = object.bodyAtoms.length - 1; index >= 0; --index)
+//                hashCode += object.bodyAtoms[index].hashCode();
+//            for(int index = object.headAtoms.length - 1; index >= 0; --index)
+//                hashCode += object.headAtoms[index].hashCode();
+//            return hashCode;
+//        }
+//    };
+//
+//    /**
+//     * Creates a clause from a string.
+//     *
+//     * @param s
+//     * @return
+//     */
+//    public static Clause create(String s) {
+//        return s_interningManager.intern(new Clause(s));
+//    }
+
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/clauses/Conjunction.java b/src/uk/ac/ox/cs/pagoda/rules/clauses/Conjunction.java
new file mode 100644
index 0000000..91bb3e7
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/clauses/Conjunction.java
@@ -0,0 +1,4 @@
+package uk.ac.ox.cs.pagoda.rules.clauses;
+
+public class Conjunction {
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/clauses/DLClause.java b/src/uk/ac/ox/cs/pagoda/rules/clauses/DLClause.java
new file mode 100644
index 0000000..7394be0
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/clauses/DLClause.java
@@ -0,0 +1,12 @@
+package uk.ac.ox.cs.pagoda.rules.clauses;
+
+public class DLClause extends Clause {
+
+//    private DLClause(Atom[] headAtoms, Atom[] bodyAtoms) {
+//        super(headAtoms, bodyAtoms);
+//    }
+//
+//    public static DLClause create(Atom[] headAtoms, Atom[] bodyAtoms) {
+//        return s_interningManager.intern(new DLClause(headAtoms, bodyAtoms));
+//    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java b/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
index 2d2198f..6fcf887 100644
--- a/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
+++ b/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
@@ -6,12 +6,12 @@ import uk.ac.ox.cs.pagoda.endomorph.Endomorph;
 import uk.ac.ox.cs.pagoda.owl.OWLHelper;
 import uk.ac.ox.cs.pagoda.query.AnswerTuple;
 import uk.ac.ox.cs.pagoda.query.AnswerTuples;
-import uk.ac.ox.cs.pagoda.query.AnswerTuplesImp;
 import uk.ac.ox.cs.pagoda.query.QueryRecord;
 import uk.ac.ox.cs.pagoda.query.QueryRecord.Step;
 import uk.ac.ox.cs.pagoda.reasoner.full.Checker;
 import uk.ac.ox.cs.pagoda.reasoner.full.HermitChecker;
 import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoder;
+import uk.ac.ox.cs.pagoda.util.SimpleProgressBar;
 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;
@@ -122,12 +122,12 @@ public class HermitSummaryFilter extends Checker {
                 if(m_record.isProcessed())
                         return 0;
 
-                Utility.logDebug("The number of answers to be checked with HermiT: " + passed.size() + "/" + counter);
+//              Utility.logDebug("The number of answers to be checked with HermiT: " + passed.size() + "/" + counter);
                 m_record.setDifficulty(Step.FULL_REASONING);
 
-                if(summarisedConsistency)
-                        return endomorphismChecker.check(new AnswerTuplesImp(m_record.getAnswerVariables(), passed));
-                else
+//              if(summarisedConsistency)
+//                      return endomorphismChecker.check(new AnswerTuplesImp(m_record.getAnswerVariables(), passed));
+//              else
                         return endomorphismChecker.check(answers);
         }
 
@@ -145,9 +145,17 @@ public class HermitSummaryFilter extends Checker {
                         Set<AnswerTuple> succ = new HashSet<AnswerTuple>();
                         Set<AnswerTuple> falsified = new HashSet<AnswerTuple>(), fail = new HashSet<AnswerTuple>();
 
+                        int numOfAnswers = 0;
+                        for(; answers.isValid(); answers.moveNext()) {
+                                numOfAnswers++;
+                        }
+                        answers.reset();
+
                         counter = 0;
                         AnswerTuple representative;
+                        SimpleProgressBar progressBar = new SimpleProgressBar("Summarised checking", numOfAnswers);
                         for(AnswerTuple answer; answers.isValid(); answers.moveNext()) {
+                                progressBar.update(counter);
                                 ++counter;
                                 answer = answers.getTuple();
                                 representative = summary.getSummary(answer);
@@ -164,6 +172,7 @@ public class HermitSummaryFilter extends Checker {
                                         falsified.add(answer);
                                 }
                         }
+                        progressBar.dispose();
                         answers.dispose();
 
                         Utility.logDebug("@TIME to filter out non-answers by summarisation: " + t.duration());
diff --git a/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java b/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
index 4991d0d..7b68400 100644
--- a/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
+++ b/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
@@ -15,6 +15,7 @@ public class PagodaProperties {
         public static final boolean DEFAULT_DEBUG = false;
         private static final boolean DEFAULT_USE_ALWAYS_SIMPLE_UPPER_BOUND;
         private static final boolean DEFAULT_USE_SKOLEM_UPPER_BOUND;
+        private static final boolean DEFAULT_TO_CALL_HERMIT;
         private static final Path DEFAULT_STATISTICS_DIR;
 
         public static boolean shellModeDefault = false;
@@ -23,6 +24,7 @@ public class PagodaProperties {
         static {
                 boolean defaultUseAlwaysSimpleUpperBound = false;
                 boolean defaultUseSkolemUpperBound = true;
+                boolean toCallHermit = true;
                 Path defaultStatisticsDir = null;
 
                 try(InputStream in = PagodaProperties.class.getClassLoader().getResourceAsStream(CONFIG_FILE)) {
@@ -52,12 +54,20 @@ public class PagodaProperties {
                                 else
                                         logger.debug("By default the Skolem upper bound is disabled");
                         }
+                        if(config.containsKey("toCallHermit")) {
+                                toCallHermit = Boolean.parseBoolean(config.getProperty("toCallHermit"));
+                                if(toCallHermit)
+                                        logger.debug("By default Hermit is enabled");
+                                else
+                                        logger.debug("By default Hermit is disabled");
+                        }
 
                 } catch(IOException e) {
                         e.printStackTrace();
                 }
                 DEFAULT_USE_ALWAYS_SIMPLE_UPPER_BOUND = defaultUseAlwaysSimpleUpperBound;
                 DEFAULT_USE_SKOLEM_UPPER_BOUND = defaultUseSkolemUpperBound;
+                DEFAULT_TO_CALL_HERMIT = toCallHermit;
                 DEFAULT_STATISTICS_DIR = defaultStatisticsDir;
         }
 
@@ -66,7 +76,7 @@ public class PagodaProperties {
         String queryPath = null;
         String answerPath = null;
         boolean toClassify = true;
-        boolean toCallHermiT = true;
+        boolean toCallHermiT = DEFAULT_TO_CALL_HERMIT;
         boolean shellMode = shellModeDefault;
         private boolean useAlwaysSimpleUpperBound = DEFAULT_USE_ALWAYS_SIMPLE_UPPER_BOUND;
         private boolean useSkolemUpperBound = DEFAULT_USE_SKOLEM_UPPER_BOUND;
diff --git a/src/uk/ac/ox/cs/pagoda/util/SimpleProgressBar.java b/src/uk/ac/ox/cs/pagoda/util/SimpleProgressBar.java
new file mode 100644
index 0000000..3c4aad7
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/util/SimpleProgressBar.java
@@ -0,0 +1,48 @@
+package uk.ac.ox.cs.pagoda.util;
+
+import uk.ac.ox.cs.pagoda.util.disposable.Disposable;
+
+public class SimpleProgressBar extends Disposable {
+
+    private final String name;
+    private int lastPercent;
+    private int maxValue;
+
+    public SimpleProgressBar() {
+        this("");
+    }
+
+    public SimpleProgressBar(String name) {
+        this(name, 100);
+    }
+
+    public SimpleProgressBar(String name, int maxValue) {
+        this.name = name;
+        this.maxValue = maxValue;
+    }
+
+    public void update(int value) {
+        int percent = value * 100 / maxValue;
+        StringBuilder template = new StringBuilder("\r" + name + " [");
+        for (int i = 0; i < 50; i++) {
+            if (i < percent * .5) {
+                template.append("=");
+            } else if (i == percent * .5) {
+                template.append(">");
+            } else {
+                template.append(" ");
+            }
+        }
+        template.append("] %s   ");
+        System.out.printf(template.toString(), percent + "%");
+        System.out.flush();
+        lastPercent = percent;
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+
+        System.out.println();
+    }
+}