//
//  Created by Ivano Bilenchi on 07/02/18.
//  Copyright © 2018-2020 SisInf Lab. All rights reserved.
//

#import <Foundation/Foundation.h>
#import "TMEIndividualType.h"

@class TMEAbduction;
@class TMEBonus;
@class TMEComposition;
@class TMEContraction;
@class TMEDataFactory;
@class TMESemanticDescription;
@class OWLIRI;
@protocol OWLOntology;

NS_ASSUME_NONNULL_BEGIN

/**
 * The main reasoner class, exposing standard and non-standard inference tasks.
 *
 * Non-standard matchmaking services are detailed in "Ruta et al., WIAS 2011":
 * http://sisinflab.poliba.it/publications/2011/RDS11
 *
 * For more information about the project, visit Tiny-ME's website:
 * http://swot.sisinflab.poliba.it/tinyme
 *
 * @see OWL API for iOS: https://github.com/sisinflab-swot/OWL-API-for-iOS
 */ 
@interface TMEReasoner : NSObject

#pragma mark - Properties

/// The root ontology.
@property (nonatomic, strong, readonly) id<OWLOntology> ontology;

/// Data factory instance.
@property (nonatomic, strong, readonly) TMEDataFactory *factory;

#pragma mark - Lifecycle

/**
 * Initializes a new reasoner instance.
 *
 * @param ontology Ontology to load into the reasoner.
 * @return Initialized reasoner instance.
 */
- (instancetype)initWithOntology:(id<OWLOntology>)ontology;

#pragma mark - Loading

/**
 * Loads the specified individual into the reasoner as either a resource or a request.
 *
 * @param iri IRI of the individual to load.
 * @param description Semantic description of the individual to load.
 * @param type Type of the individual to load (resource, request or both).
 */
- (void)loadIndividualWithIri:(OWLIRI *)iri
                  description:(TMESemanticDescription *)description
                         type:(TMEIndividualType)type;

/**
 * Loads the individuals present in the signature of the specified ontology.
 *
 * @param ontology Ontology containing the individuals to load.
 * @param type Type of the loaded individuals (resource, request or both).
 */
- (void)loadIndividualsFromOntology:(id<OWLOntology>)ontology
                               type:(TMEIndividualType)type;

/**
 * Tells the reasoner that the individual is of the specified type.
 *
 * @param iri IRI of the individual whose type should be updated.
 * @param type Type of the individual (resource, request or both).
 */
- (void)tellIndividualWithIri:(OWLIRI *)iri isOfType:(TMEIndividualType)type;

/**
 * Unloads the specified individual.
 *
 * @param iri IRI of the individual to unload.
 */
- (void)unloadIndividualWithIri:(OWLIRI *)iri;

/**
 * Unloads the individuals present in the signature of the specified ontology.
 *
 * @param ontology Ontology containing the individuals to unload.
 */
- (void)unloadIndividualsFromOntology:(id<OWLOntology>)ontology;

/**
 * Unloads all the individuals of a given type.
 *
 * @param type Type of the individuals to unload (resource, request or both).
 */
- (void)unloadIndividualsOfType:(TMEIndividualType)type;

#pragma mark - Querying

/// @return The TBox.
- (NSDictionary<OWLIRI *, TMESemanticDescription *> *)tBox;

/// @return The ABox.
- (NSDictionary<OWLIRI *, TMESemanticDescription *> *)aBox;

/**
 * Retrieves all the individuals of a specified type.
 *
 * @param type Type of individuals to retrieve (resource, request or both).
 * @return Individuals of the specified type.
 */
- (NSDictionary<OWLIRI *, TMESemanticDescription *> *)individualsOfType:(TMEIndividualType)type;

/**
 * Returns the semantic description of the specified class.
 *
 * @param iri IRI of the class whose description should be retrieved.
 * @return Semantic description of the specified class.
 */
- (TMESemanticDescription *)descriptionForClassWithIri:(OWLIRI *)iri;

/**
 * Returns the semantic description of the specified individual.
 *
 * @param iri IRI of the individual whose description should be retrieved.
 * @return Semantic description of the specified individual.
 */
- (TMESemanticDescription *)descriptionForIndividualWithIri:(OWLIRI *)iri;

#pragma mark - Reasoning

/// Computes the taxonomy of classes present in the root ontology.
- (void)classify;

/// @return True if the ontology has been classified, false otherwise.
- (BOOL)isClassified;

