/* 
 * 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.AbstractSet;
import java.util.Collection;
import java.util.Iterator;

import kodkod.util.ints.IntIterator;
import kodkod.util.ints.IntSet;
import kodkod.util.ints.Ints;


/**
 * Represents a set of {@link kodkod.instance.Tuple tuples}
 * of a given arity, constructed over a given {@link kodkod.instance.Universe universe}.
 * All polymorphic methods throw a ClassCastException when passed
 * an element that is not a Tuple.  All methods throw a NullPointerException
 * when passed null.  The iterator of a TupleSet returns tuples in the order of their
 * {@link kodkod.instance.Tuple#index() indeces}.  
 * 
 * @specfield tuples: set Tuple
 * @specfield universe: Universe
 * @specfield arity: int
 * @invariant tuples.arity = arity && tuples.universe = universe
 * 
 * @author Emina Torlak
 */
public final class TupleSet extends AbstractSet<Tuple> implements Cloneable {
	private final Universe universe;
	private final int arity;
	private final IntSet tuples;
	private IntSet indexView = null;
		
	/**
	 * Constructs an empty tuple set for storing tuples
	 * of the specified arity, over the given universe.
	 * 
	 * @ensures this.universe' = universe && this.arity' = arity && no this.tuples'
	 * @throws NullPointerException  universe = null
	 * @throws IllegalArgumentException  arity < 1
	 */
	TupleSet(Universe universe, int arity) {
		if (arity < 1) throw new IllegalArgumentException("arity < 1");
		universe.factory().checkCapacity(arity);
		this.universe = universe;
		this.arity = arity;
		tuples = Ints.bestSet(capacity());
	}
	
	/**
	 * Constructs a tuple set of the given arity, over the specified universe,
	 * which initially contains all tuples whose indeces are between fromIndex
	 * and toIndex, inclusive.
	 * 
	 * @ensures this.universe' = universe && this.arity' = arity && 
	 *          this.tuples' = {t: Tuple | t.universe=universe && t.arity=arity && 
	 *                                     fromIndex()<=t.index()<=toIndex() }
	 * @throws NullPointerException  universe = null 
	 * @throws IllegalArgumentException  arity < 1 || 
	 * @throws IndexOutOfBoundsException  fromIndex !in [0..toIndex] ||
	 *                                     toIndex !in [0..universe.size()^arity - 1]
	 */
	TupleSet(Universe universe, int arity, int fromIndex, int toIndex) {
		this(universe,arity);
		checkRange(toIndex, 0, capacity() - 1);
		checkRange(fromIndex, 0, toIndex);
		for(int i = fromIndex; i <= toIndex; i++) {
			tuples.add(i);
		}
	}
	
	/**
	 * 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.  An attempt to iterate over a tuple set backed by an invalid index
	 * set will result in a runtime exception.  
	 * @return {s: TupleSet | s.universe = this.universe && s.arity = arity &&
	 *                        s.tuples = {t: Tuple | t.index() in tupleIndeces} }
	 * @throws NullPointerException  tupleIndeces = null
	 * @throws IllegalArgumentException  arity < 1
	 * @throws IllegalArgumentException  tupleIndeces.min() < 0 || tupleIndeces.max() >= this.universe.size()^arity 
	 */
	TupleSet(Universe universe, int arity, IntSet tupleIndeces) {
		if (arity < 1) throw new IllegalArgumentException("arity < 1");
		universe.factory().checkCapacity(arity);
		this.universe = universe;
		this.arity = arity;
		if (!tupleIndeces.isEmpty()) {
			if (tupleIndeces.min()<0 || tupleIndeces.max() >= capacity())
				throw new IllegalArgumentException(tupleIndeces.min() + "<0 || " + tupleIndeces.max()+">="+universe.size()+"^"+arity);
		}
		tuples = tupleIndeces;
	}
	
	/**
	 * Copy constructor.
	 * @ensures constructs a deep copy of the given tupleset
	 */
	private TupleSet(TupleSet original) {
		this.universe = original.universe;
		this.arity = original.arity;
		try {
			this.tuples = original.tuples.clone();
		} catch (CloneNotSupportedException e) {
			throw new InternalError(); // unreachable code
		}
		this.indexView = null;
	}
	
	/**
	 * Throws an IndexOutOfBoundsException if index is not in [min..max]
	 */
	private final void checkRange(int index, int min, int max) {
		if (index < min || index > max)
			throw new IndexOutOfBoundsException(index + " !in " + "[" + min + ".." + max + "]");
	}
	
	/**
	 * Returns the capacity of this set -- the maximum number of tuples
	 * that it can hold, given its universe and arity.  
	 * @return this.universe.size() ^ this.arity
	 */
	public final int capacity() {
		return (int) StrictMath.pow(universe.size(),arity);
	}

