/* ExprTransl - Decompiled by JODE
 * Visit http://jode.sourceforge.net/
 */
package alloy.transl;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.List;

import alloy.bool.BooleanFormula;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.MultiDimArray;
import alloy.util.MultiDimIter;

public class ExprTransl extends Transl
{
    private MultiDimArray _formulas;
    private RelationType _relType;
    
    public ExprTransl(MultiDimArray multidimarray) {
	_formulas = multidimarray;
    }
    
    public List getBooleanFormulas() {
	return Collections
		   .unmodifiableList(Arrays.asList(_formulas.getFlatData()));
    }
    
    public MultiDimArray getFormulaArray() {
	return _formulas;
    }
    
    public BooleanFormula getTupleFormula(int[] is) {
	return (BooleanFormula) _formulas.get(is);
    }
    
    public BooleanFormula getTupleFormula(int i, int i_0_) {
	return getTupleFormula(new int[] { i, i_0_ });
    }
    
    void setType(RelationType relationtype) {
	_relType = relationtype;
    }
    
    public String interpret(boolean[] bools) {
	String string = "{ ";
	MultiDimIter multidimiter = new MultiDimIter(_formulas.getDims());
	while (multidimiter.hasNext()) {
	    int[] is = (int[]) multidimiter.next();
	    BooleanFormula booleanformula = (BooleanFormula) _formulas.get(is);
	    if (booleanformula.interpret(bools)) {
		string += "(";
		for (int i = 0; i < is.length; i++) {
		    String string_1_
			= (_relType == null ? String.valueOf(is[i])
			   : _relType.getBasicTypeAt(i).getAtomName(is[i]));
		    string
			= string + string_1_ + (i == is.length - 1 ? "" : " ");
		}
		string += ") ";
	    }
	}
	return string += " }";
    }
    
    void dump() {
	System.err.print("{ ");
	MultiDimIter multidimiter = new MultiDimIter(_formulas.getDims());
	while (multidimiter.hasNext()) {
	    int[] is = (int[]) multidimiter.next();
	    BooleanFormula booleanformula = (BooleanFormula) _formulas.get(is);
	    System.err.print("(");
	    for (int i = 0; i < is.length; i++)
		System.err.print(is[i] + " ");
	    System.err.println(": ");
	    booleanformula.dump();
	    System.err.print(") ");
	}
	System.err.println(" }");
    }
    
    public ExprTransl union(ExprTransl exprtransl_2_) {
	MultiDimArray multidimarray
	    = new MultiDimArray(exprtransl_2_._formulas.getDims());
	for (int i = 0; i < _formulas.getFlatSize(); i++) {
	    BooleanFormula booleanformula
		= (BooleanFormula) _formulas.getFlat(i);
	    BooleanFormula booleanformula_3_
		= (BooleanFormula) exprtransl_2_._formulas.getFlat(i);
	    multidimarray.putFlat(i, booleanformula.or(booleanformula_3_));
	}
	return new ExprTransl(multidimarray);
    }
    
    public ExprTransl intersection(ExprTransl exprtransl_4_) {
	MultiDimArray multidimarray
	    = new MultiDimArray(exprtransl_4_._formulas.getDims());
	for (int i = 0; i < _formulas.getFlatSize(); i++) {
	    BooleanFormula booleanformula
		= (BooleanFormula) _formulas.getFlat(i);
	    BooleanFormula booleanformula_5_
		= (BooleanFormula) exprtransl_4_._formulas.getFlat(i);
	    multidimarray.putFlat(i, booleanformula.and(booleanformula_5_));
	}
	return new ExprTransl(multidimarray);
    }
    
    public ExprTransl difference(ExprTransl exprtransl_6_) {
	MultiDimArray multidimarray
	    = new MultiDimArray(exprtransl_6_._formulas.getDims());
	for (int i = 0; i < _formulas.getFlatSize(); i++) {
	    BooleanFormula booleanformula
		= (BooleanFormula) _formulas.getFlat(i);
	    BooleanFormula booleanformula_7_
		= (BooleanFormula) exprtransl_6_._formulas.getFlat(i);
	    multidimarray.putFlat(i,
				  booleanformula.and(booleanformula_7_.not()));
	}
	return new ExprTransl(multidimarray);
    }
    
