From d0c209780ac209ba20de1ef2ba68551dd3321b3c Mon Sep 17 00:00:00 2001 From: RncLsn Date: Wed, 13 May 2015 16:04:41 +0100 Subject: Implemented SkolemTermsManager. --- .../cs/pagoda/rules/ExistConstantApproximator.java | 5 +- .../LimitedSkolemisationApproximator.java | 14 +-- .../rules/approximators/OverApproxExist.java | 51 +-------- .../rules/approximators/SkolemTermsDispenser.java | 74 ------------- .../rules/approximators/SkolemTermsManager.java | 116 +++++++++++++++++++++ .../approximators/TupleDependentApproximator.java | 9 +- 6 files changed, 138 insertions(+), 131 deletions(-) delete mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java (limited to 'src/uk/ac/ox/cs/pagoda/rules') diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java index 7c9562f..a7afa2e 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java @@ -1,9 +1,10 @@ package uk.ac.ox.cs.pagoda.rules; import org.semanticweb.HermiT.model.DLClause; -import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; +import org.semanticweb.HermiT.model.Individual; import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator; +import uk.ac.ox.cs.pagoda.util.tuples.Tuple; import java.util.Collection; @@ -19,7 +20,7 @@ public class ExistConstantApproximator implements TupleDependentApproximator { } @Override - public Collection convert(DLClause clause, DLClause originalClause, Collection violationTuples) { + public Collection convert(DLClause clause, DLClause originalClause, Collection> violationTuples) { return overApproxExist.convert(clause, originalClause); } } 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 8fc6b77..e53ae49 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java @@ -1,8 +1,10 @@ package uk.ac.ox.cs.pagoda.rules.approximators; import org.semanticweb.HermiT.model.DLClause; +import org.semanticweb.HermiT.model.Individual; import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; +import uk.ac.ox.cs.pagoda.util.tuples.Tuple; import java.util.*; @@ -33,7 +35,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima } @Override - public Collection convert(DLClause clause, DLClause originalClause, Collection violationTuples) { + public Collection convert(DLClause clause, DLClause originalClause, Collection> violationTuples) { switch (clause.getHeadLength()) { case 1: return overApprox(clause, originalClause, violationTuples); @@ -48,26 +50,26 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima } - private Collection overApprox(DLClause clause, DLClause originalClause, Collection violationTuples) { + private Collection overApprox(DLClause clause, DLClause originalClause, Collection> violationTuples) { ArrayList result = new ArrayList<>(); - for (AnswerTupleID violationTuple : violationTuples) + for (Tuple violationTuple : violationTuples) if (getDepth(violationTuple) > maxTermDepth) result.addAll(alternativeApproximator.convert(clause, originalClause, null)); else - result.add(getInstantiatedSkolemisation(clause, originalClause, violationTuple)); + result.add(getGroundSkolemisation(clause, originalClause, violationTuple)); return result; } - private DLClause getInstantiatedSkolemisation(DLClause clause, DLClause originalClause, AnswerTupleID violationTuple) { + private DLClause getGroundSkolemisation(DLClause clause, DLClause originalClause, Tuple violationTuple) { // TODO implement // filter the violation tuples appearing on both the sides of the rule return null; } - private int getDepth(AnswerTupleID violationTuple) { + private int getDepth(Tuple violationTuple) { if (!mapIndividualsToDepth.containsKey(violationTuple)) return 0; return mapIndividualsToDepth.get(violationTuple); } diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java index e0bafe0..d71c472 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java @@ -2,27 +2,15 @@ package uk.ac.ox.cs.pagoda.rules.approximators; import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; -import uk.ac.ox.cs.pagoda.util.Namespace; -import java.util.*; +import java.util.Collection; +import java.util.Iterator; +import java.util.LinkedList; public class OverApproxExist implements Approximator { public static final String negativeSuffix = "_neg"; - public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; private static final Variable X = Variable.create("X"); - //DEBUG - public static Collection createdIndividualIRIs = new HashSet<>(); - private static int individualCounter = 0; - private static Map individualNumber = new HashMap(); - - private static int noOfExistential(DLClause originalClause) { - int no = 0; - for (Atom atom: originalClause.getHeadAtoms()) - if (atom.getDLPredicate() instanceof AtLeast) - no += ((AtLeast) atom.getDLPredicate()).getNumber(); - return no; - } private static int indexOfExistential(Atom headAtom, DLClause originalClause) { if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1; @@ -65,36 +53,6 @@ public class OverApproxExist implements Approximator { return null; } - public static int getNumberOfSkolemisedIndividual() { - return individualCounter; - } - //DEBUG - - public static Individual getNewIndividual(DLClause originalClause, int offset) { - Individual ret; - int individualID; - if (individualNumber.containsKey(originalClause)) { - individualID = individualNumber.get(originalClause) + offset; - ret = Individual.create(skolemisedIndividualPrefix + individualID); - } - else { - individualNumber.put(originalClause, individualCounter); - individualID = individualCounter + offset; - ret = Individual.create(skolemisedIndividualPrefix + individualID); - individualCounter += noOfExistential(originalClause); - } - return ret; - } - - public static int indexOfSkolemisedIndividual(Atom atom) { - Term t; - for (int index = 0; index < atom.getArity(); ++index) { - t = atom.getArgument(index); - if (t instanceof Individual && ((Individual) t).getIRI().contains(skolemisedIndividualPrefix)) return index; - } - return -1; - } - @Override public Collection convert(DLClause clause, DLClause originalClause) { Collection ret; @@ -140,7 +98,8 @@ public class OverApproxExist implements Approximator { int card = atLeastConcept.getNumber(); Individual[] individuals = new Individual[card]; - for (int i = 0; i < card; ++i) individuals[i] = getNewIndividual(originalClause, offset + i); + SkolemTermsManager termsManager = SkolemTermsManager.getInstance(); + for (int i = 0; i < card; ++i) individuals[i] = termsManager.getFreshIndividual(originalClause, offset + i); for (int i = 0; i < card; ++i) { if (atomicConcept != null) diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java deleted file mode 100644 index a920ec5..0000000 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java +++ /dev/null @@ -1,74 +0,0 @@ -package uk.ac.ox.cs.pagoda.rules.approximators; - -import org.semanticweb.HermiT.model.AtLeast; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.Individual; -import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; -import uk.ac.ox.cs.pagoda.util.Namespace; - -import java.util.HashMap; -import java.util.Map; - -/** - * If you need a Skolem term (i.e. fresh individual), ask this class. - */ -public class SkolemTermsDispenser { - - public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; - private static SkolemTermsDispenser skolemTermsDispenser; - private int individualCounter = 0; - private Map termNumber = new HashMap<>(); - private Map mapTermToDepth = new HashMap<>(); - private int dependenciesCounter = 0; - private Map mapDependencyToId = new HashMap<>(); - - private SkolemTermsDispenser() { - } - - public static SkolemTermsDispenser getInstance() { - if (skolemTermsDispenser == null) skolemTermsDispenser = new SkolemTermsDispenser(); - return skolemTermsDispenser; - } - - private int getDependencyId(AnswerTupleID answerTupleID) { - if (mapDependencyToId.containsKey(answerTupleID)) return mapDependencyToId.get(answerTupleID); - else return mapDependencyToId.put(answerTupleID, dependenciesCounter++); - } - - public Individual getNewIndividual(DLClause originalClause, int offset, AnswerTupleID dependency) { - if (!termNumber.containsKey(originalClause)) { - termNumber.put(originalClause, individualCounter); - individualCounter += noOfExistential(originalClause); - } - if (!mapDependencyToId.containsKey(dependency)) { - mapDependencyToId.put(dependency, dependenciesCounter++); - } - - SkolemTermId termId = new SkolemTermId(termNumber.get(originalClause) + offset, getDependencyId(dependency)); - return Individual.create(skolemisedIndividualPrefix + termId); - } - - private int noOfExistential(DLClause originalClause) { - int no = 0; - for (Atom atom : originalClause.getHeadAtoms()) - if (atom.getDLPredicate() instanceof AtLeast) - no += ((AtLeast) atom.getDLPredicate()).getNumber(); - return no; - } - - private class SkolemTermId { - private final int idBase; - private final int idOffset; - - private SkolemTermId(int idBase, int idOffset) { - this.idBase = idBase; - this.idOffset = idOffset; - } - - @Override - public String toString() { - return idBase + "_" + idOffset; - } - } -} diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java new file mode 100644 index 0000000..0413e65 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java @@ -0,0 +1,116 @@ +package uk.ac.ox.cs.pagoda.rules.approximators; + +import org.semanticweb.HermiT.model.*; +import uk.ac.ox.cs.pagoda.util.Namespace; +import uk.ac.ox.cs.pagoda.util.tuples.Tuple; + +import java.util.HashMap; +import java.util.Map; + +/** + * If you need a Skolem term (i.e. fresh individual), ask this class. + */ +public class SkolemTermsManager { + + public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; + + private static SkolemTermsManager skolemTermsManager; + + private int individualCounter = 0; + private Map termNumber = new HashMap<>(); + private Map mapIndividualToDepth = new HashMap<>(); + private int dependenciesCounter = 0; + + // replace with hashcode. in case of collision you get only a different upper bound model. + private Map, Integer> mapDependencyToId = new HashMap<>(); + + /** + * Get a fresh Individual, unique for the clause, the offset and the dependency. + * */ + public Individual getFreshIndividual(DLClause originalClause, int offset, Tuple dependency) { + if (!termNumber.containsKey(originalClause)) { + termNumber.put(originalClause, individualCounter); + individualCounter += noOfExistential(originalClause); + } + if (!mapDependencyToId.containsKey(dependency)) { + mapDependencyToId.put(dependency, dependenciesCounter++); + } + + String termId = termNumber.get(originalClause) + offset + "_" + mapDependencyToId(dependency); + Individual newIndividual = Individual.create(skolemisedIndividualPrefix + termId); + + int depth = 0; + for (Individual individual : dependency) + depth = Integer.max(depth, mapIndividualToDepth(individual)); + mapIndividualToDepth.put(newIndividual, depth); + + return newIndividual; + } + + /** + * Get a fresh Individual, unique for the clause and the offset. + * */ + public Individual getFreshIndividual(DLClause originalClause, int offset) { + if (!termNumber.containsKey(originalClause)) { + termNumber.put(originalClause, individualCounter); + individualCounter += noOfExistential(originalClause); + } + + String termId = "" + termNumber.get(originalClause) + offset; + Individual newIndividual = Individual.create(skolemisedIndividualPrefix + termId); + mapIndividualToDepth.put(newIndividual, 0); + + return newIndividual; + } + + /** + * Get the depth of a term. + *

+ * The term must have been generated by this manager. + * */ + public int getDepth(Individual individual) { + return mapIndividualToDepth(individual); + } + + /** + * Get the number of individuals generated by this manager. + * */ + public int getNumberOfSkolemisedIndividual() { + return mapIndividualToDepth.keySet().size(); + } + + public static int indexOfSkolemisedIndividual(Atom atom) { + Term t; + for (int index = 0; index < atom.getArity(); ++index) { + t = atom.getArgument(index); + if (t instanceof Individual && ((Individual) t).getIRI().contains(skolemisedIndividualPrefix)) return index; + } + return -1; + } + + private SkolemTermsManager() { + } + + public static SkolemTermsManager getInstance() { + if (skolemTermsManager == null) skolemTermsManager = new SkolemTermsManager(); + return skolemTermsManager; + } + + private int mapDependencyToId(Tuple dependency) { + if (mapDependencyToId.containsKey(dependency)) return mapDependencyToId.get(dependency); + else return mapDependencyToId.put(dependency, dependenciesCounter++); + } + + private int mapIndividualToDepth(Individual dependency) { + if (mapIndividualToDepth.containsKey(dependency)) return mapIndividualToDepth.get(dependency); + else return 0; + } + + private int noOfExistential(DLClause originalClause) { + int no = 0; + for (Atom atom : originalClause.getHeadAtoms()) + if (atom.getDLPredicate() instanceof AtLeast) + no += ((AtLeast) atom.getDLPredicate()).getNumber(); + return no; + } +} diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java index 1a729e5..c99a1ad 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java @@ -1,16 +1,19 @@ package uk.ac.ox.cs.pagoda.rules.approximators; import org.semanticweb.HermiT.model.DLClause; -import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; +import org.semanticweb.HermiT.model.Individual; +import uk.ac.ox.cs.pagoda.util.tuples.Tuple; import java.util.Collection; /** - * It approximates rules according to a specific instantiation of the body. + * It can approximate clauses according to a collection of tuples of individuals. + *

+ * In particular it can be used to approximate rules given some body instantiations. */ public interface TupleDependentApproximator { Collection convert(DLClause clause, DLClause originalClause, - Collection violationTuples); + Collection> individualsTuples); } -- cgit v1.2.3