	/**
	 * Returns this.universe.
	 * @return this.universe
	 */
	public Universe universe() { return universe; }
	
	/**
	 * Returns this.arity
	 * @return this.arity
	 */
	public int arity() { return arity; }
	
	
	
	/**
	 * Returns an unmodifiable int set view of the tuples stored in this set.
	 * Specifically, the returned int set contains an integer i
	 * iff this set contains a tuple with the index i.  The 
	 * view is backed by this set, so changes to this set are
	 * reflected in the index set. 
	 * @return { s: IntSet | s.ints = {i: int | some t: this.tuples | t.index = i}
	 */
	public IntSet indexView() {
		if (indexView==null) {
			indexView = Ints.unmodifiableIntSet(tuples);
		}
		return indexView;
	}
	
	/**
	 * Returns an unmodifiable view of the this tupleset.  This method allows modules to 
	 * provide "read-only" access to internal tuple sets. Query operations on the returned set 
	 * "read through" to the specified set, and attempts to modify the returned set, whether direct 
	 * or via its iterator, result in an UnsupportedOperationException.
	 * @return an unmodifiable view of the this tupleset
	 */
	public TupleSet unmodifiableView() {
		return new TupleSet(universe,arity,indexView());
	}
	
	/**
	 * Returns a tuple set that is the cross product of this and the 
	 * specified set.
	 * @return {t: TupleSet | t.arity = this.arity + s.arity &&
	 *                        t.universe = this.universe &&
	 *                        t.tuples = this.tuples->s.tuples }
	 * @throws NullPointerException  s = null
	 * @throws IllegalArgumentException  s.universe != this.universe                              
	 */
	public TupleSet product(TupleSet s) {
		if (!s.universe().equals(universe))
			throw new IllegalArgumentException("s.universe != this.universe");
		final TupleSet ret = new TupleSet(universe, arity+s.arity());
		if (!s.isEmpty()) {
			final int mCapacity = (int) StrictMath.pow(universe.size(), s.arity);
			for(IntIterator indeces0 = tuples.iterator(); indeces0.hasNext(); ) {
				int i0 = mCapacity * indeces0.next();
				for(IntIterator indeces1 = s.tuples.iterator(); indeces1.hasNext(); ) {
					ret.tuples.add(i0 + indeces1.next());
				}
			}
		}
		return ret;
	}
	
	/**
	 * Projects this TupleSet onto the given dimension.
	 * @return {s: TupleSet | s.arity = 1 && s.universe = this.universe && 
	 *                        s.tuples = { t: Tuple | some q: this.tuples | q.atoms[dimension] = t.atoms[int] } }
	 * @throws IllegalArgumentException  dimension < 0 || dimension >= this.arity
	 */
	public TupleSet project(int dimension) {
		if (dimension < 0 || dimension >= arity) {
			throw new IllegalArgumentException("dimension < 0 || dimension >= this.arity");
		}
		final IntSet projection = Ints.bestSet(universe.size());
		final TupleFactory factory = universe.factory();
		for(IntIterator indexIter = tuples.iterator(); indexIter.hasNext();) {
			projection.add(factory.project(indexIter.next(), arity, dimension));
		}
		return new TupleSet(universe,1,projection);
	}
	
	/**
	 * Returns a deep copy of this tuple set. 
	 * @return {s: TupleSet - this | s.universe = this.universe && s.tuples = this.tuples }
	 */
	public TupleSet clone() {
		// ok to use a copy constructor to clone a final class
		return new TupleSet(this);
	}
	
	/**
	 * Returns an iterator over the tuples in this tupleset.
	 * @return an iterator over the tuples in this tupleset.
	 */
	@Override
	public Iterator<Tuple> iterator() {
		return new Iterator<Tuple>() {
			IntIterator indexIter = tuples.iterator();
			public boolean hasNext() {
				return indexIter.hasNext();
			}

			public Tuple next() {
				return universe.factory().tuple(arity, indexIter.next());
			}

			public void remove() {
				indexIter.remove();
			}
		};
	}
	
	/**
	 * Returns the index of the given tuple, if the tuple has the same
	 * arity and universe as this.  Otherwise throws an IllegalArgumentException.
	 * @return t.index
	 * @throws IllegalArgumentException  t.arity != this.arity || t.universe != this.universe
	 */
	private final int extractIndex(Tuple t) {
		if (t.arity() != arity || !t.universe().equals(universe)) {
			throw new IllegalArgumentException("t.arity != this.arity || t.universe != this.universe");
		}
		return t.index();
	}
	
	/**
	 * Returns true if this contains the given object.
	 * @return o in this.tuples
	 * @throws IllegalArgumentException o.arity != this.arity || o.universe != this.universe
	 */
	@Override
	public boolean contains(Object o) {
		return tuples.contains(extractIndex((Tuple)o));
	}
	
