//==============================================================================
//	
//	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.math.BigInteger;
import java.util.ArrayList;
import java.util.Random;

/**
 * Implements a region representation by a box (hyper-rectangle).
 * This means that for each parameter we have a lower and upper bound, and
 * the region contains all points so that the corresponding dimensions are
 * (not strictly) between these lower and upper bounds.
 * 
 * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
 * @see BoxRegionFactory
 */
final class BoxRegion extends Region {
	/** used to produce random inner points of box regions */
	static Random random = new Random();
	
	/** regions are only to be split at longest side */
	static final int SPLIT_LONGEST = 1;
	/** regions are to be split at all sides on each split */
	static final int SPLIT_ALL = 2;
	
	/** lower bound for each parameter */
	private BigRational[] lower;
	/** upper bound for each parameter */
	private BigRational[] upper;
	
	// constructors
	
	/**
	 * Constructs a new box region.
	 * Does not assign lower and upper bounds, that is the regions is
	 * not direcly usable after construction.
	 *  
	 * @param factory factory this box region belongs to
	 */
	private BoxRegion(BoxRegionFactory factory)
	{
		this.factory = factory;
		lower = new BigRational[factory.numVariables()];
		upper = new BigRational[factory.numVariables()];
	}
	
	/**
	 * Constructs a new box region.
	 * 
	 * @param factory factory this box region belongs to
	 * @param lower lower bounds for each parameter
	 * @param upper upper bounds for each parameter
	 */
	BoxRegion(BoxRegionFactory factory, BigRational[] lower, BigRational[] upper)
	{
		this.factory = factory;
		this.lower = new BigRational[lower.length];
		this.upper = new BigRational[upper.length];
		System.arraycopy(lower, 0, this.lower, 0, lower.length);
		System.arraycopy(upper, 0, this.upper, 0, upper.length);
	}
	
	/**
	 * Copy constructor for box regions.
	 * For internal use, because regions are generally immutable, so that
	 * there is no need to have external copy constructors.
	 * 
	 * @param other region to copy from
	 */
	private BoxRegion(BoxRegion other)
	{
		this.factory = other.factory;
		this.lower = new BigRational[other.lower.length];
		this.upper = new BigRational[other.upper.length];
		System.arraycopy(other.lower, 0, this.lower, 0, other.lower.length);
		System.arraycopy(other.upper, 0, this.upper, 0, other.upper.length);		
	}
	
	/**
	 * Sets lower and upper bound of given parameter.
	 * 
	 * @param dim parameter to set bounds of
	 * @param lower new lower bound of parameter
	 * @param upper new upper bound of parameter
	 */
	private void setDimension(int dim, BigRational lower, BigRational upper)
	{
		this.lower[dim] = lower;
		this.upper[dim] = upper;
	}
	
	@Override
	int getDimensions()
	{
		return lower.length;
	}
	
	/**
	 * Get lower bound of given parameter in region.
	 * 
	 * @param dim parameter to get lower bound of
	 * @return lower bound of given parameter in region
	 */
	BigRational getDimensionLower(int dim)
	{
		return lower[dim];
	}

	/**
	 * Get upper bound of given parameter in region.
	 * 
	 * @param dim parameter to get lower bound of
	 * @return upper bound of given parameter in region
	 */	
	BigRational getDimensionUpper(int dim)
	{
		return upper[dim];
	}

	@Override
	public boolean equals(Object object) {
		if (!(object instanceof BoxRegion)) {
			return false;
		}
		
		BoxRegion other = (BoxRegion) object;
		
		if (this.getDimensions() != other.getDimensions()) {
			return false;
		}
		
		for (int i = 0; i < getDimensions(); i++) {
			if (!this.lower[i].equals(other.lower[i])) {
				return false;
			}
			if (!this.upper[i].equals(other.upper[i])) {
				return false;
			}
		}
		
		return true;
	}
	
	@Override
	public int hashCode()
	{
		int hash = 0;
		
		for (int i = 0; i < getDimensions(); i++) {
			hash = lower[i].hashCode() + (hash << 6) + (hash << 16) - hash;
			hash = upper[i].hashCode() + (hash << 6) + (hash << 16) - hash;
		}
		
		return hash;
	}
	
	/**
	 * Gets the central points of the region.
	 *
	 * @return point in the centre of the region
	 */
	Point getMidPoint()
	{
		BigRational[] point = new BigRational[lower.length];
		for (int dim = 0; dim < lower.length; dim++) {
			BigRational mid = lower[dim].add(upper[dim]).divide(2);
			point[dim] = mid;
		}
		return new Point(point);
	}
	
