package de.tu_dresden.lat.proofs.tools;

import org.semanticweb.owlapi.model.OWLAxiom;

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

/**
 * @author Christian Alrabbaa
 *
 */
public class TreeProofGenerator {

	public static IProof getTreeProof(IProof proof) {
		return generateTreeOfMinimalHypergraph(proof);
	}

	/**
	 * For the given proof, extract the minimal acyclic proof and return the
	 * corresponding tree proof
	 * 
	 * @param proof
	 * @return
	 */
	private static IProof generateTreeOfMinimalHypergraph(IProof proof) {

		IProof minimal = MinimalHypergraphProofExtractor.makeUnique(proof);

		IProof tree = new Proof(minimal.getFinalConclusion());

		populateTree(tree, minimal.getFinalConclusion(), minimal);

		return tree;
	}

	/**
	 * add inferences to the provided tree proof
	 * 
	 * @param tree
	 * @param conclusionAxiom
	 * @param minimalProof
	 */
	private static void populateTree(IProof tree, OWLAxiom conclusionAxiom, IProof minimalProof) {

		minimalProof.getInferences(conclusionAxiom).forEach(inference -> {

			tree.addInference(inference);

			inference.getPremises().forEach(premise -> {

				populateTree(tree, premise, minimalProof);
			});
		});

	}
}
