001    /**
002     * Copyright (C) 2007-2011, Jens Lehmann
003     *
004     * This file is part of DL-Learner.
005     *
006     * DL-Learner is free software; you can redistribute it and/or modify
007     * it under the terms of the GNU General Public License as published by
008     * the Free Software Foundation; either version 3 of the License, or
009     * (at your option) any later version.
010     *
011     * DL-Learner is distributed in the hope that it will be useful,
012     * but WITHOUT ANY WARRANTY; without even the implied warranty of
013     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
014     * GNU General Public License for more details.
015     *
016     * You should have received a copy of the GNU General Public License
017     * along with this program.  If not, see <http://www.gnu.org/licenses/>.
018     */
019    
020    package org.dllearner.reasoning;
021    
022    import java.io.File;
023    import java.net.MalformedURLException;
024    import java.net.URL;
025    import java.util.Collection;
026    import java.util.LinkedList;
027    import java.util.List;
028    import java.util.Map;
029    import java.util.Set;
030    import java.util.SortedSet;
031    import java.util.TreeMap;
032    import java.util.TreeSet;
033    import java.util.Map.Entry;
034    
035    import org.apache.log4j.Logger;
036    import org.dllearner.core.ComponentInitException;
037    import org.dllearner.core.ComponentManager;
038    import org.dllearner.core.AbstractKnowledgeSource;
039    import org.dllearner.core.AbstractReasonerComponent;
040    import org.dllearner.core.ReasoningMethodUnsupportedException;
041    import org.dllearner.core.configurators.ComponentFactory;
042    import org.dllearner.core.configurators.FastInstanceCheckerConfigurator;
043    import org.dllearner.core.options.BooleanConfigOption;
044    import org.dllearner.core.options.ConfigEntry;
045    import org.dllearner.core.options.ConfigOption;
046    import org.dllearner.core.options.InvalidConfigOptionValueException;
047    import org.dllearner.core.options.StringConfigOption;
048    import org.dllearner.core.options.URLConfigOption;
049    import org.dllearner.core.owl.Axiom;
050    import org.dllearner.core.owl.BooleanValueRestriction;
051    import org.dllearner.core.owl.Constant;
052    import org.dllearner.core.owl.DataRange;
053    import org.dllearner.core.owl.DatatypeProperty;
054    import org.dllearner.core.owl.DatatypeSomeRestriction;
055    import org.dllearner.core.owl.DatatypeValueRestriction;
056    import org.dllearner.core.owl.Description;
057    import org.dllearner.core.owl.DoubleMaxValue;
058    import org.dllearner.core.owl.DoubleMinValue;
059    import org.dllearner.core.owl.Entity;
060    import org.dllearner.core.owl.Individual;
061    import org.dllearner.core.owl.Intersection;
062    import org.dllearner.core.owl.NamedClass;
063    import org.dllearner.core.owl.Negation;
064    import org.dllearner.core.owl.Nothing;
065    import org.dllearner.core.owl.ObjectAllRestriction;
066    import org.dllearner.core.owl.ObjectCardinalityRestriction;
067    import org.dllearner.core.owl.ObjectMaxCardinalityRestriction;
068    import org.dllearner.core.owl.ObjectMinCardinalityRestriction;
069    import org.dllearner.core.owl.ObjectProperty;
070    import org.dllearner.core.owl.ObjectPropertyExpression;
071    import org.dllearner.core.owl.ObjectSomeRestriction;
072    import org.dllearner.core.owl.ObjectValueRestriction;
073    import org.dllearner.core.owl.Thing;
074    import org.dllearner.core.owl.Union;
075    import org.dllearner.kb.OWLFile;
076    import org.dllearner.parser.KBParser;
077    import org.dllearner.parser.ParseException;
078    import org.dllearner.utilities.Helper;
079    import org.dllearner.utilities.owl.ConceptTransformation;
080    
081    /**
082     * Reasoner for fast instance checks. It works by completely dematerialising the
083     * knowledge base to speed up later reasoning requests. It then continues by
084     * only considering one model of the knowledge base (TODO: more explanation),
085     * which is neither correct nor complete, but sufficient in many cases. A big
086     * advantage of the algorithm is that it does not need even need to perform any
087     * set modifications (union, intersection, difference), so it avoids any Java
088     * object creation, which makes it extremely fast compared to standard
089     * reasoners.
090     * 
091     * Meanwhile, the algorithm has been extended to also perform fast retrieval
092     * operations. However, those need write access to memory and potentially have
093     * to deal with all individuals in a knowledge base. For many knowledge bases,
094     * they should still be reasonably fast. 
095     * 
096     * @author Jens Lehmann
097     * 
098     */
099    public class FastInstanceChecker extends AbstractReasonerComponent {
100    
101            private static Logger logger = Logger.getLogger(FastInstanceChecker.class);
102    
103    //      private boolean defaultNegation = true;
104    
105            private FastInstanceCheckerConfigurator configurator;
106    
107            @Override
108            public FastInstanceCheckerConfigurator getConfigurator() {
109                    return configurator;
110            }
111    
112            private Set<NamedClass> atomicConcepts;
113            private Set<ObjectProperty> atomicRoles;
114            private SortedSet<DatatypeProperty> datatypeProperties;
115            private SortedSet<DatatypeProperty> booleanDatatypeProperties = new TreeSet<DatatypeProperty>();
116            private SortedSet<DatatypeProperty> doubleDatatypeProperties = new TreeSet<DatatypeProperty>();
117            private SortedSet<DatatypeProperty> intDatatypeProperties = new TreeSet<DatatypeProperty>();
118            private SortedSet<DatatypeProperty> stringDatatypeProperties = new TreeSet<DatatypeProperty>();     
119            private TreeSet<Individual> individuals;
120    
121            // private ReasonerComponent rs;
122            private OWLAPIReasoner rc;
123    
124            // we use sorted sets (map indices) here, because they have only log(n)
125            // complexity for checking whether an element is contained in them
126            // instances of classes
127            private Map<NamedClass, TreeSet<Individual>> classInstancesPos = new TreeMap<NamedClass, TreeSet<Individual>>();
128            private Map<NamedClass, TreeSet<Individual>> classInstancesNeg = new TreeMap<NamedClass, TreeSet<Individual>>();
129            // object property mappings
130            private Map<ObjectProperty, Map<Individual, SortedSet<Individual>>> opPos = new TreeMap<ObjectProperty, Map<Individual, SortedSet<Individual>>>();
131            // datatype property mappings
132            // we have one mapping for true and false for efficiency reasons
133            private Map<DatatypeProperty, TreeSet<Individual>> bdPos = new TreeMap<DatatypeProperty, TreeSet<Individual>>();
134            private Map<DatatypeProperty, TreeSet<Individual>> bdNeg = new TreeMap<DatatypeProperty, TreeSet<Individual>>();
135            // for int and double we assume that a property can have several values,
136            // althoug this should be rare,
137            // e.g. hasValue(object,2) and hasValue(object,3)
138            private Map<DatatypeProperty, Map<Individual, SortedSet<Double>>> dd = new TreeMap<DatatypeProperty, Map<Individual, SortedSet<Double>>>();
139            private Map<DatatypeProperty, Map<Individual, SortedSet<Integer>>> id = new TreeMap<DatatypeProperty, Map<Individual, SortedSet<Integer>>>();
140            private Map<DatatypeProperty, Map<Individual, SortedSet<String>>> sd = new TreeMap<DatatypeProperty, Map<Individual, SortedSet<String>>>();
141            
142            /**
143             * Creates an instance of the fast instance checker.
144             * @param sources The knowledge sources used as input.
145             */
146            public FastInstanceChecker(Set<AbstractKnowledgeSource> sources) {
147                    super(sources);
148                    this.configurator = new FastInstanceCheckerConfigurator(this);
149            }
150    
151            /**
152             * @return The options of this component.
153             */
154            public static Collection<ConfigOption<?>> createConfigOptions() {
155                    Collection<ConfigOption<?>> options = new LinkedList<ConfigOption<?>>();
156                    StringConfigOption type = new StringConfigOption("reasonerType",
157                                    "FaCT++, HermiT, OWLlink or Pellet to dematerialize", "pellet", false, true);
158                    type.setAllowedValues(new String[] { "fact", "hermit", "owllink", "pellet" });
159                    // closure option? see:
160                    // http://owlapi.svn.sourceforge.net/viewvc/owlapi/owl1_1/trunk/tutorial/src/main/java/uk/ac/manchester/owl/tutorial/examples/ClosureAxiomsExample.java?view=markup
161                    options.add(type);
162                    try {
163                            URLConfigOption owlLinkURL = new URLConfigOption("owlLinkURL", "the URL to the remote OWLlink server", new URL("http://localhost:8080/"), false, true);
164                            options.add(owlLinkURL);
165                    } catch (MalformedURLException e) {
166                            e.printStackTrace();
167                    }
168                    options.add(new BooleanConfigOption("defaultNegation", "Whether to use default negation, i.e. an instance not being in a class means that it is in the negation of the class.", true, false, true));
169                    StringConfigOption forallSemantics = new StringConfigOption("forallRetrievalSemantics",
170                                    "This option controls how to interpret the all quantifier in \forall r.C. The standard option is" +
171                                    "to return all those which do not have an r-filler not in C. The domain semantics is to use those" +
172                                    "which are in the domain of r and do not have an r-filler not in C. The forallExists semantics is to" +
173                                    "use those which have at least one r-filler and do not have an r-filler not in C.", "standard");
174                    forallSemantics.setAllowedValues(new String[] { "standard", "domain", "forallExists" });
175                    // closure option? see:
176                    // http://owlapi.svn.sourceforge.net/viewvc/owlapi/owl1_1/trunk/tutorial/src/main/java/uk/ac/manchester/owl/tutorial/examples/ClosureAxiomsExample.java?view=markup
177    //              options.add(forallSemantics);           
178                    return options;
179            }
180    
181            /*
182             * (non-Javadoc)
183             * 
184             * @see org.dllearner.core.Component#applyConfigEntry(org.dllearner.core.config.ConfigEntry)
185             */
186            @Override
187            public <T> void applyConfigEntry(ConfigEntry<T> entry) throws InvalidConfigOptionValueException {
188            }
189    
190            /**
191             * @return The name of this component.
192             */
193            public static String getName() {
194                    return "fast instance checker";
195            }
196    
197            /*
198             * (non-Javadoc)
199             * 
200             * @see org.dllearner.core.Component#init()
201             */
202            @Override
203            public void init() throws ComponentInitException {
204                    // rc = new OWLAPIReasoner(sources);
205                    rc = ComponentFactory.getOWLAPIReasoner(sources);
206                    rc.getConfigurator().setReasonerType(configurator.getReasonerType());
207                    rc.getConfigurator().setOwlLinkURL(configurator.getOwlLinkURL());
208                    rc.init();
209    
210    //              try {
211                            atomicConcepts = rc.getNamedClasses();
212                            datatypeProperties = rc.getDatatypeProperties();
213                            booleanDatatypeProperties = rc.getBooleanDatatypeProperties();
214                            doubleDatatypeProperties = rc.getDoubleDatatypeProperties();
215                            intDatatypeProperties = rc.getIntDatatypeProperties();
216                            stringDatatypeProperties = rc.getStringDatatypeProperties();
217                            atomicRoles = rc.getObjectProperties();
218                            individuals = (TreeSet<Individual>) rc.getIndividuals();
219    
220                            // rs = new ReasonerComponent(rc);
221    
222                            // TODO: some code taken from Helper.createFlatABox, but pasted here
223                            // because additional things need to
224                            // be done (maybe this can be merge again with the
225                            // FastRetrievalReasoner later)
226                            long dematStartTime = System.currentTimeMillis();
227    
228                            logger.debug("dematerialising concepts");
229    
230                            for (NamedClass atomicConcept : rc.getNamedClasses()) {
231                                    SortedSet<Individual> pos = rc.getIndividuals(atomicConcept);
232                                    classInstancesPos.put(atomicConcept, (TreeSet<Individual>) pos);
233    
234                                    if (configurator.getDefaultNegation()) {
235                                            classInstancesNeg.put(atomicConcept, (TreeSet<Individual>) Helper.difference(individuals, pos));
236                                    } else {
237                                            // Pellet needs approximately infinite time to answer
238                                            // negated queries
239                                            // on the carcinogenesis data set (and probably others), so
240                                            // we have to
241                                            // be careful here
242                                            Negation negatedAtomicConcept = new Negation(atomicConcept);
243                                            classInstancesNeg.put(atomicConcept, (TreeSet<Individual>) rc.getIndividuals(negatedAtomicConcept));
244                                    }
245    
246                            }
247    
248                            logger.debug("dematerialising object properties");
249    
250                            for (ObjectProperty atomicRole : atomicRoles) {
251                                    opPos.put(atomicRole, rc.getPropertyMembers(atomicRole));
252                            }
253    
254                            logger.debug("dematerialising datatype properties");
255    
256                            for (DatatypeProperty dp : booleanDatatypeProperties) {
257                                    bdPos.put(dp, (TreeSet<Individual>) rc.getTrueDatatypeMembers(dp));
258                                    bdNeg.put(dp, (TreeSet<Individual>) rc.getFalseDatatypeMembers(dp));
259                            }
260    
261                            for (DatatypeProperty dp : intDatatypeProperties) {
262                                    id.put(dp, rc.getIntDatatypeMembers(dp));
263                            }
264    
265                            for (DatatypeProperty dp : doubleDatatypeProperties) {
266                                    dd.put(dp, rc.getDoubleDatatypeMembers(dp));
267                            }
268    
269                            for (DatatypeProperty dp : stringDatatypeProperties) {
270                                    sd.put(dp, rc.getStringDatatypeMembers(dp));
271                            }                       
272                            
273                            long dematDuration = System.currentTimeMillis() - dematStartTime;
274                            logger.debug("TBox dematerialised in " + dematDuration + " ms");
275    
276    //              } catch (ReasoningMethodUnsupportedException e) {
277    //                      throw new ComponentInitException(
278    //                                      "Underlying reasoner does not support all necessary reasoning methods.", e);
279    //              }
280            }
281    
282            @Override
283            public boolean hasTypeImpl(Description description, Individual individual)
284                            throws ReasoningMethodUnsupportedException {
285    
286    //               System.out.println("FIC: " + description + " " + individual);
287    
288                    if (description instanceof NamedClass) {
289                            return classInstancesPos.get((NamedClass) description).contains(individual);
290                    } else if (description instanceof Negation) {
291                            Description child = description.getChild(0);
292                            if (child instanceof NamedClass) {
293                                    return classInstancesNeg.get((NamedClass) child).contains(individual);
294                            } else {
295                                    // default negation
296                                    if(configurator.getDefaultNegation()) {
297                                            return !hasTypeImpl(child, individual);
298                                    } else {
299                                            logger.debug("Converting description to negation normal form in fast instance check (should be avoided if possible).");
300                                            Description nnf = ConceptTransformation.transformToNegationNormalForm(child);
301                                            return hasTypeImpl(nnf, individual);                                    
302                                    }
303    //                              throw new ReasoningMethodUnsupportedException("Instance check for description "
304    //                                              + description
305    //                                              + " unsupported. Description needs to be in negation normal form.");
306                            }
307                    } else if (description instanceof Thing) {
308                            return true;
309                    } else if (description instanceof Nothing) {
310                            return false;
311                    } else if (description instanceof Union) {
312                            // if the individual is instance of any of the subdescription of
313                            // the union, we return true
314                            List<Description> children = description.getChildren();
315                            for (Description child : children) {
316                                    if (hasTypeImpl(child, individual)) {
317                                            return true;
318                                    }
319                            }
320                            return false;
321                    } else if (description instanceof Intersection) {
322                            // if the individual is instance of all of the subdescription of
323                            // the union, we return true
324                            List<Description> children = description.getChildren();
325                            for (Description child : children) {
326                                    if (!hasTypeImpl(child, individual)) {
327                                            return false;
328                                    }
329                            }
330                            return true;
331                    } else if (description instanceof ObjectSomeRestriction) {
332                            ObjectPropertyExpression ope = ((ObjectSomeRestriction) description).getRole();
333                            if (!(ope instanceof ObjectProperty)) {
334                                    throw new ReasoningMethodUnsupportedException("Instance check for description "
335                                                    + description + " unsupported. Inverse object properties not supported.");
336                            }
337                            ObjectProperty op = (ObjectProperty) ope;
338                            Description child = description.getChild(0);
339                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);
340    
341                            if (mapping == null) {
342                                    logger.warn("Instance check of a description with an undefinied property (" + op
343                                                    + ").");
344                                    return false;
345                            }
346                            SortedSet<Individual> roleFillers = opPos.get(op).get(individual);
347                            if (roleFillers == null) {
348                                    return false;
349                            }
350                            for (Individual roleFiller : roleFillers) {
351                                    if (hasTypeImpl(child, roleFiller)) {
352                                            return true;
353                                    }
354                            }
355                            return false;
356                    } else if (description instanceof ObjectAllRestriction) {
357                            ObjectPropertyExpression ope = ((ObjectAllRestriction) description).getRole();
358                            if (!(ope instanceof ObjectProperty)) {
359                                    throw new ReasoningMethodUnsupportedException("Instance check for description "
360                                                    + description + " unsupported. Inverse object properties not supported.");
361                            }
362                            ObjectProperty op = (ObjectProperty) ope;
363                            Description child = description.getChild(0);
364                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);
365    
366                            if (mapping == null) {
367                                    logger.warn("Instance check of a description with an undefinied property (" + op
368                                                    + ").");
369                                    return true;
370                            }
371                            SortedSet<Individual> roleFillers = opPos.get(op).get(individual);
372                            if (roleFillers == null) {
373                                    return true;
374                            }
375                            for (Individual roleFiller : roleFillers) {
376                                    if (!hasTypeImpl(child, roleFiller)) {
377                                            return false;
378                                    }
379                            }
380                            return true;
381                    } else if (description instanceof ObjectMinCardinalityRestriction) {
382                            ObjectPropertyExpression ope = ((ObjectCardinalityRestriction) description).getRole();
383                            if (!(ope instanceof ObjectProperty)) {
384                                    throw new ReasoningMethodUnsupportedException("Instance check for description "
385                                                    + description + " unsupported. Inverse object properties not supported.");
386                            }
387                            ObjectProperty op = (ObjectProperty) ope;
388                            Description child = description.getChild(0);
389                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);
390    
391                            if (mapping == null) {
392                                    logger.warn("Instance check of a description with an undefinied property (" + op
393                                                    + ").");
394                                    return true;
395                            }
396    
397                            int number = ((ObjectCardinalityRestriction) description).getNumber();
398                            int nrOfFillers = 0;
399    
400    //                      SortedSet<Individual> roleFillers = opPos.get(op).get(individual);
401                            SortedSet<Individual> roleFillers = mapping.get(individual);
402    //                      System.out.println(roleFillers);
403                            
404                            // special case: there are always at least zero fillers
405                            if (number == 0) {
406                                    return true;
407                            }
408                            // return false if there are none or not enough role fillers
409                            if (roleFillers == null || roleFillers.size() < number) {
410                                    return false;
411                            }
412    
413                            int index = 0;
414                            for (Individual roleFiller : roleFillers) {
415                                    index++;
416                                    if (hasTypeImpl(child, roleFiller)) {
417                                            nrOfFillers++;
418                                            if (nrOfFillers == number) {
419                                                    return true;
420                                            }
421                                            // early abort: e.g. >= 10 hasStructure.Methyl;
422                                            // if there are 11 fillers and 2 are not Methyl, the result
423                                            // is false
424                                    } else {
425                                            if (roleFillers.size() - index < number) {
426                                                    return false;
427                                            }
428                                    }
429                            }
430                            return false;
431                    } else if (description instanceof ObjectMaxCardinalityRestriction) {
432                            ObjectPropertyExpression ope = ((ObjectCardinalityRestriction) description).getRole();
433                            if (!(ope instanceof ObjectProperty)) {
434                                    throw new ReasoningMethodUnsupportedException("Instance check for description "
435                                                    + description + " unsupported. Inverse object properties not supported.");
436                            }
437                            ObjectProperty op = (ObjectProperty) ope;
438                            Description child = description.getChild(0);
439                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);
440    
441                            if (mapping == null) {
442                                    logger.warn("Instance check of a description with an undefinied property (" + op
443                                                    + ").");
444                                    return true;
445                            }
446    
447                            int number = ((ObjectCardinalityRestriction) description).getNumber();
448                            int nrOfFillers = 0;
449    
450                            SortedSet<Individual> roleFillers = opPos.get(op).get(individual);
451                            // return true if there are none or not enough role fillers
452                            if (roleFillers == null || roleFillers.size() < number) {
453                                    return true;
454                            }
455    
456                            int index = 0;
457                            for (Individual roleFiller : roleFillers) {
458                                    index++;
459                                    if (hasTypeImpl(child, roleFiller)) {
460                                            nrOfFillers++;
461                                            if (nrOfFillers > number) {
462                                                    return false;
463                                            }
464                                            // early abort: e.g. <= 5 hasStructure.Methyl;
465                                            // if there are 6 fillers and 2 are not Methyl, the result
466                                            // is true
467                                    } else {
468                                            if (roleFillers.size() - index <= number) {
469                                                    return true;
470                                            }
471                                    }
472                            }
473                            return true;
474                    } else if (description instanceof ObjectValueRestriction) {
475                            Individual i = ((ObjectValueRestriction)description).getIndividual();
476                            ObjectProperty op = (ObjectProperty) ((ObjectValueRestriction)description).getRestrictedPropertyExpression();
477                            
478                            Set<Individual> inds = opPos.get(op).get(individual);
479                            return inds == null ? false : inds.contains(i);
480                    } else if (description instanceof BooleanValueRestriction) {
481                            DatatypeProperty dp = ((BooleanValueRestriction) description)
482                                            .getRestrictedPropertyExpression();
483                            boolean value = ((BooleanValueRestriction) description).getBooleanValue();
484    
485                            if (value) {
486                                    // check whether the individual is in the set of individuals
487                                    // mapped
488                                    // to true by this datatype property
489                                    return bdPos.get(dp).contains(individual);
490                            } else {
491                                    return bdNeg.get(dp).contains(individual);
492                            }
493                    } else if (description instanceof DatatypeSomeRestriction) {
494                            DatatypeSomeRestriction dsr = (DatatypeSomeRestriction) description;
495                            DatatypeProperty dp = (DatatypeProperty) dsr.getRestrictedPropertyExpression();
496                            DataRange dr = dsr.getDataRange();
497                            SortedSet<Double> values = dd.get(dp).get(individual);
498    
499                            // if there is no filler for this individual and property we
500                            // need to return false
501                            if (values == null) {
502                                    return false;
503                            }
504    
505                            if (dr instanceof DoubleMaxValue) {
506                                    return (values.first() <= ((DoubleMaxValue) dr).getValue());
507                            } else if (dr instanceof DoubleMinValue) {
508                                    return (values.last() >= ((DoubleMinValue) dr).getValue());
509                            }
510                    } else if (description instanceof DatatypeValueRestriction) {
511                            String i = ((DatatypeValueRestriction)description).getValue().getLiteral();
512                            DatatypeProperty dp = ((DatatypeValueRestriction)description).getRestrictedPropertyExpression();
513                            
514                            Set<String> inds = sd.get(dp).get(individual);
515                            return inds == null ? false : inds.contains(i);
516                    }
517    
518                    throw new ReasoningMethodUnsupportedException("Instance check for description "
519                                    + description + " unsupported.");
520            }
521    
522            @Override
523            public SortedSet<Individual> getIndividualsImpl(Description concept) throws ReasoningMethodUnsupportedException {
524                    return getIndividualsImplFast(concept);
525            }
526            
527            public SortedSet<Individual> getIndividualsImplStandard(Description concept)
528                    throws ReasoningMethodUnsupportedException {
529                    if (concept instanceof NamedClass) {
530                            return classInstancesPos.get((NamedClass) concept);
531                    } else if (concept instanceof Negation && concept.getChild(0) instanceof NamedClass) {
532                            return classInstancesNeg.get((NamedClass) concept.getChild(0));
533                    }
534             
535                    // return rs.retrieval(concept);
536                    SortedSet<Individual> inds = new TreeSet<Individual>();
537                    for (Individual i : individuals) {
538                            if (hasType(concept, i)) {
539                                    inds.add(i);
540                            }
541                    }
542                    return inds;
543            }
544            
545            @SuppressWarnings("unchecked")
546            public SortedSet<Individual> getIndividualsImplFast(Description description)
547                            throws ReasoningMethodUnsupportedException {
548                    // policy: returned sets are clones, i.e. can be modified
549                    // (of course we only have to clone the leafs of a class description tree)
550                    if (description instanceof NamedClass) {
551                            return (TreeSet<Individual>) classInstancesPos.get((NamedClass) description).clone();
552                    } else if (description instanceof Negation) {
553                            if(description.getChild(0) instanceof NamedClass) {
554                                    return (TreeSet<Individual>) classInstancesNeg.get((NamedClass) description.getChild(0)).clone();
555                            }
556                            // implement retrieval as default negation
557                            return Helper.difference((TreeSet<Individual>) individuals.clone(), getIndividualsImpl(description.getChild(0)));
558                    } else if (description instanceof Thing) {
559                            return (TreeSet<Individual>) individuals.clone();
560                    } else if (description instanceof Nothing) {
561                            return new TreeSet<Individual>();
562                    } else if (description instanceof Union) {
563                            // copy instances of first element and then subtract all others
564                            SortedSet<Individual> ret = getIndividualsImpl(description.getChild(0));
565                            int childNr = 0;
566                            for(Description child : description.getChildren()) {
567                                    if(childNr != 0) {
568                                            ret.addAll(getIndividualsImpl(child));
569                                    }
570                                    childNr++;
571                            }
572                            return ret;
573                    } else if (description instanceof Intersection) {
574                            // copy instances of first element and then subtract all others
575                            SortedSet<Individual> ret = getIndividualsImpl(description.getChild(0));
576                            int childNr = 0;
577                            for(Description child : description.getChildren()) {
578                                    if(childNr != 0) {
579                                            ret.retainAll(getIndividualsImpl(child));
580                                    }
581                                    childNr++;
582                            }
583                            return ret;
584                    } else if (description instanceof ObjectSomeRestriction) {
585                            SortedSet<Individual> targetSet = getIndividualsImpl(description.getChild(0));
586                            SortedSet<Individual> returnSet = new TreeSet<Individual>();
587                            
588                            ObjectPropertyExpression ope = ((ObjectSomeRestriction) description).getRole();
589                            if (!(ope instanceof ObjectProperty)) {
590                                    throw new ReasoningMethodUnsupportedException("Retrieval for description "
591                                                    + description + " unsupported. Inverse object properties not supported.");
592                            }
593                            ObjectProperty op = (ObjectProperty) ope;
594                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);                     
595                            
596                            // each individual is connected to a set of individuals via the property;
597                            // we loop through the complete mapping
598                            for(Entry<Individual, SortedSet<Individual>> entry : mapping.entrySet()) {
599                                    SortedSet<Individual> inds = entry.getValue();
600                                    for(Individual ind : inds) {
601                                            if(targetSet.contains(ind)) {
602                                                    returnSet.add(entry.getKey());
603                                                    // once we found an individual, we do not need to check the others
604                                                    continue; 
605                                            }
606                                    }
607                            }
608                            return returnSet;
609                    } else if (description instanceof ObjectAllRestriction) {
610                            // \forall restrictions are difficult to handle; assume we want to check
611                            // \forall hasChild.male with domain(hasChild)=Person; then for all non-persons
612                            // this is satisfied trivially (all of their non-existing children are male)
613    //                      if(!configurator.getForallRetrievalSemantics().equals("standard")) {
614    //                              throw new Error("Only forallExists semantics currently implemented.");
615    //                      }
616                            
617                            // problem: we need to make sure that \neg \exists r.\top \equiv \forall r.\bot
618                            // can still be reached in an algorithm (\forall r.\bot \equiv \bot under forallExists
619                            // semantics)
620                            
621                            SortedSet<Individual> targetSet = getIndividualsImpl(description.getChild(0));
622                                                    
623                            ObjectPropertyExpression ope = ((ObjectAllRestriction) description).getRole();
624                            if (!(ope instanceof ObjectProperty)) {
625                                    throw new ReasoningMethodUnsupportedException("Instance check for description "
626                                                    + description + " unsupported. Inverse object properties not supported.");
627                            }
628                            ObjectProperty op = (ObjectProperty) ope;
629                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);
630    //                      SortedSet<Individual> returnSet = new TreeSet<Individual>(mapping.keySet());
631                            SortedSet<Individual> returnSet = (SortedSet<Individual>) individuals.clone();
632                            
633                            // each individual is connected to a set of individuals via the property;
634                            // we loop through the complete mapping
635                            for(Entry<Individual, SortedSet<Individual>> entry : mapping.entrySet()) {
636                                    SortedSet<Individual> inds = entry.getValue();
637                                    for(Individual ind : inds) {
638                                            if(!targetSet.contains(ind)) {
639                                                    returnSet.remove(entry.getKey());
640                                                    continue; 
641                                            }
642                                    }
643                            }
644                            return returnSet;
645                    } else if (description instanceof ObjectMinCardinalityRestriction) {
646                            ObjectPropertyExpression ope = ((ObjectCardinalityRestriction) description).getRole();
647                            if (!(ope instanceof ObjectProperty)) {
648                                    throw new ReasoningMethodUnsupportedException("Instance check for description "
649                                                    + description + " unsupported. Inverse object properties not supported.");
650                            }
651                            ObjectProperty op = (ObjectProperty) ope;
652                            Description child = description.getChild(0);
653                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);
654                            SortedSet<Individual> targetSet = getIndividualsImpl(child);
655                            SortedSet<Individual> returnSet = new TreeSet<Individual>();
656    
657                            int number = ((ObjectCardinalityRestriction) description).getNumber();                  
658    
659                            for(Entry<Individual, SortedSet<Individual>> entry : mapping.entrySet()) {
660                                    int nrOfFillers = 0;
661                                    int index = 0;
662                                    SortedSet<Individual> inds = entry.getValue();
663                                    
664                                    // we do not need to run tests if there are not sufficiently many fillers
665                                    if(inds.size() < number) {
666                                            continue;
667                                    }
668                                    
669                                    for(Individual ind : inds) {
670                                            // stop inner loop when nr of fillers is reached
671                                            if(nrOfFillers >= number) {
672                                                    returnSet.add(entry.getKey());
673                                                    break;
674                                            }               
675                                            // early abort when too many instance checks failed
676                                            if (inds.size() - index < number) {
677                                                    break;
678                                            }                                       
679                                            if(targetSet.contains(ind)) {
680                                                    nrOfFillers++;
681                                            }
682                                            index++;
683                                    }
684                            }                       
685                            
686                            return returnSet;
687                    } else if (description instanceof ObjectMaxCardinalityRestriction) {
688                            ObjectPropertyExpression ope = ((ObjectCardinalityRestriction) description).getRole();
689                            if (!(ope instanceof ObjectProperty)) {
690                                    throw new ReasoningMethodUnsupportedException("Instance check for description "
691                                                    + description + " unsupported. Inverse object properties not supported.");
692                            }
693                            ObjectProperty op = (ObjectProperty) ope;
694                            Description child = description.getChild(0);
695                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);
696                            SortedSet<Individual> targetSet = getIndividualsImpl(child);
697                            // initially all individuals are in the return set and we then remove those
698                            // with too many fillers                        
699                            SortedSet<Individual> returnSet = (SortedSet<Individual>) individuals.clone();
700    
701                            int number = ((ObjectCardinalityRestriction) description).getNumber();                  
702    
703                            for(Entry<Individual, SortedSet<Individual>> entry : mapping.entrySet()) {
704                                    int nrOfFillers = 0;
705                                    int index = 0;
706                                    SortedSet<Individual> inds = entry.getValue();
707                                    
708                                    // we do not need to run tests if there are not sufficiently many fillers
709                                    if(number < inds.size()) {
710                                            returnSet.add(entry.getKey());
711                                            continue;
712                                    }
713                                    
714                                    for(Individual ind : inds) {
715                                            // stop inner loop when nr of fillers is reached
716                                            if(nrOfFillers >= number) {
717                                                    break;
718                                            }               
719                                            // early abort when too many instance are true already
720                                            if (inds.size() - index < number) {
721                                                    returnSet.add(entry.getKey());
722                                                    break;
723                                            }                                       
724                                            if(targetSet.contains(ind)) {
725                                                    nrOfFillers++;
726                                            }
727                                            index++;
728                                    }
729                            }                       
730                            
731                            return returnSet;
732                    } else if (description instanceof ObjectValueRestriction) {
733                            Individual i = ((ObjectValueRestriction)description).getIndividual();
734                            ObjectProperty op = (ObjectProperty) ((ObjectValueRestriction)description).getRestrictedPropertyExpression();
735                            
736                            Map<Individual, SortedSet<Individual>> mapping = opPos.get(op);                     
737                            SortedSet<Individual> returnSet = new TreeSet<Individual>();
738                            
739                            for(Entry<Individual, SortedSet<Individual>> entry : mapping.entrySet()) {
740                                    if(entry.getValue().contains(i)) {
741                                            returnSet.add(entry.getKey());
742                                    }
743                            }
744                            return returnSet;
745                    } else if (description instanceof BooleanValueRestriction) {
746                            DatatypeProperty dp = ((BooleanValueRestriction) description)
747                                            .getRestrictedPropertyExpression();
748                            boolean value = ((BooleanValueRestriction) description).getBooleanValue();
749    
750                            if (value) {
751                                    return (TreeSet<Individual>) bdPos.get(dp).clone();
752                            } else {
753                                    return (TreeSet<Individual>) bdNeg.get(dp).clone();
754                            }
755                    } else if (description instanceof DatatypeSomeRestriction) {
756                            DatatypeSomeRestriction dsr = (DatatypeSomeRestriction) description;
757                            DatatypeProperty dp = (DatatypeProperty) dsr.getRestrictedPropertyExpression();
758                            DataRange dr = dsr.getDataRange();
759    
760                            Map<Individual, SortedSet<Double>> mapping = dd.get(dp);                    
761                            SortedSet<Individual> returnSet = new TreeSet<Individual>();                        
762    
763                            if (dr instanceof DoubleMaxValue) {
764                                    for(Entry<Individual, SortedSet<Double>> entry : mapping.entrySet()) {
765                                            if(entry.getValue().first() <= ((DoubleMaxValue)dr).getValue()) {
766                                                    returnSet.add(entry.getKey());
767                                            }
768                                    }                               
769                            } else if (dr instanceof DoubleMinValue) {
770                                    for(Entry<Individual, SortedSet<Double>> entry : mapping.entrySet()) {
771                                            if(entry.getValue().last() >= ((DoubleMinValue)dr).getValue()) {
772                                                    returnSet.add(entry.getKey());
773                                            }
774                                    }
775                            }
776                    }
777                            
778                    throw new ReasoningMethodUnsupportedException("Retrieval for description "
779                                            + description + " unsupported.");               
780                            
781                    // return rs.retrieval(concept);
782    //              SortedSet<Individual> inds = new TreeSet<Individual>();
783    //              for (Individual i : individuals) {
784    //                      if (hasType(concept, i)) {
785    //                              inds.add(i);
786    //                      }
787    //              }
788    //              return inds;
789            }
790    
791            /*
792             * (non-Javadoc)
793             * 
794             * @see org.dllearner.core.Reasoner#getAtomicConcepts()
795             */
796            @Override
797            public Set<NamedClass> getNamedClasses() {
798                    return atomicConcepts;
799            }
800    
801            /*
802             * (non-Javadoc)
803             * 
804             * @see org.dllearner.core.Reasoner#getAtomicRoles()
805             */
806            @Override
807            public Set<ObjectProperty> getObjectProperties() {
808                    return atomicRoles;
809            }
810    
811            @Override
812            public SortedSet<DatatypeProperty> getDatatypePropertiesImpl() {
813                    return datatypeProperties;
814            }
815    
816            @Override
817            public SortedSet<DatatypeProperty> getBooleanDatatypePropertiesImpl() {
818                    return booleanDatatypeProperties;
819            }
820    
821            @Override
822            public SortedSet<DatatypeProperty> getDoubleDatatypePropertiesImpl() {
823                    return doubleDatatypeProperties;
824            }
825    
826            @Override
827            public SortedSet<DatatypeProperty> getIntDatatypePropertiesImpl() {
828                    return intDatatypeProperties;
829            }
830    
831            @Override
832            public SortedSet<DatatypeProperty> getStringDatatypePropertiesImpl() {
833                    return stringDatatypeProperties;
834            }       
835            
836            @Override
837            protected SortedSet<Description> getSuperClassesImpl(Description concept) throws ReasoningMethodUnsupportedException {
838                    return rc.getSuperClassesImpl(concept);
839            }
840            
841            @Override
842            protected SortedSet<Description> getSubClassesImpl(Description concept) throws ReasoningMethodUnsupportedException {
843                    return rc.getSubClassesImpl(concept);
844            }               
845    
846            @Override
847            protected SortedSet<ObjectProperty> getSuperPropertiesImpl(ObjectProperty role) throws ReasoningMethodUnsupportedException {
848                    return rc.getSuperPropertiesImpl(role);
849            }       
850    
851            @Override
852            protected SortedSet<ObjectProperty> getSubPropertiesImpl(ObjectProperty role) throws ReasoningMethodUnsupportedException {
853                    return rc.getSubPropertiesImpl(role);
854            }
855            
856            @Override
857            protected SortedSet<DatatypeProperty> getSuperPropertiesImpl(DatatypeProperty role) throws ReasoningMethodUnsupportedException {
858                    return rc.getSuperPropertiesImpl(role);
859            }       
860    
861            @Override
862            protected SortedSet<DatatypeProperty> getSubPropertiesImpl(DatatypeProperty role) throws ReasoningMethodUnsupportedException {
863                    return rc.getSubPropertiesImpl(role);
864            }       
865            
866            /*
867             * (non-Javadoc)
868             * 
869             * @see org.dllearner.core.Reasoner#getIndividuals()
870             */
871            @Override
872            public SortedSet<Individual> getIndividuals() {
873                    return individuals;
874            }
875    
876            /*
877             * (non-Javadoc)
878             * 
879             * @see org.dllearner.core.Reasoner#getReasonerType()
880             */
881            @Override
882            public ReasonerType getReasonerType() {
883                    return ReasonerType.FAST_INSTANCE_CHECKER;
884            }
885    
886    //      @Override
887    //      public ClassHierarchy getClassHierarchy() {
888    //              return rc.getClassHierarchy();
889    //      }
890    
891    //      @Override
892    //      public void prepareRoleHierarchyImpl(Set<ObjectProperty> allowedRoles) {
893    //              rc.prepareRoleHierarchy(allowedRoles);
894    //      }
895    
896    //      @Override
897    //      public ObjectPropertyHierarchy getRoleHierarchy() {
898    //              return rc.getRoleHierarchy();
899    //      }
900    
901    //      @Override
902    //      public void prepareDatatypePropertyHierarchyImpl(Set<DatatypeProperty> allowedRoles) {
903    //              rc.prepareDatatypePropertyHierarchyImpl(allowedRoles);
904    //      }
905    
906    //      @Override
907    //      public DatatypePropertyHierarchy getDatatypePropertyHierarchy() {
908    //              return rc.getDatatypePropertyHierarchy();
909    //      }
910    
911            @Override
912            public boolean isSuperClassOfImpl(Description superConcept, Description subConcept) {
913                    // Negation neg = new Negation(subConcept);
914                    // Intersection c = new Intersection(neg,superConcept);
915                    // return fastRetrieval.calculateSets(c).getPosSet().isEmpty();
916                    return rc.isSuperClassOfImpl(superConcept, subConcept);
917            }
918    
919            /**
920             * Test method for fast instance checker.
921             * 
922             * @param args
923             *            No arguments supported.
924             * @throws ComponentInitException Component cannot be initialised.
925             * @throws ParseException File cannot be parsed.
926             * @throws ReasoningMethodUnsupportedException Reasoning method not supported.
927             */
928            public static void main(String[] args) throws ComponentInitException, ParseException,
929                            ReasoningMethodUnsupportedException {
930                    ComponentManager cm = ComponentManager.getInstance();
931                    OWLFile owl = cm.knowledgeSource(OWLFile.class);
932                    String owlFile = new File("examples/family/father.owl").toURI().toString();
933                    cm.applyConfigEntry(owl, "url", owlFile);
934                    owl.init();
935                    AbstractReasonerComponent reasoner = cm.reasoner(FastInstanceChecker.class, owl);
936    //              cm.reasoningService(reasoner);
937                    reasoner.init();
938    
939                    KBParser.internalNamespace = "http://example.com/father#";
940                    String query = "(male AND EXISTS hasChild.TOP)";
941                    Description d = KBParser.parseConcept(query);
942                    System.out.println(d);
943                    Individual i = new Individual("http://example.com/father#markus");
944                    System.out.println(reasoner.hasType(d, i));
945            }
946    
947            /*
948             * (non-Javadoc)
949             * 
950             * @see org.dllearner.core.Reasoner#getBaseURI()
951             */
952            @Override
953            public String getBaseURI() {
954                    return rc.getBaseURI();
955            }
956    
957            /*
958             * (non-Javadoc)
959             * 
960             * @see org.dllearner.core.Reasoner#getPrefixes()
961             */
962            @Override
963            public Map<String, String> getPrefixes() {
964                    return rc.getPrefixes();
965            }
966    
967            @Override
968            public Description getDomainImpl(ObjectProperty objectProperty) {
969                    return rc.getDomain(objectProperty);
970            }
971    
972            @Override
973            public Description getDomainImpl(DatatypeProperty datatypeProperty) {
974                    return rc.getDomain(datatypeProperty);
975            }
976    
977            @Override
978            public Description getRangeImpl(ObjectProperty objectProperty) {
979                    return rc.getRange(objectProperty);
980            }
981    
982            @Override
983            public Map<Individual, SortedSet<Individual>> getPropertyMembersImpl(ObjectProperty atomicRole) {
984                    return opPos.get(atomicRole);
985            }
986    
987            @Override
988            public final SortedSet<Individual> getTrueDatatypeMembersImpl(DatatypeProperty datatypeProperty) {
989                    return bdPos.get(datatypeProperty);
990            }
991            
992            @Override
993            public final SortedSet<Individual> getFalseDatatypeMembersImpl(DatatypeProperty datatypeProperty) {
994                    return bdNeg.get(datatypeProperty);
995            }
996            
997            @Override
998            public Map<Individual, SortedSet<Integer>> getIntDatatypeMembersImpl(
999                            DatatypeProperty datatypeProperty) {
1000                    return id.get(datatypeProperty);
1001            }               
1002            
1003            @Override
1004            public Map<Individual, SortedSet<Double>> getDoubleDatatypeMembersImpl(
1005                            DatatypeProperty datatypeProperty) {
1006                    return dd.get(datatypeProperty);
1007            }       
1008            
1009            @Override
1010            public Map<Individual, SortedSet<Constant>> getDatatypeMembersImpl(
1011                            DatatypeProperty datatypeProperty) {
1012                    return rc.getDatatypeMembersImpl(datatypeProperty);
1013            }               
1014            
1015            @Override
1016            public Set<Individual> getRelatedIndividualsImpl(Individual individual, ObjectProperty objectProperty) throws ReasoningMethodUnsupportedException {
1017                    return rc.getRelatedIndividuals(individual, objectProperty);
1018            }
1019            
1020            @Override
1021            protected Map<ObjectProperty,Set<Individual>> getObjectPropertyRelationshipsImpl(Individual individual) {
1022                    return rc.getObjectPropertyRelationships(individual);
1023            }       
1024            
1025            @Override
1026            public Set<Constant> getRelatedValuesImpl(Individual individual, DatatypeProperty datatypeProperty) throws ReasoningMethodUnsupportedException {
1027                    return rc.getRelatedValues(individual, datatypeProperty);
1028            }       
1029            
1030            @Override
1031            public boolean isSatisfiableImpl() {
1032                    return rc.isSatisfiable();
1033            }       
1034            
1035            @Override
1036            public Set<Constant> getLabelImpl(Entity entity) throws ReasoningMethodUnsupportedException {
1037                    return rc.getLabel(entity);
1038            }       
1039            
1040            /*
1041             * (non-Javadoc)
1042             * 
1043             * @see org.dllearner.core.ReasonerComponent#releaseKB()
1044             */
1045            @Override
1046            public void releaseKB() {
1047                    rc.releaseKB();
1048            }
1049    
1050    //      @Override
1051    //      public boolean hasDatatypeSupport() {
1052    //              return true;
1053    //      }
1054    
1055            /* (non-Javadoc)
1056             * @see org.dllearner.core.ReasonerComponent#getTypesImpl(org.dllearner.core.owl.Individual)
1057             */
1058            @Override
1059            protected Set<NamedClass> getTypesImpl(Individual individual) {
1060                    return rc.getTypesImpl(individual);
1061            }
1062    
1063            /* (non-Javadoc)
1064             * @see org.dllearner.core.BaseReasoner#remainsSatisfiable(org.dllearner.core.owl.Axiom)
1065             */
1066            @Override
1067            public boolean remainsSatisfiableImpl(Axiom axiom) {
1068                    return rc.remainsSatisfiableImpl(axiom);
1069            }
1070    
1071            @Override
1072            protected Set<Description> getAssertedDefinitionsImpl(NamedClass nc) {
1073                    return rc.getAssertedDefinitionsImpl(nc);
1074            }
1075            
1076    }