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.ClauseIterator;
import ws.prova.parser.ParsingException;

/**
 * Implementation of an inference engine returning many results.
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @version 3.3.1 <9 August 2004>
 * @since 1.7.2
 */
public final class ResolutionInferenceEngine2
    extends AbstractResolutionInferenceEngine {

    /**
     * Constructor.
     */
    public ResolutionInferenceEngine2() {
        super();
    }
    /**
     * Get the feature descriptions.
     *
     * @return the feature descriptions
     */
    public InferenceEngineFeatureDescriptions getFeatureDescriptions() {
        if (featureDescriptions == null) {
            featureDescriptions = new InferenceEngineFeatureDescriptions() {
                protected void initialize() {
                    super.initialize();
                    this.supported.add(
                        InferenceEngineFeatureDescriptions.MULTIPLE_RESULTS);
                    this.supported.add(
                        InferenceEngineFeatureDescriptions.LOOP_CHECKS);
                    this.supported.add(
                        InferenceEngineFeatureDescriptions
                            .DERIVATION_EVENT_LISTENERS);
                }

            };
        }
        return featureDescriptions;
    }
    /**
     * Try to proof a goal.
     *
     * @return a derivation node
     * @param goal -
     *                    the goal that has to be proved
     * @param constraintPool -
     *                    a list of constraints
     * @param queryVariables -
     *                    a list of query variables
     * @param kb -
     *                    the knowledge base used
     * @param counter -
     *                    the proof step counter
     * @param renameVariables
     *                    a variable renaming
     * @param logEnabled -
     *                    indicates whether we must log this proof step
     * @param results -
     *                    the list collecting the results
     * @param appliedClauses -
     *                    a list of all clauses applied so far (used to detect loops)
     * @param exceptionHandlingStrategy -
     *                    an integer decoding the exception handling strategy when
     *                    fetching and resolving ClauseSetExceptions
     * @param cardinalityConstraint -
     *                    the cardinality constraint specifying the number of results
     *                    we are looking for
     * @param listeners
     *                    derivation listeners
     * @param session
     *                    a session
     * @throws InferenceException
     */
    private DerivationNodeImpl proof(
        Clause goal,
        List constraintPool,
        DerivationStepCounter counter,
        VariableRenaming renameVariables,
        boolean logEnabled,
        List appliedClauses,
        List results,
        SessionImpl session)
            throws InferenceException, ParsingException {

        int exceptionHandlingStrategy = session.getExceptionHandlingStrategy();
        int cardinalityConstraint = session.getCardinalityContraint();
        org.mandarax.kernel.KnowledgeBase kb = session.getKnowledgeBase();

        // make sure that the session is uptodate
        session.update(renameVariables.getAllRenamings(),constraintPool);

        // for performance reasons we want to minimize checks whether log is
        // enabled. On the other hand, we would like to switch log on / off
        // during a proof (e.g., to analyse a long proof). This implementation
        // checks the respective log category every 10 steps
        boolean logOn =
            (counter.count % 10 == 0)
                ? LOG_IE_STEP.isDebugEnabled()
                : logEnabled;
        DerivationNodeImpl node = new DerivationNodeImpl();
        node.setId(counter.next());
        // node.supportedSolution = results.size();
        DerivationNodeImpl nextNode = null;

        if (logOn) {
            LOG_IE_STEP.debug("PROOF STEP " + String.valueOf(counter.count));
            LOG_IE_STEP.debug("Goal       : " + goal.toString());
        }

        // try to remove clauses using the object semantics
        goal = performSemanticalEvaluation(goal, session, logOn);

        if (goal == null) {
            node.setFailed(true);
            return node;
        }

        // check whether the max proof length has been reached
        if (counter.count >= MAXSTEPS) {
            if (logOn) {
                LOG_IE_STEP.debug(
                    "Maximum number of steps reached, stop here !");
            }

            return node;
        }

        // if the goal is the empty clause, return success
        if (goal.isEmpty()) {
            if (logOn) {
                LOG_IE_STEP.debug("Derivation successful !");
            }
            results.add(node);
            // new in 3.2: notify listener
            notifyListenersOnResult(session,logOn);

            node.setResultNode(true);
            node.setSupported(results.size() - 1);
            if (logOn) {
                LOG_IE_STEP.debug(
                    "Set result node supporting result "
                        + (results.size() - 1)
                        + ": "
                        + node);
            }
            node.setFailed(false);
            // check whether we have enough results
            if (cardinalityConstraint != ALL) {
                node.setLastNode((results.size() >= cardinalityConstraint));
            }
            return node;
        }

        // check for the next clause to continue. Try resolution.
        try {
            ClauseIterator e = kb.clauses(goal, null);
            boolean useClause = true;
            while (e.hasMoreClauses()
                && (cardinalityConstraint == ALL
                    || results.size() < cardinalityConstraint)) {
                useClause = true;
                Resolution r = null;
                Clause c = null;
                Clause workCopy = null;
                try {
                    c = e.nextClause();
                    workCopy = renameVariables.cloneAndRenameVars(c);
                } catch (ClauseSetException x) {
                    String msg =
                        "Exception fetching clause from iterator for " + goal;
                    LOG_IE_STEP.error(msg, x);
                    // depending on the exception handling strategy we forward
                    // the exception or carry on
                    if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
                        throw new InferenceException(msg, x);
                    useClause = false;
                }
                if (useClause
                    && (r =
                        Resolution.resolve(
                            workCopy,
                            goal,
                            unificationAlgorithm,
                            selectionPolicy,
                            session))
                        != null) {
                    appliedClauses.add(c);
                    if (loopCheckingAlgorithm.isInfiniteLoop(appliedClauses)) {
                        if (logOn) {
                            LOG_IE_STEP.debug(
                                "LoopChecking Algorithm "
                                    + loopCheckingAlgorithm
                                    + " has detected a loop! Try to continue with next clause");
                        }
                    } else {
                        // log
                        if (logOn) {
                            LOG_IE_STEP.debug("Can apply the following rule:");
                            LOG_IE_STEP.debug("Clause     : " + c.toString());
                            LOG_IE_STEP.debug(
                                "Clause (rn): " + workCopy.toString());

                            // log unification
                            Replacement nextReplacement = null;
                            for (Iterator er =
                                r.unification.replacements.iterator();
                                 er.hasNext();
                                ) {
                                nextReplacement = (Replacement) er.next();
                                LOG_IE_STEP.debug(
                                    "unify      : "
                                        + nextReplacement.original.toString()
                                        + " -> "
                                        + nextReplacement.replacement.toString());
                            }
                        }

                        // build a new subgoal
                        Clause nextGoal = getNextGoal(workCopy, goal, r);

                        // build a new constraint pool for the next step
                        List nextConstraintPool =
                            getNextConstraintPool(constraintPool, r);

                        // apply constraints
                        nextGoal = nextGoal.apply(nextConstraintPool);

                        // rename variables in the subgoal
                        nextGoal = renameVariables.cloneAndRenameVars(nextGoal);

                        // keep the renamed var here, otherwise they get
                        // overridden in the recursion
                        Hashtable renamed =
                            renameVariables.getRecentRenamings();

                        // log renamings
                        if (logOn) {
                            Object nextRenaming = null;

                            for (Enumeration er = renamed.keys();
                                 er.hasMoreElements();
                                ) {
                                nextRenaming = er.nextElement();
                                LOG_IE_STEP.debug(
                                    "rename     : "
                                        + nextRenaming.toString()
                                        + " -> "
                                        + renamed.get(nextRenaming).toString());
                            }
                        }

                        // proof the new subgoal
                        nextNode =
                            proof(
                                nextGoal,
                                nextConstraintPool,
                                counter,
                                renameVariables,
                                logOn,
                                appliedClauses,
                                results,
                                session);

                        nextNode.setQuery(goal);
                        nextNode.setAppliedClause(c);

                        // register the subnode
                        node.addSubNode(nextNode);

                        if (!nextNode.isFailed()) {
                            // add renamings and unification
                            nextNode.varRenamings = renamed;
                            nextNode.setUnification(r.unification);
                        }
                    }
                } else {
                    if (logOn) {
                        LOG_IE_STEP.debug("Cannot apply the following rule:");
                        LOG_IE_STEP.debug("Clause     : " + c.toString());
                        LOG_IE_STEP.debug(
                            "Clause (rn): " + workCopy.toString());
                    }
                }
            }
            // new in 2.0 - release resources!
            e.close();
        } catch (ClauseSetException x) {
            String msg = "Exception getting clause iterator for " + goal;
            LOG_IE_STEP.error(msg, x);
            if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
                throw new InferenceException(msg, x);
        }
        if ((nextNode == null) || nextNode.isFailed()) {
            List l = node.getSubNodes();
            int n = l.size();
            boolean result = true;
            for (int i = 0; i < n; i++) {
                result = result && ((DerivationNodeImpl) l.get(i)).isFailed();
                node.setFailed(result);
            }
            // new in 1.9.2
            node.setFailed(result);
        }
        return node;
    }
    /**
     * Answer a query, retrieve (multiple different) result. The cardinality
     * contraints describe how many results should be computed. It is either
     * <ol>
     * <li><code>ONE</code>- indicating that only one answer is expected
     * <li><code>ALL</code>- indicating that all answers should be computed
     * <li><code>an integer value greater than 0 indicating that this number of results expected
     * </ol>
     * @see #ONE
     * @see #ALL
     * @return the result set of the query
     * @param query the query clause
     * @param kb the knowledge base used to answer the query
     * @param aCardinalityConstraint the number of results expected
     * @param exceptionHandlingPolicy one of the constants definied in this class (BUBBLE_EXCEPTIONS,TRY_NEXT)
     * @throws an InferenceException
     */
    public ResultSet query(
        Query query,
        org.mandarax.kernel.KnowledgeBase kb,
        int aCardinalityConstraint,
        int exceptionHandlingPolicy)
        throws InferenceException {
        Clause firstGoal = getGoal(query);
        VariableRenaming renameVariables = new VariableRenaming();
        List resultNodes = new ArrayList();
        SessionImpl session = new SessionImpl(kb,this,query,exceptionHandlingPolicy,aCardinalityConstraint);
        notifyListenersOnDerivationStart(session,LOG_IE_STEP.isDebugEnabled());

        // proof
        DerivationNodeImpl linResult =
                null;
        try {
            linResult = proof(
                firstGoal,
                new ArrayList(),
                new DerivationStepCounter(),
                renameVariables,
                LOG_IE_STEP.isDebugEnabled(),
                new ArrayList(MAXSTEPS),
                resultNodes,
                session);
        } catch (ParsingException e) {
        }
        for (int i = 0; i < resultNodes.size(); i++)
            ((DerivationNodeImpl) resultNodes.get(i))
                .propagateSupportedSolutions();
        linResult.setSemanticEvaluationPolicy(getSemanticEvaluationPolicy());
        return new ResultSetImpl2(linResult, resultNodes, firstGoal);

    }
}
