From 7e0ecc07285209e65f9d4d022065d06a4997fc86 Mon Sep 17 00:00:00 2001 From: RncLsn Date: Wed, 13 May 2015 11:57:06 +0100 Subject: Implementing Limited Skolemisation, in particular SkolemTermsDispenser. --- src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java | 259 ---------------------- 1 file changed, 259 deletions(-) delete mode 100644 src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java (limited to 'src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java') diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java deleted file mode 100644 index 1099acf..0000000 --- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java +++ /dev/null @@ -1,259 +0,0 @@ -package uk.ac.ox.cs.pagoda.rules; - -import org.semanticweb.HermiT.model.*; -import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; -import uk.ac.ox.cs.pagoda.util.Namespace; - -import java.util.*; - -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"); - 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; - AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate(); - if (alc.getToConcept() instanceof AtomicConcept) { - AtomicConcept ac = (AtomicConcept) alc.getToConcept(); - if (ac.getIRI().endsWith(negativeSuffix)) { - alc = AtLeastConcept.create(alc.getNumber(), alc.getOnRole(), AtomicNegationConcept.create(getNegationConcept(ac))); - headAtom = Atom.create(alc, headAtom.getArgument(0)); - } - } - - int index = 0; - for (Atom atom: originalClause.getHeadAtoms()) { - if (atom.equals(headAtom)) - return index; - if (atom.getDLPredicate() instanceof AtLeast) - index += ((AtLeast) atom.getDLPredicate()).getNumber(); - } - return -1; - } - - public static AtomicConcept getNegationConcept(DLPredicate p) { - if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING; - if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING; - - if (p instanceof AtomicConcept) { - String iri = ((AtomicConcept) p).getIRI(); - if (iri.endsWith(negativeSuffix)) - iri = iri.substring(0, iri.length() - 4); - else - iri += negativeSuffix; - - return AtomicConcept.create(iri); - } - if (p instanceof AtLeastConcept) { - // FIXME !!! here - return null; - } - return null; - } - - public static int getNumberOfSkolemisedIndividual() { - return individualCounter; - } - - public static Individual getNewIndividual(DLClause originalClause, int offset) { - Individual ret; - if (individualNumber.containsKey(originalClause)) { - ret = Individual.create(skolemisedIndividualPrefix + (individualNumber.get(originalClause) + offset)); - } - else { - individualNumber.put(originalClause, individualCounter); - ret = Individual.create(skolemisedIndividualPrefix + (individualCounter + offset)); - 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; - switch (clause.getHeadLength()) { - case 1: - return overApprox(clause.getHeadAtom(0), clause.getBodyAtoms(), originalClause); - case 0: - ret = new LinkedList(); - ret.add(clause); - return ret; - default: - ret = new LinkedList(); - for (Iterator iter = new DisjunctiveHeads(clause, originalClause); iter.hasNext(); ) - ret.add(iter.next()); - return ret; - } - } - - public Collection overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause) { - return overApprox(headAtom, bodyAtoms, originalClause, indexOfExistential(headAtom, originalClause)); - } - - public Collection overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause, int offset) { - Collection ret = new LinkedList(); - DLPredicate predicate = headAtom.getDLPredicate(); - if (predicate instanceof AtLeastConcept) { - AtLeastConcept atLeastConcept = (AtLeastConcept) predicate; - LiteralConcept concept = atLeastConcept.getToConcept(); - Role role = atLeastConcept.getOnRole(); - AtomicConcept atomicConcept = null; - - 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 = 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]; - for (int i = 0; i < card; ++i) individuals[i] = getNewIndividual(originalClause, offset + i); - - for (int i = 0; i < card; ++i) { - if (atomicConcept != null) - ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, bodyAtoms)); - - 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}, bodyAtoms)); - } - - 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])}, bodyAtoms)); - //DLClauseHelper.contructor_differentAs(individuals[i], individuals[j])); - - } - else if (predicate instanceof AtLeastDataRange) { - // TODO to be implemented ... - } - else - ret.add(DLClause.create(new Atom[] {headAtom}, bodyAtoms)); - - return ret; - } - - class DisjunctiveHeads implements Iterator { - - Atom[] bodyAtoms; - Atom[][] disjunctHeadAtoms; - int[] pointer; - int length, l; - LinkedList auxiliaryClauses = new LinkedList(); - - public DisjunctiveHeads(DLClause clause, DLClause originalClause) { - length = clause.getHeadLength(); - - bodyAtoms = clause.getBodyAtoms(); - disjunctHeadAtoms = new Atom[length][]; - pointer = new int[length]; - if (length > 0) l = length - 1; - else length = 0; - - int index = 0, offset = 0; - Collection datalogRules; - DLClause newClause; - for (Atom headAtom: clause.getHeadAtoms()) { - pointer[index] = 0; - - datalogRules = overApprox(headAtom, bodyAtoms, originalClause, offset); - - if (datalogRules.isEmpty()) { - l = -1; - auxiliaryClauses.clear(); - return ; - } - - for (Iterator iter = datalogRules.iterator(); iter.hasNext(); ) { - newClause = iter.next(); - if (!DLClauseHelper.hasSubsetBodyAtoms(newClause, clause)) { - auxiliaryClauses.add(newClause); - iter.remove(); - } - } - - disjunctHeadAtoms[index] = new Atom[datalogRules.size()]; - - int j = 0; - for (DLClause disjunct: datalogRules) { - disjunctHeadAtoms[index][j++] = disjunct.getHeadAtom(0); - } - - ++index; - if (headAtom.getDLPredicate() instanceof AtLeast) - offset += ((AtLeast) headAtom.getDLPredicate()).getNumber(); - - } - - } - - @Override - public boolean hasNext() { - return l != -1 || !auxiliaryClauses.isEmpty(); - } - - @Override - public DLClause next() { - if (l == -1) - return auxiliaryClauses.removeFirst(); - - if (length > 0) { - Atom[] headAtoms = new Atom[length]; - for (int i = 0; i < length; ++i) - headAtoms[i] = disjunctHeadAtoms[i][pointer[i]]; - - ++pointer[l]; - while (l >= 0 && pointer[l] >= disjunctHeadAtoms[l].length) { - pointer[l] = 0; - --l; - if (l >= 0) - ++pointer[l]; - } - - if (l >= 0) l = length - 1; - - return DLClauseHelper.simplified(DLClause.create(headAtoms, bodyAtoms)); -// return DLClause.create(headAtoms, bodyAtoms); - } - else { - --l; - return DLClauseHelper.simplified(DLClause.create(new Atom[0], bodyAtoms)); -// return DLClause.create(new Atom[0], bodyAtoms); - } - } - - @Override - public void remove() { } - - } -} -- cgit v1.2.3