	/**
	 * Returns the size of this tupleset.
	 * @return #this.tuples
	 */
	@Override
	public int size() { return tuples.size(); }
	
	/**
	 * Removes all tuples from this tupleset.
	 * @ensures no this.tuples' 
	 */
	@Override
	public void clear() { 
		tuples.clear(); 
	}

	/**
	 * Adds the specified tuple to this tupleset.  Returns
	 * true if this set was changed as the result of the
	 * operation.
	 * @ensures this.tuples' = this.tuples + t
	 * @return o !in this.tuples
	 * @throws IllegalArgumentException  t.universe != this.universe || t.arity != this.arity
	 */
	@Override
	public boolean add(Tuple t) {
		return tuples.add(extractIndex(t));
	}

	/**
	 * Removes the given object from this tupleset, if present, and
	 * returns true.  Otherwise does nothing and returns false.
	 * @ensures this.tuples' = this.tuples - o
	 * @return o in this.tuples
	 * @throws IllegalArgumentException  o.universe != this.universe || o.arity != this.arity
	 */
	@Override
	public boolean remove(Object o) {
		return tuples.remove(extractIndex((Tuple)o));
	}
	
	/**
	 * If c is not a TupleSet or it is a tupleset with a universe different than
	 * this.universe, returns null.  Otherwise, returns the tuples associated 
	 * with the modifiable view of c. 
	 * @requires c in TupleSet => c.arity = this.arity
	 * @return c in TupleSet && c.universe = this.universe && c.arity = this.arity => c.tuples, null
	 * @throws NullPointerException  s = null
	 * @throws IllegalArgumentException  this.arity!=s.arity
	 */
	private IntSet extractTuples(Collection<?> c) {
		if (c instanceof TupleSet) {
			final TupleSet s = (TupleSet) c;
			if (arity!=s.arity())
				throw new IllegalArgumentException("this.arity!=c.arity");
			return universe.equals(s.universe()) ? s.tuples : null;
		}
		return null;
	}
	
	/**
	 * Returns true if this contains all tuples from c.  Otherwise returns false.
	 * @return c.elements in this.tuples
	 * @throws IllegalArgumentException  some t: c.elements | t.universe != this.universe || t.arity != this.arity
	 */
	@Override
	public boolean containsAll(Collection<?> c) { 
		final IntSet cTuples = extractTuples(c);
		return cTuples==null ? super.containsAll(c) : tuples.containsAll(cTuples);
	}
	
	/**
	 * Adds all tuples from c to this, if not present, and returns
	 * true.  Otherwise does nothing and returns false.
	 * @ensures this.tuples' = this.tuples + c.elements
	 * @return c.elements !in this.tuples
	 * @throws IllegalArgumentException  some t: c.elements | t.universe != this.universe || t.arity != this.arity
	 */
	@Override
	public boolean addAll(Collection<? extends Tuple> c) {
		final IntSet cTuples = extractTuples(c);
		return cTuples==null ? super.addAll(c) : tuples.addAll(cTuples);
	}
	
	/**
	 * Removes all tuples in c from this, if present, and returns
	 * true.  Otherwise does nothing and returns false.
	 * @ensures this.tuples' = this.tuples - c.elements
	 * @return some c.elements & this.tuples
	 * @throws IllegalArgumentException  some t: c.elements | t.universe != this.universe || t.arity != this.arity
	 */
	@Override
	public boolean removeAll(Collection<?> c) {
		final IntSet cTuples = extractTuples(c);
		return cTuples==null ? super.removeAll(c) : tuples.removeAll(cTuples);
	}
	
	/**
	 * Removes all tuples from this that are not in c, if any, and
	 * returns true. Otherwise does nothing and returns false.
	 * @ensures this.tuples' = this.tuples & c.elements
	 * @return this.tuples !in c.elements
	 * @throws IllegalArgumentException  some t: c.elements | t.universe != this.universe || t.arity != this.arity
	 */
	@Override
	public boolean retainAll(Collection<?> c) {
		final IntSet cTuples = extractTuples(c);
		return cTuples==null ? super.retainAll(c) : tuples.retainAll(cTuples);
	}
	
	
	/**
	 * Returns true if o contains the same tuples as this.
	 * @return this.tuples = o.elements
	 */
	@Override
	public boolean equals(Object o) {
		if (this==o) return true;
		if (o instanceof TupleSet) {
			final TupleSet s = (TupleSet) o;
			return arity==s.arity && universe.equals(s.universe) && 
			       tuples.equals(s.tuples);
		}
		return super.equals(o);
	}
	
	/**
	 * {@inheritDoc}
	 */
	@Override
	public int hashCode() { 
		return tuples.hashCode();
	}
}
