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. --- src/resources/pagoda.properties | 2 +- .../ac/ox/cs/pagoda/endomorph/DependencyGraph.java | 1 - .../LimitedSkolemisationApproximator.java | 28 ++++++++++------------ .../rules/approximators/SkolemTermsManager.java | 28 ++++++++++++++++++---- test/resources/BugTests.xml | 2 +- test/resources/MainTests.xml | 4 ++-- .../cs/pagoda/endomorph/DependencyGraphTest.java | 3 ++- .../ox/cs/pagoda/global_tests/TestPagodaFLY.java | 2 +- 8 files changed, 43 insertions(+), 27 deletions(-) diff --git a/src/resources/pagoda.properties b/src/resources/pagoda.properties index 07a0eac..e6aa503 100644 --- a/src/resources/pagoda.properties +++ b/src/resources/pagoda.properties @@ -1,9 +1,9 @@ debug=true useAlwaysSimpleUpperBound=false skolemUpperBound=DISABLED -skolemDepth=1 #skolemUpperBound=BEFORE_SUMMARISATION #skolemUpperBound=AFTER_SUMMARISATION +skolemDepth=1 toCallHermit=true statisticsDir=/home/alessandro/Dropbox/Oxford/PAGOdA/statistics \ No newline at end of file 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; } diff --git a/test/resources/BugTests.xml b/test/resources/BugTests.xml index 1413b5b..4844fbe 100644 --- a/test/resources/BugTests.xml +++ b/test/resources/BugTests.xml @@ -6,7 +6,7 @@ - + diff --git a/test/resources/MainTests.xml b/test/resources/MainTests.xml index 255b68e..43300a1 100644 --- a/test/resources/MainTests.xml +++ b/test/resources/MainTests.xml @@ -7,9 +7,9 @@ - + - + diff --git a/test/uk/ac/ox/cs/pagoda/endomorph/DependencyGraphTest.java b/test/uk/ac/ox/cs/pagoda/endomorph/DependencyGraphTest.java index eec1e8f..a4579a3 100644 --- a/test/uk/ac/ox/cs/pagoda/endomorph/DependencyGraphTest.java +++ b/test/uk/ac/ox/cs/pagoda/endomorph/DependencyGraphTest.java @@ -2,6 +2,7 @@ package uk.ac.ox.cs.pagoda.endomorph; import org.semanticweb.owlapi.apibinding.OWLManager; import org.semanticweb.owlapi.model.*; +import org.testng.Assert; import org.testng.annotations.Test; import uk.ac.ox.cs.JRDFox.model.GroundTerm; import uk.ac.ox.cs.JRDFox.model.Individual; @@ -54,6 +55,6 @@ public class DependencyGraphTest { dependencyGraph.build(tuples); - System.out.println(dependencyGraph.getTopologicalOrder()); + Assert.assertTrue(dependencyGraph.getTopologicalOrder().size() >= 2); } } diff --git a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java index a7a562d..42f0ac1 100644 --- a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java +++ b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java @@ -62,7 +62,7 @@ public class TestPagodaFLY { // .answer(Paths.get("/home/alessandro/Desktop/answers.json")) .classify(false) .hermit(true) - .skolem(PagodaProperties.SkolemUpperBoundOptions.AFTER_SUMMARISATION) + .skolem(PagodaProperties.SkolemUpperBoundOptions.BEFORE_SUMMARISATION) .build() .run(); } -- cgit v1.2.3