/* TemplateDetectVisitor - Decompiled by JODE
 * Visit http://jode.sourceforge.net/
 */
package alloy.sharbool;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.Comparator;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.ast.ASTDepthFirstReturnVisitor;
import alloy.ast.ComprehensionExpr;
import alloy.ast.DeclIter;
import alloy.ast.Expr;
import alloy.ast.Formula;
import alloy.ast.HasType;
import alloy.ast.Leaf;
import alloy.ast.LeafId;
import alloy.ast.MultiplicityExpr;
import alloy.ast.Node;
import alloy.ast.Op;
import alloy.ast.SetMultExpr;
import alloy.ast.VarCreator;
import alloy.ast.VariableExpr;
import alloy.bool.BoolSwitch;
import alloy.bool.BooleanFormula;
import alloy.transl.Transl;
import alloy.transl.TranslInfo;
import alloy.transl.VariableValueIterator;
import alloy.util.CachingIterator;
import alloy.util.Dbg;
import alloy.util.MultiIter;
import alloy.util.ResettableIterator;

public class TemplateDetectVisitor extends ASTDepthFirstReturnVisitor
{
    private TranslInfo _translator;
    private Map _relTypeTemplate = new TreeMap();
    private Map _leafTemplate = new TreeMap();
    private Map _node2templateInstance = new TreeMap();
    private List _allTemplates = new ArrayList();
    private Map _leafIdSubst = new TreeMap();
    private Set _declaredVarIds = new TreeSet();
    private boolean _isAuxiliary;
    
    public TemplateDetectVisitor(TranslInfo translinfo) {
	_translator = translinfo;
    }
    
    private Object _visitLeaf(Leaf leaf) {
	TemplateInstance templateinstance = new TemplateInstance(leaf);
	_node2templateInstance.put(leaf,
				   Collections.singleton(templateinstance));
	LeafId leafid = leaf.getLeafId();
	if (leafid == null) {
	    System.out.println("NO LEAFID: " + leaf.fullString() + " aux: "
			       + _isAuxiliary);
	    Thread.dumpStack();
	}
	LeafId leafid_0_ = (LeafId) _leafIdSubst.get(leafid);
	if (leafid_0_ != null)
	    leafid = leafid_0_;
	Template template = (Template) _leafTemplate.get(leafid);
	if (template == null) {
	    _allTemplates.add(template = new Template());
	    _leafTemplate.put(leafid, template);
	}
	template.instances.add(templateinstance);
	templateinstance.template = template;
	_chkInst(templateinstance);
	return Collections.singleton(templateinstance);
    }
    
    private Object _visitConstExpr(Expr expr) {
	TemplateInstance templateinstance = new TemplateInstance(expr);
	_node2templateInstance.put(expr,
				   Collections.singleton(templateinstance));
	alloy.type.RelationType relationtype = expr.getType();
	Template template = (Template) _relTypeTemplate.get(relationtype);
	if (template == null) {
	    _allTemplates.add(template = new Template());
	    _relTypeTemplate.put(relationtype, template);
	}
	template.instances.add(templateinstance);
	templateinstance.template = template;
	templateinstance.args.add(expr);
	_chkInst(templateinstance);
	return Collections.singleton(templateinstance);
    }
    
    private boolean _isConstantValued(Node node) {
	if (node instanceof VarCreator)
	    return false;
	Transl transl = _translator.getNodeTransl(node);
	if (transl == null)
	    return true;
	if (!transl.isConstantValued())
	    return false;
	if (node instanceof VariableExpr && ((VariableExpr) node).isQuantified
	    && _declaredVarIds.contains(((VariableExpr) node).getLeafId()))
	    return false;
	if (!(node instanceof Leaf)) {
	    Iterator iterator = node.getChildren();
	    while (iterator.hasNext()) {
		Node node_1_ = (Node) iterator.next();
		if ((!(node instanceof VarCreator)
		     || node_1_ != ((VarCreator) node).getDecls())
		    && !_isConstantValued(node_1_))
		    return false;
	    }
	}
	return true;
    }
    
