/* APEngine.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;

import org.grinvin.conjecture.engine.apengine.ExpressionBuilder;
import org.grinvin.conjecture.engine.apengine.LabeledBinaryTree;
import org.grinvin.conjecture.engine.apengine.LabeledTreeGenerator;
import org.grinvin.conjecture.engine.apengine.Operators;
import org.grinvin.expr.Compound;
import org.grinvin.expr.Expression;
import org.grinvin.expr.StandardOperator;
import org.grinvin.invariants.InvariantExpressionNode;
import org.grinvin.invariants.InvariantManager;
import org.grinvin.invariants.InvariantValue;
import org.grinvin.invariants.UnknownInvariantException;
import org.grinvin.invariants.values.NumericValue;

/**
 * Proof of concept implementation of {@link Engine}.
 *<p>
 * <b>Note:</b> This class is not thread safe.
 */
public class APEngine extends AbstractInequalityEngine {
    
    //
    private LabeledTreeGenerator labeledTreeGenerator;
    
    //
    private final ExpressionBuilder expressionBuilder;
    
    //
    public APEngine() {
        this.expressionBuilder = new ExpressionBuilder ();
    }
    
    //
    public Expression run(InvariantValue [][] values) {
        
        try {
            Thread.sleep(2000);
        } catch (InterruptedException e) {
            //
        }
        
        int numberOfInvariants = values[0].length;
        int indexMainInvariant = 0;
        
        InvariantExpressionNode[] invariants = new InvariantExpressionNode[numberOfInvariants];
        try {
            for (int i=0; i < numberOfInvariants; i++){
                invariants[i] = InvariantManager.getInstance().getInvariantExpressionNode(values[0][i].getInvariant().getId());
                if(invariants[i].equals(InvariantManager.getInstance().getInvariant(getMainInvariant().getId())))
                    indexMainInvariant = i;
            }
        } catch (UnknownInvariantException ex) {
            throw new RuntimeException("Unexpected exception", ex);
        }
        
        labeledTreeGenerator = new LabeledTreeGenerator(numberOfInvariants, indexMainInvariant);
        
        
        //LabeledBinaryTree resultTree = nextCorrectLabeledTree(values);
        LabeledBinaryTree resultTree = bestEffortTree(values, indexMainInvariant);
        Expression expression = expressionBuilder.buildExpression(resultTree, invariants);
        return new Compound (StandardOperator.LE, invariants[indexMainInvariant], expression);
    }
    
    //
    public LabeledBinaryTree nextCorrectLabeledTree(InvariantValue [][] values, int indexMainInvariant) {
        LabeledBinaryTree result = labeledTreeGenerator.nextLabeledTree();
        while ((result != null) && (!check(result, values, indexMainInvariant))) {
            result = labeledTreeGenerator.nextLabeledTree();
        }
        return result;
    }
    
    //
    public LabeledBinaryTree bestEffortTree(InvariantValue [][] values, int indexMainInvariant) {
        
        int numberOfGraphs = values.length;
        
        LabeledBinaryTree tree = nextCorrectLabeledTree(values, indexMainInvariant);
        double error = valueError(tree, values, indexMainInvariant);
        
        LabeledBinaryTree bestTree = tree.clone();
        double bestError = error;
        
        //System.out.println(treeError(tree) + " " + numberOfGraphs + " " + (treeError(tree) * numberOfGraphs) + " " + tree + " " + error + " " + bestError);
        while(treeError(tree) * numberOfGraphs < bestError) {
            tree = nextCorrectLabeledTree(values, indexMainInvariant);
            error = valueError(tree, values, indexMainInvariant);
            //System.out.println(treeError(tree) + " " + numberOfGraphs + " " + (treeError(tree) * numberOfGraphs) + " " + tree + " " + error + " " + bestError);
            if(error < bestError) {
                bestTree = tree.clone();
                bestError = error;
            }
        }
        //System.out.println(treeError(bestTree) + " " + numberOfGraphs + " " + (treeError(bestTree) * numberOfGraphs) + " " + bestTree + " " + bestError);
        return bestTree;
    }
    
    //
    private int treeError(LabeledBinaryTree tree) {
        return (1 << (  2 * tree.getBinaryCount() + tree.getUnaryCount()));
    }
    
    //
    private double valueError(LabeledBinaryTree tree, InvariantValue[][] values, int indexMainInvariant) {
        double worst = 0;
        int worstcount = 0;
        int numberOfGraphs = values.length;
        double result = treeError(tree) * numberOfGraphs;
        for (InvariantValue [] valuelist : values) {
            double sum = ((NumericValue)valuelist[indexMainInvariant]).asDouble() - evaluate(valuelist, tree, 0);
            sum = sum*sum;
            if (Double.isNaN(sum) || Double.isInfinite(sum)) {
                sum = 0;
                worstcount++;
                if (worstcount >= (numberOfGraphs * 2 / 3)) {
                    //return result + (worstcount * worst * 2);
                    return Double.MAX_VALUE;
                }
            }
            if (sum > worst) {
                worst = sum;
            }
            result = result + sum;
        }
        return result + (worstcount * worst * 2);
    }
    
    //
    public boolean check(LabeledBinaryTree tree, InvariantValue[][] values, int indexMainInvariant) {
        boolean result = true;
        for (InvariantValue [] valuelist : values) {
            if (((NumericValue)valuelist[indexMainInvariant]).asDouble() > evaluate(valuelist, tree, 0))
                result = false;
        }
        return result;
    }
    
    //
    private double evaluate(InvariantValue[] valuelist, LabeledBinaryTree tree, int parent) {
        double result = 0;
        if (tree.hasRightChild(parent)) {
            Operators.BinaryOperator binop = (Operators.BinaryOperator)tree.operators[parent];
            result = binop.eval(evaluate(valuelist, tree, tree.leftChild(parent)), evaluate(valuelist, tree, tree.rightChild(parent)));
        } else if (tree.hasLeftChild(parent)) {
            Operators.UnaryOperator monop = (Operators.UnaryOperator)tree.operators[parent];
            result = monop.eval(evaluate(valuelist, tree, tree.leftChild(parent)));
        } else {
            Operators.Invariant inv = (Operators.Invariant)tree.operators[parent];
            result = ((NumericValue)valuelist[inv.number]).asDouble();
        }
        return result;
    }
    
}