	/**
	 * Get volume of the region.
	 * The volumes of disjoint region which cover the whole parameter
	 * space sum up to 1. This implies that the volumes are normalised
	 * according to the upper and lower bounds of the parameters.
	 * 
	 * @return volume of this region
	 */
	@Override
	BigRational volume()
	{
		BigRational volume = BigRational.ONE;
		for (int dim = 0; dim < lower.length; dim++) {
			volume = volume.multiply(upper[dim].subtract(lower[dim]));
			volume = volume.divide(factory.sideWidth(dim));
		}
		return volume;
	}
	
	@Override
	boolean contains(Point point)
	{
		for (int dim = 0; dim < getDimensions(); dim++) {
			if (point.getDimension(dim).compareTo(lower[dim]) < 0) {
				return false;
			}
			if (point.getDimension(dim).compareTo(upper[dim]) > 0) {
				return false;
			}
		}
		return true;
	}
	
	@Override
	boolean contains(Region region)
	{
		BoxRegion other = (BoxRegion) region;
		for (int dim = 0; dim < getDimensions(); dim++) {
			if (other.lower[dim].compareTo(this.lower[dim]) == -1) {
				return false;
			}
			if (other.upper[dim].compareTo(this.upper[dim]) == +1) {
				return false;
			}
		}
		return true;
	}
	
	@Override
	public String toString() {
		StringBuilder builder = new StringBuilder();
		builder.append("(");
		for (int dim = 0; dim < getDimensions(); dim++) {
			builder.append("[");
			builder.append(lower[dim].doubleValue());
			builder.append(",");
			builder.append(upper[dim].doubleValue());
			builder.append("]");
			if (dim < getDimensions() - 1) {
				builder.append(",");
			}
		}
		builder.append(")");
		return builder.toString();
	}

	@Override
	RegionValues binaryOp(int op, StateValues values1, StateValues values2) {
		RegionValues result;
		if ((op == Region.EQ || op == Region.NE || op == Region.GT || op == Region.GE || op ==  Region.LT || op == Region.LE)) {
			result = cmpOp(op, values1, values2);
		} else {
			result = new RegionValues(factory);
			int numStates = values1.getNumStates();
			StateValues values = new StateValues(numStates, factory.getInitialState());
			for (int state = 0; state < numStates; state++) {
				if (op == Region.IMPLIES || op == Region.IFF || op == Region.OR || op == Region.AND) {
					boolean stateVal = booleanOp(op, values1.getStateValueAsBoolean(state), values2.getStateValueAsBoolean(state));
					values.setStateValue(state, stateVal);
				} else if (op == Region.PLUS || op == Region.MINUS || op == Region.TIMES || op == Region.DIVIDE) {
					Function stateVal = arithOp(op, values1.getStateValueAsFunction(state), values2.getStateValueAsFunction(state));
					values.setStateValue(state, stateVal);
				} else {
					throw new UnsupportedOperationException("operator not yet implemented for parametric analyses");
				}
			}
			result.add(this, values);
		}
		return result;
	}

