import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Returns a {@link kodkod.engine.bool.BooleanMatrix matrix} m of
 * {@link kodkod.engine.bool.BooleanValue boolean formulas} representing the
 * specified constant expression.
 * 
 * @return { m: BooleanMatrix | let dset = [0..this.universe.size()^c.arity)
 *         | m.dimensions.dimensions = [0..c.arity) ->one
 *         this.universe.size() && c = UNIV => m.elements[dset] = TRUE, c =
 *         NONE => m.elements[dset] = FALSE, c = IDEN => (all i: dset |
 *         (some j: int | i = j*(1+this.universe.size())) => m.elements[i] =
 *         TRUE, m.elements[i] = FALSE), c = INT => (all i: dset | (some j:
 *         int | this.interpret(j)=i) => m.elements[i] = TRUE, m.elements[i]
 *         = FALSE }
 */
public final BooleanMatrix interpret(ConstantExpression c) {
	final int univSize = universe().size();
	if (c == Expression.UNIV) {
		final IntSet all = Ints.rangeSet(Ints.range(0, univSize - 1));
		return factory().matrix(Dimensions.square(univSize, 1), all, all);
	} else if (c == Expression.IDEN) {
		final Dimensions dim2 = Dimensions.square(univSize, 2);
		final IntSet iden = Ints.bestSet(dim2.capacity());
		for (int i = 0; i < univSize; i++) {
			iden.add(i * univSize + i);
		}
		return factory().matrix(dim2, iden, iden);
	} else if (c == Expression.NONE) {
		return factory().matrix(Dimensions.square(univSize, 1), Ints.EMPTY_SET, Ints.EMPTY_SET);
	} else if (c == Expression.INTS) {
		final IntSet ints = Ints.bestSet(univSize);
		for (IntIterator iter = ints().iterator(); iter.hasNext();) {
			ints.add(interpret(iter.next()));
		}
		return factory().matrix(Dimensions.square(univSize, 1), ints, ints);
	} else {
		throw new IllegalArgumentException("unknown constant expression: " + c);
	}
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Calls lookup(unaryExpr) 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(unaryExpr) | some t => t, let op =
 *         (unaryExpr.op).(TRANSPOSE->transpose + CLOSURE->closure +
 *         REFLEXIVE_CLOSURE->(lambda(m)(m.closure().or(iden))) |
 *         cache(unaryExpr, op(unaryExpr.child))
 */
public final BooleanMatrix visit(UnaryExpression unaryExpr) {
	BooleanMatrix ret = lookup(unaryExpr);
	if (ret != null)
		return ret;

	final BooleanMatrix child = unaryExpr.expression().accept(this);
	final ExprOperator op = unaryExpr.op();

	switch (op) {
		case TRANSPOSE :
			ret = child.transpose();
			break;
		case CLOSURE :
			ret = child.closure();
			break;
		case REFLEXIVE_CLOSURE :
			ret = child.closure().or(visit((ConstantExpression) Expression.IDEN));
			break;
		default :
			throw new IllegalArgumentException("Unknown operator: " + op);
	}
	return cache(unaryExpr, ret);
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(ConstantExpression x) {
	if (map.containsKey(x))
		return;
	String newname = null;
	if (x == Expression.NONE)
		newname = "Expression.NONE";
	else if (x == Expression.UNIV)
		newname = "Expression.UNIV";
	else if (x == Expression.IDEN)
		newname = "Expression.IDEN";
	else if (x == Expression.INTS)
		newname = "Expression.INTS";
	else
		throw new RuntimeException("Unknown kodkod ConstantExpression \"" + x + "\" encountered");
	map.put(x, newname);
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Returns a {@link kodkod.engine.bool.BooleanMatrix matrix} m of 
 * {@link kodkod.engine.bool.BooleanValue boolean formulas} representing
 * the specified constant expression.    
 * @return { m: BooleanMatrix | let dset = [0..this.universe.size()^c.arity) | 
 *           m.dimensions.dimensions = [0..c.arity) ->one this.universe.size() && 
 *           c = UNIV => m.elements[dset] = TRUE, c = NONE => m.elements[dset] = FALSE,
 *           c = IDEN => (all i: dset | (some j: int | i = j*(1+this.universe.size())) => m.elements[i] = TRUE, m.elements[i] = FALSE),
 *           c = INT => (all i: dset | (some j: int | this.interpret(j)=i) => m.elements[i] = TRUE, m.elements[i] = FALSE }
 */
public final BooleanMatrix interpret(ConstantExpression c) {
	final int univSize = universe().size();
	if (c==Expression.UNIV) {
		final IntSet all =  Ints.rangeSet(Ints.range(0, univSize-1));
		return factory().matrix(Dimensions.square(univSize, 1), all, all);
	} else if (c==Expression.IDEN) {
		final Dimensions dim2 = Dimensions.square(univSize, 2);
		final IntSet iden = Ints.bestSet(dim2.capacity());
		for(int i = 0; i < univSize; i++) {
			iden.add(i*univSize + i);
		}			
		return factory().matrix(dim2, iden, iden);
	} else if (c==Expression.NONE) {
		return factory().matrix(Dimensions.square(univSize, 1), Ints.EMPTY_SET, Ints.EMPTY_SET);
	} else if (c==Expression.INTS) {
		final IntSet ints = Ints.bestSet(univSize);
		for(IntIterator iter = ints().iterator(); iter.hasNext(); ) {
			ints.add(interpret(iter.next()));
		}
		return factory().matrix(Dimensions.square(univSize, 1), ints, ints);
	} else {
		throw new IllegalArgumentException("unknown constant expression: " + c);
	}
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Calls lookup(unaryExpr) 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(unaryExpr) | some t => t, 
 *      let op = (unaryExpr.op).(TRANSPOSE->transpose + CLOSURE->closure + REFLEXIVE_CLOSURE->(lambda(m)(m.closure().or(iden))) | 
 *       cache(unaryExpr, op(unaryExpr.child))
 */
public final BooleanMatrix visit(UnaryExpression unaryExpr) {
	BooleanMatrix ret = lookup(unaryExpr);
	if (ret!=null) return ret;

	final BooleanMatrix child = unaryExpr.expression().accept(this);
	final ExprOperator op = unaryExpr.op();

	switch(op) {
	case TRANSPOSE         	: ret = child.transpose(); break;
	case CLOSURE           	: ret = child.closure(); break;
	case REFLEXIVE_CLOSURE	: ret = child.closure().or(visit((ConstantExpression)Expression.IDEN)); break;
	default : 
		throw new IllegalArgumentException("Unknown operator: " + op);
	}
	return cache(unaryExpr,ret);
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(ConstantExpression x) {
    if (map.containsKey(x)) return;
    String newname=null;
    if (x==Expression.NONE) newname="Expression.NONE";
       else if (x==Expression.UNIV) newname="Expression.UNIV";
       else if (x==Expression.IDEN) newname="Expression.IDEN";
       else if (x==Expression.INTS) newname="Expression.INTS";
       else throw new RuntimeException("Unknown kodkod ConstantExpression \""+x+"\" encountered");
    map.put(x,newname);
}
 

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

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
@Override
public Expression visit(ConstantExpression constExpr) {
	return constExpr;
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/** @ensures this.tokens' = concat[ this.tokens, node ] */
public void visit(ConstantExpression node) {
	append(node);
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
public Boolean visit(ConstantExpression constExpr) {
	return noHOL(constExpr);
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Returns Collections.EMPTY_SET
 * @return Collections.EMPTY_SET
 */
@SuppressWarnings("unchecked")
public Set<T> visit(ConstantExpression constExpr) {
	return Collections.EMPTY_SET;
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/** @ensures this.tokens' = concat[ this.tokens, node ] */
public void visit(ConstantExpression node) { append(node); }
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
@Override
public Expression visitIdent() {
    return ConstantExpression.IDEN;
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
@Override
public Expression visitUniv() {
    return ConstantExpression.UNIV;
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
@Override
public Expression visitNone() {
    return ConstantExpression.NONE;
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/** @effects this.tokens' = concat[ this.tokens, node ] */
public void visit(ConstantExpression node) { append(node); }
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Visits the given constant expression.
 **/
public void visit(ConstantExpression constExpr);
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Calls lookup(constExpr) and returns the cached value, if any. If a
 * replacement has not been cached, the constExpr is cached and returned.
 * 
 * @return constExpr
 */
public Expression visit(ConstantExpression constExpr) {
	final Expression ret = lookup(constExpr);
	return ret == null ? cache(constExpr, constExpr) : constExpr;
}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Does nothing.
 */
public void visit(ConstantExpression constExpr) {}
 

import kodkod.ast.ConstantExpression; //导入依赖的package包/类
/**
 * Visits the given constant expression and returns the result.
 * 
 * @return the result of visiting <code>constExpr</code>
 **/
public E visit(ConstantExpression constExpr);