/* 
 * 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 static kodkod.engine.bool.Operator.AND;
import static kodkod.engine.bool.Operator.OR;

import java.util.Collection;
import java.util.Iterator;

import kodkod.engine.config.Options;
import kodkod.engine.config.Options.IntEncoding;
import kodkod.util.ints.IntSet;


/**
 * A factory for creating {@link kodkod.engine.bool.BooleanValue boolean values}, 
 * {@link kodkod.engine.bool.BooleanMatrix matrices}, and {@link kodkod.engine.bool.Int ints}.
 * 
 * @specfield comparisonDepth: int // the depth to which circuits should be checked for equality 
 * @specfield intEncoding: Options.IntEncoding // the encoding used for generating integers ({@link #integer(int)}
 * @specfield bitwidth: int // the bitwidth used for integer computations
 * @specfield components: set BooleanValue
 * @invariant no f1, f2: BooleanFactory | f1 != f2 => f1.components & f2.components = BooleanConstant
 * @author Emina Torlak
 */
public abstract class BooleanFactory {
	/**
	 * IMPLEMENTATION NOTE:  BooleanFactory is the facade and a mediator for this package.
	 */
	private static CBCFactory CONSTANT_FACTORY;
	/**
	 * A circuit factory used internally to assemble circuits.
	 */
	private final CBCFactory circuits;
	
	/** The bitwidth used for integer computations */
	final int bitwidth;
	
	/**
	 * Constructs a boolean factory with the given number of input variables.  Gates are
	 * checked for semantic equality down to the given depth.  Integers are represented
	 * using the given number of bits.
	 * @requires 0 <= numVars < Integer.MAX_VALUE
	 * @requires checkToDepth >= 0 && bitwidth > 0
	 * @ensures #this.components' = numInputVariables && this.components' in BooleanVariable 
	 * @ensures this.bitwidth' = bitwidth
	 * @ensures this.comparisonDepth' = comparisonDepth
	 */
	private BooleanFactory(int numVars, int comparisonDepth, int bitwidth) {
		if (numVars==0) {
			if (CONSTANT_FACTORY==null)
				CONSTANT_FACTORY = new CBCFactory(0, 1);
			this.circuits = CONSTANT_FACTORY;
		} else {
			this.circuits = new CBCFactory(numVars, 1<<comparisonDepth);
		}
		this.bitwidth = bitwidth;
	}
	
	/**
	 * Returns a boolean factory, initialized to contain the given number
	 * of boolean variables.  
	 * <p>Gates are checked for semantic equality 
	 * down to the depth given by options.sharing when checking for cached values.  In general,  setting the
	 * comparison depth to a higher value will result in more 
	 * subcomponents being shared.  However, it will also slow down
	 * gate construction.  </p>
	 * <p>Integers are created/manipulated according to the specifications in the given Options object.</p>
	 * @return {f: BooleanFactory | #(f.components & BooleanVariable) = numVars &&
	 *                              BooleanConstant in f.components && f.components in BooleanVariable + BooleanConstant &&
	 *                              f.comparisonDepth = options.sharing && 
	 *                              f.bitwidth = options.bitwidth && f.intEncoding = options.intEncoding && 
	 *                              (all i: [1..numVars] | one f.components.label & i }}
	 * @throws IllegalArgumentException  numVars < 0 || numVars = Integer.MAX_VALUE
	 * @throws NullPointerException  options = null
	 */
	public static BooleanFactory factory(int numVars, Options options) {
		switch(options.intEncoding()) {
		case TWOSCOMPLEMENT : 
			return new TwosComplementFactory(numVars, options.sharing(), options.bitwidth()); 
		default :
			throw new IllegalArgumentException("unknown encoding: " + options.intEncoding());
		}
	}
	
	/**
	 * Returns a BooleanFactory with no variables; the returned factory
	 * can manipulate only constants.  
	 * @return {f: BooleanFactory | f.components = BooleanConstant &&
	 *                              f.comparisonDepth = options.sharing && 
	 *                              f.bitwidth = options.bitwidth && f.intEncoding = options.intEncoding }
	 * @throws NullPointerException  options = null
	 */
	public static BooleanFactory constantFactory(Options options) {
		return factory(0, options);
	}
	
