/* TranslVisitor - Decompiled by JODE
 * Visit http://jode.sourceforge.net/
 */
package alloy.transl;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.ast.ASTDepthFirstReturnVisitor;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryFormula;
import alloy.ast.BinaryIntExpr;
import alloy.ast.CardinalityExpr;
import alloy.ast.ComprehensionExpr;
import alloy.ast.Decl;
import alloy.ast.DeclIter;
import alloy.ast.Decls;
import alloy.ast.ElemFormula;
import alloy.ast.ElemIntFormula;
import alloy.ast.EmptyFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.FieldExpr;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.GenericConstExpr;
import alloy.ast.HasType;
import alloy.ast.IdentityExpr;
import alloy.ast.IfThenElseExpr;
import alloy.ast.IfThenElseIntExpr;
import alloy.ast.ImplicationFormula;
import alloy.ast.IntExpr;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.LiteralIntExpr;
import alloy.ast.MultiplicityExpr;
import alloy.ast.NegFormula;
import alloy.ast.Node;
import alloy.ast.QuantifiedExpr;
import alloy.ast.QuantifiedFormula;
import alloy.ast.SigExpr;
import alloy.ast.SumIntExpr;
import alloy.ast.UnaryExpr;
import alloy.ast.UniversalExpr;
import alloy.ast.VarCreator;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.bool.BoolSwitch;
import alloy.bool.BooleanFormula;
import alloy.semantic.LocalScope;
import alloy.transform.LeafIdMap;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.MultiDimArray;
import alloy.util.MultiDimIter;
import alloy.util.Params;

