/* LabeledTreeGenerator.java
 * =========================================================================
 * This file is part of the GrInvIn project - http://www.grinvin.org
 * 
 * Copyright (C) 2005-2008 Universiteit Gent
 * 
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or (at
 * your option) any later version.
 * 
 * This program 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
 * General Public License for more details.
 * 
 * A copy of the GNU General Public License can be found in the file
 * LICENSE.txt provided with the source distribution of this program (see
 * the META-INF directory in the source jar). This license can also be
 * found on the GNU website at http://www.gnu.org/licenses/gpl.html.
 * 
 * If you did not receive a copy of the GNU General Public License along
 * with this program, contact the lead developer, or write to the Free
 * Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
 * 02110-1301, USA.
 */

package org.grinvin.conjecture.engine.apengine;

import java.util.Arrays;

import org.grinvin.conjecture.engine.apengine.Operators.BinaryOperator;
import org.grinvin.conjecture.engine.apengine.Operators.Invariant;
import org.grinvin.conjecture.engine.apengine.Operators.UnaryOperator;

/**
 *
 * @author adpeeter
 */
public class LabeledTreeGenerator {
    
    //
    private TreeGenerator<LabeledBinaryTree> treeGenerator;
    
    //
    private LabeledBinaryTree workingTree;
    
    //
    private int mainInvariant;

    //
    private int nrOfInvariants;
    
    //
    private boolean[] takenInvariants;
    
    //
    private Invariant[] invariants;
    
    //
    private LabeledTreeGeneratorStateStack stateStack;
    
    //
    public LabeledTreeGenerator(int nrOfInvariants, int mainInvariant) {
        this(new TreeGenerator<LabeledBinaryTree>(new LabeledBinaryTreeFactory()), nrOfInvariants, mainInvariant);
        
    }
    
    //
    public LabeledTreeGenerator(TreeGenerator<LabeledBinaryTree> treeGenerator, int nrOfInvariants, int mainInvariant) {
        this.treeGenerator = treeGenerator;
        
        workingTree = null;
        takenInvariants = new boolean[nrOfInvariants];
        this.nrOfInvariants = nrOfInvariants;
        this.mainInvariant = mainInvariant;
        invariants = new Invariant[nrOfInvariants];
        for(int i=0;i<nrOfInvariants;i++) {
            invariants[i] = new Invariant(i);
        }
        stateStack = new LabeledTreeGeneratorStateStack();
        startLabelingTree();
    }
    
    
    private static class LabeledTreeGeneratorStateStack extends StateStack<LabeledTreeGeneratorState> {
        
        //
        public LabeledTreeGeneratorState emptyState() {
            return new LabeledTreeGeneratorState(null, 0, 0);
        }
        
        //
        public LabeledTreeGeneratorState[] createArray(int size) {
            return new LabeledTreeGeneratorState[size];
        }
        
        //
        private final void push(StateType type, int pos, int looppos) {
            if(top >= size) {
                super.extend();
            }
            LabeledTreeGeneratorState state = peek();
            top++;
            state.type = type;
            state.pos = pos;
            state.looppos = looppos;
        }
        
        //
        public final void pushRecurseState(int pos, int looppos) {
            push(StateType.RECURSE, pos, looppos);
        }
        
        //
        public final void pushBinaryState(int pos, int looppos) {
            push(StateType.BINARY, pos, looppos);
        }
        
        //
        public final void pushUnaryState(int pos, int looppos) {
            push(StateType.UNARY, pos, looppos);
        }
        
        //
        public final void pushInvariantState(int pos, int looppos) {
            push(StateType.INVARIANT, pos, looppos);
        }
        
        //
        public final void pushRemoveInvariantState(int pos, int looppos) {
            push(StateType.REMOVEINVARIANT, pos, looppos);
        }
        
    }
    
    //
    public boolean hasMore() {
        return !stateStack.empty();
    }
    
    //
    private enum StateType {
        RECURSE,
        BINARY,
        UNARY,
        INVARIANT,
        REMOVEINVARIANT;
    }

