001package conexp.fx.core.dl;
002
003/*
004 * #%L
005 * Concept Explorer FX
006 * %%
007 * Copyright (C) 2010 - 2019 Francesco Kriegel
008 * %%
009 * This program is free software: you can redistribute it and/or modify
010 * it under the terms of the GNU General Public License as
011 * published by the Free Software Foundation, either version 3 of the
012 * License, or (at your option) any later version.
013 * 
014 * This program is distributed in the hope that it will be useful,
015 * but WITHOUT ANY WARRANTY; without even the implied warranty of
016 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
017 * GNU General Public License for more details.
018 * 
019 * You should have received a copy of the GNU General Public
020 * License along with this program.  If not, see
021 * <http://www.gnu.org/licenses/gpl-3.0.html>.
022 * #L%
023 */
024
025import org.semanticweb.elk.owlapi.ElkReasonerFactory;
026import org.semanticweb.owlapi.apibinding.OWLManager;
027import org.semanticweb.owlapi.model.AddAxiom;
028import org.semanticweb.owlapi.model.IRI;
029import org.semanticweb.owlapi.model.OWLClass;
030import org.semanticweb.owlapi.model.OWLClassExpression;
031import org.semanticweb.owlapi.model.OWLDataFactory;
032import org.semanticweb.owlapi.model.OWLOntology;
033import org.semanticweb.owlapi.model.OWLOntologyManager;
034import org.semanticweb.owlapi.model.OWLSubClassOfAxiom;
035import org.semanticweb.owlapi.model.RemoveAxiom;
036import org.semanticweb.owlapi.reasoner.InferenceType;
037import org.semanticweb.owlapi.reasoner.OWLReasoner;
038
039public class ELReasoner {
040
041  public static final boolean subsumes(final OWLClassExpression concept1, final OWLClassExpression concept2) {
042    return isSubsumedBy(concept2, concept1);
043  }
044
045  public static final boolean subsumes(final ELConceptDescription concept1, final ELConceptDescription concept2) {
046    return isSubsumedBy(concept2, concept1);
047  }
048
049  public static final boolean isSubsumedBy(final OWLClassExpression concept1, final OWLClassExpression concept2) {
050    return isSubsumedBy(ELConceptDescription.of(concept1), ELConceptDescription.of(concept2));
051  }
052
053  /**
054   * @param concept1
055   * @param concept2
056   * @return true, iff concept1 is subsumed by concept2 (w.r.t. empty TBox)
057   */
058  public static final boolean isSubsumedBy(final ELConceptDescription concept1, final ELConceptDescription concept2) {
059    if (concept1.isBot())
060      return true;
061    if (concept2.isTop())
062      return true;
063    if (!concept1.getConceptNames().containsAll(concept2.getConceptNames()))
064      return false;
065    return concept2
066        .getExistentialRestrictions()
067        .entries()
068        .parallelStream()
069        .allMatch(
070            existentialRestriction2 -> concept1
071                .getExistentialRestrictions()
072                .entries()
073                .parallelStream()
074                .anyMatch(
075                    existentialRestriction1 -> existentialRestriction2.getKey().equals(existentialRestriction1.getKey())
076                        && isSubsumedBy(existentialRestriction1.getValue(), existentialRestriction2.getValue())));
077  }
078
079  public static final boolean
080      isSubsumedBy(final ELConceptDescription concept1, final ELConceptDescription concept2, final ELTBox tBox) {
081    return isSubsumedBy(concept1.toOWLClassExpression(), concept2.toOWLClassExpression(), tBox.toOWLOntology());
082  }
083
084  private static int dummy = 1618;
085
086  private static final int nextDummy() {
087    return dummy++;
088  }
089
090  public static final boolean
091      isSubsumedBy(final OWLClassExpression concept1, final OWLClassExpression concept2, final OWLOntology ontology) {
092    final OWLOntologyManager om = OWLManager.createOWLOntologyManager();
093    final OWLDataFactory df = OWLManager.getOWLDataFactory();
094
095    final OWLClass c1 = df.getOWLClass(IRI.create("dummy" + nextDummy()));
096    final OWLClass c2 = df.getOWLClass(IRI.create("dummy" + nextDummy()));
097    final OWLSubClassOfAxiom ax1 = df.getOWLSubClassOfAxiom(concept1, c1);
098    final OWLSubClassOfAxiom _ax1 = df.getOWLSubClassOfAxiom(c1, concept1);
099    final OWLSubClassOfAxiom ax2 = df.getOWLSubClassOfAxiom(c2, concept2);
100    final OWLSubClassOfAxiom _ax2 = df.getOWLSubClassOfAxiom(concept2, c2);
101    om.applyChange(new AddAxiom(ontology, ax1));
102    om.applyChange(new AddAxiom(ontology, ax2));
103    om.applyChange(new AddAxiom(ontology, _ax1));
104    om.applyChange(new AddAxiom(ontology, _ax2));
105
106    final OWLReasoner reasoner = new ElkReasonerFactory().createReasoner(ontology);
107//    final OWLReasoner reasoner = new JcelReasonerFactory().createReasoner(ontology);
108    reasoner.flush();
109    reasoner.precomputeInferences(InferenceType.CLASS_HIERARCHY);
110
111    final boolean result =
112        reasoner.getEquivalentClasses(c2).contains(c1) || reasoner.getSubClasses(c2, false).getFlattened().contains(c1);
113    reasoner.dispose();
114    om.applyChange(new RemoveAxiom(ontology, ax1));
115    om.applyChange(new RemoveAxiom(ontology, ax2));
116    om.applyChange(new RemoveAxiom(ontology, _ax1));
117    om.applyChange(new RemoveAxiom(ontology, _ax2));
118    return result;
119//    return elk.isEntailed(df.getOWLSubClassOfAxiom(concept1, concept2));
120  }
121
122  public static final boolean isSubsumedBy(
123      final ELConceptDescription concept1,
124      final ELConceptDescription concept2,
125      final OWLOntology ontology) {
126    return isSubsumedBy(concept1.toOWLClassExpression(), concept2.toOWLClassExpression(), ontology);
127  }
128
129}