/* 
 * Kodkod -- Copyright (c) 2005-2011, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.engine.bool;

import kodkod.engine.CapacityExceededException;
import kodkod.util.ints.Ints;




/** 
 * Stores information about the size of a matrix.  Specifically,
 * for an n-dimensional matrix n, a Dimensions object is abstractly
 * a vector consisting of n integers; the ith integer in the vector
 * represents the size of the ith dimension of a matrix.
 * 
 * @specfield n: int
 * @specfield dimensions: [0..n) -> one int
 * @specfield capacity: dimensions[0] x ... x dimensions[n-1]
 * @invariant n > 0
 *
 * @author Emina Torlak 
 */
public abstract class Dimensions {
	private final int capacity;
	
	/**
	 * Constructs a Dimensions with the given capacity.
	 */
	private Dimensions(int capacity) { 
		this.capacity = capacity;
	}
	
	/**  
	 * Returns a new Dimensions object with n dimensions, each of
	 * which has the specified size.
	 * 
	 * @return {d: Dimensions | d.n = n && d.dimensions[int] = size }
	 * @throws IllegalArgumentException  n < 1 || size < 1
	 */
	public static Dimensions square(int size, int n) {
		if (n < 1 || size < 1) throw new IllegalArgumentException("n < 1 || size < 1");
		return new Square(n, size);
	}
	
	/**  
	 * Constructs a new Dimensions object with the given dimensions.
	 * 
	 * @return {d: Dimensions | d.n = dimensions.length && d.dimensions = dimensions }
	 * @throws NullPointerException  dimensions = null
	 * @throws IllegalArgumentException  dimensions.length = 0 || 
	 *                                    some i: [0..dimensions.n) | dimensions[i] < 1
	 */
	public static Dimensions rectangular(int[] dimensions) {
		if (dimensions.length==0) throw new IllegalArgumentException("n=0.");
		long capacity = 1;
		int size = dimensions[0];
		for (int i = 0; i < dimensions.length; i++) {
			if (dimensions[i] < 1) throw new IllegalArgumentException("Invalid dimension: " + dimensions[i]);
			capacity *= dimensions[i];
			if (size!=dimensions[i]) size = 0;
		}
		if (size>0) {
			return new Square(dimensions.length, size);
		} else {
			final int[] dims = new int[dimensions.length];
			System.arraycopy(dimensions, 0, dims, 0, dimensions.length);
			return new Rectangle(dims, capacity);
		}
	}
	
	/**
	 * Returns the capacity of this.
	 * @return this.capacity
	 */
	public final int capacity() { return capacity; }
	
	/**
	 * Returns the size of the ith dimensions
	 * @return this.dimensions[i]
	 * @throws ArrayIndexOutOfBoundsException  i < 0 || i >= this.capacity
	 */
	public abstract int dimension(int i);
	
	/**
	 * Returns the number of dimensions in this Dimensions object.
	 * @return this.n
	 */
	public abstract int numDimensions();
	
	/**
	 * Returns true if this represents the dimensions of a square matrix;
	 * otherwise returns false.
	 * 
	 * @return all i, j: [0..capacity) | this.dimensions[i] = this.dimensions[j]
	 */
	public abstract boolean isSquare();
	
	/**
	 * Returns true if the dimensions data in this object is homogeneous
	 * from start, inclusive, to end, exclusive.
	 * @return some x: int | this.dimensions[start..end) = x
	 */
	abstract boolean isSquare(int start, int end);
	
	/**
	 * Fills the destination array, beginning at destPos, with the dimension data 
	 * from this Dimensions object, beginning at srcPos. The number of components copied 
	 * is equal to the length argument. The dimensions at positions srcPos through srcPos+length-1 
	 * are copied into positions destPos through destPos+length-1, respectively, of the destination 
	 * array.
	 * @ensures dest[destPos..destPos+length) = this.dimensions[srcPos..srcPos+length)
	 */
	abstract void copy(int srcPos, int[] dest, int destPos, int length);
	
