//==============================================================================
//	
//	Copyright (c) 2013-
//	Authors:
//	* Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM 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.
//	
//	PRISM 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.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package param;

import java.util.ArrayList;

import edu.jas.arith.BigInteger;
import edu.jas.poly.ExpVector;
import edu.jas.poly.GenPolynomial;
import edu.jas.poly.Monomial;
import edu.jas.ufd.Quotient;

/**
 * Rational function representation using the Java Algebra System (JAS).
 * Functions are stored in the form {@code num / den}. JAS takes care that
 * {@code num} and {@code den} stay coprime. This decreases the memory
 * needed to represent a function, allows for easier comparism, etc. On the
 * other hand, the cancellation algorithm is expensive. The function factory
 * class used with these functions is {@code JasFunctionFactory}.
 * 
 * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
 * @see <a href="http://krum.rz.uni-mannheim.de/jas/">http://krum.rz.uni-mannheim.de/jas/</a>
 * @see Function
 * @see JasFunctionFactory
 */
final class JasFunction extends Function {
	/** JAS object the function is wrapping */
	private Quotient<BigInteger> jas;
	/** numerator of function (stored if needed) */
	Polynomial num;
	/** denominator of function (stored if needed) */
	Polynomial den;
	/** type of function (rational function, infinity, etc.) */
	int type;
	final static int NORMAL = 0;
	final static int INF = 1;
	final static int MINF = 2;
	final static int NAN = 3;
	
	// constructors
	
	/**
	 * Creates a new JAS function.
	 * 
	 * @param functionContext function context of this function
	 * @param jas JAS object this function object is wrapping
	 * @param type type of function represented
	 */
	JasFunction(JasFunctionFactory functionContext, Quotient<BigInteger> jas, int type) {
		super(functionContext);
		this.jas = jas;
		this.num = null;
		this.den = null;
		this.type = type;
	}

	@Override
	public String toString()
	{
		if (isNaN()) {
			return "NaN";
		} else if (isInf()) {
			return "Inf";
		} else if (isMInf()) {
			return "MInf";
		}
		return jas.toString();
	}
	
	@Override
	public boolean equals(Object obj) {
		if (!(obj instanceof JasFunction)) {
			return false;
		}
		JasFunction function = (JasFunction) obj;
		if (isNaN()) {
			return function.isNaN();
		}
		if (isInf()) {
			return function.isInf();
		}
		if (isMInf()) {
			return function.isMInf();
		}
		return jas.equals(function.jas);
	}
	
	@Override
	public int hashCode() {
		return jas.hashCode();
	}
	
	/**
	 * Returns JAS object this function is wrapping.
	 * 
	 * @return JAS object this function is wrapping
	 */
	Quotient<BigInteger> getJas()
	{
		return jas;
	}
	
	@Override
	public Function add(Function other)
	{
		if (this.isNaN() || other.isNaN()) {
			return factory.getNaN();
		}
		if (this.isInf() || other.isInf()) {
			if (this.isMInf() || other.isMInf()) {
				return factory.getZero();
			}
			return factory.getInf();
		}
		if (this.isMInf() || other.isMInf()) {
			return factory.getMInf();
		}
		return new JasFunction((JasFunctionFactory) factory, jas.sum(((JasFunction)other).jas), NORMAL);
	}

	@Override
	public Function negate()
	{
		if (this.isNaN()) {
			return factory.getNaN();			
		}
		if (this.isInf()) {
			return factory.getMInf();
		}
		if (this.isMInf()) {
			return factory.getMInf();			
		}
		return new JasFunction((JasFunctionFactory) factory, jas.negate(), NORMAL);
	}
	
	@Override
	public Function multiply(Function other)
	{
		if (this.isNaN() || other.isNaN()) {
			return factory.getNaN();
		}
		if (this.isZero() || other.isZero()) {
			return factory.getZero();
		}
		if (this.isInf() || other.isInf()) {
			if (this.isMInf() || other.isMInf()) {
				return factory.getMInf();
			} else {
				return factory.getInf();
			}
		}
		return new JasFunction((JasFunctionFactory) factory, jas.multiply(((JasFunction) other).jas), NORMAL);		
	}
	
	@Override
	public Function divide(Function other)
	{
		if (this.isNaN() || other.isNaN()) {
			return factory.getNaN();
		}
		if (other.isZero()) {
			if (this.isZero()) {
				return factory.getNaN();
			} else {
				return factory.getInf();
			}
		}
		if (this.isZero()) {
			return factory.getZero();
		}
		return new JasFunction((JasFunctionFactory) factory, jas.divide(((JasFunction) other).jas), NORMAL);
	}
	
