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

import java.util.Collection;
import java.util.List;

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


/**
 * A factory class that facilitates creation of tuples
 * and tuple sets drawn from a given universe.  Only one
 * factory per universe exists.
 * 
 * @specfield universe: Universe
 * @invariant no f: TupleFactory - this | f.universe = this.universe 
 * @author Emina Torlak
 */
public final class TupleFactory {

	private final Universe universe;
	private final int base;
	
	/**
	 * Constructs a factory for the given universe.
	 * @requires no (TupleFactory<:universe).universe
	 * @ensures this.universe' = universe
	 * @throws NullPointerException  universe = null
	 */
	TupleFactory(Universe universe) {
		this.universe = universe;
		this.base = universe.size();
	}
	
	/**
	 * Returns the universe to which this factory belongs.
	 * @return this.universe
	 */
	public Universe universe() { return universe; }
	
	/**  
     * Returns a tuple that contains the specified sequence of atoms, 
     * drawn from this.universe.
     * 
     * @return {t: Tuple | t.universe = this.universe && t.atoms = atoms }
     * @throws NullPointerException  atoms = null 
     * @throws IllegalArgumentException  atoms.length < 1
     * @throws IllegalArgumentException   some a: atoms[int] | a !in this.universe.atoms[int]
     */
	public Tuple tuple(Object... atoms) {
		if (atoms.length<1) throw new IllegalArgumentException("atoms.length<1");
		return new IntTuple(atoms);
	}
	
	/**  
     * Returns a tuple that contains the specified sequence of atoms, 
     * drawn from this.universe.
     * 
     * @return {t: Tuple | t.universe = this.universe && t.atoms = atoms }
     * @throws NullPointerException  atoms = null 
     * @throws IllegalArgumentException  atoms.size < 1
     * @throws IllegalArgumentException   some a: atoms[int] | a !in this.universe.atoms[int]
     */
	public Tuple tuple(List<?> atoms) {
		if (atoms.size()<1) throw new IllegalArgumentException("atoms.size()<1");
		return new IntTuple(atoms.toArray());
	}
	
	/**  
     * Returns a tuple with the specified arity whose index in an arity-dimensional 
     * space over this.universe is given by the index parameter.
     * 
     * @return {t: Tuple | t.universe = this.universe && t.arity = arity && 
     *                     index = sum({i : [0..arity) | universe.index(t.atoms[i]) * universe.size^(arity - 1 - i))}) }
     * @throws IllegalArgumentException  arity < 1 || index < 0 || index >= universe.size^arity
     */
	public Tuple tuple(final int arity, final int index) {
		return new IntTuple(arity, index);
	}
	
	/**
	 * Returns a set of all tuples of the given arity, drawn from this.universe.
	 * @return { s: TupleSet | s.universe = this.universe && s.arity = arity && 
	 *                         s.tuples = {t: Tuple | t.universe = this.universe && t.arity = arity} }
	 * @throws IllegalArgumentException  arity < 1                     
	 */
	public TupleSet allOf(int arity) {
		return new TupleSet(universe, arity, 
				                      0, ((int) Math.pow(base, arity)) - 1);
	}
	
	/**
	 * Returns a set of tuples of arity 1, each of which wraps one of the given objects. 
	 * The method requires that the specified object be atoms in this.universe.
	 *
	 * @return {s: TupleSet | s.universe = this.universe && s.arity = 1 &&
	 *                        s.tuples = { t: Tuple | t.universe=this.universe && 
	 *                                                t.arity=1 && t.atoms[0] in atoms[int]}}
	 * @throws NullPointerException  atoms = null
	 * @throws IllegalArgumentException  some atoms[int] - this.universe.atoms[int]
	 */
	public TupleSet setOf(Object... atoms) {
		final TupleSet ret = new TupleSet(universe, 1);
		for (Object atom: atoms) {
			ret.add(new IntTuple(atom));
		}
		return ret;
	}
	