/**
 * Checks the coherence of the root ontology.
 *
 * @return True if the ontology is coherent, false otherwise.
 *
 * @see Moguillansky et al., IBERAMIA 2010
        ( https://cs.uns.edu.ar/~mom/publications/iberamia2010.pdf )
 */
- (BOOL)isCoherent;

/**
 * Performs the unfolding and CNF normalization of the specified semantic description.
 *
 * @param description Semantic description to normalize.
 */
- (void)normalizeDescription:(TMESemanticDescription *)description;

/**
 * Checks whether the specified class is satisfiable.
 *
 * @param iri IRI of the class.
 * @return True if the class is satisfiable, false otherwise.
 */
- (BOOL)classWithIriIsSatisfiable:(OWLIRI *)iri;

/**
 * Checks whether a subclass relation holds between two classes.
 *
 * @param subClassIri IRI of the subclass.
 * @param superClassIri IRI of the superclass.
 * @return True if the relation holds, false otherwise.
 */
- (BOOL)classWithIri:(OWLIRI *)subClassIri isSubClassOf:(OWLIRI *)superClassIri;

/**
 * Retrieves the direct subclasses of the specified class.
 *
 * @param classIri IRI of the class whose subclasses should be retrieved.
 * @param direct True: returns the direct subclasses; false: returns the recursive subclasses.
 * @return Subclasses.
 */
- (NSArray<OWLIRI *> *)subClassesOfClassWithIri:(OWLIRI *)classIri direct:(BOOL)direct;

/**
 * Retrieves the direct superclasses of the specified class.
 *
 * @param classIri IRI of the class whose superclasses should be retrieved.
 * @param direct True: returns the direct superclasses; false: returns the recursive superclasses.
 * @return Superclasses.
 */
- (NSArray<OWLIRI *> *)superClassesOfClassWithIri:(OWLIRI *)classIri direct:(BOOL)direct;

/**
 * Retrieves the equivalent classes of the specified class.
 *
 * @param classIri IRI of the class whose equivalents should be retrieved.
 * @return Equivalent classes.
 */
- (NSArray<OWLIRI *> *)equivalentClassesOfClassWithIri:(OWLIRI *)classIri;

/**
 * Retrieves the classes that are disjoint with the specified class.
 *
 * @param classIri IRI of the class whose equivalents should be retrieved.
 * @return Disjoint classes.
 *
 * @note This is currently incomplete as it does not account for inferred disjoints.
 */
- (NSArray<OWLIRI *> *)disjointClassesOfClassWithIri:(OWLIRI *)classIri;

/// @return All the unsatisfiable classes.
- (NSArray<OWLIRI *> *)unsatisfiableClasses;

/**
 * Checks whether the given individual is consistent.
 *
 * @param iri IRI of the individual whose consistency should be checked.
 * @return True if the individual is consistent, false otherwise.
 */
- (BOOL)individualWithIriIsConsistent:(OWLIRI *)iri;

/**
 * Determines if a subsumption relation holds between two semantic profiles (that is, if one is
 * more general than the other), in which case they are referred to as subsumer and subsumed.
 * The profiles are OWL individuals previously loaded into the reasoner using the 'load' methods.
 *
 * If the subsumption relation holds, two conclusions can be drawn:
 * 1) The subsumer is more general than the subsumed, hence the former
 * (usually a requested semantic profile) is satisfied by the latter (usually a supplied resource)
 * in every aspect.
 * 2) The two elements involved in the relation are compatible.
 *
 * If the relation does not hold, abduction may be used to compute what should be hypothesized
 * in the subsumed individual in order to completely satisfy the subsumer individual.
 *
 * @param subsumed Subsumed element in the subsumption relation.
 * @param subsumer Subsumer element in the subsumption relation.
 * @return True if the subsumption relation holds, false otherwise.
 */
- (BOOL)individualWithIri:(OWLIRI *)subsumed isSubsumedBy:(OWLIRI *)subsumer;

/**
 * Checks whether the specified individual is an instance of a certain class.
 *
 * @param individualIri IRI of the individual.
 * @param classIri IRI of the class.
 * @return True if the individual is an instance of the class, false otherwise.
 *
 * @note This is currently incomplete, since the reasoner does not process the ABox.
 */
- (BOOL)individualWithIri:(OWLIRI *)individualIri isInstanceOf:(OWLIRI *)classIri;

