package org.mandarax.reference;

/*
 * Copyright (C) 1999-2004 <a href="mailto:mandarax@jbdietrich.com">Jens Dietrich</a>
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
import java.util.*;
import org.mandarax.kernel.*;
import org.mandarax.util.logging.LogCategories;

/**
 * Abstract superclass for inference engines based on resolution.
 * The design is rather modular - a selection rule, the unification
 * algorithm and a loop checking algorithm used are public properties of the engine and can be configured.
 * Note that by default we do not use loop checking, the default loop checker is the trivial do nothing
 * implementation.
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @version 3.3.1 <9 August 2004>
 * @since 1.7.2
 */
public abstract class AbstractResolutionInferenceEngine implements InferenceEngine, LogCategories {

	protected SelectionPolicy selectionPolicy = new LeftMostSelectionPolicy();
	protected UnificationAlgorithm unificationAlgorithm = new RobinsonsUnificationAlgorithm();
	protected LoopCheckingAlgorithm loopCheckingAlgorithm = new NullLoopCheckingAlgorithm();
	protected InferenceEngineFeatureDescriptions featureDescriptions = null;
	protected SemanticEvaluationPolicy semanticEvaluationPolicy = new DefaultSemanticEvaluationPolicy();

	// maximum number of resolution steps
	public int MAXSTEPS = 100000;

	/**
	 * AbstractInferenceEngine constructor comment.
	 */
	public AbstractResolutionInferenceEngine() {
		super();
	}

	/**
	 * Get the loop checking algorithm.
	 * @return an algorithm
	 */
	public LoopCheckingAlgorithm getLoopCheckingAlgorithm() {
		return loopCheckingAlgorithm;
	}
	/**
	 * Get the maximum number of proof steps that should be performed.
	 * If this number is reached without a result, the engine gives up.
	 * @return the max number of proof steps
	 */
	public int getMaxNumberOfProofSteps() {
		return MAXSTEPS;
	}
	/**
	 * Get the next constraint pool.
	 * @return a list replacements
	 * @param cp the previous constraint pool
	 * @param r a resulution
	 */
	protected List getNextConstraintPool(List cp, Resolution r) {
		List nextConstraintPool = new ArrayList(cp.size() + 5);
		nextConstraintPool.addAll(cp);

		for (Iterator it = r.unification.replacements.iterator();
			it.hasNext();
			) {
			nextConstraintPool.add(it.next());
		}
		return nextConstraintPool;
	}
	/**
	 * Build the next goal, i.e., remove the unified terms, join the remaining clauses,
	 * and apply the unifications.
	 * @return the next goal
	 * @param c1 the first unified clause
	 * @param c2 the second unified clause
	 * @param u a resolution
	 */
	protected Clause getNextGoal(Clause c1, Clause c2, Resolution r) {
		TmpClause nextClause = new TmpClause();
		nextClause.positiveLiterals =
			merge(
				c2.getPositiveLiterals(),
				c1.getPositiveLiterals(),
				r.position2);
		nextClause.negativeLiterals =
			merge(
				c1.getNegativeLiterals(),
				c2.getNegativeLiterals(),
				r.position1);
		return nextClause;
	}
	/**
	 * Build the first goal from the query.
	 * @return a goal
	 * @param query a query
	 */
	protected Clause getGoal(Query query) {
		return IEUtils.getGoal(query); 
	}
	/**
	 * Get the used selection policy.
	 * @return the used policy
	 */
	public SelectionPolicy getSelectionPolicy() {
		return selectionPolicy;
	}
	/**
	 * Get the used unification algorithm.
	 * @return the used algorithm
	 */
	public UnificationAlgorithm getUnificationAlgorithm() {
		return unificationAlgorithm;
	}

