import kodkod.ast.NaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(expr) and returns the cached value, if any. If a replacement
 * has not been cached, visits the expr's children. If nothing changes, the
 * argument is cached and returned, otherwise a replacement expr is cached
 * and returned.
 * 
 * @return { e: Expression | e.op = expr.op && #e.children = #expr.children
 *         && all i: [0..expr.children) | e.child(i) =
 *         expr.child(i).accept(delegate) }
 */
public Expression visit(NaryExpression expr) {
	Expression ret = lookup(expr);
	if (ret != null)
		return ret;

	final Expression[] visited = new Expression[expr.size()];
	boolean allSame = true;
	for (int i = 0; i < visited.length; i++) {
		final Expression child = expr.child(i);
		visited[i] = child.accept(delegate);
		allSame = allSame && visited[i] == child;
	}

	ret = allSame ? expr : Expression.compose(expr.op(), visited);
	return cache(expr, ret);
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(NaryExpression x) {
    String newname = makename(x); if (newname==null) return;
    String[] list = new String[x.size()];
    for(int i=0; i<list.length; i++)  list[i] = make(x.child(i));
    file.printf("Expression %s=Expression.compose(ExprOperator.", newname);
    switch(x.op()) {
       case INTERSECTION: file.print("INTERSECTION"); break;
       case OVERRIDE: file.print("OVERRIDE"); break;
       case PRODUCT: file.print("PRODUCT"); break;
       case UNION: file.print("UNION"); break;
       default: throw new RuntimeException("Unknown kodkod operator \""+x.op()+"\" encountered");
    }
    for(int i=0; i<list.length; i++) file.printf(", %s", list[i]);
    file.printf(");%n");
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** 
 * Calls lookup(expr) and returns the cached value, if any.  
 * If a replacement has not been cached, visits the expr's 
 * children.  If nothing changes, the argument is cached and
 * returned, otherwise a replacement expr is cached and returned.
 * @return { e: Expression | e.op = expr.op && #e.children = #expr.children && all i: [0..expr.children) | e.child(i) = expr.child(i).accept(this) }
 */
public Expression visit(NaryExpression expr) {
	Expression ret = lookup(expr);
	if (ret!=null) return ret;
	
	final Expression[] visited = new Expression[expr.size()];
	boolean allSame = true;
	for(int i = 0 ; i < visited.length; i++) { 
		final Expression child = expr.child(i);
		visited[i] = child.accept(this);
		allSame = allSame && visited[i]==child;
	}
	
	ret = allSame ? expr : Expression.compose(expr.op(), visited);
	return cache(expr,ret);
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(expr) and returns the cached value, if any.  
 * If a translation has not been cached, translates the expression,
 * calls cache(...) on it and returns it.
 * @return let t = lookup(expr) | some t => t, 
 *      let op = (expr.op).(UNION->or + INTERSECTION->and + DIFFERENCE->difference + OVERRIDE->override + JOIN->dot + PRODUCT->cross) | 
 *       cache(expr, op(expr.left.accept(this), expr.right.accept(this)))
 */
public BooleanMatrix visit(NaryExpression expr) {
	BooleanMatrix ret = lookup(expr);
	if (ret!=null) return ret;

	final ExprOperator op = expr.op();
	final BooleanMatrix first = expr.child(0).accept(this);		
	final BooleanMatrix[] rest = new BooleanMatrix[expr.size()-1];
	for(int i = 0; i < rest.length; i++) { 	rest[i] = expr.child(i+1).accept(this); }
	
	switch(op) {
	case UNION        	: ret = first.or(rest); break;
	case INTERSECTION	: ret = first.and(rest); break;
	case OVERRIDE 		: ret = first.override(rest); break;
	case PRODUCT		: ret = first.cross(rest); break;
	default : 
		throw new IllegalArgumentException("Unknown associative operator: " + op);
	}

	return cache(expr, ret);
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** @return true if e is (a product of) Expression.NONE*/
private boolean isEmpty(Expression e) { 
	if (e==Expression.NONE) return true;
	else if (e instanceof BinaryExpression) { 
		final BinaryExpression b = (BinaryExpression) e;
		return b.op()==ExprOperator.PRODUCT && isEmpty(b.left()) && isEmpty(b.right());
	} else if (e instanceof NaryExpression) { 
		final NaryExpression n = (NaryExpression) e;
		if (n.op()==ExprOperator.PRODUCT) { 
			for(int i = 0, max = n.size(); i < max; i++) { 
				if (!isEmpty(n.child(i))) return false;
			}
			return true;
		}
	}
	return false;
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
public Expression visit(NaryExpression expr) { 
	Expression ret = lookup(expr);
	if (ret!=null) return ret;
	
	final ExprOperator op = expr.op();
	
	final List<Expression> children = simplify(op, visitAll(expr));
	final int size = children.size();
	switch(size) { 
	case 0 : return cache(expr, empty(expr.arity()));
	case 1 : return cache(expr, children.get(0));
	default :
		ret = expr.size()==size && allSame(expr,children) ? expr : Expression.compose(op, children);
		return cache(expr,ret);
	}	
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/**
 * Visits the children if this.visited(expr) returns false. Otherwise does
 * nothing.
 * 
 * @ensures all i: [0..#expr.children) | expr.child(i).accept(this)
 */
public void visit(NaryExpression expr) {
	if (visited(expr))
		return;
	for (Expression child : expr) {
		child.accept(this);
	}
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(expr) and returns the cached value, if any. If no cached
 * value exists, visits each child, caches the union of the children's
 * return values and returns it.
 * 
 * @return let x = lookup(expr) | x != null => x, cache(expr,
 *         expr.child(0).accept(this) + .. +
 *         expr.child(expr.size()-1).accept(this))
 */
public Set<T> visit(NaryExpression expr) {
	Set<T> ret = lookup(expr);
	if (ret != null)
		return ret;
	ret = newSet();
	for (Expression child : expr) {
		ret.addAll(child.accept(this));
	}
	return cache(expr, ret);
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(expr) and returns the cached value, if any. If no cached
 * value exists, visits each child, caches the disjunction of the children's
 * return values and returns it.
 * 
 * @return let x = lookup(expr) | x != null => x, cache(expr,
 *         expr.child(0).accept(this) || ... ||
 *         expr.child(expr.size()-1).accept(this))
 */
public Boolean visit(NaryExpression expr) {
	final Boolean ret = lookup(expr);
	if (ret != null)
		return ret;
	for (Expression child : expr) {
		if (child.accept(this))
			return cache(expr, true);
	}
	return cache(expr, false);
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(expr) and returns the cached value, if any. If a translation
 * has not been cached, translates the expression, calls cache(...) on it
 * and returns it.
 * 
 * @return let t = lookup(expr) | some t => t, let op = (expr.op).(UNION->or
 *         + INTERSECTION->and + DIFFERENCE->difference + OVERRIDE->override
 *         + JOIN->dot + PRODUCT->cross) | cache(expr,
 *         op(expr.left.accept(this), expr.right.accept(this)))
 */
public BooleanMatrix visit(NaryExpression expr) {
	BooleanMatrix ret = lookup(expr);
	if (ret != null)
		return ret;

	final ExprOperator op = expr.op();
	final BooleanMatrix first = expr.child(0).accept(this);
	final BooleanMatrix[] rest = new BooleanMatrix[expr.size() - 1];
	for (int i = 0; i < rest.length; i++) {
		rest[i] = expr.child(i + 1).accept(this);
	}

	switch (op) {
		case UNION :
			ret = first.or(rest);
			break;
		case INTERSECTION :
			ret = first.and(rest);
			break;
		case OVERRIDE :
			ret = first.override(rest);
			break;
		case PRODUCT :
			ret = first.cross(rest);
			break;
		default :
			throw new IllegalArgumentException("Unknown associative operator: " + op);
	}

	return cache(expr, ret);
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/**
 * @ensures appends the tokenization of the given node to this.tokens
 */
public void visit(NaryExpression node) {
	final ExprOperator op = node.op();
	visitChild(node.child(0), parenthesize(op, node.child(0)));
	for (int i = 1, size = node.size(); i < size; i++) {
		infix(op);
		visitChild(node.child(i), parenthesize(op, node.child(i)));
	}
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(NaryExpression x) {
	String newname = makename(x);
	if (newname == null)
		return;
	String[] list = new String[x.size()];
	for (int i = 0; i < list.length; i++)
		list[i] = make(x.child(i));
	file.printf("Expression %s=Expression.compose(ExprOperator.", newname);
	switch (x.op()) {
		case INTERSECTION :
			file.print("INTERSECTION");
			break;
		case OVERRIDE :
			file.print("OVERRIDE");
			break;
		case PRODUCT :
			file.print("PRODUCT");
			break;
		case UNION :
			file.print("UNION");
			break;
		default :
			throw new RuntimeException("Unknown kodkod operator \"" + x.op() + "\" encountered");
	}
	for (int i = 0; i < list.length; i++)
		file.printf(", %s", list[i]);
	file.printf(");%n");
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/**
 * Visits the children if this.visited(expr) returns false.  Otherwise does nothing.
 * @ensures all i: [0..#expr.children) | expr.child(i).accept(this)
 */
public void visit(NaryExpression expr) { 
	if (visited(expr)) return;
	for(Expression child : expr) { 
		child.accept(this);
	}
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** 
 * Calls lookup(expr) and returns the cached value, if any.  
 * If no cached value exists, visits each child, caches the
 * union of the children's return values and returns it. 
 * @return let x = lookup(expr) | 
 *          x != null => x,  
 *          cache(expr, expr.child(0).accept(this) + .. + expr.child(expr.size()-1).accept(this)) 
 */
public Set<T> visit(NaryExpression expr) {
	Set<T> ret = lookup(expr);
	if (ret!=null) return ret;		
	ret = newSet();
	for(Expression child : expr) { 
		ret.addAll(child.accept(this));
	}
	return cache(expr, ret);
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** 
 * Calls lookup(expr) and returns the cached value, if any.  
 * If no cached value exists, visits each child, caches the
 * disjunction of the children's return values and returns it. 
 * @return let x = lookup(expr) | 
 *          x != null => x,  
 *          cache(expr, expr.child(0).accept(this) || ... || expr.child(expr.size()-1).accept(this)) 
 */
public Boolean visit(NaryExpression expr) {
	final Boolean ret = lookup(expr);
	if (ret!=null) return ret;
	for(Expression child : expr) { 
		if (child.accept(this))
			return cache(expr, true);
	}
	return cache(expr, false);
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** @return true if the given  expression needs to be parenthesized if a 
 * child of a binary  expression with the given operator */
private boolean parenthesize(ExprOperator op, Expression child) { 
	return child instanceof IfExpression ||
		   child instanceof NaryExpression ||
	       (child instanceof BinaryExpression && 
	        (op==ExprOperator.JOIN || 
	         ((BinaryExpression)child).op()!=op));
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** @ensures appends the tokenization of the given node to this.tokens */
public void visit(NaryExpression node) {
	final ExprOperator op = node.op();
	visitChild(node.child(0), parenthesize(op, node.child(0)));
	for(int i = 1, size = node.size(); i < size; i++) {
		infix(op);
		visitChild(node.child(i), parenthesize(op, node.child(i)));
	}
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** @return true if the given  expression needs to be parenthesized if a 
 * child of a binary  expression with the given operator */
private boolean parenthesize(ExprOperator op, Expression child) { 
	return display.containsKey(child.toString()) ? false :
		   child instanceof IfExpression ||
		   (child instanceof NaryExpression && ((NaryExpression)child).op()!=op) ||
	       (child instanceof BinaryExpression && 
	        (/*op!=ExprOperator.JOIN && */
	         ((BinaryExpression)child).op()!=op));
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
/** @effects appends the tokenization of the given node to this.tokens */
public void visit(NaryExpression node) {
	if (displayed(node)) return;
	final boolean oldTop = notTop();
	final ExprOperator op = node.op();
	visitChild(node.child(0), parenthesize(op, node.child(0)));
	for(int i = 1, size = node.size(); i < size; i++) {
		infix(op);
		visitChild(node.child(i), parenthesize(op, node.child(i)));
	}
	top = oldTop;
}
 

import kodkod.ast.NaryExpression; //导入依赖的package包/类
@Override
public E visit(NaryExpression expr) {
	start(expr);
	return end(expr, visitor.visit(expr));
}