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 only one result.
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @version 3.3.1 <9 August 2004>
 * @since 1.0
 */
public final class ResolutionInferenceEngine extends AbstractResolutionInferenceEngine {

    private static final DerivationTreeBuilder derivationTreeBuilder = new DerivationTreeBuilder();
    /**
     * Constructor.
     */
    public ResolutionInferenceEngine() {
        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.LOOP_CHECKS);
                }

            };
        }

        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 count - the proof step count
     * @param renameVariables  a variable renaming
     * @param logEnabled - indicates whether we must log this proof step
     * @param appliedClauses - a list of all clauses applied so far (used to detect loops)
     * @param session a session
     * @throws InferenceException
     */
    private DerivationNodeImpl proof(Clause goal, List constraintPool,
                                     DerivationStepCounter counter, VariableRenaming renameVariables,
                                     boolean logEnabled, List appliedClauses,SessionImpl session) throws InferenceException, ParsingException {

        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());
        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, null,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 !");
            }

            node.setFailed (false);
            node.setResultNode(true);

            return node;
        }

        // check for the next clause to continue. Try resolution.

        try {
            ClauseIterator e = kb.clauses (goal, null);
            boolean useClause = true;
            while(e.hasMoreClauses () && ((nextNode == null) || nextNode.isFailed ())) {
                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 (session.getExceptionHandlingStrategy()==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,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 (session.getExceptionHandlingStrategy()==BUBBLE_EXCEPTIONS) throw new InferenceException(msg,x);
        }

        if((nextNode == null) || nextNode.isFailed ()) {
            node.setFailed (true);
        }

        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>
     * This inference engines does not support retrieving multiple answers!
     * If requested, a runtime exception (<code>java.lang.IllegalArgumentException</code>)
     * is thrown indicating that the parameter (e.g. <code>ALL</code>) is not valid.
     * @see #ONE
     * @see #ALL
     * @return the result set of the query
     * @param query the query
     * @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(final Query query, org.mandarax.kernel.KnowledgeBase kb,int aCardinalityConstraint,int exceptionHandlingPolicy) throws InferenceException {
        final Clause firstGoal = getGoal(query);
        VariableRenaming renameVariables = new VariableRenaming ();
        DerivationNodeImpl   linResult =  null;
        try {
            linResult = proof (firstGoal, new ArrayList (), new DerivationStepCounter(), renameVariables, LOG_IE_STEP.isDebugEnabled (), new ArrayList (MAXSTEPS),new SessionImpl(kb,this,query,exceptionHandlingPolicy, InferenceEngine.ONE));
        } catch (ParsingException e) {
        }
        linResult.setSemanticEvaluationPolicy(getSemanticEvaluationPolicy());
        Replacement[]  replacements = IEUtils.getReplacements (linResult, firstGoal);
        DerivationNodeImpl root = derivationTreeBuilder.buildTree (linResult);
        final Result result = root.isFailed()?null:new Result (new Derivation (root,0), replacements);
        ResultSet rs = new ResultSet() {
                private int pos = -1;
                private List vars = null;
                /**
                 * Moves the cursor to the first row in this ResultSet object.
                 * @return true if the cursor is on a valid row; false if there are no rows in the result set
                 */
                public boolean first() {
                    pos = 0;
                    return result!=null;
                }
                /**
                 * Moves the cursor to the last row in this ResultSet object.
                 * @return true if the cursor is on a valid row; false if there are no rows in the result s
                 */
                public boolean last() {
                    pos = 0;
                    return result!=null;
                }
                /**
                 * Retrieves the current result number. Numbering starts with 1.
                 * @return a number
                 */
                public int getResultNumber() {return pos==0?1:-1;}
                /**
                 * Moves the cursor down one row from its current position. A ResultSet cursor is initially positioned
                 * before the first row; the first call to the method next makes the first row the current row;
                 * the second call makes the second row the current row, and so on.
                 * @return true if the new current row is valid; false if there are no more rows
                 */
                public boolean next() {
                    pos=pos+1;
                    return result!=null && pos==0;
                }
                /**
                 * Moves the cursor to the previous row in this ResultSet object.
                 * @return true if the cursor is on a valid row; false if it is off the result set
                 */
                public boolean previous() {
                    return false;
                };
                /**
                  * Get the current position of the cursor.
                  * @return an integer
                  */
                public int getCursorPosition() {
                    return pos;
                }
                /**
                 * Releases this ResultSet resources.
                 */
                public void close() {}
                /**
                 * Get the derivation of the current result.
                 * Throw an exception if the cursor is not positioned at a result.
                 * @return the proof (derivation)
                 */
                public Derivation getProof() throws InferenceException {
                    if (pos!=0) throw new InferenceException("Illegal cursor position " + pos + " in result set.");
                    return result.getProof();
                }
                /**
                 * Get the object that replaces the variable with the given name and type.
                 * If there is no such object, return null.
                 * Throw an exception if the cursor is not positioned at a result.
                 * @return the object that replaced the variable
                 * @param type the type of the variable
                 * @param name the name of the variable
                 * @exception an inference exception
                 */
                public Object getResult(Class type, String name) throws InferenceException {
                    if (pos!=0) throw new InferenceException("Illegal cursor position " + pos + " in result set.");
                    return result.getResult(type,name);
                }
                /**
                 * Get the object that replaces the variable.
                 * If there is no such object, return null.
                 * Throw an exception if the cursor is not positioned at a result.
                 * @return the object that replaced the variable
                 * @param term the variable term that is (perhaps) replaced
                 * @exception an inference exception
                 */
                public Object getResult(VariableTerm term)throws InferenceException {
                    if (pos!=0) throw new InferenceException("Illegal cursor position " + pos + " in result set.");
                    return result.getResult(term);
                }
                /**
                 * Get a list of all variable terms in the query.
                 * @return a list of variable terms
                 */
                public List getQueryVariables() {
                    if (vars == null) vars = IEUtils.getVars(firstGoal);
                    return vars;
                }
                /**
                 * Indicates whether the cursor is at the first position.
                 * @return a boolean
                 */
                public boolean isFirst() {
                    return result!=null && pos==0;
                }
                /**
                 * Indicates whether the cursor is at the last position.
                 * @return a boolean
                 */
                public boolean isLast() {
                    return result!=null && pos==0;
                }

                /**
                 * Moves the cursor a relative number of results, either positive or negative.
                 * @param offset the number of results
                 * @return true if the cursor is on the result set; false otherwise.
                 */
                public boolean relative(int offset) {
                    pos = pos+offset;
                    return pos==0;
                }
                /**
                 * Moves the cursor to the given result number.
                 * @param resultNo the number of results.
                 * @return true if the cursor is on the result set; false otherwise
                 */
                public boolean absolute(int resultNo) {
                    pos = resultNo-1; // like in JDBC - the number of the first result is 1, not 0 !
                    return pos==0;
                }
                /**
                 * Moves the cursor to the front of this ResultSet object, just before the first row.
                 * This method has no effect if the result set contains no rows.
                 */
                public void beforeFirst() {
                    pos = -1;
                }

                /**
                 * Moves the cursor to the end of this ResultSet object, just after the last row.
                 * This method has no effect if the result set contains no rows.
                 */
                public void afterLast() {
                    pos = 2;
                }
                /**
                 * Retrieves whether the cursor is before the first row in this ResultSet object.
                 * @return true if the cursor is before the first row; false if the cursor is at any other position or the result set contains no rows
                 */
                public boolean isBeforeFirst() throws InferenceException {
                    return pos==-1;
                }

                /**
                 * Retrieves whether the cursor is after the last result in this ResultSet object.
                 * @return true if the cursor is after the last result; false if the cursor is at any other position or the result set contains no results
                 */
                public boolean isAfterLast() throws InferenceException {
                    return pos==2;
                }
                /**
                 * Get the results as map.
                 * @return a map
                 */
                public Map getResults() throws InferenceException {
                    if (pos!=0) throw new InferenceException("Illegal cursor position " + pos + " in result set.");
                    return result.getResults();
                }


        };
        return rs;

    }
}