	private RegionValues cmpOp(int op, StateValues op1, StateValues op2) {
		ConstraintChecker checker = factory.getConstraintChecker();
		RegionsTODO remaining = new RegionsTODO();
		remaining.add(this);
		BigRational requiredVolume = this.volume().multiply(BigRational.ONE.subtract(factory.getPrecision()));
		BigRational doneVolume = BigRational.ZERO;
		RegionValues result = new RegionValues(factory);
		Function lastFunction = null;
		while (doneVolume.compareTo(requiredVolume) == -1) {
			BoxRegion region = (BoxRegion) remaining.poll();
			StateValues newValues = new StateValues(op1.getNumStates(), factory.getInitialState());
			boolean allDecided = true;
			for (int state = 0; state < op1.getNumStates(); state++) {
				StateValue op1Val = op1.getStateValue(state);
				StateValue op2Val = op2.getStateValue(state);
				Function op1ValFn = op1Val instanceof Function ? (Function) op1Val : null;
				Function op2ValFn = op2Val instanceof Function ? (Function) op2Val : null;
				if (op == Region.EQ) {
					if (op1Val instanceof StateBoolean) {
						newValues.setStateValue(state, op1Val.equals(op2Val));						
					}
					else if (op1Val.equals(op2Val)) {
						newValues.setStateValue(state, true);			
					} else if (checker.check(region, op1ValFn.subtract(op2ValFn), true)) {
						newValues.setStateValue(state, false);	
					} else if (checker.check(region, op2ValFn.subtract(op1ValFn), true)) {
						newValues.setStateValue(state, false);	
					} else {
						allDecided = false;
						break;
					}
				} else if (op == Region.NE) {
					if (op1Val instanceof StateBoolean) {
						newValues.setStateValue(state, !op1Val.equals(op2Val));
					} else if (op1Val.equals(op2Val)) {
						newValues.setStateValue(state, false);
					} else if (checker.check(region, op1ValFn.subtract(op2ValFn), true)) {
						newValues.setStateValue(state, true);
					} else if (checker.check(region, op2ValFn.subtract(op1ValFn), true)) {
						newValues.setStateValue(state, true);
					} else {
						allDecided = false;
						break;
					}
				} else {
					boolean strict = op == Region.GT || op == Region.LT;
					Function cmpTrue = (op == Region.LT || op == Region.LE) ? op2ValFn.subtract(op1ValFn) : op1ValFn.subtract(op2ValFn);
					if (checker.check(region, cmpTrue, strict)) {
						newValues.setStateValue(state, true);
					} else {
						Function cmpFalse = (op == Region.LT || op == Region.LE) ? op1ValFn.subtract(op2ValFn) : op2ValFn.subtract(op1ValFn);
						if (checker.check(region, cmpFalse, !strict)) {
							newValues.setStateValue(state, false);	
						} else {
							allDecided = false;
							lastFunction = op2ValFn.subtract(op1ValFn);
							break;
						}
					}
				}
			}
			if (allDecided) {
				result.add(region, newValues);
				doneVolume = doneVolume.add(region.volume());
			} else {
				remaining.addAll(region.split(lastFunction));
			}
		}
		
		return result;
	}
	
	/**
	 * Performs given operation on two rational functions.
	 * 
	 * @param op operation to perform, see values in {@code Region}
	 * @param op1 first operand
	 * @param op2  second operand
	 * @return value of operation
	 */
	private Function arithOp(int op, Function op1, Function op2) {
		Function result = null;
		switch (op) {
		case Region.PLUS:
			result = op1.add(op2);
			break;
		case Region.MINUS:
			result = op1.subtract(op2);
			break;
		case Region.TIMES:
			result = op1.multiply(op2);
			break;
		case Region.DIVIDE:
			result = op1.divide(op2);
			break;
		default:
			throw new IllegalArgumentException("unsupported arithmetic operator number " + op);
		}
		return result;
	}

	/**
	 * Performs given operation on two booleans.
	 * 
	 * @param op operation to perform, see values in {@code Region}
	 * @param op1 first operand
	 * @param op2  second operand
	 * @return value of operation
	 */
	private boolean booleanOp(int op, boolean op1, boolean op2) {
		boolean result = false;
		
		switch (op) {
		case Region.IMPLIES:
			result = !op1 || op2;
			break;
		case Region.IFF:
			result = op1 == op2;
			break;
		case Region.OR:
			result = op1 || op2;
			break;
		case Region.AND:
			result = op1 && op2;
			break;
		default:
			throw new IllegalArgumentException("unsupported boolean operator number " + op);
		}
		return result;
	}
	
	/**
	 * Split region in longest dimension.
	 * 
	 * @return set of new regions covering same area
	 */
	private ArrayList<Region> splitLongest()
	{
		int longestSide = -1;
		BigRational longestLength = BigRational.ZERO;
		for (int side = 0; side < lower.length; side++) {
			BigRational sideLength = upper[side].subtract(lower[side]);
			if (sideLength.compareTo(longestLength) == 1) {
				longestSide = side;
				longestLength = sideLength;
			}
		}
		
		ArrayList<Region> result = new ArrayList<Region>();
		BoxRegion region1 = new BoxRegion(this);
		BoxRegion region2 = new BoxRegion(this);
		BigRational mid = (lower[longestSide].add(upper[longestSide])).divide(2);
		region1.upper[longestSide] = mid;
		region2.lower[longestSide] = mid;
		result.add(region1);
		result.add(region2);
				
		return result;
	}
	
