001/**
002 * Copyright (C) 2007 - 2016, 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 it under
007 * the terms of the GNU General Public License as published by the Free Software
008 * Foundation; either version 3 of the License, or (at your option) any later
009 * version.
010 *
011 * DL-Learner is distributed in the hope that it will be useful, but WITHOUT ANY
012 * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR
013 * A PARTICULAR PURPOSE. See the GNU General Public License for more details.
014 *
015 * You should have received a copy of the GNU General Public License along with
016 * this program. If not, see <http://www.gnu.org/licenses/>.
017 */
018package org.dllearner.reasoning;
019
020import com.google.common.collect.Multimaps;
021import com.google.common.collect.Sets;
022import com.google.common.collect.Sets.SetView;
023import com.google.common.collect.TreeMultimap;
024import com.google.common.hash.HashFunction;
025import com.google.common.hash.Hasher;
026import com.google.common.hash.Hashing;
027import org.dllearner.core.*;
028import org.dllearner.core.annotations.NoConfigOption;
029import org.dllearner.core.config.ConfigOption;
030import org.dllearner.kb.OWLAPIOntology;
031import org.dllearner.utilities.Helper;
032import org.dllearner.utilities.MapUtils;
033import org.dllearner.utilities.OWLAPIUtils;
034import org.joda.time.DateTime;
035import org.joda.time.format.DateTimeFormatter;
036import org.semanticweb.owlapi.apibinding.OWLManager;
037import org.semanticweb.owlapi.model.*;
038import org.semanticweb.owlapi.util.DefaultPrefixManager;
039import org.semanticweb.owlapi.vocab.OWLFacet;
040import org.slf4j.Logger;
041import org.slf4j.LoggerFactory;
042import org.springframework.beans.factory.annotation.Autowired;
043import uk.ac.manchester.cs.owl.owlapi.OWLDataFactoryImpl;
044
045import java.io.*;
046import java.util.*;
047import java.util.Map.Entry;
048import java.util.concurrent.atomic.AtomicInteger;
049import java.util.concurrent.atomic.AtomicReference;
050import java.util.function.Function;
051import java.util.stream.Collectors;
052import java.util.stream.IntStream;
053
054/**
055 * Reasoner for fast instance checks. It works by completely dematerialising the
056 * knowledge base to speed up later reasoning requests. It then continues by
057 * only considering one model of the knowledge base (TODO: more explanation),
058 * which is neither correct nor complete, but sufficient in many cases. A big
059 * advantage of the algorithm is that it does not need even need to perform any
060 * set modifications (union, intersection, difference), so it avoids any Java
061 * object creation, which makes it extremely fast compared to standard
062 * reasoners.
063 *
064 * Meanwhile, the algorithm has been extended to also perform fast retrieval
065 * operations. However, those need write access to memory and potentially have
066 * to deal with all individuals in a knowledge base. For many knowledge bases,
067 * they should still be reasonably fast.
068 *
069 * @author Jens Lehmann
070 *
071 */
072@ComponentAnn(name = "closed world reasoner", shortName = "cwr", version = 0.9)
073public class ClosedWorldReasoner extends AbstractReasonerComponent {
074
075    private static Logger logger = LoggerFactory.getLogger(ClosedWorldReasoner.class);
076
077    // the underlying base reasoner implementation
078    private OWLAPIReasoner baseReasoner;
079    @ConfigOption(description = "the underlying reasoner implementation", defaultValue = "OWL API Reasoner")
080    private final OWLAPIReasoner reasonerComponent = null;
081    /**
082     * unused, see instead: baseReasoner
083     */
084
085    // we use an extra set for object properties because of punning option
086    private Set<OWLObjectProperty> objectProperties;
087
088    private TreeSet<OWLIndividual> individuals;
089
090    // instances of classes
091    private Map<OWLClass, TreeSet<OWLIndividual>> classInstancesPos = new TreeMap<>();
092    private Map<OWLClass, TreeSet<OWLIndividual>> classInstancesNeg = new TreeMap<>();
093    // object property mappings
094    private Map<OWLObjectProperty, Map<OWLIndividual, SortedSet<OWLIndividual>>> opPos = new TreeMap<>();
095//      private Map<OWLObjectProperty, Multimap<OWLIndividual, OWLIndividual>> opPos = new TreeMap<>();
096    // data property mappings
097    private Map<OWLDataProperty, Map<OWLIndividual, SortedSet<OWLLiteral>>> dpPos = new TreeMap<>();
098
099        // datatype property mappings
100    // we have one mapping for true and false for efficiency reasons
101    private Map<OWLDataProperty, TreeSet<OWLIndividual>> bdPos = new TreeMap<>();
102    private Map<OWLDataProperty, TreeSet<OWLIndividual>> bdNeg = new TreeMap<>();
103        // for int and double we assume that a property can have several values,
104    // althoug this should be rare,
105    // e.g. hasValue(object,2) and hasValue(object,3)
106    private Map<OWLDataProperty, Map<OWLIndividual, SortedSet<Double>>> dd = new TreeMap<>();
107    private Map<OWLDataProperty, Map<OWLIndividual, SortedSet<Integer>>> id = new TreeMap<>();
108    private Map<OWLDataProperty, Map<OWLIndividual, SortedSet<String>>> sd = new TreeMap<>();
109
110    private Map<OWLDataProperty, Map<OWLIndividual, SortedSet<Number>>> numericValueMappings = new TreeMap<>();
111
112    @ConfigOption(description = "Whether to use default negation, i.e. an instance not being in a class means that it is in the negation of the class.", defaultValue = "true", required = false)
113    private boolean defaultNegation = true;
114
115    @ConfigOption(description = "This option controls how to interpret the all quantifier in forall r.C. "
116            + "The standard option is to return all those which do not have an r-filler not in C. "
117            + "The domain semantics is to use those which are in the domain of r and do not have an r-filler not in C. "
118            + "The forallExists semantics is to use those which have at least one r-filler and do not have an r-filler not in C.",
119            defaultValue = "standard")
120    private ForallSemantics forAllSemantics = ForallSemantics.SomeOnly;
121
122    public enum ForallSemantics {
123
124        Standard, // standard all quantor
125        NonEmpty, // p only C for instance a returns false if there is no fact p(a,x) for any x
126        SomeOnly  // p only C for instance a returns false if there is no fact p(a,x) with x \in C
127    }
128
129    /**
130     * There are different ways on how disjointness between classes can be
131     * assumed.
132     *
133     * @author Lorenz Buehmann
134     *
135     */
136    public enum DisjointnessSemantics {
137
138        EXPLICIT,
139        INSTANCE_BASED
140    }
141
142    private DisjointnessSemantics disjointnessSemantics = DisjointnessSemantics.INSTANCE_BASED;
143
144    @ConfigOption(defaultValue = "false")
145    private boolean materializeExistentialRestrictions = false;
146    @ConfigOption(defaultValue = "true")
147    private boolean useMaterializationCaching = true;
148    @ConfigOption(defaultValue = "false")
149    private boolean handlePunning = false;
150    private boolean precomputeNegations = true;
151
152    public ClosedWorldReasoner() {
153    }
154
155    public ClosedWorldReasoner(TreeSet<OWLIndividual> individuals,
156            Map<OWLClass, TreeSet<OWLIndividual>> classInstancesPos,
157            Map<OWLObjectProperty, Map<OWLIndividual, SortedSet<OWLIndividual>>> opPos,
158            Map<OWLDataProperty, Map<OWLIndividual, SortedSet<Integer>>> id,
159            Map<OWLDataProperty, TreeSet<OWLIndividual>> bdPos,
160            Map<OWLDataProperty, TreeSet<OWLIndividual>> bdNeg,
161            KnowledgeSource... sources) {
162        super(new HashSet<>(Arrays.asList(sources)));
163        this.individuals = individuals;
164        this.classInstancesPos = classInstancesPos;
165        this.opPos = opPos;
166        this.id = id;
167        this.bdPos = bdPos;
168        this.bdNeg = bdNeg;
169
170        if (baseReasoner == null) {
171            baseReasoner = new OWLAPIReasoner(new HashSet<>(Arrays.asList(sources)));
172            try {
173                baseReasoner.init();
174            } catch (ComponentInitException e) {
175                throw new RuntimeException("Intialization of base reasoner failed.", e);
176            }
177        }
178
179        for (OWLClass atomicConcept : baseReasoner.getClasses()) {
180            TreeSet<OWLIndividual> pos = classInstancesPos.get(atomicConcept);
181            if (pos != null) {
182                classInstancesNeg.put(atomicConcept, new TreeSet<>(Sets.difference(individuals, pos)));
183            } else {
184                classInstancesPos.put(atomicConcept, new TreeSet<>());
185                classInstancesNeg.put(atomicConcept, individuals);
186            }
187        }
188
189        for (OWLObjectProperty p : baseReasoner.getObjectProperties()) {
190            opPos.computeIfAbsent(p, k -> new HashMap<>());
191        }
192
193        for (OWLDataProperty dp : baseReasoner.getBooleanDatatypeProperties()) {
194            bdPos.computeIfAbsent(dp, k -> new TreeSet<>());
195            bdNeg.computeIfAbsent(dp, k -> new TreeSet<>());
196
197        }
198    }
199
200    public ClosedWorldReasoner(Set<KnowledgeSource> sources) {
201        super(sources);
202    }
203
204    public ClosedWorldReasoner(KnowledgeSource... sources) {
205        super(new HashSet<>(Arrays.asList(sources)));
206    }
207
208    public ClosedWorldReasoner(OWLAPIReasoner baseReasoner) {
209        super(baseReasoner.getSources());
210        this.baseReasoner = baseReasoner;
211    }
212
213    /*
214     * (non-Javadoc)
215     * 
216     * @see org.dllearner.core.Component#init()
217     */
218    @Override
219    public void init() throws ComponentInitException {
220        if (baseReasoner == null) {
221            baseReasoner = new OWLAPIReasoner(sources);
222            baseReasoner.init();
223        }
224
225//              loadOrDematerialize();
226        materialize();
227        
228        initialized = true;
229    }
230
231    private void loadOrDematerialize() {
232        if (useMaterializationCaching) {
233            File cacheDir = new File("cache");
234            if(!cacheDir.mkdirs()) {
235                throw new RuntimeException("Failed to create cache directory at "  + cacheDir.getAbsolutePath());
236            }
237            HashFunction hf = Hashing.goodFastHash(128);
238            Hasher hasher = hf.newHasher();
239            hasher.putBoolean(materializeExistentialRestrictions);
240            hasher.putBoolean(handlePunning);
241            for (OWLOntology ont : Collections.singleton(baseReasoner.getOntology())) {
242                hasher.putInt(ont.getLogicalAxioms().hashCode());
243                hasher.putInt(ont.getAxioms().hashCode());
244            }
245            String filename = hasher.hash().toString() + ".obj";
246
247            File cacheFile = new File(cacheDir, filename);
248            if (cacheFile.exists()) {
249                logger.debug("Loading materialization from disk...");
250                try (ObjectInputStream ois = new ObjectInputStream(new FileInputStream(cacheFile))) {
251                    Materialization mat = (Materialization) ois.readObject();
252                    classInstancesPos = mat.classInstancesPos;
253                    classInstancesNeg = mat.classInstancesNeg;
254                    opPos = mat.opPos;
255                    dpPos = mat.dpPos;
256                    bdPos = mat.bdPos;
257                    bdNeg = mat.bdNeg;
258                    dd = mat.dd;
259                    id = mat.id;
260                    sd = mat.sd;
261                } catch (ClassNotFoundException | IOException e) {
262                    e.printStackTrace();
263                }
264                logger.debug("done.");
265            } else {
266                materialize();
267                Materialization mat = new Materialization();
268                mat.classInstancesPos = classInstancesPos;
269                mat.classInstancesNeg = classInstancesNeg;
270                mat.opPos = opPos;
271                mat.dpPos = dpPos;
272                mat.bdPos = bdPos;
273                mat.bdNeg = bdNeg;
274                mat.dd = dd;
275                mat.id = id;
276                mat.sd = sd;
277                try (ObjectOutputStream oos = new ObjectOutputStream(new FileOutputStream(cacheFile))) {
278                    oos.writeObject(mat);
279                } catch (IOException e) {
280                    e.printStackTrace();
281                }
282            }
283        } else {
284            materialize();
285        }
286    }
287
288    private void materialize() {
289        logger.info("Materializing TBox...");
290        long dematStartTime = System.currentTimeMillis();
291
292        objectProperties = baseReasoner.getObjectProperties();
293
294        individuals = (TreeSet<OWLIndividual>) baseReasoner.getIndividuals();
295
296        int totalEntities = baseReasoner.getClasses().size() +
297                            baseReasoner.getObjectProperties().size() +
298                            baseReasoner.getDatatypeProperties().size();
299
300        AtomicInteger i = new AtomicInteger();
301
302        logger.info("materialising concepts");
303        baseReasoner.getClasses().stream().filter(cls -> !cls.getIRI().isReservedVocabulary()).forEach(cls -> {
304            Helper.displayProgressPercentage(i.getAndIncrement(), totalEntities);
305            TreeSet<OWLIndividual> pos = (TreeSet<OWLIndividual>) baseReasoner.getIndividuals(cls);
306            classInstancesPos.put(cls, pos);
307
308            if (isDefaultNegation()) {
309                    /*
310                     *  we should avoid this operation because it returns a new
311                     *  set and thus could lead to memory issues
312                     *  Instead, we could later answer '\neg A(x)' by just check
313                     *  for A(x) and return the inverse.
314                     */
315                if (precomputeNegations) {
316                    classInstancesNeg.put(cls, new TreeSet<>(Sets.difference(individuals, pos)));
317                }
318            } else {
319                OWLObjectComplementOf negatedClass = df.getOWLObjectComplementOf(cls);
320                classInstancesNeg.put(cls, (TreeSet<OWLIndividual>) baseReasoner.getIndividuals(negatedClass));
321            }
322        });
323//        for (OWLClass cls : baseReasoner.getClasses()) {
324//            if (!cls.getIRI().isReservedVocabulary()) {
325//                SortedSet<OWLIndividual> pos = baseReasoner.getIndividuals(cls);
326//                classInstancesPos.put(cls, (TreeSet<OWLIndividual>) pos);
327//
328//                if (isDefaultNegation()) {
329//                    /*
330//                     *  we should avoid this operation because it returns a new
331//                     *  set and thus could lead to memory issues
332//                     *  Instead, we could later answer '\neg A(x)' by just check
333//                     *  for A(x) and return the inverse.
334//                     */
335//                    if (precomputeNegations) {
336//                        classInstancesNeg.put(cls, new TreeSet<>(Sets.difference(individuals, pos)));
337//                    }
338//                } else {
339//                    OWLObjectComplementOf negatedClass = df.getOWLObjectComplementOf(cls);
340//                    classInstancesNeg.put(cls, (TreeSet<OWLIndividual>) baseReasoner.getIndividuals(negatedClass));
341//                }
342//            } else {
343//                System.err.println(cls);
344//            }
345//        }
346
347        // materialize the object property facts
348        logger.info("materialising object properties ...");
349        baseReasoner.getObjectProperties().forEach(p -> {
350            Helper.displayProgressPercentage(i.getAndIncrement(), totalEntities);
351            opPos.put(p, baseReasoner.getPropertyMembers(p));
352        });
353
354        // materialize the data property facts
355        logger.info("materialising datatype properties");
356        baseReasoner.getDatatypeProperties().forEach(p -> {
357            Helper.displayProgressPercentage(i.getAndIncrement(), totalEntities);
358            dpPos.put(p, baseReasoner.getDatatypeMembers(p));
359        });
360
361        for (OWLDataProperty dp : baseReasoner.getBooleanDatatypeProperties()) {
362            bdPos.put(dp, (TreeSet<OWLIndividual>) baseReasoner.getTrueDatatypeMembers(dp));
363            bdNeg.put(dp, (TreeSet<OWLIndividual>) baseReasoner.getFalseDatatypeMembers(dp));
364        }
365
366//        id = baseReasoner.getIntDatatypeProperties().stream().collect(Collectors.toMap(Function.identity(), baseReasoner::getIntDatatypeMembers));
367//        dd = baseReasoner.getDoubleDatatypeProperties().stream().collect(Collectors.toMap(Function.identity(), baseReasoner::getDoubleDatatypeMembers));
368//        sd = baseReasoner.getStringDatatypeProperties().stream().collect(Collectors.toMap(Function.identity(), baseReasoner::getStringDatatypeMembers));
369
370        for (OWLDataProperty dp : baseReasoner.getIntDatatypeProperties()) {
371            id.put(dp, baseReasoner.getIntDatatypeMembers(dp));
372        }
373
374        for (OWLDataProperty dp : baseReasoner.getDoubleDatatypeProperties()) {
375            dd.put(dp, baseReasoner.getDoubleDatatypeMembers(dp));
376        }
377
378        for (OWLDataProperty dp : baseReasoner.getStringDatatypeProperties()) {
379            sd.put(dp, baseReasoner.getStringDatatypeMembers(dp));
380        }
381        logger.debug("finished materialising data properties.");
382
383        if (materializeExistentialRestrictions) {
384            ExistentialRestrictionMaterialization materialization = new ExistentialRestrictionMaterialization(baseReasoner.getReasoner().getRootOntology());
385            for (OWLClass cls : baseReasoner.getClasses()) {
386                TreeSet<OWLIndividual> individuals = classInstancesPos.get(cls);
387                Set<OWLClassExpression> superClass = materialization.materialize(cls.toStringID());
388                for (OWLClassExpression sup : superClass) {
389                    fill(individuals, sup);
390                }
391            }
392        }
393
394                //materialize facts based on OWL punning, i.e.:
395        //for each A in N_C
396        if (handlePunning && OWLPunningDetector.hasPunning(baseReasoner.getReasoner().getRootOntology())) {
397            OWLOntology ontology = baseReasoner.getReasoner().getRootOntology();
398
399            OWLIndividual genericIndividual = df.getOWLNamedIndividual(IRI.create("http://dl-learner.org/punning#genInd"));
400            Map<OWLIndividual, SortedSet<OWLIndividual>> map = new HashMap<>();
401            for (OWLIndividual individual : individuals) {
402                SortedSet<OWLIndividual> objects = new TreeSet<>();
403                objects.add(genericIndividual);
404                map.put(individual, objects);
405            }
406            for (OWLClass cls : baseReasoner.getClasses()) {
407                classInstancesNeg.get(cls).add(genericIndividual);
408                if (OWLPunningDetector.hasPunning(ontology, cls)) {
409                    OWLIndividual clsAsInd = df.getOWLNamedIndividual(IRI.create(cls.toStringID()));
410                    //for each x \in N_I with A(x) we add relatedTo(x,A)
411                    SortedSet<OWLIndividual> individuals = classInstancesPos.get(cls);
412                    for (OWLIndividual individual : individuals) {
413                        SortedSet<OWLIndividual> objects = map.computeIfAbsent(individual, k -> new TreeSet<>());
414                        objects.add(clsAsInd);
415
416                    }
417                }
418            }
419            opPos.put(OWLPunningDetector.punningProperty, map);
420            objectProperties = new TreeSet<>(objectProperties);
421            objectProperties.add(OWLPunningDetector.punningProperty);
422            objectProperties = Collections.unmodifiableSet(objectProperties);
423//                                      individuals.add(genericIndividual);
424        }
425
426        long dematDuration = System.currentTimeMillis() - dematStartTime;
427        logger.info("...TBox materialised in " + dematDuration + " ms.");
428    }
429
430    private void fill(SortedSet<OWLIndividual> individuals, OWLClassExpression d) {
431        if (!d.isAnonymous()) {
432            classInstancesPos.get(d.asOWLClass()).addAll(individuals);
433        } else if (d instanceof OWLObjectIntersectionOf) {
434            Set<OWLClassExpression> operands = ((OWLObjectIntersectionOf) d).getOperands();
435            for (OWLClassExpression operand : operands) {
436                fill(individuals, operand);
437            }
438        } else if (d instanceof OWLObjectSomeValuesFrom) {
439            OWLObjectProperty role = ((OWLObjectSomeValuesFrom) d).getProperty().asOWLObjectProperty();
440            OWLClassExpression filler = ((OWLObjectSomeValuesFrom) d).getFiller();
441            Map<OWLIndividual, SortedSet<OWLIndividual>> map = opPos.get(role);
442            //create new individual as object value for each individual
443            SortedSet<OWLIndividual> newIndividuals = new TreeSet<>();
444            int i = 0;
445            for (OWLIndividual individual : individuals) {
446                OWLIndividual newIndividual = df.getOWLNamedIndividual(IRI.create("http://dllearner.org#genInd_" + i++));
447                newIndividuals.add(newIndividual);
448                map
449                        .computeIfAbsent(individual, k -> new TreeSet<>())
450                        .add(newIndividual);
451            }
452            fill(newIndividuals, filler);
453
454        } else {
455            throw new UnsupportedOperationException("Should not happen.");
456        }
457    }
458
459    @Override
460    public boolean hasTypeImpl(OWLClassExpression description, OWLIndividual individual)
461            throws ReasoningMethodUnsupportedException {
462
463        if (description.isOWLThing()) {
464            return true;
465        } else if (description.isOWLNothing()) {
466            return false;
467        } else if (!description.isAnonymous()) {
468            return classInstancesPos.get(description.asOWLClass()).contains(individual);
469        } else if (description instanceof OWLObjectComplementOf) {
470            OWLClassExpression operand = ((OWLObjectComplementOf) description).getOperand();
471            if (!operand.isAnonymous()) {
472                if (isDefaultNegation()) {
473                    return !classInstancesPos.get(operand).contains(individual);
474                } else {
475                    return classInstancesNeg.get(operand).contains(individual);
476                }
477            } else {
478                if (isDefaultNegation()) {
479                    return !hasTypeImpl(operand, individual);
480                } else {
481                    logger.debug("Converting class expression to negation normal form in fast instance check (should be avoided if possible).");
482                    return hasTypeImpl(description.getNNF(), individual);
483                }
484            }
485        } else if (description instanceof OWLObjectUnionOf) {
486            for (OWLClassExpression operand : ((OWLObjectUnionOf) description).getOperands()) {
487                if (hasTypeImpl(operand, individual)) {
488                    return true;
489                }
490            }
491            return false;
492        } else if (description instanceof OWLObjectIntersectionOf) {
493            for (OWLClassExpression operand : ((OWLObjectIntersectionOf) description).getOperands()) {
494                if (!hasTypeImpl(operand, individual)) {
495                    return false;
496                }
497            }
498            return true;
499        } else if (description instanceof OWLObjectSomeValuesFrom) {
500            OWLObjectPropertyExpression property = ((OWLObjectSomeValuesFrom) description).getProperty();
501            OWLClassExpression fillerConcept = ((OWLObjectSomeValuesFrom) description).getFiller();
502
503            if (property.isAnonymous()) {// \exists r^{-1}.C
504                Map<OWLIndividual, SortedSet<OWLIndividual>> mapping = opPos.get(property.getNamedProperty());
505
506                for (Entry<OWLIndividual, SortedSet<OWLIndividual>> entry : mapping.entrySet()) {
507                    OWLIndividual subject = entry.getKey();
508                    SortedSet<OWLIndividual> objects = entry.getValue();
509
510                                        // check if the individual is contained in the objects and
511                    // subject is of type C
512                    if (objects.contains(individual)) {
513                        if (hasTypeImpl(fillerConcept, subject)) {
514                            return true;
515                        }
516                    }
517                }
518            } else {// \exists r.C
519                if (handlePunning && property == OWLPunningDetector.punningProperty && fillerConcept.isOWLThing()) {
520                    return true;
521                }
522
523                SortedSet<OWLIndividual> values = opPos.get(property).get(individual);
524
525                if (values == null) {
526                    return false;
527                }
528
529                for (OWLIndividual value : values) {
530                    if (hasTypeImpl(fillerConcept, value)) {
531                        return true;
532                    }
533                }
534            }
535
536            return false;
537        } else if (description instanceof OWLObjectAllValuesFrom) {
538            OWLObjectPropertyExpression property = ((OWLObjectAllValuesFrom) description).getProperty();
539            OWLClassExpression fillerConcept = ((OWLObjectAllValuesFrom) description).getFiller();
540
541            // \forall r.\top \equiv \top -> TRUE
542            if (fillerConcept.isOWLThing()) {
543                return true;
544            }
545
546            if (property.isAnonymous()) {// \forall r^{-1}.C
547                Map<OWLIndividual, SortedSet<OWLIndividual>> mapping = opPos.get(property.getNamedProperty());
548
549                Set<OWLIndividual> values = new HashSet<>();
550
551                for (Entry<OWLIndividual, SortedSet<OWLIndividual>> entry : mapping.entrySet()) {
552                    OWLIndividual subject = entry.getKey();
553                    SortedSet<OWLIndividual> objects = entry.getValue();
554
555                    if (objects.contains(individual)) {
556                        values.add(subject);
557                    }
558                }
559
560                // if there is no value, by standard semantics we have to return TRUE
561                if (values.isEmpty()) {
562                    return forAllSemantics == ForallSemantics.Standard;
563                }
564
565                boolean hasCorrectFiller = false;
566                for (OWLIndividual value : values) {
567                    if (hasTypeImpl(fillerConcept, value)) {
568                        hasCorrectFiller = true;
569                    } else {
570                        return false;
571                    }
572                }
573
574                if (forAllSemantics == ForallSemantics.SomeOnly) {
575                    return hasCorrectFiller;
576                } else {
577                    return true;
578                }
579
580            } else {// \forall r.C
581                SortedSet<OWLIndividual> values = opPos.get(property).get(individual);
582
583                // if there is no value, by standard semantics we have to return TRUE
584                if (values == null) {
585                    return forAllSemantics == ForallSemantics.Standard;
586                }
587
588                boolean hasCorrectFiller = false;
589                for (OWLIndividual value : values) {
590                    if (hasTypeImpl(fillerConcept, value)) {
591                        hasCorrectFiller = true;
592                    } else {
593                        return false;
594                    }
595                }
596
597                if (forAllSemantics == ForallSemantics.SomeOnly) {
598                    return hasCorrectFiller;
599                } else {
600                    return true;
601                }
602            }
603
604        } else if (description instanceof OWLObjectMinCardinality) {
605            int cardinality = ((OWLObjectMinCardinality) description).getCardinality();
606
607            // special case: there are always at least zero fillers
608            if (cardinality == 0) {
609                return true;
610            }
611
612            OWLObjectPropertyExpression property = ((OWLObjectMinCardinality) description).getProperty();
613            OWLClassExpression fillerConcept = ((OWLObjectMinCardinality) description).getFiller();
614
615            if (property.isAnonymous()) {
616                Map<OWLIndividual, SortedSet<OWLIndividual>> mapping = opPos.get(property.getNamedProperty());
617
618                int index = 0;
619                int nrOfFillers = 0;
620                int nrOfEntries = mapping.keySet().size();
621                for (Entry<OWLIndividual, SortedSet<OWLIndividual>> entry : mapping.entrySet()) {
622                    OWLIndividual subject = entry.getKey();
623                    SortedSet<OWLIndividual> objects = entry.getValue();
624
625                                        // count the number of subjects which are related to the individual such that
626                    // subject is of type C
627                    if (objects.contains(individual)) {
628                        if (hasTypeImpl(fillerConcept, subject)) {
629                            nrOfFillers++;
630
631                            if (nrOfFillers == cardinality) {
632                                return true;
633                            }
634                        } else {
635                            if (nrOfEntries - index < cardinality) {
636                                return false;
637                            }
638                        }
639                    }
640                }
641            } else {
642                Map<OWLIndividual, SortedSet<OWLIndividual>> mapping = opPos.get(property);
643
644                int nrOfFillers = 0;
645
646                SortedSet<OWLIndividual> values = mapping.get(individual);
647
648                // return false if there are none or not enough role fillers
649                if (values == null || (values.size() < cardinality && property != OWLPunningDetector.punningProperty)) {
650                    return false;
651                }
652
653                int index = 0;
654                for (OWLIndividual roleFiller : values) {
655                    index++;
656                    if (hasTypeImpl(fillerConcept, roleFiller)) {
657                        nrOfFillers++;
658                        if (nrOfFillers == cardinality
659                                || (handlePunning && property == OWLPunningDetector.punningProperty)) {
660                            return true;
661                        }
662                                                // early abort: e.g. >= 10 hasStructure.Methyl;
663                        // if there are 11 fillers and 2 are not Methyl, the result
664                        // is false
665                    } else {
666                        if (values.size() - index < cardinality) {
667                            return false;
668                        }
669                    }
670                }
671            }
672
673            return false;
674        } else if (description instanceof OWLObjectMaxCardinality) {
675            OWLObjectPropertyExpression property = ((OWLObjectMaxCardinality) description).getProperty();
676            OWLClassExpression fillerConcept = ((OWLObjectMaxCardinality) description).getFiller();
677            int cardinality = ((OWLObjectMaxCardinality) description).getCardinality();
678
679            if (property.isAnonymous()) {
680                Map<OWLIndividual, SortedSet<OWLIndividual>> mapping = opPos.get(property.getNamedProperty());
681
682                int nrOfFillers = 0;
683                int nrOfSubjects = mapping.keySet().size();
684
685                // return TRUE if there are none or not enough subjects
686                if (nrOfSubjects < cardinality) {
687                    return true;
688                }
689
690                int index = 0;
691                for (Entry<OWLIndividual, SortedSet<OWLIndividual>> entry : mapping.entrySet()) {
692                    index++;
693                    OWLIndividual subject = entry.getKey();
694                    SortedSet<OWLIndividual> objects = entry.getValue();
695                    if (objects.contains(individual) && hasTypeImpl(fillerConcept, subject)) {
696                        nrOfFillers++;
697                        if (nrOfFillers > cardinality) {
698                            return false;
699                        }
700                                                // early abort: e.g. <= 5 hasStructure.Methyl;
701                        // if there are 6 fillers and 2 are not Methyl, the result
702                        // is true
703                    } else {
704                        if (nrOfSubjects - index <= cardinality) {
705                            return true;
706                        }
707                    }
708                }
709            } else {
710                Map<OWLIndividual, SortedSet<OWLIndividual>> mapping = opPos.get(property);
711
712                int nrOfFillers = 0;
713
714                SortedSet<OWLIndividual> roleFillers = mapping.get(individual);
715
716                // return true if there are none or not enough role fillers
717                if (roleFillers == null || roleFillers.size() < cardinality) {
718                    return true;
719                }
720
721                int index = 0;
722                for (OWLIndividual roleFiller : roleFillers) {
723                    index++;
724                    if (hasTypeImpl(fillerConcept, roleFiller)) {
725                        nrOfFillers++;
726                        if (nrOfFillers > cardinality) {
727                            return false;
728                        }
729                                                // early abort: e.g. <= 5 hasStructure.Methyl;
730                        // if there are 6 fillers and 2 are not Methyl, the result
731                        // is true
732                    } else {
733                        if (roleFillers.size() - index <= cardinality) {
734                            return true;
735                        }
736                    }
737                }
738            }
739
740            return true;
741        } else if (description instanceof OWLObjectExactCardinality) {
742            OWLObjectPropertyExpression property = ((OWLObjectExactCardinality) description).getProperty();
743            OWLClassExpression fillerConcept = ((OWLObjectExactCardinality) description).getFiller();
744            int cardinality = ((OWLObjectExactCardinality) description).getCardinality();
745
746            // the mapping of instances related by r
747            Map<OWLIndividual, ? extends Collection<OWLIndividual>> mapping = getTargetIndividuals(property);
748
749            int nrOfFillers = 0;
750
751            Collection<OWLIndividual> roleFillers = mapping.get(individual);
752
753            // return true if there are none or not enough role fillers
754            if (roleFillers == null || roleFillers.size() < cardinality) {
755                return false;
756            }
757
758            int index = 0;
759            for (OWLIndividual roleFiller : roleFillers) {
760                index++;
761                if (hasTypeImpl(fillerConcept, roleFiller)) {
762                    nrOfFillers++;
763
764                    // too many individuals that already belong to filler class
765                    if (nrOfFillers > cardinality) {
766                        return false;
767                    }
768                    // early abort: e.g. <= 5 hasStructure.Methyl;
769                    // if there are 6 fillers and 2 are not Methyl, the result
770                    // is false
771                } else {
772                    // not enough remaining individuals that could belong to filler class
773                    if (roleFillers.size() - index <= cardinality) {
774                        return false;
775                    }
776                }
777            }
778            return true;
779
780        } else if (description instanceof OWLObjectHasValue) {
781            OWLObjectPropertyExpression property = ((OWLObjectHasValue) description).getProperty();
782            OWLIndividual value = ((OWLObjectHasValue) description).getFiller();
783
784            Map<OWLIndividual, SortedSet<OWLIndividual>> mapping = opPos.get(property.getNamedProperty());
785
786            if (property.isAnonymous()) {
787
788                for (Entry<OWLIndividual, SortedSet<OWLIndividual>> entry : mapping
789                        .entrySet()) {
790                    OWLIndividual subject = entry.getKey();
791                    SortedSet<OWLIndividual> objects = entry.getValue();
792
793                    if (objects.contains(individual) && subject.equals(value)) {
794                        return true;
795                    }
796                }
797                return false;
798            } else {
799
800                SortedSet<OWLIndividual> values = mapping.get(individual);
801
802                return values != null && values.contains(value);
803            }
804        } //            else if (OWLClassExpression instanceof BooleanValueRestriction) {
805        //                      DatatypeProperty dp = ((BooleanValueRestriction) description)
806        //                                      .getRestrictedPropertyExpression();
807        //                      boolean value = ((BooleanValueRestriction) description).getBooleanValue();
808        //
809        //                      if (value) {
810        //                              // check whether the OWLIndividual is in the set of individuals
811        //                              // mapped
812        //                              // to true by this datatype property
813        //                              return bdPos.get(dp).contains(individual);
814        //                      } else {
815        //                              return bdNeg.get(dp).contains(individual);
816        //                      }
817        //              }
818        else if (description instanceof OWLDataSomeValuesFrom) {
819            OWLDataPropertyExpression property = ((OWLDataSomeValuesFrom) description).getProperty();
820            OWLDataRange filler = ((OWLDataSomeValuesFrom) description).getFiller();
821
822            if (property.isAnonymous()) {
823                throw new ReasoningMethodUnsupportedException("Retrieval for class expression "
824                        + description + " unsupported. Inverse object properties not supported.");
825            }
826
827            if (filler.isDatatype()) { // filler is a datatype
828                return dpPos.get(property).containsKey(individual);
829            } else if (filler instanceof OWLDatatypeRestriction) {
830                OWLDatatype datatype = ((OWLDatatypeRestriction) filler).getDatatype();
831                Set<OWLFacetRestriction> facetRestrictions = ((OWLDatatypeRestriction) filler).getFacetRestrictions();
832
833                if (OWLAPIUtils.floatDatatypes.contains(datatype)) {
834                    SortedSet<Double> values = dd.get(property).get(individual);
835
836                    // no value exists
837                    if (values == null) {
838                        return false;
839                    }
840
841                    double min = -Double.MAX_VALUE;
842                    double max = Double.MAX_VALUE;
843                    for (OWLFacetRestriction facet : facetRestrictions) {
844                        if (facet.getFacet() == OWLFacet.MIN_INCLUSIVE) {
845                            min = Double.parseDouble(facet.getFacetValue().getLiteral());
846                        } else if (facet.getFacet() == OWLFacet.MAX_INCLUSIVE) {
847                            max = Double.parseDouble(facet.getFacetValue().getLiteral());
848                        }
849                    }
850
851                    //we can return false if largest number is below minimum or lowest number is above maximum
852                    if (values.last() < min || values.first() > max) {
853                        return false;
854                    }
855
856                    //search a value which is in the interval
857                    for (Double value : values) {
858                        if (value >= min && value <= max) {
859                            return true;
860                        }
861                    }
862                } else if (OWLAPIUtils.intDatatypes.contains(datatype)) {
863                    SortedSet<Integer> values = id.get(property).get(individual);
864
865                    // no value exists
866                    if (values == null) {
867                        return false;
868                    }
869
870                    int min = Integer.MIN_VALUE;
871                    int max = Integer.MAX_VALUE;
872                    for (OWLFacetRestriction facet : facetRestrictions) {
873                        if (facet.getFacet() == OWLFacet.MIN_INCLUSIVE) {
874                            min = facet.getFacetValue().parseInteger();
875                        } else if (facet.getFacet() == OWLFacet.MAX_INCLUSIVE) {
876                            max = facet.getFacetValue().parseInteger();
877                        }
878                    }
879
880                    //we can return false if largest number is below minimum or lowest number is above maximum
881                    if (values.last() < min || values.first() > max) {
882                        return false;
883                    }
884
885                    //search a value which is in the interval
886                    for (Integer value : values) {
887                        if (value >= min && value <= max) {
888                            return true;
889                        }
890                    }
891                } else if (OWLAPIUtils.dtDatatypes.contains(datatype)) {
892                    SortedSet<OWLLiteral> values = dpPos.get(property).get(individual);
893
894                                                // TODO we cannot ensure the sorting, because OWL API does only String comparison
895                    // on the lexical String value
896                    // no value exists
897                    if (values == null) {
898                        return false;
899                    }
900
901                    OWLLiteral min = null;
902                    OWLLiteral max = null;
903                    for (OWLFacetRestriction facet : facetRestrictions) {
904                        if (facet.getFacet() == OWLFacet.MIN_INCLUSIVE) {
905                            min = facet.getFacetValue();
906                        } else if (facet.getFacet() == OWLFacet.MAX_INCLUSIVE) {
907                            max = facet.getFacetValue();
908                        }
909                    }
910
911                    // we can return false if largest number is below minimum or lowest number is above maximum
912                    DateTimeFormatter parser = OWLAPIUtils.dateTimeParsers.get(datatype);
913                    DateTime minDateTime = null;
914                    if (min != null) {
915                        minDateTime = parser.parseDateTime(min.getLiteral());
916                    }
917                    DateTime maxDateTime = null;
918                    if (max != null) {
919                        maxDateTime = parser.parseDateTime(max.getLiteral());
920                    }
921
922                    if ((minDateTime != null && parser.parseDateTime(values.last().getLiteral()).isBefore(minDateTime))
923                            || (maxDateTime != null && parser.parseDateTime(values.first().getLiteral()).isAfter(maxDateTime))) {
924                        return false;
925                    }
926
927                    //search a value which is in the interval
928                    for (OWLLiteral value : values) {
929                        if (OWLAPIUtils.inRange(value, min, max)) {
930                            return true;
931                        }
932                    }
933                    return false;
934                }
935            } else if (filler.getDataRangeType() == DataRangeType.DATA_ONE_OF) {
936                OWLDataOneOf dataOneOf = (OWLDataOneOf) filler;
937                Set<OWLLiteral> values = dataOneOf.getValues();
938
939                                // given \exists r.{v_1,...,v_n} we can check for each value v_i
940                // if (\exists r.{v_i})(ind) holds
941                for (OWLLiteral value : values) {
942
943                    boolean hasValue = hasTypeImpl(df.getOWLDataHasValue(property, value), individual);
944
945                    if (hasValue) {
946                        return true;
947                    }
948                }
949                return false;
950            }
951        } else if (description instanceof OWLDataHasValue) {
952            OWLDataPropertyExpression property = ((OWLDataHasValue) description).getProperty();
953            OWLLiteral value = ((OWLDataHasValue) description).getFiller();
954
955            if (property.isAnonymous()) {
956                throw new ReasoningMethodUnsupportedException("Retrieval for class expression "
957                        + description + " unsupported. Inverse object properties not supported.");
958            }
959
960            Map<OWLIndividual, SortedSet<OWLLiteral>> mapping = dpPos.get(property);
961
962            SortedSet<OWLLiteral> values = mapping.get(individual);
963
964            return values != null && values.contains(value);
965        } else if (description instanceof OWLObjectOneOf) {
966            return ((OWLObjectOneOf) description).getIndividuals().contains(individual);
967        }
968
969        throw new ReasoningMethodUnsupportedException("Instance check for class expression "
970                + description + " of type " + description.getClassExpressionType() + " unsupported.");
971    }
972
973    @Override
974    public SortedSet<OWLIndividual> getIndividualsImpl(OWLClassExpression concept) throws ReasoningMethodUnsupportedException {
975        return getIndividualsImplFast(concept);
976    }
977
978    public SortedSet<OWLIndividual> getIndividualsImplStandard(OWLClassExpression concept) {
979        if (!concept.isAnonymous()) {
980            return classInstancesPos.get(concept);
981        } else if (concept instanceof OWLObjectComplementOf) {
982            OWLClassExpression operand = ((OWLObjectComplementOf) concept).getOperand();
983            if (!operand.isAnonymous()) {
984                return classInstancesNeg.get(operand);
985            }
986        }
987
988        // return rs.retrieval(concept);
989        SortedSet<OWLIndividual> inds = new TreeSet<>();
990        for (OWLIndividual i : individuals) {
991            if (hasType(concept, i)) {
992                inds.add(i);
993            }
994        }
995        return inds;
996    }
997
998    @SuppressWarnings("unchecked")
999    public SortedSet<OWLIndividual> getIndividualsImplFast(OWLClassExpression description)
1000            throws ReasoningMethodUnsupportedException {
1001                // policy: returned sets are clones, i.e. can be modified
1002        // (of course we only have to clone the leafs of a class OWLClassExpression tree)
1003        if (description.isOWLThing()) {
1004            return (TreeSet<OWLIndividual>) individuals.clone();
1005        } else if (description.isOWLNothing()) {
1006            return new TreeSet<>();
1007        } else if (!description.isAnonymous()) {
1008            if (classInstancesPos.containsKey(description.asOWLClass())) {
1009                return (TreeSet<OWLIndividual>) classInstancesPos.get(description).clone();
1010            } else {
1011                return new TreeSet<>();
1012            }
1013        } else if (description instanceof OWLObjectComplementOf) {
1014            OWLClassExpression operand = ((OWLObjectComplementOf) description).getOperand();
1015            if (!operand.isAnonymous()) {
1016                if (isDefaultNegation()) {
1017                    if (precomputeNegations) {
1018                        return (TreeSet<OWLIndividual>) classInstancesNeg.get(operand).clone();
1019                    }
1020                    SetView<OWLIndividual> diff = Sets.difference(individuals, classInstancesPos.get(operand));
1021                    return new TreeSet<>(diff);
1022                } else {
1023                    return (TreeSet<OWLIndividual>) classInstancesNeg.get(operand).clone();
1024                }
1025            }
1026            // implement retrieval as default negation
1027            return new TreeSet<>(Sets.difference(individuals, getIndividualsImpl(operand)));
1028        } else if (description instanceof OWLObjectUnionOf) {
1029            SortedSet<OWLIndividual> ret = new TreeSet<>();
1030            for (OWLClassExpression operand : ((OWLObjectUnionOf) description).getOperands()) {
1031                ret.addAll(getIndividualsImpl(operand));
1032            }
1033            return ret;
1034        } else if (description instanceof OWLObjectIntersectionOf) {
1035            Iterator<OWLClassExpression> iterator = ((OWLObjectIntersectionOf) description).getOperands().iterator();
1036            // copy instances of first element and then subtract all others
1037            SortedSet<OWLIndividual> ret = getIndividualsImpl(iterator.next());
1038            while (iterator.hasNext()) {
1039                ret.retainAll(getIndividualsImpl(iterator.next()));
1040            }
1041            return ret;
1042        } else if (description instanceof OWLObjectSomeValuesFrom) {
1043            OWLObjectPropertyExpression property = ((OWLObjectSomeValuesFrom) description).getProperty();
1044            OWLClassExpression filler = ((OWLObjectSomeValuesFrom) description).getFiller();
1045
1046            // get instances of filler concept
1047            SortedSet<OWLIndividual> targetSet = getIndividualsImpl(filler);
1048
1049            // the mapping of instances related by r
1050            Map<OWLIndividual, ? extends Collection<OWLIndividual>> mapping = getTargetIndividuals(property);
1051
1052            // each individual is connected to a set of individuals via the property;
1053            // we loop through the complete mapping
1054            return mapping.entrySet().stream()
1055                    .filter(e -> e.getValue().stream().anyMatch(targetSet::contains))
1056                    .map(Entry::getKey)
1057                    .collect(Collectors.toCollection(TreeSet::new));
1058        } else if (description instanceof OWLObjectAllValuesFrom) {
1059            // \forall restrictions are difficult to handle; assume we want to check
1060            // \forall hasChild.male with domain(hasChild)=Person; then for all non-persons
1061            // this is satisfied trivially (all of their non-existing children are male)
1062//                      if(!configurator.getForallRetrievalSemantics().equals("standard")) {
1063//                              throw new Error("Only forallExists semantics currently implemented.");
1064//                      }
1065
1066            // problem: we need to make sure that \neg \exists r.\top \equiv \forall r.\bot
1067            // can still be reached in an algorithm (\forall r.\bot \equiv \bot under forallExists
1068            // semantics)
1069            OWLObjectPropertyExpression property = ((OWLObjectAllValuesFrom) description).getProperty();
1070            OWLClassExpression filler = ((OWLObjectAllValuesFrom) description).getFiller();
1071
1072            // get instances of filler concept
1073            SortedSet<OWLIndividual> targetSet = getIndividualsImpl(filler);
1074
1075            // the mapping of instances related by r
1076            Map<OWLIndividual, ? extends Collection<OWLIndividual>> mapping = getTargetIndividuals(property);
1077
1078//                      SortedSet<OWLIndividual> returnSet = new TreeSet<OWLIndividual>(mapping.keySet());
1079            SortedSet<OWLIndividual> returnSet = (SortedSet<OWLIndividual>) individuals.clone();
1080
1081            // each individual is connected to a set of individuals via the property;
1082            // we loop through the complete mapping
1083            mapping.entrySet().stream()
1084                    .filter(e -> e.getValue().stream().anyMatch(ind -> !targetSet.contains(ind)))
1085                    .forEach(e -> returnSet.remove(e.getKey()));
1086
1087            return returnSet;
1088        } else if (description instanceof OWLObjectMinCardinality) {
1089            OWLObjectPropertyExpression property = ((OWLObjectMinCardinality) description).getProperty();
1090            OWLClassExpression filler = ((OWLObjectMinCardinality) description).getFiller();
1091
1092            // get instances of filler concept
1093            SortedSet<OWLIndividual> targetSet = getIndividualsImpl(filler);
1094
1095            // the mapping of instances related by r
1096            Map<OWLIndividual, ? extends Collection<OWLIndividual>> mapping = getTargetIndividuals(property);
1097
1098            SortedSet<OWLIndividual> returnSet = new TreeSet<>();
1099
1100            int number = ((OWLObjectMinCardinality) description).getCardinality();
1101
1102            for (Entry<OWLIndividual, ? extends Collection<OWLIndividual>> entry : mapping.entrySet()) {
1103                int nrOfFillers = 0;
1104                int index = 0;
1105                Collection<OWLIndividual> inds = entry.getValue();
1106
1107                // we do not need to run tests if there are not sufficiently many fillers
1108                if (inds.size() < number) {
1109                    continue;
1110                }
1111
1112                for (OWLIndividual ind : inds) {
1113                    // stop inner loop when nr of fillers is reached
1114                    if (nrOfFillers >= number) {
1115                        break;
1116                    }
1117                    // early abort when too many instance checks failed, i.e. there are not enough remaining candidates
1118                    if (inds.size() - index < number - nrOfFillers) {
1119                        break;
1120                    }
1121
1122                    if (targetSet.contains(ind)) {
1123                        nrOfFillers++;
1124                    }
1125                    index++;
1126                }
1127
1128                if(nrOfFillers >= number) {
1129                    returnSet.add(entry.getKey());
1130                }
1131            }
1132            return returnSet;
1133        } else if (description instanceof OWLObjectMaxCardinality) { // <=n r.C
1134            OWLObjectPropertyExpression property = ((OWLObjectMaxCardinality) description).getProperty();
1135            OWLClassExpression filler = ((OWLObjectMaxCardinality) description).getFiller();
1136            int number = ((OWLObjectMaxCardinality) description).getCardinality();
1137
1138            // get instances of filler concept
1139            SortedSet<OWLIndividual> targetSet = getIndividualsImpl(filler);
1140
1141            // the mapping of instances related by r
1142            Map<OWLIndividual, ? extends Collection<OWLIndividual>> mapping = getTargetIndividuals(property);
1143
1144                        // initially all individuals are in the return set and we then remove those
1145            // with too many fillers
1146            SortedSet<OWLIndividual> returnSet = (SortedSet<OWLIndividual>) individuals.clone();
1147
1148            for (Entry<OWLIndividual, ? extends Collection<OWLIndividual>> entry : mapping.entrySet()) {
1149                int nrOfFillers = 0;
1150                int index = 0;
1151                Collection<OWLIndividual> fillers = entry.getValue();
1152
1153                // we do not need to run tests if there are not sufficiently many fillers
1154                if (fillers.size() <= number) {
1155                    continue;
1156                }
1157
1158                for (OWLIndividual ind : fillers) {
1159                    // stop inner loop when there are more fillers than allowed
1160                    if (nrOfFillers > number) {
1161                        returnSet.remove(entry.getKey());
1162                        break;
1163                    }
1164                    // early termination when there are not enough remaining candidates that could belong to C
1165                    if (fillers.size() - index + nrOfFillers <= number) {
1166                        break;
1167                    }
1168                    if (targetSet.contains(ind)) {
1169                        nrOfFillers++;
1170                    }
1171                    index++;
1172                }
1173            }
1174
1175            return returnSet;
1176        } else if (description instanceof OWLObjectExactCardinality) {
1177            OWLObjectPropertyExpression property = ((OWLObjectExactCardinality) description).getProperty();
1178            OWLClassExpression filler = ((OWLObjectExactCardinality) description).getFiller();
1179
1180            // get instances of filler concept
1181            SortedSet<OWLIndividual> targetSet = getIndividualsImpl(filler);
1182
1183            // the mapping of instances related by r
1184            Map<OWLIndividual, ? extends Collection<OWLIndividual>> mapping = getTargetIndividuals(property);
1185
1186            SortedSet<OWLIndividual> returnSet = new TreeSet<>();
1187
1188            int number = ((OWLObjectExactCardinality) description).getCardinality();
1189
1190            for (Entry<OWLIndividual, ? extends Collection<OWLIndividual>> entry : mapping.entrySet()) {
1191                Collection<OWLIndividual> inds = entry.getValue();
1192
1193                // we do not need to run tests if there are not sufficiently many fillers
1194                if (inds.size() < number) {
1195                    continue;
1196                }
1197
1198                // check for all fillers that belong to target set
1199                int matchCnt = Sets.intersection((Set)inds, targetSet).size();
1200
1201                if(matchCnt == number) {
1202                    returnSet.add(entry.getKey());
1203                }
1204
1205            }
1206
1207            return returnSet;
1208        } else if (description instanceof OWLObjectHasValue) {
1209            OWLObjectPropertyExpression property = ((OWLObjectHasValue) description).getProperty();
1210            OWLIndividual value = ((OWLObjectHasValue) description).getFiller();
1211
1212            // the mapping of instances related by r
1213            Map<OWLIndividual, ? extends Collection<OWLIndividual>> mapping =
1214                    property.isAnonymous() ? // \exists r^{-1}.{a} -> invert the mapping, i.e. get all objects that
1215                            // are related by r to (at least) one subject which is of type C
1216                            Multimaps.invertFrom(
1217                                    MapUtils.createSortedMultiMap(opPos.get(property.getNamedProperty())),
1218                                    TreeMultimap.create()).asMap() :
1219                            opPos.get(property.getNamedProperty());
1220
1221            return mapping.entrySet().stream()
1222                    .filter(e -> e.getValue().contains(value))
1223                    .map(Entry::getKey)
1224                    .collect(Collectors.toCollection(TreeSet::new));
1225        } else if (description instanceof OWLDataSomeValuesFrom) {
1226            OWLDataPropertyExpression property = ((OWLDataSomeValuesFrom) description).getProperty();
1227            OWLDataRange filler = ((OWLDataSomeValuesFrom) description).getFiller();
1228
1229            if (filler.isDatatype()) {
1230                // we assume that the values are of the given datatype
1231                return new TreeSet<>(dpPos.get(property).keySet());
1232            } else if (filler instanceof OWLDataIntersectionOf) {
1233                return ((OWLDataIntersectionOf) filler).getOperands().stream()
1234                        .map(dr -> getIndividuals(df.getOWLDataSomeValuesFrom(property, dr)))
1235                        .reduce((s1, s2) -> {
1236                            s1.retainAll(s2);
1237                            return s1;
1238                        })
1239                        .orElse(new TreeSet<>());
1240            } else if (filler instanceof OWLDataUnionOf) {
1241                return ((OWLDataUnionOf) filler).getOperands().stream()
1242                        .map(dr -> getIndividuals(df.getOWLDataSomeValuesFrom(property, dr)))
1243                        .reduce((s1, s2) -> {
1244                            s1.addAll(s2);
1245                            return s1;
1246                        })
1247                        .orElse(new TreeSet<>());
1248            } else if (filler instanceof OWLDataComplementOf) {
1249                return new TreeSet<>(Sets.difference(
1250                        individuals,
1251                        getIndividualsImpl(df.getOWLDataSomeValuesFrom(
1252                                property,
1253                                ((OWLDataComplementOf) filler).getDataRange()))));
1254            } else if (filler instanceof OWLDatatypeRestriction) {
1255                OWLDatatype datatype = ((OWLDatatypeRestriction) filler).getDatatype();
1256                Set<OWLFacetRestriction> facetRestrictions = ((OWLDatatypeRestriction) filler).getFacetRestrictions();
1257
1258                if (OWLAPIUtils.floatDatatypes.contains(datatype)) {
1259                    double min = facetRestrictions.stream()
1260                            .filter(fr -> fr.getFacet() == OWLFacet.MIN_INCLUSIVE)
1261                            .map(fr -> fr.getFacetValue().isDouble() ? fr.getFacetValue().parseDouble() : (double) fr.getFacetValue().parseFloat())
1262                            .findAny().orElse(-Double.MAX_VALUE);
1263                    double max = facetRestrictions.stream()
1264                            .filter(fr -> fr.getFacet() == OWLFacet.MAX_INCLUSIVE)
1265                            .map(fr -> fr.getFacetValue().isDouble() ? fr.getFacetValue().parseDouble() : (double) fr.getFacetValue().parseFloat())
1266                            .findAny().orElse(Double.MAX_VALUE);
1267
1268                    return dd.getOrDefault(property, new HashMap<>()).entrySet().stream()
1269                            .filter(e -> {
1270                                SortedSet<Double> values = e.getValue();
1271
1272                                // we can skip if largest number is below minimum or lowest number is above maximum
1273                                if (values.last() < min || values.first() > max) {
1274                                    return false;
1275                                }
1276
1277                                // search a value which is in the interval
1278                                return values.stream().anyMatch(val -> val >= min && val <= max);
1279                            })
1280                            .map(Entry::getKey)
1281                            .collect(Collectors.toCollection(TreeSet::new));
1282//
1283                } else if (OWLAPIUtils.intDatatypes.contains(datatype)) {
1284                    int min = facetRestrictions.stream()
1285                            .filter(fr -> fr.getFacet() == OWLFacet.MIN_INCLUSIVE)
1286                            .map(fr -> fr.getFacetValue().parseInteger())
1287                            .findAny().orElse(-Integer.MAX_VALUE);
1288                    int max = facetRestrictions.stream()
1289                            .filter(fr -> fr.getFacet() == OWLFacet.MAX_INCLUSIVE)
1290                            .map(fr -> fr.getFacetValue().parseInteger())
1291                            .findAny().orElse(Integer.MAX_VALUE);
1292
1293                    return id.getOrDefault(property, new HashMap<>()).entrySet().stream()
1294                            .filter(e -> {
1295                                SortedSet<Integer> values = e.getValue();
1296
1297                                // we can skip if largest number is below minimum or lowest number is above maximum
1298                                if (values.last() < min || values.first() > max) {
1299                                    return false;
1300                                }
1301
1302                                // search a value which is in the interval
1303                                return values.stream().anyMatch(val -> val >= min && val <= max);
1304                            })
1305                            .map(Entry::getKey)
1306                            .collect(Collectors.toCollection(TreeSet::new));
1307                } else if (OWLAPIUtils.dtDatatypes.contains(datatype)) {
1308                    OWLLiteral min = facetRestrictions.stream()
1309                            .filter(fr -> fr.getFacet() == OWLFacet.MIN_INCLUSIVE)
1310                            .map(OWLFacetRestriction::getFacetValue)
1311                            .findAny().orElse(null);
1312                    OWLLiteral max = facetRestrictions.stream()
1313                            .filter(fr -> fr.getFacet() == OWLFacet.MAX_INCLUSIVE)
1314                            .map(OWLFacetRestriction::getFacetValue)
1315                            .findAny().orElse(null);
1316
1317                    return dpPos.getOrDefault(property, new HashMap<>()).entrySet().stream()
1318                            .filter(e -> e.getValue().stream().anyMatch(val -> OWLAPIUtils.inRange(val, min, max)))
1319                            .map(Entry::getKey)
1320                            .collect(Collectors.toCollection(TreeSet::new));
1321                }
1322            } else if (filler.getDataRangeType() == DataRangeType.DATA_ONE_OF) {
1323                OWLDataOneOf dataOneOf = (OWLDataOneOf) filler;
1324                Set<OWLLiteral> values = dataOneOf.getValues();
1325
1326                return dpPos.getOrDefault(property, new HashMap<>()).entrySet().stream()
1327                        .filter(e -> !Sets.intersection(e.getValue(), values).isEmpty())
1328                        .map(Entry::getKey)
1329                        .collect(Collectors.toCollection(TreeSet::new));
1330            }
1331        } else if (description instanceof OWLDataHasValue) {
1332            OWLDataPropertyExpression property = ((OWLDataHasValue) description).getProperty();
1333            OWLLiteral value = ((OWLDataHasValue) description).getFiller();
1334
1335            return dpPos.getOrDefault(property, new HashMap<>()).entrySet().stream()
1336                    .filter(e -> e.getValue().contains(value))
1337                    .map(Entry::getKey)
1338                    .collect(Collectors.toCollection(TreeSet::new));
1339        } else if (description instanceof OWLObjectOneOf) {
1340            return new TreeSet(((OWLObjectOneOf) description).getIndividuals());
1341        }
1342
1343        throw new ReasoningMethodUnsupportedException("Retrieval for class expression "
1344                + description + " unsupported.");
1345
1346    }
1347
1348    // get all objects that are related by r to (at least) one subject which is of type C
1349    // or if r^{-1} invert the mapping
1350    private Map<OWLIndividual, ? extends Collection<OWLIndividual>> getTargetIndividuals(OWLObjectPropertyExpression ope) {
1351        return ope.isAnonymous()
1352                ? Multimaps.invertFrom(
1353                        MapUtils.createSortedMultiMap(opPos.get(ope.getNamedProperty())),
1354                        TreeMultimap.create()).asMap()
1355                : opPos.get(ope.getNamedProperty());
1356    }
1357
1358    /*
1359     * (non-Javadoc)
1360     * 
1361     * @see org.dllearner.core.Reasoner#getAtomicConcepts()
1362     */
1363    @Override
1364    public Set<OWLClass> getClasses() {
1365        return baseReasoner.getClasses();
1366    }
1367
1368    /*
1369     * (non-Javadoc)
1370     * 
1371     * @see org.dllearner.core.Reasoner#getAtomicRoles()
1372     */
1373    @Override
1374    public Set<OWLObjectProperty> getObjectPropertiesImpl() {return objectProperties;
1375//        return baseReasoner.getObjectProperties();
1376    }
1377
1378    @Override
1379    public Set<OWLDataProperty> getDatatypePropertiesImpl() {
1380        return baseReasoner.getDatatypeProperties();
1381    }
1382
1383    @Override
1384    public Set<OWLDataProperty> getBooleanDatatypePropertiesImpl() {
1385        return baseReasoner.getBooleanDatatypeProperties();
1386    }
1387
1388    @Override
1389    public Set<OWLDataProperty> getDoubleDatatypePropertiesImpl() {
1390        return baseReasoner.getDoubleDatatypeProperties();
1391    }
1392
1393    @Override
1394    public Set<OWLDataProperty> getIntDatatypePropertiesImpl() {
1395        return baseReasoner.getIntDatatypeProperties();
1396    }
1397
1398    @Override
1399    public Set<OWLDataProperty> getStringDatatypePropertiesImpl() {
1400        return baseReasoner.getStringDatatypeProperties();
1401    }
1402
1403    @Override
1404    protected SortedSet<OWLClassExpression> getSuperClassesImpl(OWLClassExpression concept) {
1405        return baseReasoner.getSuperClassesImpl(concept);
1406    }
1407
1408    @Override
1409    protected SortedSet<OWLClassExpression> getSubClassesImpl(OWLClassExpression concept) {
1410        return baseReasoner.getSubClassesImpl(concept);
1411    }
1412
1413    @Override
1414    protected SortedSet<OWLObjectProperty> getSuperPropertiesImpl(OWLObjectProperty role) {
1415        return baseReasoner.getSuperPropertiesImpl(role);
1416    }
1417
1418    @Override
1419    protected SortedSet<OWLObjectProperty> getSubPropertiesImpl(OWLObjectProperty role) {
1420        return baseReasoner.getSubPropertiesImpl(role);
1421    }
1422
1423    @Override
1424    protected SortedSet<OWLDataProperty> getSuperPropertiesImpl(OWLDataProperty role) {
1425        return baseReasoner.getSuperPropertiesImpl(role);
1426    }
1427
1428    @Override
1429    protected SortedSet<OWLDataProperty> getSubPropertiesImpl(OWLDataProperty role) {
1430        return baseReasoner.getSubPropertiesImpl(role);
1431    }
1432
1433    /*
1434     * (non-Javadoc)
1435     * 
1436     * @see org.dllearner.core.Reasoner#getIndividuals()
1437     */
1438    @Override
1439    public SortedSet<OWLIndividual> getIndividuals() {
1440        return individuals;
1441    }
1442
1443    /*
1444     * (non-Javadoc)
1445     * 
1446     * @see org.dllearner.core.Reasoner#getReasonerType()
1447     */
1448    @Override
1449    public ReasonerType getReasonerType() {
1450        return ReasonerType.CLOSED_WORLD_REASONER;
1451    }
1452
1453    @Override
1454    public boolean isSuperClassOfImpl(OWLClassExpression superConcept, OWLClassExpression subConcept) {
1455                // Negation neg = new Negation(subConcept);
1456        // Intersection c = new Intersection(neg,superConcept);
1457        // return fastRetrieval.calculateSets(c).getPosSet().isEmpty();
1458        return baseReasoner.isSuperClassOfImpl(superConcept, subConcept);
1459    }
1460
1461    /* (non-Javadoc)
1462     * @see org.dllearner.core.Reasoner#isDisjoint(OWLClass class1, OWLClass class2)
1463     */
1464    @Override
1465    public boolean isDisjointImpl(OWLClass clsA, OWLClass clsB) {
1466        if (disjointnessSemantics == DisjointnessSemantics.INSTANCE_BASED) {
1467            TreeSet<OWLIndividual> instancesA = classInstancesPos.get(clsA);
1468            TreeSet<OWLIndividual> instancesB = classInstancesPos.get(clsB);
1469
1470            // trivial case if one of the sets is empty
1471            if (instancesA.isEmpty() || instancesB.isEmpty()) {
1472                return false;
1473            }
1474
1475            return Sets.intersection(instancesA, instancesB).isEmpty();
1476        } else {
1477            return baseReasoner.isDisjoint(clsA, clsB);
1478        }
1479    }
1480
1481    /*
1482     * (non-Javadoc)
1483     * 
1484     * @see org.dllearner.core.Reasoner#getBaseURI()
1485     */
1486    @Override
1487    public String getBaseURI() {
1488        return baseReasoner.getBaseURI();
1489    }
1490
1491    /*
1492     * (non-Javadoc)
1493     * 
1494     * @see org.dllearner.core.Reasoner#getPrefixes()
1495     */
1496    @Override
1497    public Map<String, String> getPrefixes() {
1498        return baseReasoner.getPrefixes();
1499    }
1500
1501    public void setPrefixes(Map<String, String> prefixes) {
1502        baseReasoner.setPrefixes(prefixes);
1503    }
1504
1505    /**
1506     * @param baseURI the baseURI to set
1507     */
1508    public void setBaseURI(String baseURI) {
1509        baseReasoner.setBaseURI(baseURI);
1510    }
1511
1512    @Override
1513    public OWLClassExpression getDomainImpl(OWLObjectProperty objectProperty) {
1514        return baseReasoner.getDomain(objectProperty);
1515    }
1516
1517    @Override
1518    public OWLClassExpression getDomainImpl(OWLDataProperty datatypeProperty) {
1519        return baseReasoner.getDomain(datatypeProperty);
1520    }
1521
1522    @Override
1523    public OWLClassExpression getRangeImpl(OWLObjectProperty objectProperty) {
1524        return baseReasoner.getRange(objectProperty);
1525    }
1526
1527    @Override
1528    public OWLDataRange getRangeImpl(OWLDataProperty datatypeProperty) {
1529        return baseReasoner.getRange(datatypeProperty);
1530    }
1531
1532    @Override
1533    public Map<OWLIndividual, SortedSet<OWLIndividual>> getPropertyMembersImpl(OWLObjectProperty atomicRole) {
1534        return opPos.get(atomicRole);
1535    }
1536
1537    @Override
1538    public final SortedSet<OWLIndividual> getTrueDatatypeMembersImpl(OWLDataProperty datatypeProperty) {
1539        return bdPos.get(datatypeProperty);
1540    }
1541
1542    @Override
1543    public final SortedSet<OWLIndividual> getFalseDatatypeMembersImpl(OWLDataProperty datatypeProperty) {
1544        return bdNeg.get(datatypeProperty);
1545    }
1546
1547    @Override
1548    public Map<OWLIndividual, SortedSet<Integer>> getIntDatatypeMembersImpl(OWLDataProperty datatypeProperty) {
1549        return id.get(datatypeProperty);
1550    }
1551
1552    @Override
1553    public Map<OWLIndividual, SortedSet<Double>> getDoubleDatatypeMembersImpl(OWLDataProperty datatypeProperty) {
1554        return dd.get(datatypeProperty);
1555    }
1556
1557    @Override
1558    protected Map<OWLDataProperty, Set<OWLLiteral>> getDataPropertyRelationshipsImpl(OWLIndividual individual) {
1559        return baseReasoner.getDataPropertyRelationships(individual);
1560    }
1561
1562    @Override
1563    public Map<OWLIndividual, SortedSet<OWLLiteral>> getDatatypeMembersImpl(OWLDataProperty datatypeProperty) {
1564        return dpPos.get(datatypeProperty);
1565//              return rc.getDatatypeMembersImpl(OWLDataProperty);
1566    }
1567
1568    @Override
1569    public Set<OWLIndividual> getRelatedIndividualsImpl(OWLIndividual individual, OWLObjectProperty objectProperty) {
1570        return baseReasoner.getRelatedIndividuals(individual, objectProperty);
1571    }
1572
1573    @Override
1574    protected Map<OWLObjectProperty, Set<OWLIndividual>> getObjectPropertyRelationshipsImpl(OWLIndividual individual) {
1575        return baseReasoner.getObjectPropertyRelationships(individual);
1576    }
1577
1578    @Override
1579    public Set<OWLLiteral> getRelatedValuesImpl(OWLIndividual individual, OWLDataProperty datatypeProperty) {
1580        return baseReasoner.getRelatedValues(individual, datatypeProperty);
1581    }
1582
1583    @Override
1584    public boolean isSatisfiableImpl() {
1585        return baseReasoner.isSatisfiable();
1586    }
1587
1588    @Override
1589    public Set<OWLLiteral> getLabelImpl(OWLEntity entity) {
1590        return baseReasoner.getLabel(entity);
1591    }
1592
1593    /*
1594     * (non-Javadoc)
1595     * 
1596     * @see org.dllearner.core.ReasonerComponent#releaseKB()
1597     */
1598    @Override
1599    public void releaseKB() {
1600        baseReasoner.releaseKB();
1601    }
1602
1603//      @Override
1604//      public boolean hasDatatypeSupport() {
1605//              return true;
1606//      }
1607
1608    /* (non-Javadoc)
1609     * @see org.dllearner.core.ReasonerComponent#getTypesImpl(org.dllearner.core.owl.Individual)
1610     */
1611    @Override
1612    protected Set<OWLClass> getTypesImpl(OWLIndividual individual) {
1613        return baseReasoner.getTypesImpl(individual);
1614    }
1615
1616    /* (non-Javadoc)
1617     * @see org.dllearner.core.BaseReasoner#remainsSatisfiable(org.dllearner.core.owl.Axiom)
1618     */
1619    @Override
1620    public boolean remainsSatisfiableImpl(OWLAxiom axiom) {
1621        return baseReasoner.remainsSatisfiableImpl(axiom);
1622    }
1623
1624    @Override
1625    protected Set<OWLClassExpression> getAssertedDefinitionsImpl(OWLClass nc) {
1626        return baseReasoner.getAssertedDefinitionsImpl(nc);
1627    }
1628
1629    /* (non-Javadoc)
1630     * @see org.dllearner.core.AbstractReasonerComponent#getInconsistentClassesImpl()
1631     */
1632    @Override
1633    protected Set<OWLClass> getInconsistentClassesImpl() {
1634        return baseReasoner.getInconsistentClasses();
1635    }
1636
1637    public OWLAPIReasoner getReasonerComponent() {
1638        return baseReasoner;
1639    }
1640
1641    @Autowired(required = false)
1642    public void setReasonerComponent(OWLAPIReasoner rc) {
1643        this.baseReasoner = rc;
1644    }
1645
1646    public boolean isDefaultNegation() {
1647        return defaultNegation;
1648    }
1649
1650    public void setDefaultNegation(boolean defaultNegation) {
1651        this.defaultNegation = defaultNegation;
1652    }
1653
1654    public ForallSemantics getForAllSemantics() {
1655        return forAllSemantics;
1656    }
1657
1658    public void setForAllSemantics(ForallSemantics forAllSemantics) {
1659        this.forAllSemantics = forAllSemantics;
1660    }
1661
1662    /**
1663     * @param useMaterializationCaching the useMaterializationCaching to set
1664     */
1665    public void setUseMaterializationCaching(boolean useMaterializationCaching) {
1666        this.useMaterializationCaching = useMaterializationCaching;
1667    }
1668
1669    /**
1670     * @param handlePunning the handlePunning to set
1671     */
1672    public void setHandlePunning(boolean handlePunning) {
1673        this.handlePunning = handlePunning;
1674    }
1675
1676    /**
1677     * @param materializeExistentialRestrictions the
1678     * materializeExistentialRestrictions to set
1679     */
1680    public void setMaterializeExistentialRestrictions(boolean materializeExistentialRestrictions) {
1681        this.materializeExistentialRestrictions = materializeExistentialRestrictions;
1682    }
1683
1684    /* (non-Javadoc)
1685     * @see org.dllearner.core.AbstractReasonerComponent#getDatatype(org.semanticweb.owlapi.model.OWLDataProperty)
1686     */
1687    @Override
1688    @NoConfigOption
1689    public OWLDatatype getDatatype(OWLDataProperty dp) {
1690        return baseReasoner.getDatatype(dp);
1691    }
1692
1693    /* (non-Javadoc)
1694     * @see org.dllearner.core.AbstractReasonerComponent#setSynchronized()
1695     */
1696    @Override
1697    @NoConfigOption
1698    public void setSynchronized() {
1699        baseReasoner.setSynchronized();
1700    }
1701
1702    public static void main(String[] args) throws Exception{
1703
1704        StringRenderer.setRenderer(StringRenderer.Rendering.DL_SYNTAX);
1705
1706        OWLOntologyManager man = OWLManager.createOWLOntologyManager();
1707        OWLOntology ontology = man.createOntology();
1708        OWLDataFactory df = new OWLDataFactoryImpl();
1709        PrefixManager pm = new DefaultPrefixManager();
1710        pm.setDefaultPrefix("http://test.org/");
1711
1712        OWLDataProperty dp = df.getOWLDataProperty("dp", pm);
1713        OWLObjectProperty op = df.getOWLObjectProperty("p", pm);
1714        OWLClass clsA = df.getOWLClass("A", pm);
1715        OWLClass cls1 = df.getOWLClass("C", pm);
1716        OWLClass cls2 = df.getOWLClass("C2", pm);
1717//        man.addAxiom(ontology,
1718//                df.getOWLDataPropertyAssertionAxiom(
1719//                        dp,
1720//                        df.getOWLNamedIndividual("a", pm),
1721//                        df.getOWLLiteral(2.0d)));
1722//        man.addAxiom(ontology,
1723//                df.getOWLDataPropertyAssertionAxiom(
1724//                        dp,
1725//                        df.getOWLNamedIndividual("b", pm),
1726//                        df.getOWLLiteral(1.3d)));
1727//        man.addAxiom(ontology, df.getOWLDataPropertyRangeAxiom(dp, df.getDoubleOWLDatatype()));
1728        man.addAxiom(ontology, df.getOWLClassAssertionAxiom(clsA, df.getOWLNamedIndividual("s", pm)));
1729        IntStream.range(0, 5).forEach( i -> {
1730            man.addAxiom(ontology, df.getOWLObjectPropertyAssertionAxiom(op,
1731                    df.getOWLNamedIndividual("s", pm),
1732                    df.getOWLNamedIndividual("o" + i, pm)));
1733        });
1734        IntStream.range(0, 5).forEach( i -> {
1735            man.addAxiom(ontology, df.getOWLClassAssertionAxiom(cls1, df.getOWLNamedIndividual("o" + i, pm)));
1736        });
1737//        IntStream.range(5, 20).forEach( i -> {
1738//            man.addAxiom(ontology, df.getOWLObjectPropertyAssertionAxiom(op,
1739//                    df.getOWLNamedIndividual("s", pm),
1740//                    df.getOWLNamedIndividual("o" + i, pm)));
1741//            man.addAxiom(ontology, df.getOWLClassAssertionAxiom(cls2, df.getOWLNamedIndividual("o" + i, pm)));
1742//        });
1743
1744        ontology.getLogicalAxioms().forEach(System.out::println);
1745//        ontology.saveOntology(new TurtleDocumentFormat(), System.out);
1746
1747        OWLAPIOntology ks = new OWLAPIOntology(ontology);
1748        ks.init();
1749
1750        ClosedWorldReasoner reasoner = new ClosedWorldReasoner(ks);
1751        reasoner.init();
1752
1753
1754        OWLClassExpression ce;
1755
1756        SortedSet<OWLIndividual> individuals = reasoner.getIndividuals(
1757                df.getOWLDataSomeValuesFrom(
1758                        dp,
1759                        df.getOWLDatatypeMinMaxInclusiveRestriction(1.0d, 2.0d)));
1760        System.out.println(individuals);
1761
1762        individuals = reasoner.getIndividuals(
1763                df.getOWLDataSomeValuesFrom(
1764                        dp,
1765                        df.getOWLDatatypeMinMaxInclusiveRestriction(1.0d, 1.9d)));
1766        System.out.println(individuals);
1767
1768        individuals = reasoner.getIndividuals(
1769                df.getOWLDataSomeValuesFrom(
1770                        dp,
1771                        df.getOWLDataUnionOf(
1772                                df.getOWLDatatypeMinMaxInclusiveRestriction(1.0d, 1.5d),
1773                                df.getOWLDatatypeMinMaxInclusiveRestriction(2.0d, 2.5d))
1774                        ));
1775        System.out.println(individuals);
1776
1777        individuals = reasoner.getIndividuals(
1778                df.getOWLDataSomeValuesFrom(
1779                        dp,
1780                        df.getOWLDataComplementOf(
1781                                df.getOWLDatatypeMinMaxInclusiveRestriction(1.0d, 1.5d))
1782                ));
1783//        System.out.println(individuals);
1784
1785        System.out.println(df.getOWLObjectIntersectionOf(clsA,
1786                df.getOWLObjectMaxCardinality(2, op, cls1)));
1787        individuals = reasoner.getIndividuals(
1788                df.getOWLObjectIntersectionOf(clsA,
1789                        df.getOWLObjectMaxCardinality(2, op, cls1))
1790        );
1791        System.out.println(individuals);
1792
1793        individuals = reasoner.getIndividuals(
1794                df.getOWLObjectMaxCardinality(10, op, cls1)
1795        );
1796        System.out.println(individuals);
1797
1798        individuals = reasoner.getIndividuals(
1799                df.getOWLObjectMaxCardinality(8, op, cls1)
1800        );
1801        System.out.println(individuals);
1802
1803        individuals = reasoner.getIndividuals(
1804                df.getOWLObjectMaxCardinality(3, op, cls1)
1805        );
1806        System.out.println(individuals);
1807
1808        ce = df.getOWLObjectExactCardinality(5, op, cls1);
1809        individuals = reasoner.getIndividuals(ce);
1810        System.out.println(ce + ": " + individuals);
1811
1812        System.out.println(reasoner.hasType(ce, df.getOWLNamedIndividual("s", pm)));
1813        System.out.println(reasoner.hasType(ce, df.getOWLNamedIndividual("o1", pm)));
1814
1815    }
1816
1817}