	/**
	 * Returns the depth (from the root) to which components are checked for 
	 * semantic equality during gate construction.
	 * @return this.comparisonDepth
	 */
	public final int comparisonDepth() { return Integer.numberOfTrailingZeros(circuits.cmpMax()); }
	
	/**
	 * Sets the comparison depth to the given value.  Setting the
	 * comparison depth to a high value will result in more 
	 * subcomponents being shared.  However, it will also slow down
	 * gate construction.
	 * @ensures this.comparisonDepth' = newDepth
	 * @throws IllegalArgumentException  newDepth < 1
	 */
	public final void setComparisonDepth(int newDepth) {
		if (newDepth < 1)
			throw new IllegalArgumentException("newDepth < 1: " + newDepth);
		circuits.setCmpMax(1<<newDepth);
	}
	
	/**
	 * Returns the bitwidth used for integer representation.
	 * @return this.bitwidth
	 */
	public final int bitwidth() { return bitwidth; }
	
	/**
	 * Returns the encoding used by this factory to represent integers.
	 * @return this.intEncoding
	 */
	public abstract Options.IntEncoding intEncoding();
	
	/**
	 * Returns true if v is in this.components.
	 * @return v in this.components
	 * @throws NullPointerException  v = null
	 */
	public final boolean contains(BooleanValue v) {
		return circuits.canAssemble(v);
	}
	
	
	
	/**
	 * Returns the number of variables in this.components
	 * @return #(BooleanVariable & this.components)
	 */
	public final int numberOfVariables() { return circuits.numVars(); }
	
	/**
	 * Returns the variable with the given label.
	 * @requires 0 < label <= numberOfVariables()
	 * @return (this.components & BooleanVariable).label
	 */
	public final BooleanVariable variable(int label) {
		return circuits.variable(label);
	}
	
	/**
	 * Returns the negation of the given boolean value.
	 * @return {n: BooleanValue | n.label = -v.label && [[n]] = ![[v]] }
	 * @ensures (components.v).components' = (components.v).components + n 
	 * @throws NullPointerException  v = null                             
	 */
	public final BooleanValue not(BooleanValue v) {
		return v.negation();
	}
	
	/**
	 * Returns a boolean value whose meaning is the conjunction of the input components.  
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return {v: BooleanValue | [[v]] = [[v0]] AND [[v1]] }
	 * @ensures this.components' = this.components + v 
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue and(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(AND, v0, v1);
	}
	
	/**
	 * Returns a boolean value whose meaning is the disjunction of the input components.  
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return {v: BooleanValue | [[v]] = [[v0]] OR [[v1]] }
	 * @ensures this.components' = this.components + v 
	 * @throws NullPointerException  any of the arguments are null
	 * @throws IllegalArgumentException  v0 + v1 !in this.components
	 */
	public final BooleanValue or(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(OR, v0, v1);
	}
	
	/**
	 * Returns a boolean value whose meaning is [[v0]] ^ [[v1]].  
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return { v: BooleanValue | [[v]] = [[v0]] xor [[v1]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue xor(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(v0, v1.negation(), v1);
	}
	
	/**
	 * Returns a boolean value whose meaning is [[v0]] => [[v1]].  
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return { v: BooleanValue | [[v]] = [[v0]] => [[v1]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue implies(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(OR, v0.negation(), v1);
	}
	
	/**
	 * Returns a boolean value whose meaning is [[v0]] <=> [[v1]].
	 * The behavior of this method is unspecified if v0 or v1 are not components of this factory.
	 * @requires v0 + v1 in this.components
	 * @return { v: BooleanValue | [[v]] = [[v0]] iff [[v1]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue iff(BooleanValue v0, BooleanValue v1) {
		return circuits.assemble(v0, v1, v1.negation());
	}
	
	/**
	 * Returns a boolean value whose meaning is [[i]] ? [[t]] : [[e]].
	 * The behavior of this method is unspecified if i, t, or e are not components of this factory.
	 * @requires i + t + e in this.components 
	 * @return { v: BooleanValue | [[v]] = [[i]] ? [[t]] : [[e]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue ite(BooleanValue i, BooleanValue t, BooleanValue e) {
		return circuits.assemble(i, t, e);
	}
	
	/**
	 * Returns a boolean value whose meaning is the sum bit of a full binary adder.
	 * The behavior of this method is unspecified if v0, v1, or cin are not components of this factory.
	 * @requires v0 + v1 + cin in this.components 
	 * @return { v: BooleanValue | [[v]] = [[cin]] xor [[v0]] xor [[v1]] }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue sum(BooleanValue v0, BooleanValue v1, BooleanValue cin) {
		return xor(cin, xor(v0, v1));
	}
	
	/**
	 * Returns a boolean value whose meaning is the carry out bit of a full binary adder.
	 * The behavior of this method is unspecified if v0, v1, or cin are not components of this factory.
	 * @requires v0 + v1 + cin in this.components 
	 * @return { v: BooleanValue | [[v]] = ([[v0]] and [[v1]]) or ([[cin]] and ([[v0]] xor [[v1]]))  }
	 * @ensures this.components' = this.components + v
	 * @throws NullPointerException  any of the arguments are null
	 */
	public final BooleanValue carry(BooleanValue v0, BooleanValue v1, BooleanValue cin) {
		return or(and(v0, v1), and(cin, xor(v0, v1)));
	}
	
