import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/**
 * Calls lookup(intExpr) 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(intExpr) | some t => t, cache(intExpr,
 *         translate(intExpr))
 */
public final Int visit(ExprToIntCast intExpr) {
	Int ret = lookup(intExpr);
	if (ret != null)
		return ret;
	vars = vars.createNested();
	BooleanMatrix expr = intExpr.expression().accept(this);
	switch (intExpr.op()) {
		case CARDINALITY :
			ret = expr.cardinality();
			break;
		case SUM :
			final IntSet ints = interpreter.ints();
			ret = sum(expr, ints.iterator(), 0, ints.size() - 1);
			break;
		default :
			throw new IllegalArgumentException("unknown operator: " + intExpr.op());
	}
	for (Variable v : vars)
		ret.defCond().addVar(v);
	vars = vars.parent();
	return cache(intExpr, ret);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/**
 * @ensures this.tokens' = concat[ this.tokens, "int","[",
 *          tokenize[node.expression], "]" ]
 **/
public void visit(ExprToIntCast node) {
	switch (node.op()) {
		case SUM :
			append("int");
			append("[");
			node.expression().accept(this);
			append("]");
			break;
		case CARDINALITY :
			append("#");
			append("(");
			node.expression().accept(this);
			append(")");
			break;
		default :
			throw new IllegalArgumentException("unknown operator: " + node.op());
	}

}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(ExprToIntCast x) {
	String newname = makename(x);
	if (newname == null)
		return;
	String sub = make(x.expression());
	switch (x.op()) {
		case CARDINALITY :
			file.printf("IntExpression %s=%s.count();%n", newname, sub);
			break;
		case SUM :
			file.printf("IntExpression %s=%s.sum();%n", newname, sub);
			break;
		default :
			throw new RuntimeException("Unknown kodkod operator \"" + x.op() + "\" encountered");
	}
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
private IntExpression toInt(Expr x, Object y) throws Err, ErrorFatal {
	// simplify: if y is int[Int[sth]] then return sth
	if (y instanceof ExprToIntCast) {
		ExprToIntCast y2 = (ExprToIntCast) y;
		if (y2.expression() instanceof IntToExprCast)
			return ((IntToExprCast) y2.expression()).intExpr();
	}
	// simplify: if y is Int[sth], then return sth
	if (y instanceof IntToExprCast)
		return ((IntToExprCast) y).intExpr();
	if (y instanceof IntExpression)
		return (IntExpression) y;
	// [AM]: maybe this conversion should be removed
	if (y instanceof Expression)
		return ((Expression) y).sum();
	throw new ErrorFatal(x.span(), "This should have been an integer expression.\nInstead it is " + y);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
private IntExpression toInt(Expr x, Object y) throws Err, ErrorFatal {
    // simplify: if y is int[Int[sth]] then return sth
    if (y instanceof ExprToIntCast) {
        ExprToIntCast y2 = (ExprToIntCast) y;
        if (y2.expression() instanceof IntToExprCast)
            return ((IntToExprCast)y2.expression()).intExpr();
    }
    // simplify: if y is Int[sth], then return sth
    if (y instanceof IntToExprCast)
        return ((IntToExprCast) y).intExpr();
    if (y instanceof IntExpression) 
        return (IntExpression)y;
    //[AM]: maybe this conversion should be removed
    if (y instanceof Expression) return ((Expression) y).sum();
    throw new ErrorFatal(x.span(), "This should have been an integer expression.\nInstead it is "+y);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** 
 * Calls lookup(intExpr) 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(intExpr) | some t => t, 
 * 	cache(intExpr, translate(intExpr))
 */
public final Int visit(ExprToIntCast intExpr) {
	Int ret = lookup(intExpr);
	if (ret!=null) return ret;
	vars = vars.createNested();
	BooleanMatrix expr = intExpr.expression().accept(this);
       switch(intExpr.op()) {
	case CARDINALITY : 
		ret = expr.cardinality(); break;
	case SUM         :
		final IntSet ints = interpreter.ints();
		ret = sum(expr, ints.iterator(), 0, ints.size()-1); break;
	default: 
		throw new IllegalArgumentException("unknown operator: " + intExpr.op());
	}
       for (Variable v : vars) ret.defCond().addVar(v); 
       vars = vars.parent(); 
	return cache(intExpr, ret);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** @ensures this.tokens' = concat[ this.tokens, "int","[",
 *   tokenize[node.expression], "]" ] **/
public void visit(ExprToIntCast node) {
	switch(node.op()) { 
	case SUM:
		append("int");
		append("[");
		node.expression().accept(this);
		append("]");
		break;
	case CARDINALITY : 
		append("#");
		append("(");
		node.expression().accept(this);
		append(")");
		break;
	default : throw new IllegalArgumentException("unknown operator: " + node.op());
	}
	
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
public IntExpression visit(ExprToIntCast expr) { 
	IntExpression ret = lookup(expr);
	if (ret!=null) return ret;
	
	final ExprCastOperator op = expr.op();
	final Expression child = expr.expression().accept(this);
	
	final int hash = hash(op, child);
	for(Iterator<PartialCannonicalizer.Holder<IntExpression>> itr = intExprs.get(hash); itr.hasNext(); ) {
		final IntExpression next = itr.next().obj;
		if (next.getClass()==ExprToIntCast.class) { 
			if (((ExprToIntCast)next).expression()==child)
				return cache(expr, next);
		}
	}
	ret = child==expr.expression() ? expr : child.apply(op);
	intExprs.add(new PartialCannonicalizer.Holder<IntExpression>(ret, hash));
	return cache(expr,ret);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** @effects this.tokens' = concat[ this.tokens, "int","[",
 *   tokenize[node.expression], "]" ] **/
public void visit(ExprToIntCast node) {
	if (displayed(node)) return;
	final boolean oldTop = notTop();
	switch(node.op()) { 
	case SUM:
		append("int");
		append("[");
		node.expression().accept(this);
		append("]");
		break;
	case CARDINALITY : 
		append("#");
		append("(");
		node.expression().accept(this);
		append(")");
		break;
	default : throw new IllegalArgumentException("unknown operator: " + node.op());
	}
	top = oldTop;
}
 

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

	final Expression expr = intExpr.expression().accept(delegate);
	ret = expr == intExpr.expression() ? intExpr : expr.apply(intExpr.op());
	return cache(intExpr, ret);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/**
 * Calls lookup(intExpr) and returns the cached value, if any. If no cached
 * value exists, visits the child, caches its return value and returns it.
 * 
 * @return let x = lookup(intExpr) | x != null => x, cache(intExpr,
 *         intExpr.expression.accept(this))
 */
public Set<T> visit(ExprToIntCast intExpr) {
	Set<T> ret = lookup(intExpr);
	if (ret != null)
		return ret;
	ret = newSet();
	ret.addAll(intExpr.expression().accept(this));
	return cache(intExpr, ret);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(ExprToIntCast x) {
    String newname=makename(x); if (newname==null) return;
    String sub=make(x.expression());
    switch(x.op()) {
       case CARDINALITY: file.printf("IntExpression %s=%s.count();%n", newname, sub); break;
       case SUM: file.printf("IntExpression %s=%s.sum();%n", newname, sub); break;
       default: throw new RuntimeException("Unknown kodkod operator \""+x.op()+"\" encountered");
    }
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** 
* Calls lookup(intExpr) and returns the cached value, if any.  
* If a replacement has not been cached, visits the expression's 
* child.  If nothing changes, the argument is cached and
* returned, otherwise a replacement expression is cached and returned.
* @return { i: ExprToIntCast | i.expression = intExpr.expression.accept(this) && i.op = intExpr.op}
*/
  public IntExpression visit(ExprToIntCast intExpr) {
IntExpression ret = lookup(intExpr);
if (ret!=null) return ret;
	
final Expression expr = intExpr.expression().accept(this);
ret = expr==intExpr.expression() ? intExpr : expr.apply(intExpr.op());
return cache(intExpr, ret);
  }
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** 
 * Calls lookup(intExpr) and returns the cached value, if any.  
 * If no cached value exists, visits the child, caches its return value and returns it. 
 * @return let x = lookup(intExpr) | 
 *          x != null => x,  
 *          cache(intExpr, intExpr.expression.accept(this)) 
 */
public Set<T> visit(ExprToIntCast intExpr) {
	Set<T> ret = lookup(intExpr);
	if (ret!=null) return ret;
	ret = newSet();
	ret.addAll(intExpr.expression().accept(this));
	return cache(intExpr,ret);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** 
 * Calls lookup(intExpr) 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(intExpr) | some t => t, 
 * 	cache(intExpr, translate(intExpr))
 */
public final Int visit(ExprToIntCast intExpr) {
	Int ret = lookup(intExpr);
	if (ret!=null) return ret;
	switch(intExpr.op()) {
	case CARDINALITY : 
		ret = intExpr.expression().accept(this).cardinality(); break;
	case SUM         :
		final IntSet ints = interpreter.ints();
		ret = sum(intExpr.expression().accept(this), ints.iterator(), 0, ints.size()-1); break;
	default: 
		throw new IllegalArgumentException("unknown operator: " + intExpr.op());
	}
	return cache(intExpr, ret);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/** converts a Kodkod node to a Kodkod expression. */
protected Expression node2expr(Node node) {
    if (node instanceof Expression)
        return (Expression)node;
    if (node instanceof IntExpression) 
        return ((IntExpression) node).toExpression();
    if (node instanceof ExprToIntCast)
        return ((ExprToIntCast) node).expression();
    if (node instanceof Formula)
        return form2expr((Formula) node);
    throw new RuntimeException("don't know how to convert " + node.getClass().getSimpleName() + " to expression");
}
 

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

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
@Override
public IntExpression visit(ExprToIntCast intExpr) {
	return intExpr;
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
/**
 * @return true if the given expression should be parenthesized when a
 *         child of a compound parent
 */
private boolean parenthesize(IntExpression child) {
	return !(child instanceof UnaryIntExpression || child instanceof IntConstant
			|| child instanceof ExprToIntCast);
}
 

import kodkod.ast.ExprToIntCast; //导入依赖的package包/类
public Boolean visit(ExprToIntCast e) {
	return checkVisitedThenAccumA(e, Boolean.FALSE, e.expression());
}