    //
    private static class LabeledTreeGeneratorState {
        private StateType type;
        private int pos;
        private int looppos;
        public LabeledTreeGeneratorState(StateType type, int pos, int looppos) {
            this.type = type;
            this.pos = pos;
            this.looppos = looppos;
        }
    }

    /**
     * Return the next {@link LabeledBinaryTree} or {@code null} when no more tree is available.
     */
    public LabeledBinaryTree nextLabeledTree() {

        while(hasMore() && (!label())) {
            if (!hasMore()) {
                startLabelingTree();
            }
        }
        
        return workingTree;
    }
    
    
    /**
     * Start labeling a blank generated tree.
     */
    private void startLabelingTree() {
        workingTree = treeGenerator.nextTree();
        
        prepareOrder(workingTree);
        
        Arrays.fill(takenInvariants, false);
        takenInvariants[mainInvariant] = true;
        
        assert stateStack.empty() : "The stack should be empty!";
        stateStack.pushRecurseState(0, 0);
    }

    //
    private boolean label() {
        
        LabeledTreeGeneratorState item = stateStack.pop();
        
        int position = item.pos;
        int looppos = item.looppos;
        
        switch(item.type) {
            case RECURSE:
                //label the next node in the list
                if (position >= order.length) {
                    // all nodes are labeled: we have a finished working tree
                    return true;
                } else {
                    switch (workingTree.childCount(order[position])) {
                        case 2:
                            stateStack.pushBinaryState(position, 0);
                            break;
                        case 1:
                            stateStack.pushUnaryState(position, 0);
                            break;
                        case 0:
                            stateStack.pushInvariantState(position, 0);
                            break;
                        default:
                            assert false : "Unexpected childcount: " + workingTree.childCount(order[position]);
                    }
                }
                break;
            case BINARY:
                BinaryOperator[] binops = BinaryOperator.values();
                if (looppos < binops.length) {
                    // make sure the left hand side of commutative operators is always smaller than the right hand side
                    if (binops[looppos].isCommutative() &&
                            (workingTree.toString(workingTree.leftChild(order[position])).compareTo(workingTree.toString(workingTree.rightChild(order[position]))) > 0)) {
                        stateStack.pushBinaryState(position, looppos + 1);
                    } else {
                        workingTree.labelNode(order[position], binops[looppos]);
                        stateStack.pushBinaryState(position, looppos + 1);
                        stateStack.pushRecurseState(position + 1, 0);
                    }
                }
                break;
            case UNARY:
                UnaryOperator[] unops = UnaryOperator.values();
                if (looppos < unops.length) {
                    workingTree.labelNode(order[position], unops[looppos]);
                    stateStack.pushUnaryState(position, looppos + 1);
                    stateStack.pushRecurseState(position + 1, 0);
                }
                break;
            case INVARIANT:
                if (looppos < nrOfInvariants) {
                    stateStack.pushInvariantState(position, looppos + 1);
                    if (!takenInvariants[looppos]) {
                        takenInvariants[looppos] = true;
                        workingTree.labelNode(order[position], invariants[looppos]);
                        stateStack.pushRemoveInvariantState(0, looppos);
                        stateStack.pushRecurseState(position + 1, 0);
                    }
                }
                break;
            case REMOVEINVARIANT:
                takenInvariants[looppos] = false;
                break;
            default:
                assert false : "Unexpected case: " + item.type;
        }
        return false;
    }

    //
    private int counter = 0;
    
    //
    private int[] order;

    /**
     * Prepare the order in which the nodes of the given {@link LabeledBinaryTree} will be labeled.
     * @param tree the {@link LabeledBinaryTree}
     */
    private void prepareOrder(LabeledBinaryTree tree) {
        counter = 0;
        order = new int[tree.getNodeCount()];
        prepareOrder(tree, 0);
    }
    
    /**
     * Prepare the order in which the nodes of the given {@link LabeledBinaryTree} will be labeled.
     * All nodes are traversed recursively.
     * @param tree the {@link LabeledBinaryTree}
     * @param parent the parent from which to start ordering
     */
    private void prepareOrder(LabeledBinaryTree tree, int parent) {
        for (int child : tree.children(parent)) {
            prepareOrder(tree, child);
        }
        order[counter] = parent;
        counter++;
    }
    
    
}