	/**
	 * Merge both lists, skip the element at the index "skip" in the second list.
	 * @return a new list
	 * @param v1 the first list
	 * @param v2 the second list
	 * @param skip the index to be skipped in the second list
	 */
	protected List merge(List v1, List v2, int skip) {
		List merged = new ArrayList(v1.size() + v2.size());
		for (int i = 0; i < v1.size(); i++) {
			merged.add(v1.get(i));
		}
		for (int i = 0; i < v2.size(); i++) {
			if (skip != i) {
				merged.add(v2.get(i));
			}
		}
		return merged;
	}
	/**
	 * Try to execute literals in the clause, and remove those literals if the
	 * result ist true. E.g., the result of performing +[]-[L1,L2,2&lt4,L3]
	 * would be +[]-[L1,L2,2&lt4,L3]. If  the parameter was +[]-[L1,L2,2&gt4,L3],
	 * null would be returned.
	 * <p>
	 * Check whether we should use the selection policy here, right now we
	 * use a from the left to the right policy.
	 * <p>
	 * A rather sensible question is how to handle exceptions that occur when
	 * evaluating literals. The approach taken here is that an exception will render
	 * the literal as "false".
	 * @param c a clause
	 * @param session a session
	 * @param logOn indicates whether we should log
	 * @return another clause
	 */
	protected Clause performSemanticalEvaluation(Clause c, Session session,boolean logOn) {
		return semanticEvaluationPolicy.evaluate(c,session, logOn);
	}
	/**
	 * Set a new loop checking algorithm.
	 * @param lp a loop checker
	 */
	public void setLoopCheckingAlgorithm(LoopCheckingAlgorithm anAlgorithm) {
		loopCheckingAlgorithm = anAlgorithm;
	}
	/**
	 * Set the maximum number of proof steps that should be performed.
	 * If this number is reached without a result, the engine gives up.
	 * @param steps the max number of steps
	 */
	public void setMaxNumberOfProofSteps(int steps) {
		MAXSTEPS = steps;
	}
	/**
	 * Set a selection policy.
	 * @param aPolicy the new selection policy
	 */
	public void setSelectionPolicy(SelectionPolicy aPolicy) {
		selectionPolicy = aPolicy;
	}
	/**
	 * Set a unification algorithm.
	 * @param anAlgorithm the new algorithm
	 */
	public void setUnificationAlgorithm(UnificationAlgorithm anAlgorithm) {
		unificationAlgorithm = anAlgorithm;

		if (unificationAlgorithm != null
			&& unificationAlgorithm instanceof ExtendedUnificationAlgorithm) {
			(
				(
					ExtendedUnificationAlgorithm) unificationAlgorithm)
						.setSemanticEvaluationPolicy(
				semanticEvaluationPolicy);
		}
	}
	/**
	 * Returns the semantic evaluation policy.
	 * @return the current policy
	 */
	public SemanticEvaluationPolicy getSemanticEvaluationPolicy() {
		return semanticEvaluationPolicy;
	}

	/**
	 * Sets the semantic evaluation policy.
	 * @param policy The policy to set
	 */
	public void setSemanticEvaluationPolicy(SemanticEvaluationPolicy policy) {
		semanticEvaluationPolicy = policy;

		if (unificationAlgorithm != null
			&& unificationAlgorithm instanceof ExtendedUnificationAlgorithm) {
			(
				(
					ExtendedUnificationAlgorithm) unificationAlgorithm)
						.setSemanticEvaluationPolicy(
				policy);
		}
	}

	/**
	 * Returns the max number of resolution steps.
	 * @return int
	 */
	public int getMaxSteps() {
		return MAXSTEPS;
	}

	/**
	 * Sets the max number of resolution steps.
	 * @param value the max number of resolution steps
	 */
	public void setMaxSteps(int value) {
		MAXSTEPS = value;
	}

	/**
	 * Invoke a procedural attachment. 
	 * @param session a session
	 * @param debugOn whether debug is switched on
	 */
	protected void notifyListenersOnResult(Session session,boolean debugOn) throws InferenceException {
		DerivationEventListener[] listeners = session.getQuery().getDerivationEventListeners();
		if (listeners != null && listeners.length>0) {
			Map varReplacements = new Hashtable();
			for (int i=0;i<listeners.length;i++) {
				listeners[i].onResultDo(session);
			}
		}
	}
	/**
	 * Invoke a procedural attachment. 
	 * @param session a session
	 * @param debugOn whether debug is switched on
	 */
	protected void notifyListenersOnDerivationStart(Session session,boolean debugOn) throws InferenceException {
		DerivationEventListener[] listeners = session.getQuery().getDerivationEventListeners();
		if (listeners != null && listeners.length>0) {
			for (int i=0;i<listeners.length;i++) {
				listeners[i].beforeDerivationDo(session);
			}
		}
	}



}