    public Object visit(Node node) {
	Set set = (Set) _node2templateInstance.get(node);
	if (set != null)
	    return set;
	if (node instanceof Expr && _isConstantValued(node))
	    return _visitConstExpr((Expr) node);
	if (node instanceof Leaf)
	    return _visitLeaf((Leaf) node);
	TemplateInstance templateinstance = new TemplateInstance(node);
	_node2templateInstance.put(node,
				   Collections.singleton(templateinstance));
	VarCreator varcreator
	    = node instanceof VarCreator ? (VarCreator) node : null;
	boolean bool = varcreator != null;
	TreeSet treeset = new TreeSet();
	if (bool) {
	    DeclIter decliter = new DeclIter(varcreator);
	    while (decliter.hasNext()) {
		decliter.next();
		treeset.add(decliter.getLeafId());
	    }
	}
	ArrayList arraylist = new ArrayList();
	Iterator iterator = node.getChildren();
	while (iterator.hasNext()) {
	    Node node_2_ = (Node) iterator.next();
	    if (!bool || node_2_ != varcreator.getDecls())
		arraylist.add(node_2_);
	}
	TemplateInstance[] templateinstances
	    = new TemplateInstance[arraylist.size()];
	for (int i = 0; i < templateinstances.length; i++) {
	    Node node_3_ = (Node) arraylist.get(i);
	    templateinstances[i]
		= _chooseInst(node_3_.applyReturnVisitor(this));
	}
	Object object = null;
	if (!bool) {
	    for (int i = 0; i < templateinstances.length; i++)
		templateinstance.args.addAll(templateinstances[i].args);
	    if (node.numChildren() == 3 && templateinstances.length == 3
		&& node.childAt(1) instanceof Op
		&& ((Op) node.childAt(1)).isCommutative()
		&& (templateinstances[0].template
		    == templateinstances[2].template)) {
		ArrayList arraylist_4_ = new ArrayList();
		arraylist_4_.addAll(templateinstances[2].args);
		Dbg.check(templateinstances[1].args.isEmpty());
		arraylist_4_.addAll(templateinstances[0].args);
	    }
	} else {
	    TemplateInstance templateinstance_5_
		= _getInst(varcreator.getBody());
	    Iterator iterator_6_ = templateinstance_5_.args.iterator();
	    while (iterator_6_.hasNext()) {
		Expr expr = (Expr) iterator_6_.next();
		TemplateDetectVisitor templatedetectvisitor_7_
		    = new TemplateDetectVisitor(_translator);
		templatedetectvisitor_7_._declaredVarIds = treeset;
		templatedetectvisitor_7_._isAuxiliary = true;
		TemplateInstance templateinstance_8_
		    = (_chooseInst
		       (expr.applyReturnVisitor(templatedetectvisitor_7_)));
		templateinstance.args.addAll(templateinstance_8_.args);
	    }
	}
	Dbg.check(templateinstances[0]);
	Dbg.check(templateinstances[0].template);
	TreeSet treeset_9_
	    = new TreeSet(templateinstances[0].template.parents);
	for (int i = 1; i < templateinstances.length; i++) {
	    Dbg.check(templateinstances[i]);
	    Dbg.check(templateinstances[i].template);
	    treeset_9_.retainAll(templateinstances[i].template.parents);
	}
	boolean bool_10_ = false;
	Iterator iterator_11_ = treeset_9_.iterator();
	while (!bool_10_ && iterator_11_.hasNext()) {
	    Template template = (Template) iterator_11_.next();
	    TemplateInstance templateinstance_12_ = template.getAnInstance();
	    Node node_13_ = templateinstance_12_.node;
	    if (node_13_.getClass().equals(node.getClass())
		&& (!(node instanceof HasType)
		    || ((HasType) node).getType()
			   .equals(((HasType) node_13_).getType()))
		&& template.children.length == arraylist.size()) {
		boolean bool_14_ = true;
		for (int i = 0; i < templateinstances.length; i++)
		    bool_14_ = bool_14_ & (templateinstances[i].template
					   == template.children[i]);
		if (bool_14_) {
		    boolean bool_15_ = true;
		    if (bool) {
			DeclIter decliter = new DeclIter(varcreator);
			DeclIter decliter_16_
			    = new DeclIter((VarCreator) node_13_);
			boolean bool_17_ = false;
			TreeMap treemap = new TreeMap();
			while (!bool_17_ && decliter.hasNext()
			       && decliter_16_.hasNext()) {
			    decliter.next();
			    decliter_16_.next();
			    MultiplicityExpr multiplicityexpr
				= decliter.getMultiplicity();
			    MultiplicityExpr multiplicityexpr_18_
				= decliter_16_.getMultiplicity();
			    bool_17_ = (bool_17_
					| (!decliter.getType()
						.equals(decliter_16_.getType())
					   || !(multiplicityexpr.isSameAs
						(multiplicityexpr_18_))));
			    treemap.put(decliter.getLeafId(),
					decliter_16_.getLeafId());
			}
			bool_17_ = bool_17_ | (decliter.hasNext()
					       || decliter_16_.hasNext());
			if (bool_17_)
			    bool_15_ = false;
			else {
			    TemplateInstance templateinstance_19_
				= _getInst(varcreator.getBody());
			    TemplateInstance templateinstance_20_
				= _getInst(((VarCreator) node_13_).getBody());
			    Dbg.check(templateinstance_19_.template
				      == templateinstance_20_.template);
			    Dbg.check(templateinstance_19_.args.size()
				      == templateinstance_20_.args.size());
			    for (int i = 0;
				 (bool_15_
				  && i < templateinstance_19_.args.size());
				 i++) {
				Expr expr
				    = (Expr) templateinstance_19_.args.get(i);
				Expr expr_21_
				    = (Expr) templateinstance_20_.args.get(i);
				TemplateDetectVisitor templatedetectvisitor_22_
				    = new TemplateDetectVisitor(_translator);
				templatedetectvisitor_22_._isAuxiliary = true;
				templatedetectvisitor_22_._leafIdSubst
				    = treemap;
				templatedetectvisitor_22_._declaredVarIds
				    = new TreeSet();
				templatedetectvisitor_22_._declaredVarIds
				    .addAll(treemap.keySet());
				templatedetectvisitor_22_._declaredVarIds
				    .addAll(treemap.values());
				TemplateInstance templateinstance_23_
				    = _chooseInst(expr.applyReturnVisitor
						  (templatedetectvisitor_22_));
				TemplateInstance templateinstance_24_
				    = _chooseInst(expr_21_.applyReturnVisitor
						  (templatedetectvisitor_22_));
				if (templateinstance_23_.template
				    != templateinstance_24_.template)
				    bool_15_ = false;
			    }
			}
		    }
		    if (bool_15_) {
			Dbg.check(templateinstance.args.size()
				  == templateinstance_12_.args.size());
			templateinstance.template = template;
			template.instances.add(templateinstance);
			bool_10_ = true;
		    }
		}
	    }
	}
	if (!bool_10_) {
	    Template template = new Template();
	    _allTemplates.add(template);
	    templateinstance.template = template;
	    template.instances.add(templateinstance);
	    template.children = new Template[templateinstances.length];
	    for (int i = 0; i < templateinstances.length; i++) {
		template.children[i] = templateinstances[i].template;
		templateinstances[i].template.parents.add(template);
	    }
	}
	_chkInst(templateinstance);
	return Collections.singleton(templateinstance);
    }
    
