From 6fd8b21066852cbc21e247e7cf0a2f423ebc1658 Mon Sep 17 00:00:00 2001 From: RncLsn Date: Wed, 13 May 2015 19:22:07 +0100 Subject: Fast implementation of all the other things to get something working, but it doesn't. --- .../LimitedSkolemisationApplication.java | 3 +- .../pagoda/multistage/MultiStageQueryEngine.java | 12 +++ .../ox/cs/pagoda/multistage/StageQueryEngine.java | 6 +- .../cs/pagoda/multistage/TwoStageQueryEngine.java | 16 +-- .../ox/cs/pagoda/reasoner/ConsistencyManager.java | 31 ++++-- .../ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java | 26 ++++- .../cs/pagoda/reasoner/light/BasicQueryEngine.java | 33 +++--- .../LimitedSkolemisationApproximator.java | 116 +++++++++++++++++---- .../rules/approximators/OverApproxExist.java | 2 +- 9 files changed, 184 insertions(+), 61 deletions(-) (limited to 'src/uk/ac/ox/cs') diff --git a/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java b/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java index f729158..b548d39 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java @@ -2,7 +2,6 @@ package uk.ac.ox.cs.pagoda.multistage; import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; -import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; import uk.ac.ox.cs.pagoda.rules.Program; import uk.ac.ox.cs.pagoda.rules.approximators.LimitedSkolemisationApproximator; @@ -12,6 +11,6 @@ public class LimitedSkolemisationApplication extends RestrictedApplication { public LimitedSkolemisationApplication(Program program, BottomStrategy upperBottom) { super(program, upperBottom); - m_approxExist = new LimitedSkolemisationApproximator(MAX_DEPTH, new ExistConstantApproximator()); + m_approxExist = new LimitedSkolemisationApproximator(MAX_DEPTH); } } diff --git a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java index f0f631a..f80da5f 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java @@ -55,6 +55,18 @@ public class MultiStageQueryEngine extends StageQueryEngine { treatment.dispose(); return ret; } + + /** + * delta-chase + */ + @Override + public int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap) { + materialise("lower program", dProgram.getLower().toString()); + Program generalProgram = dProgram.getGeneral(); + LimitedSkolemisationApplication program = new LimitedSkolemisationApplication(generalProgram, dProgram.getUpperBottomStrategy()); + Treatment treatment = new Pick4NegativeConceptNaive(this, program); + return materialise(program, treatment, gap); + } private int materialise(MultiStageUpperProgram program, Treatment treatment, GapByStore4ID gap) { if (gap != null) diff --git a/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java index 5d2e0d1..84798ce 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java @@ -18,8 +18,10 @@ public abstract class StageQueryEngine extends BasicQueryEngine { public abstract void materialiseFoldedly(DatalogProgram dProgram, GapByStore4ID gap); - public abstract int materialiseRestrictedly(DatalogProgram dProgram, GapByStore4ID gap); - + public abstract int materialiseRestrictedly(DatalogProgram dProgram, GapByStore4ID gap); + + public abstract int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap); + public void dispose() { super.dispose(); } diff --git a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java index b7f989f..29cf23a 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/TwoStageQueryEngine.java @@ -1,14 +1,8 @@ package uk.ac.ox.cs.pagoda.multistage; -import java.io.FileInputStream; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.util.Collection; - import org.openrdf.rio.RDFHandlerException; import org.openrdf.rio.RDFParseException; import org.openrdf.rio.turtle.TurtleParser; - import uk.ac.ox.cs.JRDFox.JRDFStoreException; import uk.ac.ox.cs.JRDFox.model.Individual; import uk.ac.ox.cs.pagoda.query.GapByStore4ID; @@ -17,6 +11,11 @@ import uk.ac.ox.cs.pagoda.rules.DatalogProgram; import uk.ac.ox.cs.pagoda.util.Timer; import uk.ac.ox.cs.pagoda.util.Utility; +import java.io.FileInputStream; +import java.io.FileNotFoundException; +import java.io.IOException; +import java.util.Collection; + public class TwoStageQueryEngine extends StageQueryEngine { IndividualCollector m_collector = new IndividualCollector(); @@ -64,6 +63,11 @@ public class TwoStageQueryEngine extends StageQueryEngine { return program.materialise(); } + @Override + public int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap) { + throw new UnsupportedOperationException("This method is not available in " + getClass()); + } + public void materialise(String programText, GapByStore4ID gap, boolean incrementally) { try { if (gap != null) { diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java index 9b862ce..d179d14 100644 --- a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java +++ b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java @@ -1,7 +1,5 @@ package uk.ac.ox.cs.pagoda.reasoner; -import java.util.LinkedList; - import org.semanticweb.HermiT.model.Atom; import org.semanticweb.HermiT.model.AtomicConcept; import org.semanticweb.HermiT.model.DLClause; @@ -9,7 +7,9 @@ import org.semanticweb.HermiT.model.Variable; import org.semanticweb.owlapi.model.OWLOntology; import org.semanticweb.owlapi.model.OWLOntologyCreationException; import org.semanticweb.owlapi.model.OWLOntologyManager; - +import uk.ac.ox.cs.JRDFox.JRDFStoreException; +import uk.ac.ox.cs.JRDFox.store.DataStore; +import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; import uk.ac.ox.cs.pagoda.query.AnswerTuples; import uk.ac.ox.cs.pagoda.query.QueryManager; @@ -21,9 +21,8 @@ import uk.ac.ox.cs.pagoda.tracking.QueryTracker; import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoder; import uk.ac.ox.cs.pagoda.util.Timer; import uk.ac.ox.cs.pagoda.util.Utility; -import uk.ac.ox.cs.JRDFox.JRDFStoreException; -import uk.ac.ox.cs.JRDFox.store.DataStore; -import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType; + +import java.util.LinkedList; public class ConsistencyManager { @@ -85,6 +84,23 @@ public class ConsistencyManager { } return false; } + + boolean checkSkolemUpper() { + if (m_reasoner.limitedSkolemUpperStore != null) { + AnswerTuples tuples = null; + try { + tuples = m_reasoner.limitedSkolemUpperStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables()); + if (!tuples.isValid()) { + Utility.logInfo("There are no contradictions derived in the limited-skolem upper bound materialisation."); + return satisfiability(t.duration()); + } + } + finally { + if (tuples != null) tuples.dispose(); + } + } + return false; + } boolean check() { // if (!checkRLLowerBound()) return false; @@ -288,5 +304,6 @@ public class ConsistencyManager { public QueryRecord[] getQueryRecords() { return botQueryRecords; } - + + } diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java index 3c0a001..233963e 100644 --- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java +++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java @@ -49,7 +49,8 @@ public class MyQueryReasoner extends QueryReasoner { private Collection predicatesWithGap = null; private Boolean satisfiable; private ConsistencyManager consistency = new ConsistencyManager(this); - + BasicQueryEngine limitedSkolemUpperStore; + public MyQueryReasoner() { setup(true, true); } @@ -102,10 +103,10 @@ public class MyQueryReasoner extends QueryReasoner { if (multiStageTag && !program.getGeneral().isHorn()) { lazyUpperStore = getUpperStore("lazy-upper-bound", true); // new MultiStageQueryEngine("lazy-upper-bound", true); // + // TODO CHECK + limitedSkolemUpperStore = getUpperStore("limited-skolem-upper-bound", true); } - // TODO add new upper store creation - importData(program.getAdditionalDataFile()); elho_ontology = new ELHOProfile().getFragment(ontology); @@ -151,7 +152,21 @@ public class MyQueryReasoner extends QueryReasoner { Utility.logInfo("time for satisfiability checking: " + t.duration()); } - // TODO add new upper store preprocessing + // TODO check + if (limitedSkolemUpperStore != null) { + limitedSkolemUpperStore.importRDFData(name, datafile); + limitedSkolemUpperStore.materialise("saturate named individuals", originalMarkProgram); + int tag = limitedSkolemUpperStore.materialiseSkolemly(program, null); + if (tag != 1) { + limitedSkolemUpperStore.dispose(); + limitedSkolemUpperStore = null; + } + if (tag == -1) return false; + } + if (consistency.checkSkolemUpper()) { + satisfiable = true; + Utility.logInfo("time for satisfiability checking: " + t.duration()); + } trackingStore.importRDFData(name, datafile); trackingStore.materialise("saturate named individuals", originalMarkProgram); @@ -223,6 +238,9 @@ public class MyQueryReasoner extends QueryReasoner { if (!queryRecord.isBottom() && lazyUpperStore != null) { queryUpperBound(trackingStore, queryRecord, queryRecord.getQueryText(), queryRecord.getAnswerVariables()); } + if (!queryRecord.isBottom() && limitedSkolemUpperStore != null) { + queryUpperBound(limitedSkolemUpperStore, queryRecord, queryRecord.getQueryText(), queryRecord.getAnswerVariables()); + } // END: trying to intersect queryRecord.addProcessingTime(Step.UpperBound, t.duration()); diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java b/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java index 11588ce..5d2e411 100644 --- a/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java +++ b/src/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java @@ -1,29 +1,21 @@ package uk.ac.ox.cs.pagoda.reasoner.light; -import java.util.Arrays; -import java.util.Collection; -import java.util.HashSet; -import java.util.Iterator; -import java.util.Set; - import org.semanticweb.HermiT.model.DLClause; - +import uk.ac.ox.cs.JRDFox.JRDFStoreException; +import uk.ac.ox.cs.JRDFox.store.DataStore; +import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType; +import uk.ac.ox.cs.JRDFox.store.Parameters; +import uk.ac.ox.cs.JRDFox.store.TripleStatus; +import uk.ac.ox.cs.JRDFox.store.TupleIterator; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; import uk.ac.ox.cs.pagoda.query.AnswerTuples; import uk.ac.ox.cs.pagoda.query.GapByStore4ID; import uk.ac.ox.cs.pagoda.rules.DatalogProgram; import uk.ac.ox.cs.pagoda.rules.Program; -import uk.ac.ox.cs.pagoda.util.ConjunctiveQueryHelper; -import uk.ac.ox.cs.pagoda.util.Namespace; +import uk.ac.ox.cs.pagoda.util.*; import uk.ac.ox.cs.pagoda.util.Timer; -import uk.ac.ox.cs.pagoda.util.UFS; -import uk.ac.ox.cs.pagoda.util.Utility; -import uk.ac.ox.cs.JRDFox.JRDFStoreException; -import uk.ac.ox.cs.JRDFox.store.DataStore; -import uk.ac.ox.cs.JRDFox.store.Parameters; -import uk.ac.ox.cs.JRDFox.store.TripleStatus; -import uk.ac.ox.cs.JRDFox.store.TupleIterator; -import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType; + +import java.util.*; public class BasicQueryEngine extends RDFoxQueryEngine { @@ -74,6 +66,10 @@ public class BasicQueryEngine extends RDFoxQueryEngine { return 1; } + + public int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap) { + throw new UnsupportedOperationException(); + } @Override public AnswerTuples evaluate(String queryText) { @@ -163,8 +159,7 @@ public class BasicQueryEngine extends RDFoxQueryEngine { instanceTuples = null; try { instanceTuples = getDataStore().compileQuery("SELECT ?X ?Z WHERE { ?X " + predicate + " ?Z }", prefixes, parameters); - ; - long totalCount = 0; + long totalCount = 0; for (long multi1 = instanceTuples.open(); multi1 != 0; multi1 = instanceTuples.getNext()) totalCount += instanceTuples.getMultiplicity(); number.add(predicate + " * " + totalCount); 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 e53ae49..4444c00 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java @@ -1,26 +1,29 @@ package uk.ac.ox.cs.pagoda.rules.approximators; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.Individual; +import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; +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; import java.util.*; /** - * Approximates existential rules by a limited form of Skolemisation. + * Approximates existential rules through a limited form of Skolemisation. *

