content: /* 
   * Kodkod -- Copyright (c) 2005-present, 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.BooleanConstant.FALSE;
  import static kodkod.engine.bool.BooleanConstant.TRUE;
  import static kodkod.engine.bool.Operator.AND;
  import static kodkod.engine.bool.Operator.CONST;
  import static kodkod.engine.bool.Operator.ITE;
  import static kodkod.engine.bool.Operator.OR;
  
  import java.util.Iterator;
  import java.util.LinkedList;
  import java.util.List;
  import java.util.ListIterator;
  
  import kodkod.util.collections.CacheSet;
  
  /**
   * A factory for creating variables, binary gates, and if-then-else gates, in RBC form.
   * @specfield values: set (BooleanVariable + MultiGate + ITEGate)
   * @specfield cmpMax: int // the maximum number of comparisons made when comparing circuits for equality
   * @invariant no disj factory, factory' : CircuitFactory | some factory.values & factory'.values
   * @author Emina Torlak
   */
  final class RBCFactory {
  	/**
  	 * Stores input variables.
  	 * @invariant all i: [1..iLits.size()] | vars[i-1].positive.label = i
  	 */
  	private final BooleanVariable[] vars;
  	/**
  	 * Caches the AND, OR, and ITE gates.  
  	 * @invariant all i: [0..2] | c[i].op.ordinal = i
  	 */
  	private final CacheSet<BooleanFormula>[] cache;
  	private int label, cmpMax;
  	
  	
  	/**
  	 * Constructs a CircuitFactory using the given max comparison parameter, initialized
  	 * to contain the given number of variables. 
  	 * @requires cmpMax > 0 && numVars >= 0
  	 * @ensures #this.values' = numVars && this.values in BooleanVariable
  	 * @ensures this.cmpMax' = cmpMax
  	 */
  	@SuppressWarnings("unchecked") RBCFactory(int numVars, int cmpMax) {
  		assert cmpMax > 0 && numVars >= 0;
  		this.cmpMax = cmpMax;
  		this.label = numVars + 1;
  		vars = new BooleanVariable[numVars];
  		for(int i = 0; i < numVars; i++) {
  			vars[i]= new BooleanVariable(i+1);                                                                        
  		}
  
  		cache = new CacheSet[]{new CacheSet<BooleanFormula>(), new CacheSet<BooleanFormula>(), new CacheSet<BooleanFormula>()};
  	}
  	
  	/**
  	 * Returns the cache for gates with the given operator.
  	 * @requires op in AND + OR + ITE
  	 * @return cache[op.ordinal]
  	 */
  	private CacheSet<BooleanFormula> opCache(Operator op) {
  		return cache[op.ordinal];
  	}
  	
  	/**
  	 * Sets this.cmpMax to the given value.
  	 * @requires cmpMax > 0
  	 * @ensures this.cmpMax' = cmpMax
  	 */
  	void setCmpMax(int cmpMax) {
  		assert cmpMax > 0;
  		this.cmpMax = cmpMax;
  	}
  	
  	/**
  	 * Returns this.cmpMax.
  	 * @return this.cmpMax
  	 */
  	int cmpMax() { return cmpMax; }
  	
  	/**
  	 * Removes all MultiGates and ITEGates from this.factory.
  	 * @ensures this.values' = this.values & BooleanVariable 
  	 */
  	void clear() {
  		label = vars.length+1;
  		cache[0].clear();
  		cache[1].clear();
  		cache[2].clear();
  	}
  	
  	/**
  	 * Returns true if the given value
  	 * is a valid argument to one of the <tt>assemble</tt>
  	 * methods.  Otherwise returns false.
  	 * @return v in this.values + this.values.negation + BooleanConstant
  	 */
  	boolean canAssemble(BooleanValue v) {
  		if (v.op()==CONST) return true;
  		if (v.label() < 0) v = v.negation();
  		final int absLit = v.label();
  		if (absLit <= vars.length) {
  			return v == vars[absLit-1];
  		} else {
  			final BooleanFormula g = (BooleanFormula) v;
  			for(Iterator<BooleanFormula> gates = opCache(g.op()).get(g.hashCode()); gates.hasNext(); ) {
  			    	if (gates.next()==g) return true;
  		    }
  			return false;
  		}
  	}
  	
  	/**
  	 * Returns the number of variables in this factory.
  	 * @return #(this.values & BooleanVariable)
  	 */
  	int numVars() { return vars.length; }
  	
  	/**
  	 * Returns the boolean variable from this.values with the given label.
  	 * @requires 0 < label <= #(this.values & BooleanVariable)
  	 * @return (this.values & BooleanVariable).label 
  	 */
  	BooleanVariable variable(int label) {
  		return vars[label-1];
  	}
  	
  	/**
  	 * Returns a boolean value whose meaning is (if [[i]] then [[t]] else [[e]]).
  	 * @requires i + t + e in (this.values + this.values.negation + BooleanConstant)
  	 * @return v: BooleanValue | [[v]] = if [[i]] then [[t]] else [[e]] 
  	 * @ensures v in BooleanFormula - NotGate => this.values' = this.values + v, this.values' = this.values
  	 * @throws NullPointerException  any of the arguments are null
  	 */
  	BooleanValue assemble(BooleanValue i, BooleanValue t, BooleanValue e) {
  		if (i==TRUE || t==e) return t;
  		else if (i==FALSE) return e;
  		else if (t==TRUE || i==t) return assemble(OR, i, e);
  		else if (t==FALSE || i.negation()==t) return assemble(AND, i.negation(), e);
  		else if (e==TRUE || i.negation()==e) return assemble(OR, i.negation(), t);
  		else if (e==FALSE || i==e) return assemble(AND, i, t);
  		else {
  			final int ilabel = i.label(), tlabel = t.label(), elabel = e.label();
  			boolean neg = false;
  			BooleanFormula f0 = (BooleanFormula) i, f1 = (BooleanFormula) t, f2 = (BooleanFormula) e;
  			if (Math.abs(tlabel)==Math.abs(elabel)) { 
  				if (ilabel>0 && tlabel<0 && elabel>0) { // (a <=> !b) becomes !(a <=> b)
  					neg = true;
  					f1 = f1.negation();
  					f2 = f2.negation();
  				} else if (ilabel<0 && tlabel>0 && elabel<0) { // (!a <=> b) becomes !(a <=> b)
  					neg = true;
  					f0 = f0.negation(); 
  				} else if (ilabel<0 && tlabel<0 && elabel>0) {// (!a <=> !b) becomes (a <=> b)
  					f0 = f0.negation();
  					f1 = f1.negation();
  					f2 = f2.negation();
  				}
  			} 
  			
  			final int hash = ITE.hash(f0, f1, f2);
  			
  			for(Iterator<BooleanFormula> gates = opCache(ITE).get(hash); gates.hasNext();) {
  				BooleanFormula gate = gates.next();
  				if (gate.input(0)==i && gate.input(1)==t && gate.input(2)==e)
  					return gate;
  			}
  			final BooleanFormula ret = new ITEGate(label++, hash, f0, f1, f2);
  			opCache(ITE).add(ret);
  			return neg ? ret.negation() : ret;
  		}
  	}
  	
  	/**
  	 * Returns a boolean value whose meaning is ([[v0]] op [[v1]]).
  	 * @requires v0 + v1 in (this.values + this.values.negation + BooleanConstant)
  	 * @return  v: BooleanValue | [[v]] = [[v0]] op [[v1]] 
  	 * @ensures v in BooleanFormula - NotGate => this.values' = this.values + v, this.values' = this.values
  	 * @throws NullPointerException  any of the arguments are null
  	 */
  	BooleanValue assemble(Operator.Nary op, BooleanValue v0, BooleanValue v1) {
  		if (op==OR) {
  			return assemble(AND, v0.negation(), v1.negation()).negation();
  		}
  		
  		if (v0==v1) return v0;
  		if (v0.label()==-v1.label()) return FALSE;
  		if (v0==TRUE) return v1;
  		if (v1==TRUE) return v0;
  		if (v0==FALSE) return FALSE;
  		if (v1==FALSE) return FALSE;
  		
  		return cache(op, (BooleanFormula)v0, (BooleanFormula)v1);
  	}
  	
  	/**
  	 * Returns a boolean value with the same meaning as the given accumulator.
  	 * @requires acc.components in (this.values + this.values.negation + BooleanConstant)
  	 * @return v: BooleanValue | [[v]] = [[acc]] 
  	 * @ensures v in BooleanFormula - NotGate => this.values' = this.values + v, this.values' = this.values
  	 * @throws NullPointerException  any of the arguments are null
  	 */
  	BooleanValue assemble(BooleanAccumulator acc) {
  		final int asize = acc.size();
  		final Operator.Nary op = acc.op;
  		switch(asize) {
  		case 0 : return op.identity();
  		case 1 : return acc.iterator().next();
  		case 2 : 
  			final Iterator<BooleanValue> inputs = acc.iterator();
  			return assemble(op, inputs.next(), inputs.next());
  		default :
  			final List<BooleanValue> vals = new LinkedList<BooleanValue>();
  			for(BooleanValue v : acc) { 
  				vals.add(v);
  			}
  			while(vals.size()>1) { 
  				final ListIterator<BooleanValue> itr = vals.listIterator();
  				for(int i = 0, max = vals.size()-1; i < max; i+=2) { 
  					final BooleanValue v0 = itr.next();
  					itr.remove();
  					final BooleanValue v1 = itr.next();
  					final BooleanValue v0opv1 = assemble(op, v0, v1);
  					if (v0opv1==op.shortCircuit()) return op.shortCircuit();
  					else if (v0opv1==op.identity()) itr.remove();
  					else itr.set(v0opv1);
  				}
  			}
  			return vals.get(0);
  		}
  	}
  	
  	/**
  	 * Returns a BooleanFormula f such that [[f]] = f0 op f1.  The method
  	 * requires that the formulas f0 and f1 be already reduced with respect to op.
  	 * A new formula is created and cached iff the circuit with the meaning
  	 * [[f0]] op [[f1]] has not already been created.
  	 * @requires f0 and f1 have already been reduced with respect to op; i.e.  
  	 * f0 op f1 cannot be reduced to a constant or a simple circuit 
  	 * by applying absorption, idempotence, etc. laws to f0 and f1.
  	 * @return f : BooleanFormula | [[f]] = [[f0]] op [[f1]]
  	 * @ensures f !in this.values => this.values' = this.values + f,
  	 * 	        this.values' = this.values
  	 */
  	private BooleanFormula cache(Operator.Nary op, BooleanFormula f0, BooleanFormula f1) {
  		final BooleanFormula l, h;
  		if (f0.label()<f1.label()) {
  			l = f0; h = f1;
  		} else {
  			l = f1; h = f0;
  		}
  		final int hash = op.hash(l,h);
  		for(Iterator<BooleanFormula> gates = opCache(op).get(hash); gates.hasNext(); ) {
  			BooleanFormula gate = gates.next();
  			if (gate.size()==2 && gate.input(0)==l && gate.input(1)==h)
  				return gate;
  		}
  		final BooleanFormula ret = new BinaryGate(op, label++, hash, l, h);
  		opCache(op).add(ret);
  		return ret;
  	}
  	
  	
  }
  