    public Map getNodeTemplates() {
	return _node2templateInstance;
    }
    
    private List _quantVarsUsedIn(Node node) {
	if (node instanceof VariableExpr && ((VariableExpr) node).isQuantified)
	    return Arrays.asList(new Node[] { node });
	ArrayList arraylist = new ArrayList();
	Iterator iterator = node.getChildren();
	while (iterator.hasNext())
	    arraylist.addAll(_quantVarsUsedIn((Node) iterator.next()));
	return arraylist;
    }
    
    private List _freeVarsUsedIn(Node node) {
	if (node instanceof VariableExpr && ((VariableExpr) node).isQuantified)
	    return Arrays.asList(new Node[] { node });
	ArrayList arraylist = new ArrayList();
	TreeSet treeset = new TreeSet();
	if (node instanceof VarCreator) {
	    DeclIter decliter = new DeclIter((VarCreator) node);
	    while (decliter.hasNext()) {
		decliter.next();
		treeset.add(decliter.getLeafId());
	    }
	}
	Iterator iterator = node.getChildren();
	while (iterator.hasNext()) {
	    List list = _freeVarsUsedIn((Node) iterator.next());
	    Iterator iterator_25_ = list.iterator();
	    while (iterator_25_.hasNext()) {
		VariableExpr variableexpr = (VariableExpr) iterator_25_.next();
		if (!treeset.contains(variableexpr.getLeafId()))
		    arraylist.add(variableexpr);
	    }
	}
	return arraylist;
    }
    