	@Override
	public Function star()
	{
		if (this.isNaN()) {
			return factory.getNaN();
		}
		Quotient<BigInteger> one =  ((JasFunctionFactory) factory).getJasQuotRing().getONE();
		Quotient<BigInteger> result = one.subtract(jas);
		result = one.divide(result);
		return new JasFunction((JasFunctionFactory) factory, result, NORMAL);
	}

	/**
	 * Transforms a JAS polynomial to a Polynomial object.
	 * 
	 * @param j JAS polynomial
	 * @return polynomial of Polynomial class
	 */
	private Polynomial jasToPoly(GenPolynomial<BigInteger> j)
	{
		int numVariables = j.numberOfVariables();
		Polynomial result = new Polynomial(numVariables, j.length());
		for (Monomial<BigInteger> jasMono : j) {
			java.math.BigInteger coeff = (jasMono.coefficient()).getVal();
			ExpVector jasExpo = jasMono.exponent();
			ArrayList<Integer> expo = new ArrayList<Integer>();
			for (int var = 0; var < numVariables; var++) {
				expo.add((int)jasExpo.getVal(var));
			}
			result.addTerm(coeff, expo);
		}
		
		return result;
	}
	
	@Override
	public Function toConstraint() {
		if (isNaN() || isInf() || isMInf()) {
			return this;
		}
		if (num == null) {
			num = jasToPoly(jas.num);
		}
		if (den == null) {
			den = jasToPoly(jas.den);
		}
		BigRational[] offset = new BigRational[factory.getNumVariables()]; 
		for (int dim = 0; dim < factory.getNumVariables(); dim++) {
			offset[dim] = factory.getUpperBound(dim).subtract(factory.getLowerBound(dim));
		}
		BigRational evaluated = BigRational.ZERO;
		while (evaluated.isZero() || evaluated.isSpecial()) {
			for (int dim = 0; dim < factory.getNumVariables(); dim++) {
				offset[dim] = offset[dim].divide(2);
			}
			BigRational[] point = new BigRational[factory.getNumVariables()];
			for (int dim = 0; dim < factory.getNumVariables(); dim++) {
				point[dim] = factory.getLowerBound(dim).add(offset[dim]);
			}
			evaluated = den.evaluate(new Point(point), false);
		}
		if (evaluated.signum() == -1) {
			return new JasFunction((JasFunctionFactory) factory, jas.multiply(jas.den).negate(), NORMAL);
		} else {
			return new JasFunction((JasFunctionFactory) factory, jas.multiply(jas.den), NORMAL);
		}
	}

	@Override
	public BigRational evaluate(Point point, boolean cancel) {
		if (isNaN()) {
			return BigRational.NAN;
		} else if (isInf()) {
			return BigRational.INF;
		} else if (isMInf()) {
			return BigRational.MINF;
		}
		if (num == null) {
			num = jasToPoly(jas.num);
		}
		if (den == null) {
			den = jasToPoly(jas.den);
		}
		if (isNaN()) {
			return BigRational.NAN;
		}
		return num.evaluate(point, cancel).divide(den.evaluate(point, cancel), cancel);
	}

	@Override
	public BigRational evaluate(Point point) {
		return evaluate(point, true);
	}
	
	@Override
	public boolean check(Point point, boolean strict)
	{
		BigRational value = evaluate(point, false);
		int compare = value.signum();
		return strict ? (compare > 0) : (compare >= 0);
	}

	@Override
	public BigRational asBigRational() {
		if (isNaN()) {
			return BigRational.NAN;
		} else if (isInf()) {
			return BigRational.INF;
		} else if (isMInf()) {
			return BigRational.MINF;
		}
		BigRational[] point = new BigRational[factory.getNumVariables()];
		for (int dim = 0; dim < factory.getNumVariables(); dim++) {
			point[dim] = new BigRational(0);
		}
		return evaluate(new Point(point));
	}

	@Override
	public boolean isNaN() {
		return type == NAN;
	}

	@Override
	public boolean isInf() {
		return type == INF;
	}

	@Override
	public boolean isMInf() {
		return type == MINF;
	}

	@Override
	public boolean isOne() {
		if (type != NORMAL) {
			return false;
		}
		return jas.isONE();
	}

	@Override
	public boolean isZero() {
		if (type != NORMAL) {
			return false;
		}
		return jas.isZERO();
	}

	@Override
	public boolean isConstant()
	{
		// inf, NaN are constant
		if (type != NORMAL)
			return true;

		// special handling for ZERO, as jas.isConstant() returns false
		// for zero...
		if (jas.isZERO()) {
			return true;
		}

		return jas.isConstant();
	}


}
