From 0c39145b3b76b3db73db0a38d5324caa7ff3c434 Mon Sep 17 00:00:00 2001 From: RncLsn Date: Mon, 3 Aug 2015 17:07:39 +0100 Subject: The LimitedSkolemisation now employs a fixed-depth term instead of a constant. Performed some testing before merging with master. --- .../ac/ox/cs/pagoda/endomorph/DependencyGraph.java | 1 - .../LimitedSkolemisationApproximator.java | 28 ++++++++++------------ .../rules/approximators/SkolemTermsManager.java | 28 ++++++++++++++++++---- 3 files changed, 36 insertions(+), 21 deletions(-) (limited to 'src/uk') diff --git a/src/uk/ac/ox/cs/pagoda/endomorph/DependencyGraph.java b/src/uk/ac/ox/cs/pagoda/endomorph/DependencyGraph.java index 320af09..0f215ad 100644 --- a/src/uk/ac/ox/cs/pagoda/endomorph/DependencyGraph.java +++ b/src/uk/ac/ox/cs/pagoda/endomorph/DependencyGraph.java @@ -241,7 +241,6 @@ public class DependencyGraph { ++homomorphismCheckCounter; homomorphismChecker.setMapping(u, v); - // TODO recently added, test it if(!homomorphismChecker.isMappingTo(u, v)) return false; 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 2c8e23d..7d29c74 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java @@ -2,7 +2,6 @@ package uk.ac.ox.cs.pagoda.rules.approximators; import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.multistage.MultiStageUpperProgram; -import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; import uk.ac.ox.cs.pagoda.util.tuples.Tuple; import uk.ac.ox.cs.pagoda.util.tuples.TupleBuilder; @@ -23,16 +22,10 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima private static final Atom[] EMPTY_BODY = new Atom[0]; private static final Variable X = Variable.create("X"); private final int maxTermDepth; - private final TupleDependentApproximator alternativeApproximator; private final SkolemTermsManager skolemTermsManager; public LimitedSkolemisationApproximator(int maxTermDepth) { - this(maxTermDepth, new ExistConstantApproximator()); - } - - public LimitedSkolemisationApproximator(int maxTermDepth, TupleDependentApproximator alternativeApproximator) { this.maxTermDepth = maxTermDepth; - this.alternativeApproximator = alternativeApproximator; this.skolemTermsManager = SkolemTermsManager.getInstance(); } @@ -64,10 +57,8 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima private Collection overApprox(DLClause clause, DLClause originalClause, Collection> violationTuples) { ArrayList result = new ArrayList<>(); for(Tuple violationTuple : violationTuples) { - if(getMaxDepth(violationTuple) < maxTermDepth) - result.addAll(getGroundSkolemisation(clause, originalClause, violationTuple)); - else - result.addAll(alternativeApproximator.convert(clause, originalClause, null)); + result.addAll(getGroundSkolemisation(clause, + originalClause, violationTuple, getMaxDepth(violationTuple) >= maxTermDepth)); } return result; @@ -75,7 +66,8 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima private Collection getGroundSkolemisation(DLClause clause, DLClause originalClause, - Tuple violationTuple) { + Tuple violationTuple, + boolean useClauseUniqueIndividual) { String[] commonVars = MultiStageUpperProgram.getCommonVars(clause); @@ -100,7 +92,6 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima AtomicConcept atomicConcept; if(concept instanceof AtomicNegationConcept) { - // TODO CHECK: is this already in MultiStageUpperProgram? Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X); Atom atom2 = Atom.create(atomicConcept = OverApproxExist.getNegationConcept(atomicConcept), X); @@ -116,9 +107,14 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima Individual[] individuals = new Individual[card]; SkolemTermsManager termsManager = SkolemTermsManager.getInstance(); for(int i = 0; i < card; ++i) - individuals[i] = termsManager.getFreshIndividual(originalClause, - offset + i, - commonIndividuals); + if(useClauseUniqueIndividual) + individuals[i] = termsManager.getFreshIndividual(originalClause, + offset + i, + maxTermDepth + 1); + else + individuals[i] = termsManager.getFreshIndividual(originalClause, + offset + i, + commonIndividuals); for(int i = 0; i < card; ++i) { if(atomicConcept != null) 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 a78aabe..ed93d0e 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java @@ -13,6 +13,7 @@ import java.util.Map; public class SkolemTermsManager { public static final String SKOLEMISED_INDIVIDUAL_PREFIX = Namespace.PAGODA_ANONY + "individual"; + public static final String RULE_UNIQUE_SKOLEMISED_INDIVIDUAL_PREFIX = SKOLEMISED_INDIVIDUAL_PREFIX + "_unique"; private static SkolemTermsManager skolemTermsManager; @@ -54,10 +55,29 @@ public class SkolemTermsManager { + "_" + mapDependencyToId(dependency); Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId); - int depth = 0; - for(Individual individual : dependency) - depth = Integer.max(depth, getDepthOf(individual)); - individualToDepth_map.put(newIndividual, depth + 1); + if(!individualToDepth_map.containsKey(newIndividual)) { + int depth = 0; + for (Individual individual : dependency) + depth = Integer.max(depth, getDepthOf(individual)); + individualToDepth_map.put(newIndividual, depth + 1); + } + + return newIndividual; + } + + /*** + * Create a term of a given depth, unique for the clause and the depth. + * + * @param originalClause + * @param offset + * @param depth + * @return + */ + public Individual getFreshIndividual(DLClause originalClause, int offset, int depth) { + String termId = Integer.toString(mapClauseToId(originalClause) + offset) + "_depth_" + depth; + Individual newIndividual = Individual.create(RULE_UNIQUE_SKOLEMISED_INDIVIDUAL_PREFIX + termId); + + individualToDepth_map.putIfAbsent(newIndividual, depth); return newIndividual; } -- cgit v1.2.3