package de.tu_dresden.lat.proofs.data;

import java.util.Collection;
import java.util.Collections;
import java.util.LinkedList;
import java.util.List;
import java.util.NoSuchElementException;
import java.util.Set;

import org.semanticweb.owlapi.model.OWLAxiom;

import com.fasterxml.jackson.annotation.JsonCreator;
import com.fasterxml.jackson.annotation.JsonIgnore;
import com.fasterxml.jackson.annotation.JsonProperty;

import de.tu_dresden.lat.proofs.interfaces.IInference;
import de.tu_dresden.lat.proofs.interfaces.IProof;
import de.tu_dresden.lat.proofs.tools.MultiMap;

/**
 * @author Christian Alrabbaa
 *
 */
public class Proof implements IProof {

	private final MultiMap<OWLAxiom, IInference> conclusions2inferences;
	private final List<IInference> inferences;

	private final OWLAxiom finalConclusion;

	@JsonCreator
	public Proof(@JsonProperty("finalConclusion") OWLAxiom finalConclusion,
			@JsonProperty("inferences") List<IInference> inferences) {
		this.finalConclusion = finalConclusion;
		this.inferences = new LinkedList<>(inferences);

		conclusions2inferences = new MultiMap<>();

		for (IInference inference : inferences) {
			conclusions2inferences.add(inference.getConclusion(), inference);
		}
	}

	public Proof(OWLAxiom finalConclusion) {
		this.finalConclusion = finalConclusion;
		inferences = new LinkedList<>();
		conclusions2inferences = new MultiMap<>();
	}

	@Override
	public OWLAxiom getFinalConclusion() {
		return finalConclusion;
	}

	@Override
	public List<IInference> getInferences() {
		return Collections.unmodifiableList(inferences);
	}

	@Override
	public Set<IInference> getInferences(OWLAxiom conclusion) {
		return conclusions2inferences.get(conclusion);
	}

	@Override
	public void addInference(IInference inference) {
		inferences.add(inference);
		conclusions2inferences.add(inference.getConclusion(), inference);
	}

	@Override
	public void addInferences(Collection<IInference> inference) {
		inferences.forEach(this::addInference);
	}

	@Override
	public boolean hasInferenceFor(OWLAxiom conclusion) {
		return conclusions2inferences.hasKey(conclusion);
	}

	@JsonIgnore
	@Override
	public int getNumberOfRuleApplications() {
		return inferences.size();
	}

	@Override
	public int getSizeOfLargestInferencePremise() {
		return inferences.stream().mapToInt(inf -> inf.getPremises().size()).max()
				.orElseThrow(NoSuchElementException::new);
	}

	@Override
	public String toString() {
		StringBuffer string = new StringBuffer();
		inferences.forEach(string::append);
		return string.toString();
	}

	@Override
	public int hashCode() {
		final int prime = 31;
		int result = 1;
		result = prime * result + ((inferences == null) ? 0 : inferences.hashCode());
		return result;
	}

	@Override
	public boolean equals(Object obj) {
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		Proof other = (Proof) obj;
		if (inferences == null) {
			if (other.inferences != null)
				return false;
		} else if (!inferences.equals(other.inferences))
			return false;
		return true;
	}

}