	/**
	 * Split region in all dimensions.
	 * 
	 * @return set of new regions covering same area
	 */
	private ArrayList<Region> splitAll()
	{
		ArrayList<Region> result = new ArrayList<Region>();
		final int numParts = 2;
		final int numNewRegions = (int) Math.pow(numParts, lower.length);
		BigRational[] newLower = new BigRational[lower.length];
		BigRational[] newUpper = new BigRational[upper.length];
		for (int newRegionNr = 0; newRegionNr < numNewRegions; newRegionNr++) {
			int regionRest = newRegionNr;
			for (int var = 0; var < lower.length; var++) {
				int lowerPart = regionRest % numParts;
				regionRest /= numParts;
				BigRational partLength = upper[var].subtract(lower[var]).divide(numParts);
				newLower[var] = lower[var].add(partLength.multiply(lowerPart));
				newUpper[var] = lower[var].add(partLength.multiply(lowerPart + 1));
			}
			result.add(new BoxRegion((BoxRegionFactory) factory, newLower, newUpper));
		}
		return result;
	}
	
	@Override
	ArrayList<Region> split(Function constraint)
	{
		// TODO could implement more clever splitting using constraints
		if (((BoxRegionFactory) factory).getSplitMethod() == SPLIT_LONGEST) {
			return splitLongest();
		} else if (((BoxRegionFactory) factory).getSplitMethod() == SPLIT_ALL) {
			return splitAll();
		} else {
			throw new RuntimeException();
		}
	}	
	
	@Override
	ArrayList<Point> specialPoints()
	{
		ArrayList<Point> result = new ArrayList<Point>();
		int numEdges = (int) Math.pow(2, lower.length);
		for (int edgeNr = 0; edgeNr < numEdges; edgeNr++) {
			int regionRest = edgeNr;
			BigRational[] point = new BigRational[lower.length];
			for (int dim = 0; dim < lower.length; dim++) {
				boolean useLower = ( 0 == (regionRest % 2));
				regionRest /= 2;
				if (useLower) {
					point[dim] = lower[dim];
				} else {
					point[dim] = upper[dim];					
				}
			}
			result.add(new Point(point));
		}
		return result;
	}
	
	@Override
	Point randomPoint()
	{
		BigRational[] point = new BigRational[lower.length];
		BigInteger maxInt = new BigInteger(Long.toString((long) Math.pow(2, 60))); 
		for (int dim = 0; dim < lower.length; dim++) {
			BigInteger rndInt = new BigInteger(60, random);
			BigRational rndRat = new BigRational(rndInt, maxInt);
			rndRat = lower[dim].add(upper[dim].subtract(lower[dim]).multiply(rndRat));
			point[dim] = rndRat;
		}
		
		return new Point(point);
	}

	@Override
	BoxRegion conjunct(Region region) {
		BoxRegion other = (BoxRegion) region;
		
		BoxRegion result = new BoxRegion((BoxRegionFactory) factory);
		for (int dim = 0; dim < lower.length; dim++) {
			if (this.upper[dim].compareTo(other.lower[dim]) <= 0) {
				return null;
			}
			if (this.lower[dim].compareTo(other.upper[dim]) >= 0) {
				return null;
			}
			BigRational newLower = this.lower[dim].max(other.lower[dim]);
			BigRational newUpper = this.upper[dim].min(other.upper[dim]);
			if (newLower.equals(newUpper)) {
				return null;
			}
			result.setDimension(dim, newLower, newUpper);
		}
		return result;
	}

	/**
	 * Checks whether this region is adjacent to another region in given dimension.
	 * In this case, both can be glued by @{code glue}.
	 * 
	 * @param other region to check whether adjacent in given dimension
	 * @param adjDim dimension where to check adjacency
	 * @return true iff regions are adjacent in given dimension
	 */
	private boolean adjacent(Region region, int adjDim)
	{
		BoxRegion other = (BoxRegion) region;
		for (int dim = 0; dim < this.getDimensions(); dim++) {
			if (dim != adjDim) {
				if (!this.getDimensionLower(dim).equals(other.getDimensionLower(dim))) {
					return false;
				}
				if (!this.getDimensionUpper(dim).equals(other.getDimensionUpper(dim))) {
					return false;
				}
			}
		}
		
		return this.getDimensionUpper(adjDim).equals(other.getDimensionLower(adjDim));
	}

	@Override
	boolean adjacent(Region region)
	{
		BoxRegion other = (BoxRegion) region;
		for (int dim = 0; dim < getDimensions(); dim++) {
			if (adjacent(other, dim)) {
				return true;
			}
		}
		
		return false;
	}
	
	@Override
	Region glue(Region region) {
		BoxRegion other = (BoxRegion) region;
		BoxRegion result = new BoxRegion((BoxRegionFactory) this.getFactory());
		
		for (int dim = 0; dim < result.getDimensions(); dim++) {
			result.setDimension(dim, this.getDimensionLower(dim), other.getDimensionUpper(dim));
		}

		return result;
	}
}