	/**
	 * Returns the dimensions of a matrix that would result from multiplying a 
	 * matrix of dimensions given by this by a matrix whose dimensions are 
	 * specified by dim. 
	 * 
	 * @return { d: Dimensions | d.n = this.n + dim.n - 2 &&
	 *                           (all i: [0..this.n-1) | d.dimensions[i] = this.dimensions[i]) &&
	 *                           (all i: [this.n-1..d.n) | d.dimensions[i] = dim.dimensions[i-this.n+1])}
	 * @throws IllegalArgumentException  this.n + dim.n < 3 || this.dimensions[n-1] != dim.dimensions[0]
	 */
	public final Dimensions dot(Dimensions dim) {
		final int n0 = numDimensions(), n1 = dim.numDimensions();
		final int n = n0 + n1 - 2, drop = dim.dimension(0);
		if (n == 0  || dimension(n0-1) != drop) {
			throw new IllegalArgumentException();
		}
		
		if (isSquare(0,n0-1) && dim.isSquare(1,n1) && 
				(n0==1 || n1==1 || dimension(0)==dim.dimension(1))) {
			return new Square(n, dimension(0));
		} else {
			final int[] dims = new int[n];
			copy(0, dims, 0, n0-1);
			dim.copy(1, dims, n0-1, n1-1);
			return new Rectangle(dims, (capacity*dim.capacity) / (drop*drop));
		}
	}
	
	/**
	 * Returns the dimensions of a matrix that would result from taking the cross 
	 * product of a matrix of dimensions given by this and a matrix whose dimensions are 
	 * specified by dim. 
	 * 
	 * @return { d: Dimensions | d.n = this.n + dim.n &&
	 *                           (all i: [0..this.n) | d.dimensions[i] = this.dimensions[i]) &&
	 *                           (all i: [this.n..d.n) | d.dimensions[i] = dim.dimensions[i-this.n])}
	 */
	public final Dimensions cross(Dimensions dim) {
		final int n0 = numDimensions(), n1 = dim.numDimensions();
		if (isSquare() && dim.isSquare() && dimension(0)==dim.dimension(0))
			return new Square(n0+n1, dimension(0));
		else {
			final int[] dims = new int[n0+n1];
			copy(0, dims, 0, n0);
			dim.copy(0, dims, n0, n1);
			return new Rectangle(dims, (long)capacity*(long)dim.capacity);
		}
	}
	
	
	/**
	 * Returns the transpose of these dimensions.
	 * 
	 * @return { d: Dimensions | d.n = 2 && d.dimensions[0] = this.dimensions[1] &&
	 *                           d.dimensions[1] = this.dimensions[0] }
	 * @throws UnsupportedOperationException  this.n != 2
	 */
	public abstract Dimensions transpose();
	
	/**
	 * @return true if index is positive and less than bound.
	 */
	private static boolean positiveBounded(int index, int bound) {
		return 0 <= index && index < bound;
	}
	
	/**
	 * Returns true if index is a valid flat index for a matrix with 
	 * these dimensions;  otherwise returns false.
	 * 
	 * @return 0 <= i < this.capacity
	 */
	public final boolean validate(int index) {
		return positiveBounded(index, capacity);
	}
	
	/**
	 * Returns true if index is a valid vector index for a matrix
	 * with these dimensions; otherwise returns false.
	 * 
	 * @return index.length = n && 
	 *         (all i: [0..this.capacity) | 0 <= index[i] < this.dimensions[i])
	 * @throws NullPointerException  index = null
	 */
	public final boolean validate(int[] index) {
		final int length = numDimensions();
		if (index.length != length)  return false;
		for (int i = 0; i < length; i++) {
			if (!positiveBounded(index[i], dimension(i))) return false;
		}
		return true;
	}
	