    private void _shortenTemplateArgLists() {
	Iterator iterator = _allTemplates.iterator();
	while (iterator.hasNext()) {
	    Template template = (Template) iterator.next();
	    int i = template.getNumArgs();
	    ArrayList arraylist = new ArrayList();
	    for (int i_26_ = 0; i_26_ < i; i_26_++) {
		Expr expr = null;
		boolean bool = false;
		Iterator iterator_27_ = template.instances.iterator();
		while (!bool && iterator_27_.hasNext()) {
		    TemplateInstance templateinstance
			= (TemplateInstance) iterator_27_.next();
		    Expr expr_28_ = (Expr) templateinstance.args.get(i_26_);
		    Transl transl = _translator.getNodeTransl(expr_28_);
		    if (!transl.isConstant())
			bool = true;
		    else if (expr == null)
			expr = expr_28_;
		    else if (!expr_28_.isSameAs(expr))
			bool = true;
		}
		if (bool)
		    arraylist.add(new Integer(i_26_));
	    }
	    template.keepOnlyArgs(arraylist);
	    for (i = 0; i < template.getNumArgs(); i++) {
		Expr expr = null;
		boolean bool = false;
		Iterator iterator_29_ = template.instances.iterator();
		while (!bool && iterator_29_.hasNext()) {
		    TemplateInstance templateinstance
			= (TemplateInstance) iterator_29_.next();
		    Expr expr_30_ = (Expr) templateinstance.args.get(i);
		    Transl transl = _translator.getNodeTransl(expr_30_);
		    if (expr == null)
			expr = expr_30_;
		    else if (!expr_30_.isSameAs(expr))
			bool = true;
		}
		if (!bool && !(expr instanceof VariableExpr)) {
		    Iterator iterator_31_ = template.instances.iterator();
		    while (iterator_31_.hasNext()) {
			TemplateInstance templateinstance
			    = (TemplateInstance) iterator_31_.next();
			Expr expr_32_ = (Expr) templateinstance.args.get(i);
			List list = templateinstance.args.subList(i, i + 1);
			list.clear();
			list.addAll(_freeVarsUsedIn(expr_32_));
		    }
		}
	    }
	    i = template.getNumArgs();
	    if (i >= 2) {
		arraylist = new ArrayList();
		arraylist.add(new Integer(0));
		for (int i_33_ = 1; i_33_ < i; i_33_++) {
		    boolean bool = false;
		    for (int i_34_ = 0; !bool && i_34_ < i_33_; i_34_++) {
			boolean bool_35_ = true;
			Iterator iterator_36_ = template.instances.iterator();
			while (bool_35_ && iterator_36_.hasNext()) {
			    TemplateInstance templateinstance
				= (TemplateInstance) iterator_36_.next();
			    Dbg.check(templateinstance.args.size() == i);
			    Expr expr
				= (Expr) templateinstance.args.get(i_33_);
			    Expr expr_37_
				= (Expr) templateinstance.args.get(i_34_);
			    if (!expr.isSameAs(expr_37_))
				bool_35_ = false;
			}
			if (bool_35_)
			    bool = true;
		    }
		    if (!bool)
			arraylist.add(new Integer(i_33_));
		}
		template.keepOnlyArgs(arraylist);
	    }
	}
    }
    
