package de.tu_dresden.lat.proofs.tools;

import java.util.AbstractMap.SimpleEntry;
import java.util.Collections;
import java.util.Comparator;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map.Entry;
import java.util.Set;

import org.semanticweb.owlapi.model.OWLAxiom;

import de.tu_dresden.lat.proofs.data.Proof;
import de.tu_dresden.lat.proofs.interfaces.IInference;
import de.tu_dresden.lat.proofs.interfaces.IProof;

public class MinimalHypergraphProofExtractor {

	public static IProof makeUnique(IProof proof) {
		RankedInferenceSet selectedInferences = selectBestInferences(proof, proof.getFinalConclusion(),
				Collections.emptyList());
		return new Proof(proof.getFinalConclusion(), new LinkedList<>(selectedInferences.inferences));
	}

	private static RankedInferenceSet selectBestInferences(IProof proof, OWLAxiom conclusion, List<OWLAxiom> trace) {
		if (trace.contains(conclusion)) {
			// avoid loops
			return new RankedInferenceSet(new HashSet<>(), Integer.MAX_VALUE);
		}
		List<OWLAxiom> newTrace = new LinkedList<>(trace);
		newTrace.add(conclusion);

		// chooses the subproof with the best hypergraph size
		return proof.getInferences(conclusion).stream().distinct()
				.map(inf -> new SimpleEntry<>(inf, selectBestInferences(proof, inf.getPremises(), newTrace)))
				.min(Comparator.comparing(Entry::getValue)).map(e -> e.getValue().combineWith(e.getKey()))
				.orElse(new RankedInferenceSet());
	}

	private static RankedInferenceSet selectBestInferences(IProof proof, List<? extends OWLAxiom> premises,
			List<OWLAxiom> trace) {
		return premises.stream().map(premise -> selectBestInferences(proof, premise, trace))
				.reduce(RankedInferenceSet::combineWith).orElse(new RankedInferenceSet());
	}

	static class RankedInferenceSet implements Comparable<RankedInferenceSet> {
		private Set<IInference> inferences;
		private Integer rank;

		public RankedInferenceSet() {
			this(new HashSet<>(), 0);
		}

		public RankedInferenceSet(Set<IInference> inferences, Integer rank) {
			this.inferences = inferences;
			this.rank = rank;
		}

		public RankedInferenceSet combineWith(RankedInferenceSet ris2) {
			this.inferences.addAll(ris2.inferences);
			if (this.rank.equals(Integer.MAX_VALUE) || ris2.rank.equals(Integer.MAX_VALUE)) {
				this.rank = Integer.MAX_VALUE;
			} else {
				this.rank += ris2.rank;
			}
			return this;
		}

		public RankedInferenceSet combineWith(IInference inf) {
			this.inferences.add(inf);
			if (!this.rank.equals(Integer.MAX_VALUE)) {
				this.rank++;
			}
			return this;
		}

		@Override
		public int compareTo(RankedInferenceSet ris2) {
			return this.rank.compareTo(ris2.rank);
		}

		@Override
		public String toString() {
			return inferences.toString() + ":" + rank.toString();
		}
	}

}
