package org.semanticweb.elk.reasoner.saturation.conclusions;

import org.semanticweb.elk.reasoner.indexing.hierarchy.IndexedClassExpression;
import org.semanticweb.elk.reasoner.saturation.conclusions.visitors.ConclusionVisitor;
import org.semanticweb.elk.reasoner.saturation.context.ContextPremises;
import org.semanticweb.elk.reasoner.saturation.rules.ConclusionProducer;
import org.semanticweb.elk.reasoner.saturation.rules.Rule;
import org.semanticweb.elk.reasoner.saturation.rules.RuleVisitor;

/*
 * #%L
 * ELK Reasoner
 * $Id:$
 * $HeadURL:$
 * %%
 * Copyright (C) 2011 - 2012 Department of Computer Science, University of Oxford
 * %%
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 * 
 *      http://www.apache.org/licenses/LICENSE-2.0
 * 
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 * #L%
 */

/**
 * A general type of conclusions, produced by inference rules and used as
 * premises of inference rules. The rules can be applied to {@link Conclusion}s
 * together with other conclusions stored in {@link ContextPremises}. There are
 * different type of rules that can be applied to {@link Conclusion}.
 * Non-redundant rules are the (optimized) rules that do not cause
 * incompleteness (all atomic subsumers are guaranteed to be computed). These
 * rules are non-monotonic in the sense that a rule can be applicable with
 * {@link ContextPremises} but not applicable if some {@link Conclusion}s are
 * added to {@link ContextPremises}. This can result in non-deterministic result
 * if the rules are applied in different order. Redundant rules are in the sense
 * those rules that were not applied to {@link ContextPremises} but could be
 * applied if some {@link Conclusion}s were not inserted to
 * {@link ContextPremises}. Next, one can apply only local rules, namely those
 * rules that produce {@link Conclusion}s with the same source root as the
 * {@link Conclusion} to which the rule was applied. These rules are again
 * distinguished on redundant and non-redundant: redundant local rules is the
 * intersection of redundant rules and local rules, and similarly redundant
 * non-local rules.
 * 
 * @see Rule
 * 
 * @author "Yevgeny Kazakov"
 * 
 */
public interface Conclusion {

	public <I, O> O accept(ConclusionVisitor<I, O> visitor, I input);

	/**
	 * Every {@link Conclusion}, depending in which {@link ContextPremises} it
	 * is to be stored, represents a subsumer of some root
	 * {@link IndexedClassExpression}, which is computed by this method.
	 * 
	 * @param rootWhereStored
	 * @return The {@link IndexedClassExpression} for which this conclusion is
	 *         logically derived; it cannot be {@code null}
	 */
	public IndexedClassExpression getSourceRoot(
			IndexedClassExpression rootWhereStored);

	public IndexedClassExpression getDeterminingRoot(
			IndexedClassExpression rootWhereStored);

	/**
	 * Apply all non-redundant inferences for this {@link Conclusion} with other
	 * {@link ContextPremises}
	 * 
	 * @see #applyRedundantRules(RuleVisitor, ContextPremises,
	 *      ConclusionProducer)
	 * 
	 * @param ruleAppVisitor
	 * @param premises
	 * @param producer
	 */
	public void applyNonRedundantRules(RuleVisitor ruleAppVisitor,
			ContextPremises premises, ConclusionProducer producer);

	/**
	 * Apply all redundant rules for this {@link Conclusion} and given
	 * {@link ContextPremises}. A rule is redundant if its application is not
	 * necessary for completeness. Redundancy of a rule depends on other
	 * {@link ContextPremises}: a non-redundant rule might become redundant when
	 * other {@link ContextPremises} are added.
	 * 
	 * @see #applyNonRedundantRules(RuleVisitor, ContextPremises,
	 *      ConclusionProducer)
	 * 
	 * @param ruleAppVisitor
	 * @param premises
	 * @param producer
	 */
	public void applyRedundantRules(RuleVisitor ruleAppVisitor,
			ContextPremises premises, ConclusionProducer producer);

	/**
	 * Apply all non-redundant rules that produce {@link Conclusion}s that
	 * logically belong to the same root as this {@link Conclusion}
	 * 
	 * @see #isLocalFor(IndexedClassExpression)
	 * @see #applyRedundantLocalRules(RuleVisitor, ContextPremises,
	 *      ConclusionProducer)
	 * 
	 * @param ruleAppVisitor
	 * @param premises
	 * @param producer
	 */
	public void applyNonRedundantLocalRules(RuleVisitor ruleAppVisitor,
			ContextPremises premises, ConclusionProducer producer);

	/**
	 * Apply all redundant rules that produce {@link Conclusion}s that logically
	 * belong to the same root as this {@link Conclusion}
	 * 
	 * @see #applyNonRedundantLocalRules(RuleVisitor, ContextPremises,
	 *      ConclusionProducer)
	 * 
	 * @param ruleAppVisitor
	 * @param premises
	 * @param producer
	 */
	public void applyRedundantLocalRules(RuleVisitor ruleAppVisitor,
			ContextPremises premises, ConclusionProducer producer);

}

@@ -3138,16 +3138,455 @@
 ored);%0A%0A
+%09/**%0A%09 * TODO: this is a temporary solution to deal with %7B@link Propagation%7Ds; a%0A%09 * more robust solution should be found later.%0A%09 * %0A%09 * Returns the root %7B@link IndexedClassExpression%7D by which this%0A%09 * %7B@link Conclusion%7D is determined, i.e., after computing the saturation%0A%09 * for this root, %7B@link Conclusion%7Ds that determine by this root will not%0A%09 * be produced. Could be %7B@code null%7D%0A%09 * %0A%09 * @param rootWhereStored%0A%09 * @return%0A%09 */%0A
 %09public 

comment on a temporary solution for propagations