    public FormulaTransl subset(ExprTransl exprtransl_8_) {
	int i = _formulas.getFlatSize();
	BooleanFormula[] booleanformulas = new BooleanFormula[i];
	for (int i_9_ = 0; i_9_ < i; i_9_++) {
	    BooleanFormula booleanformula
		= (BooleanFormula) _formulas.getFlat(i_9_);
	    BooleanFormula booleanformula_10_
		= (BooleanFormula) exprtransl_8_._formulas.getFlat(i_9_);
	    Dbg.chk(booleanformula);
	    Dbg.chk(booleanformula_10_);
	    booleanformulas[i_9_] = booleanformula.implies(booleanformula_10_);
	}
	return new FormulaTransl(BooleanFormula.makeAnd(booleanformulas));
    }
    
    public FormulaTransl equality(ExprTransl exprtransl_11_) {
	int i = _formulas.getFlatSize();
	BooleanFormula[] booleanformulas = new BooleanFormula[i];
	for (int i_12_ = 0; i_12_ < i; i_12_++) {
	    BooleanFormula booleanformula
		= (BooleanFormula) _formulas.getFlat(i_12_);
	    BooleanFormula booleanformula_13_
		= (BooleanFormula) exprtransl_11_._formulas.getFlat(i_12_);
	    booleanformulas[i_12_] = booleanformula.iff(booleanformula_13_);
	}
	return new FormulaTransl(BooleanFormula.makeAnd(booleanformulas));
    }
    
    public ExprTransl dot(ExprTransl exprtransl_14_) {
	int[] is = _formulas.getDims();
	int[] is_15_ = exprtransl_14_._formulas.getDims();
	int[] is_16_ = new int[is.length + is_15_.length - 2];
	System.arraycopy(is, 0, is_16_, 0, is.length - 1);
	System.arraycopy(is_15_, 1, is_16_, is.length - 1, is_15_.length - 1);
	MultiDimArray multidimarray = new MultiDimArray(is_16_);
	int i = is_15_[0];
	int[] is_17_ = new int[is.length];
	int[] is_18_ = new int[is_15_.length];
	MultiDimIter multidimiter = new MultiDimIter(is_16_);
	while (multidimiter.hasNext()) {
	    int[] is_19_ = (int[]) multidimiter.next();
	    System.arraycopy(is_19_, 0, is_17_, 0, is_17_.length - 1);
	    System.arraycopy(is_19_, is_17_.length - 1, is_18_, 1,
			     is_18_.length - 1);
	    ArrayList arraylist = new ArrayList();
	    for (int i_20_ = 0; i_20_ < i; i_20_++) {
		is_17_[is_17_.length - 1] = is_18_[0] = i_20_;
		BooleanFormula booleanformula
		    = (BooleanFormula) _formulas.get(is_17_);
		BooleanFormula booleanformula_21_
		    = (BooleanFormula) exprtransl_14_._formulas.get(is_18_);
		arraylist.add(booleanformula.and(booleanformula_21_));
	    }
	    multidimarray.put(is_19_, BooleanFormula.makeOr(arraylist));
	}
	return new ExprTransl(multidimarray);
    }
    