- * Given a rule and a grounding substitution, - * it Skolemises the rule if - * all the terms in the substitution have depth less than a given depth, + * Given a rule and a ground substitution, + * 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]; + private final int maxTermDepth; private final TupleDependentApproximator alternativeApproximator; + private final SkolemTermsManager skolemTermsManager; private Map mapIndividualsToDepth; @@ -32,19 +35,21 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima this.maxTermDepth = maxTermDepth; this.alternativeApproximator = alternativeApproximator; this.mapIndividualsToDepth = new HashMap<>(); + this.skolemTermsManager = SkolemTermsManager.getInstance(); } @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); case 0: return Arrays.asList(clause); default: - ArrayList result = new ArrayList<>(); - // TODO implement - return result; + throw new IllegalArgumentException( + "Expected clause with head length < 1, but it is " + clause.getHeadLength()); } @@ -54,23 +59,94 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima ArrayList result = new ArrayList<>(); for (Tuple violationTuple : violationTuples) - if (getDepth(violationTuple) > maxTermDepth) + if (getMaxDepth(violationTuple) > maxTermDepth) result.addAll(alternativeApproximator.convert(clause, originalClause, null)); else - result.add(getGroundSkolemisation(clause, originalClause, violationTuple)); + result.addAll(getGroundSkolemisation(clause, originalClause, violationTuple)); return result; } + private static final Variable X = Variable.create("X"); + + private Collection getGroundSkolemisation(DLClause clause, + DLClause originalClause, + Tuple violationTuple) { + + String[] commonVars = MultiStageUpperProgram.getCommonVars(clause); + + // TODO check: strong assumption, the first tuples are the common ones + TupleBuilder commonIndividualsBuilder = new TupleBuilder<>(); + for (int i = 0; i < commonVars.length; i++) + commonIndividualsBuilder.add(violationTuple.get(i)); + + Atom headAtom = clause.getHeadAtom(0); + Atom[] bodyAtoms = clause.getBodyAtoms(); + int offset = OverApproxExist.indexOfExistential(headAtom, originalClause); + + // BEGIN: copy and paste + ArrayList ret = new ArrayList<>(); + DLPredicate predicate = headAtom.getDLPredicate(); + if (predicate instanceof AtLeastConcept) { + AtLeastConcept atLeastConcept = (AtLeastConcept) predicate; + LiteralConcept concept = atLeastConcept.getToConcept(); + Role role = atLeastConcept.getOnRole(); + 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); + ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2})); + } + else { + atomicConcept = (AtomicConcept) concept; + 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) + individuals[i] = termsManager.getFreshIndividual(originalClause, + offset + i, + commonIndividualsBuilder.create()); + + 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, X, individuals[i]) : + Atom.create(((InverseRole) role).getInverseOf(), individuals[i], X); + + ret.add(DLClause.create(new Atom[] {atom}, EMPTY_BODY)); + } + + 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)); + + } + else if (predicate instanceof AtLeastDataRange) { + // TODO to be implemented ... + } + else + ret.add(DLClause.create(new Atom[] {headAtom}, EMPTY_BODY)); - 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; + return ret; + + // END: copy and paste } - private int getDepth(Tuple violationTuple) { - if (!mapIndividualsToDepth.containsKey(violationTuple)) return 0; - return mapIndividualsToDepth.get(violationTuple); + + public int getMaxDepth(Tuple violationTuple) { + int maxDepth = 0; + for (Individual individual : violationTuple) + maxDepth = Integer.max(maxDepth, skolemTermsManager.getDepth(individual)); + + return maxDepth; } } 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 d71c472..028568c 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java @@ -12,7 +12,7 @@ public class OverApproxExist implements Approximator { public static final String negativeSuffix = "_neg"; private static final Variable X = Variable.create("X"); - private static int indexOfExistential(Atom headAtom, DLClause originalClause) { + static int indexOfExistential(Atom headAtom, DLClause originalClause) { if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1; AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate(); if (alc.getToConcept() instanceof AtomicConcept) { -- cgit v1.2.3