	/**
	 * Returns a tuple set consisting of specified tuples.  The method requires that
	 * all given tuples have the same arity and be drawn from this.universe.
	 *
	 * @return {s: TupleSet | s.universe = this.universe && s.arity = first.arity &&
	 *                        s.tuples = first + rest[int] }
	 * @throws NullPointerException  first = null || rest = null
	 * @throws IllegalArgumentException  first.universe != this.universe 
	 * @throws IllegalArgumentException  some t: rest[int] | t.universe != this.universe || t.arity != first.arity
	 */
	public TupleSet setOf(Tuple first, Tuple... rest) {
		if (!first.universe().equals(universe))
			throw new IllegalArgumentException("first.universe != this.universe");

		final TupleSet ret = new TupleSet(universe, first.arity(), first.index(), first.index());
		for(Tuple tuple: rest) {
			ret.add(tuple);
		}
		return ret;
	}
	
	/**
	 * Returns a tuple set consisting of specified tuples.  The method requires that
	 * all given tuples have the same arity and be drawn from this.universe.
	 *
	 * @return {s: TupleSet | s.universe = this.universe && s.arity = first.arity &&
	 *                        s.tuples = tuples }
	 * @throws NullPointerException  tuples = null 
	 * @throws IllegalArgumentException  tuples.isEmpty()  
	 * @throws IllegalArgumentException  tuples.universe != this.universe || #tuples.arity > 1
	 */
	public TupleSet setOf(Collection<Tuple> tuples) {
		if (tuples.isEmpty())
			throw new IllegalArgumentException("tuples.isEmpty()");
		final TupleSet ret = new TupleSet(universe, tuples.iterator().next().arity());
		for(Tuple t : tuples) {
			ret.add(t);
		}
		return ret;
	}
	
	/**
	 * Returns a set of the given arity that contains all tuples whose indeces
	 * are contained in the given int set.  Throws an IllegalArgumentException
	 * if the set contains an index that is either negative or greater than
	 * this.universe.size()^arity - 1.  The returned TupleSet is backed by a clone
	 * of tupleIndices.  
	 * @requires tupleIndices is cloneable
	 * @return {s: TupleSet | s.universe = this.universe && s.arity = arity &&
	 *                        s.tuples = {t: Tuple | t.index() in tupleIndices} }
	 * @throws NullPointerException  tupleIndices = null
	 * @throws IllegalArgumentException  tupleIndices is uncloneable
	 * @throws IllegalArgumentException  arity < 1
	 * @throws IllegalArgumentException  tupleIndices.min() < 0 || tupleIndices.max() >= this.universe.size()^arity 
	 */
	public TupleSet setOf(int arity, IntSet tupleIndices) {
		try {
			return new TupleSet(universe,arity,tupleIndices.clone());
		} catch (CloneNotSupportedException cne){
			throw new IllegalArgumentException("uncloneable int set");
		}
	}
	
	/**
	 * Returns an initially empty tuple set of the given arity, based on this.universe.
	 * @return { s: TupleSet | s.universe = this.universe && s.arity = arity && no s.tuples }
	 * @throws IllegalArgumentException  arity < 1    
	 */
	public TupleSet noneOf(int arity) {
		return new TupleSet(universe, arity);
	}
	
	/**
	 * Returns a tuple set that contains all tuples between <code>from</code>
	 * and <code>to</code>, inclusive.  More formally, the returned set contains
	 * all tuples whose indeces are in the range [from.index()..to.index()].
	 * @return { s: TupleSet | s.universe = this.universe && s.arity = from.arity &&
	 *                         s.tuples = {t: Tuple | t.universe = this.universe &&
	 *                                                t.arity = s.arity &&
	 *                                                from.index()<=t.index()<=to.index() }}
	 * @throws NullPointerException  from = null || to = null
	 * @throws IllegalArgumentException  from.arity != to.arity 
	 * @throws IllegalArgumentException  from.universe != this.universe || to.universe != this.universe
	 * @throws IllegalArgumentException  from.index > to.index
	 */
	public TupleSet range(Tuple from, Tuple to) {
		if (from.arity()!=to.arity()) 
			throw new IllegalArgumentException("from.arity!=to.arity");
		if (!(from.universe().equals(universe)&&to.universe().equals(universe)))
			throw new IllegalArgumentException("from.universe != this.universe || to.universe != this.universe");
		return new TupleSet(universe, from.arity(), from.index(), to.index());
	}
	