    private void _markSharedBooleanFormulas() {
	int i = 0;
	Dbg.info("marking shared boolean formulas...");
	Iterator iterator = _allTemplates.iterator();
	while (iterator.hasNext()) {
	    Template template = (Template) iterator.next();
	    if (!(template.getAnInstance().node instanceof Leaf)
		&& !_isConstantValued(template.getAnInstance().node)
		&& !_relTypeTemplate.containsValue(template)
		&& !_leafTemplate.containsValue(template)) {
		int i_38_ = i;
		Iterator iterator_39_ = template.instances.iterator();
		while (iterator_39_.hasNext()) {
		    TemplateInstance templateinstance
			= (TemplateInstance) iterator_39_.next();
		    i = i_38_;
		    ArrayList arraylist = new ArrayList();
		    int[] is = new int[templateinstance.args.size()];
		    int i_40_ = 0;
		    Iterator iterator_41_ = templateinstance.args.iterator();
		    while (iterator_41_.hasNext()) {
			Node node = (Node) iterator_41_.next();
			Transl transl = _translator.getNodeTransl(node);
			Dbg.check(transl);
			List list = transl.getBooleanFormulas();
			is[i_40_++] = list.size();
			arraylist.addAll(list);
		    }
		    _chkInst(templateinstance);
		    Transl transl
			= _translator.getNodeTransl(templateinstance.node);
		    Dbg.check(transl);
		    Iterator iterator_42_
			= transl.getBooleanFormulas().iterator();
		    while (iterator_42_.hasNext()) {
			BooleanFormula booleanformula
			    = (BooleanFormula) iterator_42_.next();
			int[] is_43_ = new int[is.length];
			for (int i_44_ = 0; i_44_ < is.length; i_44_++)
			    is_43_[i_44_]
				= ((Integer) template.argMults.get(i_44_))
				      .intValue();
			booleanformula.recordCachingInfo
			    (i++,
			     ((BooleanFormula[])
			      arraylist.toArray(new BooleanFormula[0])),
			     is, is_43_);
		    }
		}
	    }
	}
	Dbg.info("marked shared boolean formulas.");
    }
    
    public void preprocess(Formula formula) {
	/* empty */
    }
    
    public void postprocess() {
	_shortenTemplateArgLists();
	_determineArgMults();
	_markSharedBooleanFormulas();
    }
    
    private void _determineArgMults() {
	Dbg.info("Determining arg multiplicities...");
	Iterator iterator = _allTemplates.iterator();
	while (iterator.hasNext()) {
	    Template template = (Template) iterator.next();
	    template.argMults = new ArrayList();
	    for (int i = 0; i < template.getNumArgs(); i++) {
		int i_45_ = 1;
		Iterator iterator_46_ = template.instances.iterator();
		while (iterator_46_.hasNext()) {
		    TemplateInstance templateinstance
			= (TemplateInstance) iterator_46_.next();
		    Expr expr = (Expr) templateinstance.args.get(i);
		    i_45_ = _updateArgValInfo(expr, i_45_);
		    if (i_45_ == 0)
			break;
		}
		template.argMults.add(new Integer(i_45_));
	    }
	}
	Dbg.info("Determined arg multiplicities.");
    }
    
    private static String _mult2str(int i) {
	switch (i) {
	case 0:
	    return "set";
	case 1:
	    return "scalar";
	case 2:
	    return "option";
	default:
	    return "unknown";
	}
    }
    
    public void showTemplates() {
	ArrayList arraylist = new ArrayList(_allTemplates);
	Collections.sort(arraylist, new Comparator() {
	    public int compare(Object object, Object object_48_) {
		Template template = (Template) object;
		Template template_49_ = (Template) object_48_;
		Integer integer
		    = new Integer(template.getAnInstance().args.size());
		Integer integer_50_
		    = new Integer(template_49_.getAnInstance().args.size());
		return integer.compareTo(integer_50_);
	    }
	});
	System.out.println("========= Templates ============");
	Iterator iterator = arraylist.iterator();
	while (iterator.hasNext()) {
	    Template template = (Template) iterator.next();
	    System.out.println("-----------------------------");
	    System.out.println(template.argMults);
	    Iterator iterator_51_ = template.instances.iterator();
	    while (iterator_51_.hasNext()) {
		TemplateInstance templateinstance
		    = (TemplateInstance) iterator_51_.next();
		System.out.println(" args=" + templateinstance.args);
	    }
	}
	System.out.println("================================");
    }
    