	/**
	 * Converts an integer index into a matrix with these dimensions into a vector index.
	 * The effect of this method is the same as calling 
	 * this.convert(index, new int[this.numDimensions()]).
	 * @return an array of ints that represents a vector index corresponding to the specified 
	 * integer index into a this.dimensions[0]x...xthis.dimensions[n-1] matrix
	 * @throws IndexOutOfBoundsException  !validate(index)
	 */
	public final int[] convert(int index) {
		final int[] vector = new int[numDimensions()];
		convert(index, vector);
		return vector;
	}
	
	/**
	 * Converts an integer index into a matrix with these dimensions into a vector index, 
	 * and stores the result in the provided array.  This method requires that
	 * the array argument have at least this.n cells, which are used to store the
	 * vector representation of the given index.  The contents of the cells of <code>vectorIndex</code> 
	 * beyond the first this.n cells are left unchanged. 
	 * @requires vectorIndex.length <= this.n
	 * @ensures the first this.numDimensions entries of <code>vectorIndex</code> contain 
	 * the vector index representation of the specified integer index into a 
	 * this.dimensions[0]x...xthis.dimensions[n-1] matrix
	 * @throws NullPointerException  vectorIndex = null
	 * @throws IllegalArgumentException  vectorIndex.length < this.numDimensions
	 * @throws IndexOutOfBoundsException  !validate(index)
	 */
	public final void convert(int index, int[] vectorIndex) {
		final int length = numDimensions();	
		if (vectorIndex.length < length)
			throw new IllegalArgumentException("arrayIndex.length<this.numDimensions");
		if (!validate(index)) 
			throw new IndexOutOfBoundsException("index");    
		int conversionFactor = capacity;
		int remainder = index;
		for (int i = 0; i < length; i++) {
			conversionFactor = conversionFactor / dimension(i);
			vectorIndex[i] = remainder / conversionFactor;
			remainder = remainder % conversionFactor;
		}
	}
	
	/**
	 * Converts the first this.n positions of the given vector index 
	 * into an integer index.
	 * 
	 * @return an integer index corresponding to the first this.numDimensions positions of the specified 
	 * vector index into a this.dimensions[0]x...xthis.dimensions[n-1] matrix
	 * @throws NullPointerException  index == null
	 * @throws IllegalArgumentException  index.length < this.n
	 * @throws IndexOutOfBoundsException  some i: [0..n) | index[i] < 0 || 
	 *                                                      index[i] >= this.dimensions[i]
	 */
	public final int convert(int[] vectorIndex) {
		final int length = numDimensions();
		if (vectorIndex.length < length) {
			throw new IllegalArgumentException("index.length < this.n");
		}
		int intIndex = 0;
		int conversionFactor = capacity;
		for(int i = 0; i < length; i++) {
			int dim = dimension(i);
			if (!positiveBounded(vectorIndex[i], dim)) throw new IndexOutOfBoundsException("index["+i+"]");    
			conversionFactor = conversionFactor / dim;
			intIndex += conversionFactor * vectorIndex[i];
		}
		return intIndex;
	}
	
	/**
	 * @see java.lang.Object#toString()
	 */
	public String toString() {
		StringBuilder buffer = new StringBuilder("[ ");
		for (int i = 0; i < numDimensions(); i++) {
			buffer.append(dimension(i));
			buffer.append(" ");
		}
		buffer.append("]");
		return buffer.toString();
	}
	
	/**
	 * Represents a Dimensions object whose dimensions are all of the 
	 * same size. 
	 */
	private static final class Square extends Dimensions {
		private final int n, size;
		/**  
		 * Constructs a new Dimensions object with n dimensions, each of
		 * which has the specified size.
		 * 
		 * @ensures this.n' = n && this.dimensions[int] = size
		 * @requires size > 0 && n > 0
		 * @throws IllegalArgumentException  n < 1 || size < 1
		 */
		Square(int n, int size) {
			super(capacity(n, size));	
			this.size = size;
			this.n = n;
		}
		
