From 51cfc39903ae53cbcaba9a9f5c69cac08ae63fa7 Mon Sep 17 00:00:00 2001 From: RncLsn Date: Thu, 4 Jun 2015 14:37:25 +0100 Subject: Restored fixed SkolemTermsManager (went lost in some revert). --- src/uk/ac/ox/cs/pagoda/query/QueryRecord.java | 2 +- .../ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java | 6 +-- .../LimitedSkolemisationApproximator.java | 39 +++++++------- .../rules/approximators/SkolemTermsManager.java | 59 ++++++++++------------ 4 files changed, 52 insertions(+), 54 deletions(-) (limited to 'src/uk/ac/ox/cs') diff --git a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java index dee2966..7f02741 100644 --- a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java +++ b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java @@ -707,7 +707,7 @@ public class QueryRecord extends Disposable { UPPER_BOUND, SIMPLE_UPPER_BOUND, LAZY_UPPER_BOUND, - L_SKOLEM_UPPER_BOUND, + SKOLEM_UPPER_BOUND, EL_LOWER_BOUND, FRAGMENT, FRAGMENT_REFINEMENT, diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java index ed6589a..123bd5e 100644 --- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java +++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java @@ -370,10 +370,10 @@ class MyQueryReasoner extends QueryReasoner { relevantStore.importDataFromABoxOf(relevantSubset); - int queryDependentMaxTermDepth = 10; // TODO make it dynamic + int queryDependentMaxTermDepth = 1; // TODO make it dynamic int materialisationTag = relevantStore.materialiseSkolemly(relevantProgram, null, queryDependentMaxTermDepth); - queryRecord.addProcessingTime(Step.L_SKOLEM_UPPER_BOUND, t.duration()); + queryRecord.addProcessingTime(Step.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"); @@ -385,7 +385,7 @@ class MyQueryReasoner extends QueryReasoner { boolean isFullyProcessed = queryUpperStore(relevantStore, queryRecord, queryRecord.getExtendedQueryText(), - Step.L_SKOLEM_UPPER_BOUND); + Step.SKOLEM_UPPER_BOUND); Utility.logInfo("Semi-Skolemised relevant upper store has been evaluated"); return isFullyProcessed; } 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 5f6e362..dc2ba8a 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java @@ -18,7 +18,7 @@ import java.util.Collection; * it Skolemises the rule * if all the terms in the substitution have depth less than a given depth, * otherwise it approximates using an alternative TupleDependentApproximator. - * */ + */ public class LimitedSkolemisationApproximator implements TupleDependentApproximator { private static final Atom[] EMPTY_BODY = new Atom[0]; @@ -41,7 +41,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima public Collection convert(DLClause clause, DLClause originalClause, Collection> violationTuples) { - switch (clause.getHeadLength()) { + switch(clause.getHeadLength()) { case 1: return overApprox(clause, originalClause, violationTuples); case 0: @@ -65,7 +65,7 @@ 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(alternativeApproximator.convert(clause, originalClause, null)); Utility.logDebug("Approximating maximal individual by a constant in rule:" + originalClause); @@ -84,7 +84,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima // TODO check: strong assumption, the first tuples are the common ones TupleBuilder commonIndividualsBuilder = new TupleBuilder<>(); - for (int i = 0; i < commonVars.length; i++) + for(int i = 0; i < commonVars.length; i++) commonIndividualsBuilder.append(violationTuple.get(i)); Tuple commonIndividuals = commonIndividualsBuilder.build(); @@ -96,54 +96,55 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima // BEGIN: copy and paste ArrayList ret = new ArrayList<>(); DLPredicate predicate = headAtom.getDLPredicate(); - if (predicate instanceof AtLeastConcept) { + if(predicate instanceof AtLeastConcept) { AtLeastConcept atLeastConcept = (AtLeastConcept) predicate; LiteralConcept concept = atLeastConcept.getToConcept(); Role role = atLeastConcept.getOnRole(); AtomicConcept atomicConcept; - if (concept instanceof AtomicNegationConcept) { + if(concept instanceof AtomicNegationConcept) { // TODO CHECK: is this already in MultiStageUpperProgram? - Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X); + Atom atom1 = + Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X); Atom atom2 = Atom.create(atomicConcept = OverApproxExist.getNegationConcept(atomicConcept), X); - ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2})); + ret.add(DLClause.create(new Atom[0], new Atom[]{atom1, atom2})); } else { atomicConcept = (AtomicConcept) concept; - if (atomicConcept.equals(AtomicConcept.THING)) + if(atomicConcept.equals(AtomicConcept.THING)) atomicConcept = null; } int card = atLeastConcept.getNumber(); Individual[] individuals = new Individual[card]; SkolemTermsManager termsManager = SkolemTermsManager.getInstance(); - for (int i = 0; i < card; ++i) + for(int i = 0; i < card; ++i) individuals[i] = termsManager.getFreshIndividual(originalClause, offset + i, commonIndividuals); - for (int i = 0; i < card; ++i) { - if (atomicConcept != null) - ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY)); + for(int i = 0; i < card; ++i) { + if(atomicConcept != null) + ret.add(DLClause.create(new Atom[]{Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY)); Atom atom = role instanceof AtomicRole ? Atom.create((AtomicRole) role, commonIndividuals.get(0), individuals[i]) : Atom.create(((InverseRole) role).getInverseOf(), individuals[i], commonIndividuals.get(0)); - ret.add(DLClause.create(new Atom[] {atom}, EMPTY_BODY)); + ret.add(DLClause.create(new Atom[]{atom}, EMPTY_BODY)); } - for (int i = 0; i < card; ++i) - for (int j = i + 1; j < card; ++j) + for(int i = 0; i < card; ++i) + for(int j = i + 1; j < card; ++j) // TODO to be checked ... different as - ret.add(DLClause.create(new Atom[] {Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, EMPTY_BODY)); + ret.add(DLClause.create(new Atom[]{Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, EMPTY_BODY)); } - else if (predicate instanceof AtLeastDataRange) { + else if(predicate instanceof AtLeastDataRange) { // TODO to be implemented ... } else - ret.add(DLClause.create(new Atom[] {headAtom}, EMPTY_BODY)); + ret.add(DLClause.create(new Atom[]{headAtom}, EMPTY_BODY)); return ret; diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java index 368c014..07ad1f9 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java @@ -17,13 +17,12 @@ public class SkolemTermsManager { private static SkolemTermsManager skolemTermsManager; private int termsCounter = 0; - private Map mapClauseToId = new HashMap<>(); - private Map mapTermToDepth = new HashMap<>(); + private Map clauseToId_map = new HashMap<>(); + private Map individualToDepth_map = new HashMap<>(); private int dependenciesCounter = 0; - // TODO replace with hashcode. in case of collision you get only a different upper bound model. - // TODO you can use a cash. - private Map, Integer> mapDependencyToId = new HashMap<>(); + // TODO replace with hashcode. in case of collision you would get only a different upper bound model. + private Map, Integer> dependencyToId_map = new HashMap<>(); private SkolemTermsManager() { } @@ -38,6 +37,11 @@ public class SkolemTermsManager { return -1; } + /** + * Returns the existing unique SkolemTermsManager or a new one. + *

+ * Indeed the SkolemTermsManager is a singleton. + */ public static SkolemTermsManager getInstance() { if(skolemTermsManager == null) skolemTermsManager = new SkolemTermsManager(); return skolemTermsManager; @@ -47,21 +51,14 @@ public class SkolemTermsManager { * Get a fresh Individual, unique for the clause, the offset and the dependency. * */ public Individual getFreshIndividual(DLClause originalClause, int offset, Tuple dependency) { - if(!mapClauseToId.containsKey(originalClause)) { - mapClauseToId.put(originalClause, termsCounter); - termsCounter += noOfExistential(originalClause); - } - if (!mapDependencyToId.containsKey(dependency)) { - mapDependencyToId.put(dependency, dependenciesCounter++); - } - - String termId = mapClauseToId.get(originalClause) + offset + "_" + mapDependencyToId(dependency); + String termId = Integer.toString(mapClauseToId(originalClause) + offset) + + "_" + mapDependencyToId(dependency); Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId); int depth = 0; for (Individual individual : dependency) - depth = Integer.max(depth, mapIndividualToDepth(individual)); - mapTermToDepth.put(newIndividual, depth); + depth = Integer.max(depth, getDepthOf(individual)); + individualToDepth_map.put(newIndividual, depth); return newIndividual; } @@ -70,14 +67,9 @@ public class SkolemTermsManager { * Get a fresh Individual, unique for the clause and the offset. * */ public Individual getFreshIndividual(DLClause originalClause, int offset) { - if(!mapClauseToId.containsKey(originalClause)) { - mapClauseToId.put(originalClause, termsCounter); - termsCounter += noOfExistential(originalClause); - } - - String termId = "" + mapClauseToId.get(originalClause) + offset; + String termId = Integer.toString(mapClauseToId(originalClause) + offset); Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId); - mapTermToDepth.put(newIndividual, 0); +// individualToDepth_map.put(newIndividual, 0); // TODO REMOVE return newIndividual; } @@ -88,24 +80,29 @@ public class SkolemTermsManager { * The term must have been generated by this manager. * */ public int getDepthOf(Individual individual) { - return mapIndividualToDepth(individual); + if(individualToDepth_map.containsKey(individual)) return individualToDepth_map.get(individual); + else return 0; } /** * Get the number of individuals generated by this manager. * */ public int getNumberOfSkolemisedIndividual() { - return mapTermToDepth.keySet().size(); + return individualToDepth_map.keySet().size(); } - private int mapDependencyToId(Tuple dependency) { - if (mapDependencyToId.containsKey(dependency)) return mapDependencyToId.get(dependency); - else return mapDependencyToId.put(dependency, dependenciesCounter++); + private int mapClauseToId(DLClause clause) { + if(!clauseToId_map.containsKey(clause)) { + clauseToId_map.put(clause, termsCounter); + termsCounter += noOfExistential(clause); + } + return clauseToId_map.get(clause); } - private int mapIndividualToDepth(Individual dependency) { - if(mapTermToDepth.containsKey(dependency)) return mapTermToDepth.get(dependency); - else return 0; + private int mapDependencyToId(Tuple dependency) { + if(!dependencyToId_map.containsKey(dependency)) + dependencyToId_map.put(dependency, dependenciesCounter++); + return dependencyToId_map.get(dependency); } private int noOfExistential(DLClause originalClause) { -- cgit v1.2.3