    public ExprTransl arrow(ExprTransl exprtransl_22_) {
	int[] is = _formulas.getDims();
	int[] is_23_ = exprtransl_22_._formulas.getDims();
	int[] is_24_ = new int[is.length + is_23_.length];
	System.arraycopy(is, 0, is_24_, 0, is.length);
	System.arraycopy(is_23_, 0, is_24_, is.length, is_23_.length);
	MultiDimArray multidimarray = new MultiDimArray(is_24_);
	int[] is_25_ = new int[is.length];
	int[] is_26_ = new int[is_23_.length];
	MultiDimIter multidimiter = new MultiDimIter(is_24_);
	while (multidimiter.hasNext()) {
	    int[] is_27_ = (int[]) multidimiter.next();
	    System.arraycopy(is_27_, 0, is_25_, 0, is_25_.length);
	    System.arraycopy(is_27_, is_25_.length, is_26_, 0, is_26_.length);
	    BooleanFormula booleanformula
		= (BooleanFormula) _formulas.get(is_25_);
	    BooleanFormula booleanformula_28_
		= (BooleanFormula) exprtransl_22_._formulas.get(is_26_);
	    multidimarray.put(is_27_, booleanformula.and(booleanformula_28_));
	}
	return new ExprTransl(multidimarray);
    }
    
    public ExprTransl transitiveClosure() {
	int[] is = _formulas.getDims();
	Dbg.chk(is.length == 2 && is[0] == is[1]);
	ExprTransl exprtransl_29_ = this;
	for (int i = 1; i < is[0]; i *= 2) {
	    ExprTransl exprtransl_30_ = exprtransl_29_.dot(exprtransl_29_);
	    exprtransl_29_ = exprtransl_29_.union(exprtransl_30_);
	}
	return exprtransl_29_;
    }
    
    public ExprTransl transpose() {
	int[] is = _formulas.getDims();
	Dbg.chk(is.length == 2);
	int[] is_31_ = { is[1], is[0] };
	MultiDimArray multidimarray = new MultiDimArray(is_31_);
	int[] is_32_ = new int[2];
	int[] is_33_ = new int[2];
	for (int i = 0; i < is_31_[0]; i++) {
	    for (int i_34_ = 0; i_34_ < is_31_[1]; i_34_++) {
		is_33_[0] = i;
		is_33_[1] = i_34_;
		is_32_[0] = i_34_;
		is_32_[1] = i;
		multidimarray.put(is_33_, _formulas.get(is_32_));
	    }
	}
	return new ExprTransl(multidimarray);
    }
    
    public ExprTransl reflexiveTransitiveClosure() {
	return transitiveClosure()
		   .union(makeIdentityRelation(_formulas.getDims()));
    }
    
    public static ExprTransl makeZeroRelation(int[] is) {
	MultiDimArray multidimarray = new MultiDimArray(is);
	Arrays.fill(multidimarray.getFlatData(), BooleanFormula.FALSE);
	return new ExprTransl(multidimarray);
    }
    
    public static ExprTransl makeUniversalRelation(int[] is) {
	MultiDimArray multidimarray = new MultiDimArray(is);
	Arrays.fill(multidimarray.getFlatData(), BooleanFormula.TRUE);
	return new ExprTransl(multidimarray);
    }
    
    public static ExprTransl makeIdentityRelation(int[] is) {
	Dbg.chk(is.length == 2 && is[0] == is[1]);
	ExprTransl exprtransl = makeZeroRelation(is);
	int[] is_35_ = new int[2];
	for (int i = 0; i < is[0]; i++) {
	    is_35_[0] = is_35_[1] = i;
	    exprtransl._formulas.put(is_35_, BooleanFormula.TRUE);
	}
	return exprtransl;
    }
    
    public static ExprTransl ifThenElse(FormulaTransl formulatransl,
					ExprTransl exprtransl,
					ExprTransl exprtransl_36_) {
	BooleanFormula booleanformula = formulatransl.formula;
	MultiDimArray multidimarray
	    = new MultiDimArray(exprtransl._formulas.getDims());
	for (int i = 0; i < exprtransl._formulas.getFlatSize(); i++) {
	    BooleanFormula booleanformula_37_
		= (BooleanFormula) exprtransl._formulas.getFlat(i);
	    BooleanFormula booleanformula_38_
		= (BooleanFormula) exprtransl_36_._formulas.getFlat(i);
	    multidimarray.putFlat
		(i,
		 booleanformula.implies(booleanformula_37_)
		     .and(booleanformula.not().implies(booleanformula_38_)));
	}
	return new ExprTransl(multidimarray);
    }
}