	/**
	 * Returns a tuple set that contains all tuples in the specified area
	 * of the n-dimensional space, where n is the arity of the argument
	 * tuples.  For example, suppose that this.universe consists of atoms
	 * {atom0, atom1, atom2, atom3}, where atom0 has index 0, atom1 has index 1, etc.  
	 * Calling this method with tuples [atom0, atom2] and [atom1, atom3] as the 
	 * first and second arguments would result in the set {[atom0, atom2],
	 * [atom0,atom3], [atom1,atom2], [atom1, atom3]}.  That is, the returned set
	 * consists of all points in the rectangle whose upper left corner is the 
	 * point [atom0, atom2] and whose lower right corner is at [atom1, atom3].
	 * @return {s: TupleSet | s.arity = upperLeft.arity &&
	 *                        s.universe = this.universe &&
	 *                        s.tuples = {t: Tuple | all i: [0..s.arity) | 
	 *                                     this.universe.index(upperLeft.atoms[i]) <=
	 *                                     this.universe.index(t.atoms[i]) <= 
	 *                                     this.universe.index(lowerRight.atoms[i]}}
	 * @throws NullPointerException  upperLeft = null || lowerRight = null
	 * @throws IllegalArgumentException  upperLeft.arity != lowerRight.arity 
	 * @throws IllegalArgumentException  lowerRight.universe != this.universe || upperLeft.universe != this.universe
	 * @throws IllegalArgumentException  some i: [0..upperLeft.arity) | 
	 *                                       this.universe.index(upperLeft.atoms[i]) > 
	 *                                       this.universe.index(lowerRight.atoms[i])
	 */
	public TupleSet area(Tuple upperLeft, Tuple lowerRight) {
		if (!upperLeft.universe().equals(universe) || upperLeft.arity()!=lowerRight.arity()) 
			throw new IllegalArgumentException();
		TupleSet ret = new TupleSet(universe, 1, upperLeft.atomIndex(0),lowerRight.atomIndex(0));
		for(int i = 1; i < upperLeft.arity(); i++) {
			ret = ret.product(new TupleSet(universe, 1, upperLeft.atomIndex(i),lowerRight.atomIndex(i)));
		}
		return ret;
	}
	
	/**
	 * Throws a CapacityExceededException if all tuples of the given arity 
	 * drawn from this.universe cannot be represented as an integer.
	 * @throws CapacityExceededException if all tuples of the given arity 
	 * drawn from this.universe cannot be represented as an integer.
	 */
	void checkCapacity(int arity) { 
		if (StrictMath.pow(base,arity) > Integer.MAX_VALUE) {
			throw new CapacityExceededException("Arity too large (" + arity + ") for a universe of size " + universe.size(), Ints.nCopies(arity, base));
		}
	}
	
	/**
	 * Projects the tuple with the specified index and arity onto the 
	 * specified column.    
	 * @requires tupleIndex >= 0 && tupleIndex < this.universe.size() ^ arity
	 * @return this.universe.index(this.tuple(arity, tupleIndex).atoms[i])
	 */
	int project(int tupleIndex, int arity, int column) {
		if (column < 0 || column >= arity) throw new IndexOutOfBoundsException(column+"");
        return (tupleIndex / ((int) Math.pow(base, arity-1-column))) % base;
	}
	
	/**
	 * An implementation of the Tuple interface that stores
	 * only the tuple's arity and index, rather than the full
	 * sequence of atoms.  Parts of the sequence are computed on
	 * demand, e.g. when the <code>get</code> method is invoked.
	 * 
	 * @specfield universe: TupleFactory.this.universe
	 * @specfield arity: int
	 * @specfield index: int
	 * @invariant arity >= 1 && 0 <= index < TupleFactory.this.base^arity
	 * @invariant index = sum({i: [0..arity) | TupleFactory.this.universe.index(atoms[i]) * TupleFactory.this.base^(arity - 1 - i))
	 * @author Emina Torlak
	 */
	private final class IntTuple extends Tuple {
		private final int arity, index;
		