	/**
	 * Converts the given accumulator into an immutable boolean value and adds it to this.components.
	 * This method requires that all of g's inputs are in this.components.  If g has no inputs,
	 * its operator's identity constant is returned.  If g has one input, that input is returned.
	 * Otherwise, an immutable value that is semantically equivalent to g is returned.
	 * The behavior of this method is unspecified if the components of g are not components of this factory.
	 * @requires g.components in this.components 
	 * @return no g.inputs => g.op.identity(), 
	 *         one g.inputs => g.inputs, 
	 *         {g' : BooleanValue - BooleanAccumulator | [[g']] = [[g]] }
	 * @ensures this.components' = this.components + g'
	 */
	public final BooleanValue accumulate(BooleanAccumulator g) {
		return circuits.assemble(g);
	}
	
	/**
	 * Returns an Int that represents the given number using this.intEncoding.
	 * @return { i: Int | [[i]] = number && i.encoding && this.intEncoding && i.factory = this}
	 * @throws IllegalArgumentException  the number cannot be represented using 
	 * the specified encoding
	 */
	public abstract Int integer(int number);
	
	/**
	 * Returns an Int that represents 0 or the given number, depending on the value of the given bit.
	 * The behavior of this method is unspecified if the bit is not a component of this factory.
	 * @return { i: Int | [[bit]] => [[i]] = number, [[i]] = 0 && i.encoding = this.intEncoding && i.factory = this}
	 */
	public abstract Int integer(int number, BooleanValue bit);
	
	/**
	 * Returns an Int that represents the sum of the elements returned by the iterator,
	 * using this.intEncoding.
	 * @param lo the first element of the current partial sum. Initial should be 0.
	 * @param hi the last element of the current partial sum.  Initial should be size-1, where size is the total
	 * number of elements returned by the iterator.
	 * @return  an Int that represents the sum of the elements returned by the iterator,
	 * using this.intEncoding.
	 */
	private Int sum(Iterator<BooleanValue> values, int low, int high) {
		if (low > high) 
			return integer(0);
		else if (low == high) 
			return integer(1, values.next());
		else {
			final int mid = (low + high) / 2;
			final Int lsum = sum(values, low, mid);
			final Int hsum = sum(values, mid+1, high);
			return lsum.plus(hsum);
		}
	}
	
	/**
	 * Returns an Int that represents the sum of all values in the given collection.
	 * @return an Int that represents the sum of all values in the given collection.
	 */
	public final Int sum(Collection<BooleanValue> bits) {
		return sum(bits.iterator(), 0, bits.size()-1);
	}
	
	/**
	 * Removes all formulas with one or more inputs from this.components.
	 * @ensures this.componets' = 
	 *    BooleanConstant + this.components & BooleanVariable
	 */
	public final void clear() {
		circuits.clear();
	}
	
	/**
	 * Returns a BooleanMatrix with the given dimensions and this 
	 * as the factory for its non-FALSE components.  The returned matrix 
	 * can store any value from this.components at all
	 * indices between 0, inclusive, and d.capacity(), exclusive.  
	 * @throws NullPointerException  d = null
	 * @return { m: BooleanMatrix | m.factory = this && m.dimensions = d && m.elements = [0..d.capacity) -> one FALSE }
	 */
	public final BooleanMatrix matrix(Dimensions d) {
		if (d == null ) throw new NullPointerException();
		return new BooleanMatrix(d, this);
	}
	
