package de.tu_dresden.lat.proofs.interfaces;

import java.util.Collection;
import java.util.List;
import java.util.Set;
import java.util.stream.Collectors;

import org.semanticweb.owlapi.model.OWLAxiom;

import com.fasterxml.jackson.annotation.JsonIgnore;
import com.fasterxml.jackson.databind.annotation.JsonDeserialize;
import com.fasterxml.jackson.databind.annotation.JsonSerialize;

import de.tu_dresden.lat.proofs.data.Proof;
import de.tu_dresden.lat.proofs.json.JsonAxiom2StringConverter;
import de.tu_dresden.lat.proofs.json.JsonString2AxiomConverter;

/**
 * @author Christian Alrabbaa
 *
 */
@JsonDeserialize(as = Proof.class)
public interface IProof {

	// Note: we use a list, as the order of inferences might be relevant,
	// if we choose the linear representation of proofs.
	List<IInference> getInferences();

	@JsonSerialize(converter = JsonAxiom2StringConverter.class)
	@JsonDeserialize(converter = JsonString2AxiomConverter.class)
	OWLAxiom getFinalConclusion();

	/**
	 * Return all inferences that have the given axiom as a conclusion.
	 */

	Collection<IInference> getInferences(OWLAxiom conclusion);

	void addInference(IInference inference);

	void addInferences(Collection<IInference> inference);

	boolean hasInferenceFor(OWLAxiom conclusion);

	/**
	 * The Number of Rule application is equal to the number of inferences involved
	 * in a proof.
	 */
	@JsonIgnore
	int getNumberOfRuleApplications();

	/**
	 * Return the size of the largest premise in all inferences involved in a proof.
	 */
	@JsonIgnore
	int getSizeOfLargestInferencePremise();
}