		static int capacity(int n, int size) { 
			final long cap = Math.round(Math.pow(size,n));
			if (cap>Integer.MAX_VALUE || cap<=0) 
				throw new CapacityExceededException("Matrix too large: requested capacity of " + cap, Ints.nCopies(n, size));
			return (int)cap;
		}
		
		@Override
		void copy(int srcPos, int[] dest, int destPos, int length){
			if (srcPos < 0 || length < 0 || srcPos+length > n) throw new ArrayIndexOutOfBoundsException();
			while(srcPos++ < length) {
				dest[destPos++] = size;
			}
		}
		
		@Override
		boolean isSquare(int start, int end) {
			if (start <= end && start >= 0 && end <= n) {
				return true;
			}
			throw new ArrayIndexOutOfBoundsException();
		}
		
		@Override
		public int numDimensions() { return n; }
		
		@Override
		public int dimension(int i) {
			if (!positiveBounded(i,n)) throw new ArrayIndexOutOfBoundsException();
			return size;
		}
		
		@Override
		public boolean isSquare() { return true; }
		
		@Override
		public Dimensions transpose() {
			if (numDimensions() != 2) throw new UnsupportedOperationException("n!=2");
			return this;
		}
		
		/**
		 * Returns true if the given object is logically equivalent to this; 
		 * otherwise returns false.
		 * 
		 * @return this.dimensions = o.dimensions
		 */
		public boolean equals(Object o) {
			if (o instanceof Square) {
				final Square s = (Square) o;
				return n==s.n && size==s.size;
			}
			return false;
		}
		
		public int hashCode() {
			return n ^ size;
		}
		
	}
	
	/**
	 * Represents a Dimensions object with at least two dimensions of different size.
	 */
	private static final class Rectangle extends Dimensions {
		private final int[] dimensions;
		
		
		/**  
		 * Constructs a new Dimensions object with the given dimensions.
		 * 
		 * @ensures this.n' = dimensions.length && this.dimensions' = dimensions
		 * @requires - dimensions.length > 0 && 
		 *             (all i: [0..dimensions.n) | dimensions[i] > 0) &&
		 *             (some i, j: [0..dimensions.n) | dimensions[i] != dimensions[j]) &&
		 *             capacity = dimensions[0]*dimensions[1]*...*dimensions[dimensions.length-1] 
		 */
		Rectangle(int[] dims, long capacity) {
			super((int)capacity);
			if (capacity>Integer.MAX_VALUE || capacity<=0) 
				throw new CapacityExceededException("Matrix too large: requested capacity of " + capacity, Ints.asIntVector(dims));
			this.dimensions = dims;
		}
				
		@Override
		void copy(int srcPos, int[] dest, int destPos, int length){
			System.arraycopy(dimensions, srcPos, dest, destPos, length);
		}
		
		@Override
		boolean isSquare(int start, int end) {
			for(int i = start + 1; i < end; i++) {
				if (dimensions[i-1] != dimensions[i]) return false;
			}
			return true;
		}
		
		@Override
		public boolean isSquare() { return false; }
		
		@Override
		public int dimension(int i) { return dimensions[i]; }
		
		@Override
		public int numDimensions() { return dimensions.length; }
		
		@Override
		public Dimensions transpose() {
			if (numDimensions() != 2) throw new UnsupportedOperationException("n!=2");
			int[] dims = {dimensions[1], dimensions[0]};
			return new Rectangle(dims, capacity());
		}
		
		/**
		 * Returns true if the given object is logically equivalent to this; otherwise returns false.
		 * 
		 * @return this.dimensions = dim.dimensions
		 */
		public boolean equals(Object o) {
			if (o instanceof Rectangle) {
				final Rectangle r = (Rectangle) o;
				if (dimensions.length != r.dimensions.length || capacity() != r.capacity()) return false;
				for (int i = 0; i < dimensions.length;  i++) {
					if (dimensions[i] != r.dimensions[i]) return false;
				}
				return true;
			}
			return false;
			
		}
		
		public int hashCode() {
			return dimensions.length ^ capacity();
		}
		
		
	}
	
	
	
	
}