/**
 * Determines if a supplied resource and a requested semantic profile are compatible
 * (that is, whether the semantic description of the resource does not contain
 * any information in conflict with the request). Resource and request are OWL individuals
 * previously loaded into the reasoner using the 'load' methods.
 *
 * If the compatibility relation between the two individuals holds, then they don't contain
 * any conflicting part. If the relation does not hold, contraction may be used
 * to compute the conflicting part.
 *
 * @param resourceIri IRI of the resource against which the request is checked for compatibility.
 * @param requestIri IRI of the request against which the resource is checked for compatibility.
 * @return True if the compatibility relation holds, false otherwise.
 */
- (BOOL)compatibilityBetweenResource:(OWLIRI *)resourceIri
                          andRequest:(OWLIRI *)requestIri;

/**
 * Performs the Concept Abduction non-standard matchmaking task,
 * comparing a requested semantic profile with a supplied resource. Resource and request
 * are OWL individuals previously loaded into the reasoner using the 'load' methods.
 *
 * @param resourceIri IRI of the resource.
 * @param requestIri IRI of the request.
 * @return Result of the abduction inference service.
 *
 * @see Ruta et al., WIAS 2011 (Section 4, Chapter 2)
 *      ( http://sisinflab.poliba.it/publications/2011/RDS11 )
 */
- (TMEAbduction *)abductionBetweenResource:(OWLIRI *)resourceIri
                                andRequest:(OWLIRI *)requestIri;

/**
 * Performs the Concept Bonus non-standard matchmaking task,
 * comparing a requested semantic profile with a supplied resource. Resource and request
 * are OWL individuals previously loaded into the reasoner using the 'load' methods.
 *
 * @param resourceIri IRI of the resource.
 * @param requestIri IRI of the request.
 * @return Result of the bonus inference service.
 *
 * @see Scioscia et al., SRLGIPD18
 *      ( http://sisinflab.poliba.it/publications/2018/SRLGIPD18 )
 */
- (TMEBonus *)bonusBetweenResource:(OWLIRI *)resourceIri
                        andRequest:(OWLIRI *)requestIri;

/**
 * Performs the Concept Contraction non-standard matchmaking task,
 * comparing a requested semantic profile with a supplied resource. Resource and request
 * are OWL individuals previously loaded into the reasoner using the 'load' methods.
 *
 * @param resourceIri IRI of the resource.
 * @param requestIri IRI of the request.
 * @return Result of the contraction inference service.
 *
 * @see Ruta et al., WIAS 2011 (Section 4, Chapter 2)
 *      ( http://sisinflab.poliba.it/publications/2011/RDS11 )
 */
- (TMEContraction *)contractionBetweenResource:(OWLIRI *)resourceIri
                                    andRequest:(OWLIRI *)requestIri;

/**
 * Performs the Concept Covering non-standard matchmaking task,
 * comparing a requested semantic profile with available resources. Request is an OWL individual
 * previously loaded into the reasoner using the 'load' methods.
 *
 * @param requestIri IRI of the request.
 * @return Result of the covering inference service.
 *
 * @see Di Noia et al., Concept Covering ( http://sisinflab.poliba.it/publications/2004/DDD04a )
 */
- (TMEComposition *)coveringForRequest:(OWLIRI *)requestIri;

/**
 * Computes the Concept Difference between two individuals.
 *
 * @param lhsIri LHS of the difference.
 * @param rhsIri RHS of the difference.
 * @return Result of the difference task.
 */
- (TMESemanticDescription *)differenceBetween:(OWLIRI *)lhsIri and:(OWLIRI *)rhsIri;

/**
 * Computes the maximum penalty for the specified individual.
 *
 * @param iri IRI of the individual.
 * @return Maximum penalty.
 */
- (double)maxPenaltyFor:(OWLIRI *)iri;

/**
 * Determines if the specified description is satisfiable with respect to the root ontology.
 *
 * @param description Description whose satisfiability should be checked.
 * @return True if the description is satisfiable, false otherwise.
 */
- (BOOL)descriptionIsSatisfiable:(TMESemanticDescription *)description;

/**
 * Determines if a subsumption relation holds between two semantic profiles (that is,
 * if one is more general than the other), in which case they are referred to
 * as subsumer and subsumed.
 *
 * @param subsumed Subsumed element in the subsumption relation.
 * @param subsumer Subsumer element in the subsumption relation.
 * @return True if the subsumption relation holds, false otherwise.
 */
- (BOOL)description:(TMESemanticDescription *)subsumed
       isSubsumedBy:(TMESemanticDescription *)subsumer;

@end

NS_ASSUME_NONNULL_END