	/**
	 * @throws IllegalArgumentException  indices !in [0..d.capacity())
	 */
	private static void validate(IntSet indices, Dimensions d) {
		if (!indices.isEmpty()) {
			if (!d.validate(indices.min()) ||	!d.validate(indices.max()))
				throw new IllegalArgumentException();
		}
	}
	
	/**
	 * Returns a BooleanMatrix <tt>m</tt> with the given dimensions, this
	 * as its factory, and the indices from the set <tt>trueIndices</tt> initialized
	 * to TRUE.  An IndexOutOfBoundsException may be thrown
	 * if {@link BooleanMatrix#set(int, BooleanValue)} is called on <tt>m</tt> with an index 
	 * not contained in <tt>allIndices</tt>.  If <tt>allIndices.equals(trueIndices)</tt>, 
	 * <tt>m</tt> may be a constant matrix; that is, an IllegalArgumentException may be
	 * thrown if {@link BooleanMatrix#set(int, BooleanValue)} is called on <tt>m</tt> with
	 * a non-constant value.  Finally, if cloning <tt>trueIndices</tt> results in an immutable
	 * set, then {@link BooleanMatrix#set(int, BooleanValue) m.set(int, BooleanValue)} may throw
	 * an UnsupportedOperationException when called with a member of <tt>trueIndices</tt>.
	 * @requires allIndices.containsAll(trueIndices)
	 * @return { m: BooleanMatrix |  m.factory = this && m.dimensions = dims && 
	 *           m.elements = [0..d.capacity()-1] ->one FALSE ++ indices->TRUE }
	 * @throws IllegalArgumentException  allIndices !in [0..d.capacity())
	 * @throws IllegalArgumentException  one of the input sets is not cloneable
	 * @throws NullPointerException  d = null || allIndices = null || trueIndices = null	 	 
	 */
	public final BooleanMatrix matrix(Dimensions d, IntSet allIndices, IntSet trueIndices) {
		assert allIndices.size() >= trueIndices.size(); // sanity check
		validate(allIndices, d); validate(trueIndices, d);
		try {
			return new BooleanMatrix(d, this, allIndices, trueIndices.clone());
		} catch (CloneNotSupportedException e) {
			throw new IllegalArgumentException();
		}
	
	}
		
	/**
	 * BooleanFactory that produces TwosComplementInts.
	 * @invariant encoding = TwosComplement
	 * @author Emina Torlak
	 */
	private static final class TwosComplementFactory extends BooleanFactory {

		/**
		 * Constructs a boolean factory with the given number of input variables.  Gates are
		 * checked for semantic equality down to the given depth.  Integers are represented
		 * using the given number of bits.
		 * @requires 0 <= numVars < Integer.MAX_VALUE
		 * @requires checkToDepth >= 0 && bitwidth > 0
		 * @ensures #this.components' = numInputVariables && this.components' in BooleanVariable 
		 * @ensures this.bitwidth' = bitwidth
		 * @ensures this.comparisonDepth' = comparisonDepth
		 * @ensures this.intEncoding' = BINARY
		 */
		TwosComplementFactory(int numVars, int comparisonDepth, int bitwidth) {
			super(numVars, comparisonDepth, bitwidth);
		}
		/**
		 * Returns TWOSCOMPLEMENT.
		 * @return TWOSCOMPLEMENT
		 * @see kodkod.engine.bool.BooleanFactory#intEncoding()
		 */
		@Override
		public IntEncoding intEncoding() {
			return IntEncoding.TWOSCOMPLEMENT;
		}
		
		/**
		 * {@inheritDoc}
		 * @see kodkod.engine.bool.BooleanFactory#integer(int)
		 */
		@Override
		public Int integer(int number) {
			return new TwosComplementInt(this, number, BooleanConstant.TRUE);
		}
		
		/**
		 * {@inheritDoc}
		 * @see kodkod.engine.bool.BooleanFactory#integer(int, kodkod.engine.bool.BooleanValue)
		 */
		@Override
		public Int integer(int number, BooleanValue bit) {
			return new TwosComplementInt(this, number, bit);
		}
		
	}
}