		/**  
	     * Constructs a tuple with the specified arity and index, whose atoms
	     * are drawn from the factory's universe.
	     * 
	     * @ensures this.arity' = arity && 
	     *          this.index' = index 
	     * @throws IllegalArgumentException  arity < 1 || index < 0 || index >= TupleFactory.this.base^arity
	     */
	    IntTuple(final int arity, final int index) {
	    	checkCapacity(arity);
	        if (arity < 1 || index < 0 || index >= Math.pow(base, arity)) {
	            throw new IllegalArgumentException("arity < 1 || index < 0 || index >= universe.size^arity");
	        }
	        this.arity = arity;
	        this.index = index;
	    }
	    
	    /**  
	     * Constructs a tuple that contains the specified sequence of atoms, drawn from the
	     * enclosing factory's universe.
	     * 
	     * @requires atoms.length > 0
	     * @ensures this.atoms' = atoms
	     * @throws NullPointerException  atoms = null
	     * @throws IllegalArgumentException   some a: atoms[int] | a !in universe.atoms[int]
	     */
	    IntTuple(final Object... atoms) {
	        this.arity = atoms.length;
	        checkCapacity(arity);
	        int tempIndex = 0, multiplier = 1;
	        for (int i = arity - 1; i >= 0; i--) { 
	            tempIndex += universe.index(atoms[i]) * multiplier;
	            multiplier *= base;
	        }
	        this.index = tempIndex;
	        assert this.index >= 0;
	    }
	    
	    /**
		 * Constructs a tuple with the specified arity, with the specified atom
		 * at each position.  
		 * @ensures this.arity' = arity && this.atoms = [0..arity)->atom 
		 * @throws NullPointerException  atom = null
	     * @throws IllegalArgumentException  arity < 1 || atom !in this.universe.atoms[int]
	     */
	    @SuppressWarnings("unused")
		IntTuple(final int arity, final Object atom) {
	    	checkCapacity(arity);
	    	if (arity < 1) throw new IllegalArgumentException("arity < 1");
	    	this.arity = arity;
	    	int tempIndex = 1;
			for (int i = 0; i < arity; i++) {
				tempIndex = tempIndex*base + 1;
			}
			this.index = universe.index(atom) * tempIndex;
	        assert this.index >= 0;
	    }
	    
	    /** {@inheritDoc} */
	    public Universe universe() { return universe; }
	    
	    /** {@inheritDoc} */
	    public int arity() { return arity; }
	    
	    /** {@inheritDoc} */
	    public int index() { return index; }
	    
	    /** {@inheritDoc} */
	    public Object atom(int i) {
	        return universe.atom(atomIndex(i));
	    }
	    
	    /** {@inheritDoc} */
	   public int atomIndex(int i) {
		   return project(index,arity,i);
//	        if (i < 0 || i >= arity) throw new IndexOutOfBoundsException("i < 0 || i >= this.arity");
//	        return (index / ((int) Math.pow(base, arity-1-i))) % base;
	    }
	    
	    /** {@inheritDoc} */
	    public boolean contains(Object atom) {
	        for (int remainder = index, atomIndex = universe.index(atom); 
	                 remainder > 0; remainder = remainder / base) {
	            if (remainder % base == atomIndex) return true;
	        }
	        return false;
	    }

	    /** {@inheritDoc} */
	    public Tuple product(Tuple tuple) {
	    	if (!universe.equals(tuple.universe())) throw new IllegalArgumentException("tuple.universe != this.universe");
	        return new IntTuple(arity + tuple.arity(), 
	        		                index * ((int)Math.pow(base, tuple.arity())) + tuple.index());
	    }
	}
	
	
}