public class TranslVisitor extends ASTDepthFirstReturnVisitor
    implements TranslInfo
{
    private Map _leafTransl = new TreeMap();
    private Map _leafType = new TreeMap();
    private Map _leafMult = new TreeMap();
    private Map _leafRep = new TreeMap();
    private Map _node2transl = new TreeMap();
    private Map _relations = new TreeMap();
    private Map _var2switch = new TreeMap();
    private Map _var2creator = new TreeMap();
    private BoolVarAllocator _boolVarAllocator = null;
    private RelationAllocator _relationAllocator = null;
    private Formula _formula;
    private ASTInfoVisitor _astInfoVisitor;
    private long _boolNodesAllocated = 0L;
    
    private Transl _saveTransl(Node node, Transl transl) {
	if (node instanceof HasType)
	    ((ExprTransl) transl).setType(((HasType) node).getType());
	_node2transl.put(node, transl);
	return transl;
    }
    
    private void _countBoolNode() throws TranslException {
	if (_boolNodesAllocated++
	    > Params.glob.getLongParam("MAIN", "maxBoolNodes"))
	    throw new TranslException
		      ("Too many Boolean nodes.  \nCheck for higher-order quantifiers.\nTry increasing MAIN.maxBoolNodes parameter");
	if (Runtime.getRuntime().freeMemory() < 100000L) {
	    System.gc();
	    System.gc();
	    System.gc();
	    if (Runtime.getRuntime().freeMemory() < 100000L)
		throw new TranslException("Translation ran out of memory.");
	}
    }
    
    private TranslVisitor(RelationAllocator relationallocator) {
	_relationAllocator = relationallocator;
	_boolVarAllocator = relationallocator.getBoolVarAllocator();
    }
    
    public static TranslInfo translate
	(Formula formula, RelationAllocator relationallocator)
	throws TranslException {
	formula.applyVisitor(new TranslatableASTCheckVisitor());
	ASTInfoVisitor astinfovisitor = new ASTInfoVisitor();
	formula.applyVisitor(astinfovisitor);
	TranslVisitor translvisitor = new TranslVisitor(relationallocator);
	translvisitor.setFormula(formula);
	translvisitor._astInfoVisitor = astinfovisitor;
	formula.applyReturnVisitor(translvisitor);
	return translvisitor;
    }
    
    private Object _visitLeafExpr(LeafExpr leafexpr) {
	Dbg.chk(leafexpr.getLeafId());
	ExprTransl exprtransl
	    = (ExprTransl) _leafTransl.get(leafexpr.getLeafId());
	if (exprtransl != null)
	    return _saveTransl(leafexpr, exprtransl);
	RelationType relationtype = leafexpr.getType();
	int[] is = new int[relationtype.numBasicTypes()];
	for (int i = 0; i < is.length; i++)
	    is[i] = relationtype.getBasicTypeAt(i).getScope();
	exprtransl = _relationAllocator.allocRelation(leafexpr, is);
	_leafTransl.put(leafexpr.getLeafId(), exprtransl);
	_relations.put(leafexpr.getLeafId(), leafexpr);
	_leafType.put(leafexpr.getLeafId(), relationtype);
	return _saveTransl(leafexpr, exprtransl);
    }
    
    public void interpretRelations(boolean[] bools) {
	System.out.println
	    ("=============================================================");
	Iterator iterator = _relations.entrySet().iterator();
	while (iterator.hasNext()) {
	    Map.Entry entry = (Map.Entry) iterator.next();
	    LeafId leafid = (LeafId) entry.getKey();
	    LeafExpr leafexpr = (LeafExpr) entry.getValue();
	    String string = leafexpr.nodeString();
	    ExprTransl exprtransl = (ExprTransl) _leafTransl.get(leafid);
	    exprtransl.setType(leafexpr.getType());
	    RelationType relationtype = leafexpr.getType();
	    String string_0_ = relationtype.getBasicTypeAt(0).toShortString();
	    string = (relationtype.numBasicTypes() == 1 ? string
		      : string_0_ + "$" + string);
	    System.out.println("---------------------------");
	    System.out.println("relation: " + string + " (type: "
			       + relationtype.toShortString() + ")");
	    System.out.println(exprtransl.interpret(bools));
	}
	System.out.println
	    ("=============================================================");
    }
    
    public Object visit(SigExpr sigexpr) {
	return _visitLeafExpr(sigexpr);
    }
    
    public Object visit(FieldExpr fieldexpr) {
	return _visitLeafExpr(fieldexpr);
    }
    
    public Object visit(VariableExpr variableexpr) {
	ExprTransl exprtransl
	    = (ExprTransl) _leafTransl.get(variableexpr.getLeafId());
	if (exprtransl != null)
	    return _saveTransl(variableexpr, exprtransl);
	return (variableexpr.isQuantified
		? _visitQuantifiedVariable(variableexpr,
					   variableexpr.getType(),
					   variableexpr.getLeafId())
		: _visitLeafExpr(variableexpr));
    }
    
    private MultiDimArray _allocFormulas(RelationType relationtype) {
	int[] is = new int[relationtype.numBasicTypes()];
	for (int i = 0; i < is.length; i++)
	    is[i] = relationtype.getBasicTypeAt(i).getScope();
	return new MultiDimArray(is);
    }
    
    private Object _visitQuantifiedVariable
	(VariableExpr variableexpr, RelationType relationtype, LeafId leafid) {
	MultiDimArray multidimarray = _allocFormulas(relationtype);
	BoolSwitch boolswitch = new BoolSwitch(variableexpr.toString());
	_var2switch.put(leafid, boolswitch);
	if (multidimarray.getFlatSize() >= 64)
	    throw new TranslException("Quantifier too large");
	MultiDimIter multidimiter = new MultiDimIter(multidimarray.getDims());
	while (multidimiter.hasNext()) {
	    int[] is = (int[]) multidimiter.next();
	    _countBoolNode();
	    BooleanFormula booleanformula
		= (BooleanFormula.makeSwitchableConst
		   (boolswitch,
		    (long) _computeBitNumber(relationtype, is, 0)));
	    multidimarray.put(is, booleanformula);
	}
	ExprTransl exprtransl = new ExprTransl(multidimarray);
	_leafTransl.put(leafid, exprtransl);
	return _saveTransl(variableexpr, exprtransl);
    }
    
    public Object visit(ElemFormula elemformula) {
	ExprTransl exprtransl
	    = (ExprTransl) elemformula.getLeft().applyReturnVisitor(this);
	ExprTransl exprtransl_1_
	    = (ExprTransl) elemformula.getRight().applyReturnVisitor(this);
	FormulaTransl formulatransl = null;
	switch (elemformula.getOp().getOpCode()) {
	case 0:
	case 2:
	    formulatransl = exprtransl.subset(exprtransl_1_);
	    break;
	case 1:
	    formulatransl = exprtransl.equality(exprtransl_1_);
	    break;
	}
	if (elemformula.getOp().getNeg())
	    formulatransl = formulatransl.not();
	return _saveTransl(elemformula, formulatransl);
    }
    
    public Object visit(FormulaSeq formulaseq) {
	ArrayList arraylist = new ArrayList();
	Iterator iterator = formulaseq.getFormulas().getFormulaIter();
	while (iterator.hasNext()) {
	    Formula formula = (Formula) iterator.next();
	    FormulaTransl formulatransl
		= (FormulaTransl) formula.applyReturnVisitor(this);
	    arraylist.add(formulatransl.formula);
	}
	_countBoolNode();
	FormulaTransl formulatransl
	    = new FormulaTransl(BooleanFormula.makeAnd(arraylist));
	_saveTransl(formulaseq.getFormulas(), formulatransl);
	return _saveTransl(formulaseq, formulatransl);
    }
    
    public Object visit(Node node) {
	Dbg.fatal("untranslated node: " + node);
	return null;
    }
    
    public Object visit(EmptyFormula emptyformula) {
	return _saveTransl(emptyformula, FormulaTransl.TRUE);
    }
    
    public Object visit(BinaryFormula binaryformula) {
	FormulaTransl formulatransl
	    = (FormulaTransl) binaryformula.getLeft().applyReturnVisitor(this);
	FormulaTransl formulatransl_2_
	    = ((FormulaTransl)
	       binaryformula.getRight().applyReturnVisitor(this));
	FormulaTransl formulatransl_3_ = null;
	switch (binaryformula.getOp().getOpCode()) {
	case 0:
	    formulatransl_3_ = formulatransl.and(formulatransl_2_);
	    break;
	case 1:
	    formulatransl_3_ = formulatransl.or(formulatransl_2_);
	    break;
	case 2:
	    formulatransl_3_ = formulatransl.iff(formulatransl_2_);
	    break;
	}
	return _saveTransl(binaryformula, formulatransl_3_);
    }
    
    public Object visit(ImplicationFormula implicationformula) {
	FormulaTransl formulatransl
	    = ((FormulaTransl)
	       implicationformula.getIfFormula().applyReturnVisitor(this));
	FormulaTransl formulatransl_4_
	    = ((FormulaTransl)
	       implicationformula.getThenFormula().applyReturnVisitor(this));
	FormulaTransl formulatransl_5_
	    = ((FormulaTransl)
	       implicationformula.getElseFormula().applyReturnVisitor(this));
	return _saveTransl(implicationformula,
			   (formulatransl.implies(formulatransl_4_).and
			    (formulatransl.not().implies(formulatransl_5_))));
    }
    
    public Object visit(NegFormula negformula) {
	FormulaTransl formulatransl
	    = (FormulaTransl) negformula.getFormula().applyReturnVisitor(this);
	return _saveTransl(negformula, formulatransl.not());
    }
    
    public Object visit(QuantifiedExpr quantifiedexpr) {
	ExprTransl exprtransl
	    = (ExprTransl) quantifiedexpr.getExpr().applyReturnVisitor(this);
	IntTransl inttransl = IntTransl.fromExprTransl(exprtransl);
	FormulaTransl formulatransl = null;
	switch (quantifiedexpr.getQuantifier().getOpCode()) {
	case 1:
	    formulatransl = inttransl.eq(IntTransl.ZERO);
	    /* fall through */
	case 4:
	    formulatransl = inttransl.eq(IntTransl.ONE);
	    /* fall through */
	case 5:
	    formulatransl = inttransl.eq(IntTransl.TWO);
	    /* fall through */
	case 3:
	    formulatransl = inttransl.le(IntTransl.ONE);
	    /* fall through */
	case 2:
	    formulatransl = inttransl.gt(IntTransl.ZERO);
	    /* fall through */
	case 0:
	    Dbg.unimpl("all expr");
	    /* fall through */
	default:
	    return _saveTransl(quantifiedexpr, formulatransl);
	}
    }
    
    public Object visit(SumIntExpr sumintexpr) {
	IntTransl inttransl
	    = (IntTransl) sumintexpr.getBody().applyReturnVisitor(this);
	BooleanFormula[] booleanformulas = inttransl.getBits();
	LocalScope localscope = sumintexpr.getLocalScope();
	LeafIdMap leafidmap = sumintexpr.getLeafIdMap();
	Decls decls = sumintexpr.getDecls();
	Iterator iterator = decls.getDeclIter();
	while (iterator.hasNext()) {
	    Decl decl = (Decl) iterator.next();
	    Iterator iterator_6_ = decl.getVariables().getVariableIter();
	    while (iterator_6_.hasNext()) {
		Variable variable = (Variable) iterator_6_.next();
		String string = variable.nodeString();
		LeafId leafid = leafidmap.lookupLeafId(string);
		RelationType relationtype = localscope.lookupType(string);
		MultiplicityExpr multiplicityexpr = decl.getExpr();
		_leafType.put(leafid, relationtype);
		_leafMult.put(leafid, multiplicityexpr);
		_leafRep.put(leafid, variable);
		_var2creator.put(leafid, sumintexpr);
		BoolSwitch boolswitch = (BoolSwitch) _var2switch.get(leafid);
		if (boolswitch != null) {
		    Dbg.chk(relationtype.numBasicTypes() == 1);
		    int i = relationtype.getBasicTypeAt(0).getScope();
		    ArrayList arraylist = new ArrayList();
		    Iterator iterator_7_
			= VariableValueIterator.makeIterator(relationtype,
							     multiplicityexpr,
							     false);
		    while (iterator_7_.hasNext()) {
			Long var_long = (Long) iterator_7_.next();
			BooleanFormula[] booleanformulas_8_
			    = new BooleanFormula[booleanformulas.length];
			for (int i_9_ = 0; i_9_ < booleanformulas_8_.length;
			     i_9_++) {
			    _countBoolNode();
			    booleanformulas_8_[i_9_]
				= BooleanFormula.makeSwitch(boolswitch,
							    var_long
								.longValue(),
							    (booleanformulas
							     [i_9_]));
			}
			arraylist.add(new IntTransl(booleanformulas_8_));
		    }
		    booleanformulas = IntTransl.makeSum(arraylist).getBits();
		}
	    }
	}
	return _saveTransl(sumintexpr, new IntTransl(booleanformulas));
    }
    
    public Object visit(QuantifiedFormula quantifiedformula) {
	FormulaTransl formulatransl
	    = ((FormulaTransl)
	       quantifiedformula.getFormula().applyReturnVisitor(this));
	BooleanFormula booleanformula = formulatransl.formula;
	int i = quantifiedformula.getQuantifier().getOpCode();
	Dbg.chk(i == 0 || i == 2);
	DeclIter decliter = new DeclIter(quantifiedformula);
	while (decliter.hasNext()) {
	    Variable variable = decliter.nextVar();
	    String string = variable.nodeString();
	    LeafId leafid = decliter.getLeafId();
	    RelationType relationtype = decliter.getType();
	    MultiplicityExpr multiplicityexpr = decliter.getMultiplicity();
	    _leafType.put(leafid, relationtype);
	    _leafMult.put(leafid, multiplicityexpr);
	    _leafRep.put(leafid, variable);
	    _var2creator.put(leafid, quantifiedformula);
	    BoolSwitch boolswitch = (BoolSwitch) _var2switch.get(leafid);
	    if (boolswitch != null) {
		ArrayList arraylist = new ArrayList();
		Iterator iterator
		    = VariableValueIterator
			  .makeIterator(relationtype, multiplicityexpr, false);
		while (iterator.hasNext()) {
		    Long var_long = (Long) iterator.next();
		    _countBoolNode();
		    BooleanFormula booleanformula_10_
			= BooleanFormula.makeSwitch(boolswitch,
						    var_long.longValue(),
						    booleanformula);
		    booleanformula_10_.setDescr(string);
		    arraylist.add(booleanformula_10_);
		}
		_countBoolNode();
		booleanformula = (i == 0 ? BooleanFormula.makeAnd(arraylist)
				  : BooleanFormula.makeOr(arraylist));
	    }
	}
	return _saveTransl(quantifiedformula,
			   new FormulaTransl(booleanformula));
    }
    
    public Object visit(ComprehensionExpr comprehensionexpr) {
	FormulaTransl formulatransl
	    = ((FormulaTransl)
	       comprehensionexpr.getFormula().applyReturnVisitor(this));
	LocalScope localscope = comprehensionexpr.getLocalScope();
	LeafIdMap leafidmap = comprehensionexpr.getLeafIdMap();
	MultiDimArray multidimarray
	    = _allocFormulas(comprehensionexpr.getType());
	Arrays.fill(multidimarray.getFlatData(), formulatransl.formula);
	int i = 0;
	Decls decls = comprehensionexpr.getDecls();
	Iterator iterator = decls.getDeclIter();
	while (iterator.hasNext()) {
	    Decl decl = (Decl) iterator.next();
	    Iterator iterator_11_ = decl.getVariables().getVariableIter();
	    while (iterator_11_.hasNext()) {
		Variable variable = (Variable) iterator_11_.next();
		String string = variable.nodeString();
		LeafId leafid = leafidmap.lookupLeafId(string);
		BoolSwitch boolswitch = (BoolSwitch) _var2switch.get(leafid);
		Dbg.chk(boolswitch);
		RelationType relationtype = localscope.lookupType(string);
		_leafType.put(leafid, relationtype);
		_leafMult.put(leafid, decl.getExpr());
		_leafRep.put(leafid, variable);
		_var2creator.put(leafid, comprehensionexpr);
		MultiDimIter multidimiter
		    = new MultiDimIter(multidimarray.getDims());
		while (multidimiter.hasNext()) {
		    int[] is = (int[]) multidimiter.next();
		    BooleanFormula booleanformula
			= (BooleanFormula) multidimarray.get(is);
		    int i_12_ = _computeBitNumber(relationtype, is, i);
		    _countBoolNode();
		    booleanformula
			= BooleanFormula.makeSwitch(boolswitch,
						    (long) (1 << i_12_),
						    booleanformula);
		    i_12_++;
		    multidimarray.put(is, booleanformula);
		}
		i += relationtype.numBasicTypes();
	    }
	}
	return _saveTransl(comprehensionexpr, new ExprTransl(multidimarray));
    }
    
    private static int _computeBitNumber(RelationType relationtype, int[] is,
					 int i) {
	int i_13_ = 0;
	int i_14_ = 1;
	for (int i_15_ = i + relationtype.numBasicTypes() - 1; i_15_ >= i;
	     i_15_--) {
	    i_13_ += is[i_15_] * i_14_;
	    i_14_ *= relationtype.getBasicTypeAt(i_15_ - i).getScope();
	}
	return i_13_;
    }
    
    public Object visit(BinaryExpr binaryexpr) {
	ExprTransl exprtransl
	    = (ExprTransl) binaryexpr.getLeft().applyReturnVisitor(this);
	ExprTransl exprtransl_16_
	    = (ExprTransl) binaryexpr.getRight().applyReturnVisitor(this);
	ExprTransl exprtransl_17_ = null;
	switch (binaryexpr.getOp().getOpCode()) {
	case 0:
	case 1:
	case 2:
	    exprtransl_17_ = exprtransl.dot(exprtransl_16_);
	    break;
	case 3:
	    exprtransl_17_ = exprtransl.union(exprtransl_16_);
	    break;
	case 4:
	    exprtransl_17_ = exprtransl.difference(exprtransl_16_);
	    break;
	case 5:
	    exprtransl_17_ = exprtransl.intersection(exprtransl_16_);
	    break;
	case 6:
	    exprtransl_17_ = exprtransl.arrow(exprtransl_16_);
	    break;
	}
	return _saveTransl(binaryexpr, exprtransl_17_);
    }
    
    public Object visit(GenericConstExpr genericconstexpr) {
	RelationType relationtype = genericconstexpr.getType();
	MultiDimArray multidimarray = _allocFormulas(relationtype);
	boolean bool = genericconstexpr instanceof EmptySetExpr;
	boolean bool_18_ = genericconstexpr instanceof UniversalExpr;
	boolean bool_19_ = genericconstexpr instanceof IdentityExpr;
	MultiDimIter multidimiter = new MultiDimIter(multidimarray.getDims());
	while (multidimiter.hasNext()) {
	    int[] is = (int[]) multidimiter.next();
	    multidimarray.put(is, (bool ? BooleanFormula.FALSE : bool_18_
				   ? BooleanFormula.TRUE : bool_19_
				   ? BooleanFormula.makeConst(is[0] == is[1])
				   : null));
	}
	return _saveTransl(genericconstexpr, new ExprTransl(multidimarray));
    }
    
    public Object visit(UniversalExpr universalexpr) {
	return visit((GenericConstExpr) universalexpr);
    }
    
    public Object visit(EmptySetExpr emptysetexpr) {
	return visit((GenericConstExpr) emptysetexpr);
    }
    
    public Object visit(IdentityExpr identityexpr) {
	return visit((GenericConstExpr) identityexpr);
    }
    
    public Object visit(UnaryExpr unaryexpr) {
	ExprTransl exprtransl
	    = (ExprTransl) unaryexpr.getExpr().applyReturnVisitor(this);
	ExprTransl exprtransl_20_ = null;
	switch (unaryexpr.getOp().getOpCode()) {
	case 0:
	    exprtransl_20_ = exprtransl.transpose();
	    break;
	case 2:
	    exprtransl_20_ = exprtransl.transitiveClosure();
	    break;
	case 1:
	    exprtransl_20_ = exprtransl.reflexiveTransitiveClosure();
	    break;
	}
	return _saveTransl(unaryexpr, exprtransl_20_);
    }
    
    public Object visit(IfThenElseExpr ifthenelseexpr) {
	FormulaTransl formulatransl
	    = ((FormulaTransl)
	       ifthenelseexpr.getIfFormula().applyReturnVisitor(this));
	ExprTransl exprtransl
	    = ((ExprTransl)
	       ifthenelseexpr.getThenExpr().applyReturnVisitor(this));
	ExprTransl exprtransl_21_
	    = ((ExprTransl)
	       ifthenelseexpr.getElseExpr().applyReturnVisitor(this));
	ExprTransl exprtransl_22_
	    = ExprTransl.ifThenElse(formulatransl, exprtransl, exprtransl_21_);
	return _saveTransl(ifthenelseexpr, exprtransl_22_);
    }
    
    public Object visit(LiteralIntExpr literalintexpr) {
	return _saveTransl(literalintexpr,
			   IntTransl.fromIntConst(literalintexpr.getVal()));
    }
    
    public Object visit(ElemIntFormula elemintformula) {
	IntExpr intexpr = elemintformula.getLeft();
	IntExpr intexpr_23_ = elemintformula.getRight();
	IntTransl inttransl = (IntTransl) intexpr.applyReturnVisitor(this);
	IntTransl inttransl_24_
	    = (IntTransl) intexpr_23_.applyReturnVisitor(this);
	FormulaTransl formulatransl = null;
	switch (elemintformula.getOp().getOpCode()) {
	case 0:
	    formulatransl = inttransl.eq(inttransl_24_);
	    break;
	case 1:
	    formulatransl = inttransl.le(inttransl_24_);
	    break;
	case 2:
	    formulatransl = inttransl.ge(inttransl_24_);
	    break;
	case 3:
	    formulatransl = inttransl.lt(inttransl_24_);
	    break;
	case 4:
	    formulatransl = inttransl.gt(inttransl_24_);
	    break;
	}
	if (elemintformula.getOp().getNeg())
	    formulatransl = formulatransl.not();
	return _saveTransl(elemintformula, formulatransl);
    }
    
    public Object visit(BinaryIntExpr binaryintexpr) {
	IntTransl inttransl
	    = (IntTransl) binaryintexpr.getLeft().applyReturnVisitor(this);
	IntTransl inttransl_25_
	    = (IntTransl) binaryintexpr.getRight().applyReturnVisitor(this);
	switch (binaryintexpr.getOp().getOpCode()) {
	case 0:
	    return _saveTransl(binaryintexpr, inttransl.plus(inttransl_25_));
	default:
	    throw new TranslException
		      ("Only integer addition implemented at this time.");
	}
    }
    
    public Object visit(CardinalityExpr cardinalityexpr) {
	ExprTransl exprtransl
	    = (ExprTransl) cardinalityexpr.getExpr().applyReturnVisitor(this);
	return _saveTransl(cardinalityexpr,
			   IntTransl.fromExprTransl(exprtransl));
    }
    
    public Object visit(IfThenElseIntExpr ifthenelseintexpr) {
	FormulaTransl formulatransl
	    = ((FormulaTransl)
	       ifthenelseintexpr.getIfFormula().applyReturnVisitor(this));
	IntTransl inttransl
	    = ((IntTransl)
	       ifthenelseintexpr.getThenIntExpr().applyReturnVisitor(this));
	IntTransl inttransl_26_
	    = ((IntTransl)
	       ifthenelseintexpr.getElseIntExpr().applyReturnVisitor(this));
	IntTransl inttransl_27_
	    = IntTransl.ifThenElse(formulatransl, inttransl, inttransl_26_);
	return _saveTransl(ifthenelseintexpr, inttransl_27_);
    }
    
    public Map getNodeTranslations() {
	return _node2transl;
    }
    
    public Transl getNodeTransl(Node node) {
	return (Transl) _node2transl.get(node);
    }
    
    public Map getVarSwitches() {
	return _var2switch;
    }
    
    public BoolSwitch getVarSwitch(LeafId leafid) {
	return (BoolSwitch) _var2switch.get(leafid);
    }
    
    public Map getRelationTransls() {
	TreeMap treemap = new TreeMap();
	Iterator iterator = _relations.entrySet().iterator();
	while (iterator.hasNext()) {
	    Map.Entry entry = (Map.Entry) iterator.next();
	    LeafId leafid = (LeafId) entry.getKey();
	    LeafExpr leafexpr = (LeafExpr) entry.getValue();
	    RelationType relationtype = leafexpr.getType();
	    ExprTransl exprtransl = (ExprTransl) _leafTransl.get(leafid);
	    treemap.put(exprtransl, relationtype);
	}
	return treemap;
    }
    
    public Map getRelations() {
	return _relations;
    }
    
    public Map getLeafTransls() {
	return _leafTransl;
    }
    
    public Transl getLeafTransl(LeafId leafid) {
	return (Transl) _leafTransl.get(leafid);
    }
    
    public RelationType getLeafType(LeafId leafid) {
	return (RelationType) _leafType.get(leafid);
    }
    
    public MultiplicityExpr getLeafMultiplicity(LeafId leafid) {
	return (MultiplicityExpr) _leafMult.get(leafid);
    }
    
    public Variable getVariable(LeafId leafid) {
	return (Variable) _leafRep.get(leafid);
    }
    
    public Map getRelationExprsToTransls() {
	TreeMap treemap = new TreeMap();
	Iterator iterator = _relations.entrySet().iterator();
	while (iterator.hasNext()) {
	    Map.Entry entry = (Map.Entry) iterator.next();
	    LeafId leafid = (LeafId) entry.getKey();
	    LeafExpr leafexpr = (LeafExpr) entry.getValue();
	    ExprTransl exprtransl = (ExprTransl) _leafTransl.get(leafid);
	    treemap.put(leafexpr, exprtransl);
	}
	return treemap;
    }
    
    public BoolVarAllocator getBoolVarAllocator() {
	return _boolVarAllocator;
    }
    
    public RelationAllocator getRelationAllocator() {
	return _relationAllocator;
    }
    
    public Set getBasicTypes() {
	TreeSet treeset = new TreeSet();
	Iterator iterator = _relations.entrySet().iterator();
	while (iterator.hasNext()) {
	    Map.Entry entry = (Map.Entry) iterator.next();
	    LeafExpr leafexpr = (LeafExpr) entry.getValue();
	    RelationType relationtype = leafexpr.getType();
	    Iterator iterator_28_ = relationtype.getTypeIter();
	    while (iterator_28_.hasNext())
		treeset.add(iterator_28_.next());
	}
	return treeset;
    }
    
    public VarCreator getVarCreator(LeafId leafid) {
	return (VarCreator) _var2creator.get(leafid);
    }
    
    public void setFormula(Formula formula) {
	_formula = formula;
    }
    
    public Formula getFormula() {
	return _formula;
    }
    
    public Node getParent(Node node) {
	return _astInfoVisitor.getParent(node);
    }
    
    public boolean isAncestor(Node node, Node node_29_) {
	return _astInfoVisitor.isAncestor(node, node_29_);
    }
}