    private int _updateArgValInfo(Expr expr, int i) {
	if (i == 0)
	    return i;
	if (expr instanceof VariableExpr
	    && ((VariableExpr) expr).isQuantified) {
	    VariableExpr variableexpr = (VariableExpr) expr;
	    LeafId leafid = variableexpr.getLeafId();
	    if (_translator.getVarCreator(leafid) instanceof ComprehensionExpr)
		return _weakestMult(i, 1);
	    MultiplicityExpr multiplicityexpr
		= _translator.getLeafMultiplicity(((Leaf) expr).getLeafId());
	    if (multiplicityexpr instanceof SetMultExpr) {
		SetMultExpr setmultexpr = (SetMultExpr) multiplicityexpr;
		switch (setmultexpr.getSetMult().getOpCode()) {
		case 0:
		    return _weakestMult(i, 0);
		case 1:
		    return _weakestMult(i, 1);
		case 2:
		    return _weakestMult(i, 2);
		case 3:
		    return _weakestMult(i, 1);
		default:
		    Dbg.check(false, "missing set multiplicity");
		    return 0;
		}
	    }
	    return _weakestMult(i, 0);
	}
	List list = _freeVarsUsedIn(expr);
	TreeSet treeset = new TreeSet();
	Iterator iterator = list.iterator();
	while (iterator.hasNext())
	    treeset.add(((Leaf) iterator.next()).getLeafId());
	ArrayList arraylist = new ArrayList(treeset);
	BoolSwitch[] boolswitches = new BoolSwitch[arraylist.size()];
	ResettableIterator[] resettableiterators
	    = new ResettableIterator[arraylist.size()];
	for (int i_52_ = 0; i_52_ < arraylist.size(); i_52_++) {
	    LeafId leafid = (LeafId) arraylist.get(i_52_);
	    boolswitches[i_52_] = _translator.getVarSwitch(leafid);
	    resettableiterators[i_52_]
		= new CachingIterator(VariableValueIterator
					  .makeIterator(leafid, _translator));
	}
	Transl transl = _translator.getNodeTransl(expr);
	List list_53_ = transl.getBooleanFormulas();
	MultiIter multiiter = new MultiIter(resettableiterators);
	while (multiiter.hasNext()) {
	    Object[] objects = (Object[]) multiiter.next();
	    for (int i_54_ = 0; i_54_ < objects.length; i_54_++)
		boolswitches[i_54_]
		    .setVarValue(((Long) objects[i_54_]).longValue());
	    int i_55_ = 0;
	    Iterator iterator_56_ = list_53_.iterator();
	    while (iterator_56_.hasNext()) {
		BooleanFormula booleanformula
		    = (BooleanFormula) iterator_56_.next();
		if (booleanformula.interpret())
		    i_55_++;
		if (i_55_ > 1) {
		    for (int i_57_ = 0; i_57_ < objects.length; i_57_++)
			boolswitches[i_57_].clearVarValue();
		    return 0;
		}
	    }
	    for (int i_58_ = 0; i_58_ < objects.length; i_58_++)
		boolswitches[i_58_].clearVarValue();
	    if (i_55_ == 0)
		i = _weakestMult(i, 2);
	}
	return i;
    }
    
    private static int _weakestMult(int i, int i_59_) {
	if (i == 0 || i_59_ == 0)
	    return 0;
	if (i == 2 || i_59_ == 2)
	    return 2;
	Dbg.check(i == 1 && i_59_ == 1);
	return 1;
    }
    
    private void _chkInst(TemplateInstance templateinstance) {
	Iterator iterator = templateinstance.args.iterator();
	while (iterator.hasNext()) {
	    Node node = (Node) iterator.next();
	    Dbg.check(_isConstantValued(node));
	    List list = _freeVarsUsedIn(node);
	    Iterator iterator_60_ = list.iterator();
	    while (iterator_60_.hasNext()) {
		LeafId leafid
		    = ((VariableExpr) iterator_60_.next()).getLeafId();
		VarCreator varcreator = _translator.getVarCreator(leafid);
		Dbg.check(_translator.isAncestor(varcreator,
						 templateinstance.node));
	    }
	}
    }
    
    private static TemplateInstance _chooseInst(Object object) {
	return (TemplateInstance) ((Set) object).iterator().next();
    }
    
    private TemplateInstance _getInst(Node node) {
	return _chooseInst(_node2templateInstance.get(node));
    }
}