From 39b60d4225f5efa4e0287a2c6ce69d90391c69db Mon Sep 17 00:00:00 2001 From: RncLsn Date: Fri, 3 Jul 2015 19:09:31 +0100 Subject: Many little changes. --- src/uk/ac/ox/cs/pagoda/Pagoda.java | 58 +++++++++--- .../ox/cs/pagoda/endomorph/plan/OpenEndPlan.java | 9 +- src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java | 2 +- src/uk/ac/ox/cs/pagoda/query/QueryRecord.java | 26 ++++-- .../ac/ox/cs/pagoda/query/rollup/QueryGraph.java | 5 +- .../ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java | 19 ++-- .../ox/cs/pagoda/reasoner/full/HermitChecker.java | 27 +++--- src/uk/ac/ox/cs/pagoda/rules/Program.java | 7 +- .../LimitedSkolemisationApproximator.java | 4 +- src/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java | 100 +++++++++++++++++++++ .../ac/ox/cs/pagoda/rules/clauses/Conjunction.java | 4 + src/uk/ac/ox/cs/pagoda/rules/clauses/DLClause.java | 12 +++ .../ox/cs/pagoda/summary/HermitSummaryFilter.java | 19 ++-- src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java | 12 ++- src/uk/ac/ox/cs/pagoda/util/SimpleProgressBar.java | 48 ++++++++++ 15 files changed, 298 insertions(+), 54 deletions(-) create mode 100644 src/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/clauses/Conjunction.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/clauses/DLClause.java create mode 100644 src/uk/ac/ox/cs/pagoda/util/SimpleProgressBar.java (limited to 'src/uk') 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 queryRecords = pagoda.getQueryManager().collectQueryRecords(queryFile); + pagoda.evaluate(queryRecords); + + if(PagodaProperties.isDebuggingMode()) { + HashMap> 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 getStatistics() { + HashMap 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 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 getExistentialAxioms() { + public Set getExistentialAxioms(Map assignment) { if(!rollable_edges.isEmpty()) return null; + Visitor visitor = new Visitor(factory, assignment); Set axioms = new HashSet<>(); for(Map.Entry> 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 sub = answerTuple.getAssignment(answerVariable[1]); Set toCheckAxioms = qGraph.getAssertions(sub); - // TODO complete - Set 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 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 overApprox(DLClause clause, DLClause originalClause, Collection> violationTuples) { ArrayList result = new ArrayList<>(); - for(Tuple violationTuple : violationTuples) + for(Tuple 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> head; +// protected final List 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 s_interningManager = new InterningManager() { +// 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 succ = new HashSet(); Set falsified = new HashSet(), fail = new HashSet(); + 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(); + } +} -- cgit v1.2.3