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/multistage/IndividualCollector.java | 6 +- .../pagoda/multistage/MultiStageUpperProgram.java | 3 +- .../ac/ox/cs/pagoda/multistage/Normalisation.java | 8 +- .../ac/ox/cs/pagoda/multistage/ViolationTuple.java | 19 ++++ .../treatement/Pick4NegativeConcept.java | 17 ++- .../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 +- .../pagoda/tracking/TrackingRuleEncoderDisj.java | 11 +- src/uk/ac/ox/cs/pagoda/util/tuples/Tuple.java | 44 ++++++++ .../ac/ox/cs/pagoda/util/tuples/TupleBuilder.java | 25 +++++ 14 files changed, 259 insertions(+), 143 deletions(-) create mode 100644 src/uk/ac/ox/cs/pagoda/multistage/ViolationTuple.java 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 create mode 100644 src/uk/ac/ox/cs/pagoda/util/tuples/Tuple.java create mode 100644 src/uk/ac/ox/cs/pagoda/util/tuples/TupleBuilder.java diff --git a/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java b/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java index 22d90c4..a9c127b 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java @@ -7,7 +7,7 @@ import org.openrdf.model.impl.URIImpl; import org.openrdf.rio.RDFHandler; import org.openrdf.rio.RDFHandlerException; import uk.ac.ox.cs.JRDFox.model.Individual; -import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.SkolemTermsManager; import uk.ac.ox.cs.pagoda.util.Namespace; import java.util.Collection; @@ -58,9 +58,9 @@ public class IndividualCollector implements RDFHandler { public Collection getAllIndividuals() { if (!addedSkolemised) { - int number = OverApproxExist.getNumberOfSkolemisedIndividual(); + int number = SkolemTermsManager.getInstance().getNumberOfSkolemisedIndividual(); for (int i = 0; i < number; ++i) - individuals.add(Individual.create(OverApproxExist.skolemisedIndividualPrefix + i)); + individuals.add(Individual.create(SkolemTermsManager.skolemisedIndividualPrefix + i)); addedSkolemised = true; } return individuals; diff --git a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java index 33ba345..1664c99 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java @@ -15,6 +15,7 @@ import uk.ac.ox.cs.pagoda.util.Namespace; import uk.ac.ox.cs.pagoda.util.SparqlHelper; import uk.ac.ox.cs.pagoda.util.Timer; import uk.ac.ox.cs.pagoda.util.Utility; +import uk.ac.ox.cs.pagoda.util.tuples.Tuple; import java.io.*; import java.util.*; @@ -376,7 +377,7 @@ public abstract class MultiStageUpperProgram { return m_bottom.process(m_approxExist.convert(clause, originalDLClause, null)); } - public Collection convertExist(DLClause clause, DLClause originalDLClause, List violationTuples) { + public Collection convertExist(DLClause clause, DLClause originalDLClause, Collection> violationTuples) { return m_bottom.process(m_approxExist.convert(clause, originalDLClause, violationTuples)); } diff --git a/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java b/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java index b31d138..c5482e7 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java @@ -7,6 +7,7 @@ import uk.ac.ox.cs.pagoda.approx.Clause; import uk.ac.ox.cs.pagoda.approx.Clausifier; import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.SkolemTermsManager; import uk.ac.ox.cs.pagoda.util.Namespace; import uk.ac.ox.cs.pagoda.util.Utility; @@ -102,7 +103,9 @@ public class Normalisation { return ; } AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate(); - AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); + // TODO test +// AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); + AtomicConcept ac = getRightAuxiliaryConcept(alc, SkolemTermsManager.getInstance().getFreshIndividual(clause, 0)); DLClause newClause; m_normClauses.add(DLClause.create(new Atom[] {Atom.create(ac, headAtom.getArgument(0)) }, clause.getBodyAtoms())); m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, X)}, new Atom[] {Atom.create(ac, X)})); @@ -140,7 +143,8 @@ public class Normalisation { } } else { AtLeastConcept alc = toAtLeastConcept((AtLeast) headAtom.getDLPredicate()); - AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); +// AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); + AtomicConcept ac = getRightAuxiliaryConcept(alc, SkolemTermsManager.getInstance().getFreshIndividual(clause, 0)); newHeadAtoms[index] = Atom.create(ac, headAtom.getArgument(0)); m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, headAtom.getArgument(0))}, new Atom[] {newHeadAtoms[index]})); exist2original.put(newClause, clause); diff --git a/src/uk/ac/ox/cs/pagoda/multistage/ViolationTuple.java b/src/uk/ac/ox/cs/pagoda/multistage/ViolationTuple.java new file mode 100644 index 0000000..129f5dd --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/multistage/ViolationTuple.java @@ -0,0 +1,19 @@ +package uk.ac.ox.cs.pagoda.multistage; + +import org.semanticweb.HermiT.model.Individual; + +import java.util.ArrayList; + +/** + * Just a list of Individuals. + * */ +public class ViolationTuple extends ArrayList { + + public ViolationTuple() { + super(); + } + + public ViolationTuple(int size) { + super(size); + } +} diff --git a/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConcept.java b/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConcept.java index 244eb7a..fefb8b2 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConcept.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConcept.java @@ -14,6 +14,8 @@ import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager; import uk.ac.ox.cs.pagoda.util.Namespace; import uk.ac.ox.cs.pagoda.util.SparqlHelper; import uk.ac.ox.cs.pagoda.util.Utility; +import uk.ac.ox.cs.pagoda.util.tuples.Tuple; +import uk.ac.ox.cs.pagoda.util.tuples.TupleBuilder; import java.util.*; @@ -99,7 +101,20 @@ public abstract class Pick4NegativeConcept implements Treatment { } else { Set headAtoms = new HashSet(); - for (DLClause clause : program.convertExist(constraint, violation.getClause(), violation.getTuples())) { + + ArrayList> violationTuples = new ArrayList<>(violation.getTuples().size()); + for (int i = 0; i < violation.getTuples().size(); i++) { + AnswerTupleID answerTupleID = violation.getTuples().get(i); + TupleBuilder tupleBuilder = new TupleBuilder<>(); + for (int j = 0; j < answerTupleID.getArity(); j++) { + String rawTerm = tripleManager.getRawTerm(answerTupleID.getTerm(j)); + Individual individual = Individual.create(rawTerm.substring(1, rawTerm.length()-1)); + tupleBuilder.add(individual); + } + violationTuples.add(tupleBuilder.create()); + } + + for (DLClause clause : program.convertExist(constraint, violation.getClause(), violationTuples)) { if (!DLClauseHelper.hasSubsetBodyAtoms(clause, constraint)) { Utility.logError("There might be an error here... Cannot happen!!!"); 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); } diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java index 331ad12..b169053 100644 --- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java +++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java @@ -4,7 +4,7 @@ import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; -import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.SkolemTermsManager; import uk.ac.ox.cs.pagoda.util.Namespace; import java.util.*; @@ -22,8 +22,9 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap */ protected void processDisjunctiveRules() { Map> auxiliaryAtoms = new HashMap>(); - Map> skolemisedAtoms = new HashMap>(); - + Map> skolemisedAtoms = new HashMap>(); + SkolemTermsManager termsManager = SkolemTermsManager.getInstance(); + for (Map.Entry> entry: disjunctiveRules.entrySet()) { DLClause original = entry.getKey(); Collection overClauses = entry.getValue(); @@ -33,7 +34,7 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap DLClause subClause = iter.next(); if (DLClauseHelper.hasSubsetBodyAtoms(subClause, original)) { Atom headAtom = subClause.getHeadAtom(0); - if ((index = OverApproxExist.indexOfSkolemisedIndividual(headAtom)) != -1) { + if ((index = SkolemTermsManager.indexOfSkolemisedIndividual(headAtom)) != -1) { Individual i = (Individual) headAtom.getArgument(index); Collection clauses = skolemisedAtoms.get(i); if (clauses == null) { @@ -55,7 +56,7 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap Collection clauses = new HashSet(); Individual[] individuals = new Individual[alc.getNumber()]; for (int i = 0; i < alc.getNumber(); ++i) { - individuals[i] = OverApproxExist.getNewIndividual(original, i); + individuals[i] = termsManager.getFreshIndividual(original, i); clauses.addAll(skolemisedAtoms.get(individuals[i])); } auxiliaryAtoms.put(getAuxiliaryAtom(original, headAtom, individuals), clauses); diff --git a/src/uk/ac/ox/cs/pagoda/util/tuples/Tuple.java b/src/uk/ac/ox/cs/pagoda/util/tuples/Tuple.java new file mode 100644 index 0000000..3e72748 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/util/tuples/Tuple.java @@ -0,0 +1,44 @@ +package uk.ac.ox.cs.pagoda.util.tuples; + +import java.util.ArrayList; +import java.util.Iterator; +import java.util.Spliterator; +import java.util.function.Consumer; + +public class Tuple implements Iterable { + + final ArrayList elements = new ArrayList<>(); + + Tuple() { } + + public Tuple(T... elements) { + for(T t: elements) { + this.elements.add(t); + } + } + + public Tuple(Iterable iterable) { + for (T t : iterable) { + this.elements.add(t); + } + } + + public T get(int i) { + return elements.get(i); + } + + @Override + public Iterator iterator() { + return elements.iterator(); + } + + @Override + public void forEach(Consumer action) { + elements.forEach(action); + } + + @Override + public Spliterator spliterator() { + return elements.spliterator(); + } +} diff --git a/src/uk/ac/ox/cs/pagoda/util/tuples/TupleBuilder.java b/src/uk/ac/ox/cs/pagoda/util/tuples/TupleBuilder.java new file mode 100644 index 0000000..aacd15e --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/util/tuples/TupleBuilder.java @@ -0,0 +1,25 @@ +package uk.ac.ox.cs.pagoda.util.tuples; + +/** + * Allows to create an immutable Tuple in a non-atomic way. + * It can create only one Tuple. + * */ +public class TupleBuilder { + + private Tuple tuple = new Tuple(); + + private boolean building = true; + + public boolean add(T t) { + if(building) tuple.elements.add(t); + return building; + } + + public Tuple create() { + if(building) { + building = false; + return tuple; + } + return null; + } +} -- cgit v1.2.3