import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(binExpr) 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(binExpr) | some t => t, 
 *      let op = (binExpr.op).(UNION->or + INTERSECTION->and + DIFFERENCE->difference + OVERRIDE->override + JOIN->dot + PRODUCT->cross) | 
 *       cache(binExpr, op(binExpr.left.accept(this), binExpr.right.accept(this)))
 */
public BooleanMatrix visit(BinaryExpression binExpr) {
	BooleanMatrix ret = lookup(binExpr);
	if (ret!=null) return ret;

	final BooleanMatrix left = binExpr.left().accept(this);
	final BooleanMatrix right = binExpr.right().accept(this);
	final ExprOperator op = binExpr.op();

	switch(op) {
	case UNION        	: ret = left.or(right); break;
	case INTERSECTION	: ret = left.and(right); break;
	case DIFFERENCE 	: ret = left.difference(right); break;
	case OVERRIDE 		: ret = left.override(right); break;
	case JOIN 			: ret = left.dot(right); break;
	case PRODUCT		: ret = left.cross(right); break;
	default : 
		throw new IllegalArgumentException("Unknown operator: " + op);
	}

	return cache(binExpr, ret);
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/** @effects appends the tokenization of the given node to this.tokens */
public void visit(BinaryExpression node) {
	if (displayed(node)) return;
	final boolean oldTop = notTop();
	final ExprOperator op = node.op();
	final Expression left = node.left(), right = node.right();
	if (op==ExprOperator.JOIN && left.arity()==1 && right.arity()==2 && right instanceof Relation) { 
		append(right);
		append("[");
		visitChild(left, false);
		append("]");
	} else {
		visitChild(left, parenthesize(op, left));
		infix(op);
		visitChild(right, parenthesize(op, right));
	}
	top = oldTop;
}
 

import kodkod.ast.BinaryExpression; //导入依赖的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.BinaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(binExpr) and returns the cached value, if any. If a
 * replacement has not been cached, visits the expression's children. If
 * nothing changes, the argument is cached and returned, otherwise a
 * replacement expression is cached and returned.
 * 
 * @return { b: BinaryExpression | b.left = binExpr.left.accept(delegate) &&
 *         b.right = binExpr.right.accept(delegate) && b.op = binExpr.op }
 */
public Expression visit(BinaryExpression binExpr) {
	Expression ret = lookup(binExpr);
	if (ret != null)
		return ret;

	final Expression left = binExpr.left().accept(delegate);
	final Expression right = binExpr.right().accept(delegate);
	ret = (left == binExpr.left() && right == binExpr.right()) ? binExpr : left.compose(binExpr.op(), right);
	return cache(binExpr, ret);
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/**
 * Visits the left and right subexpressions if this.visited(binExpr) returns
 * false. Otherwise does nothing.
 * 
 * @ensures binExpr.left.accept(this) && binExpr.right.accept(this)
 */
public void visit(BinaryExpression binExpr) {
	if (visited(binExpr))
		return;
	binExpr.left().accept(this);
	binExpr.right().accept(this);
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(binExpr) 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(binExpr) | x != null => x, cache(binExpr,
 *         binExpr.left.accept(this) + binExpr.right.accept(this))
 */
public Set<T> visit(BinaryExpression binExpr) {
	Set<T> ret = lookup(binExpr);
	if (ret != null)
		return ret;
	ret = newSet();
	ret.addAll(binExpr.left().accept(this));
	ret.addAll(binExpr.right().accept(this));
	return cache(binExpr, ret);
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/**
 * Calls lookup(binExpr) 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(binExpr) | some t => t, let op =
 *         (binExpr.op).(UNION->or + INTERSECTION->and +
 *         DIFFERENCE->difference + OVERRIDE->override + JOIN->dot +
 *         PRODUCT->cross) | cache(binExpr, op(binExpr.left.accept(this),
 *         binExpr.right.accept(this)))
 */
public BooleanMatrix visit(BinaryExpression binExpr) {
	BooleanMatrix ret = lookup(binExpr);
	if (ret != null)
		return ret;

	final BooleanMatrix left = binExpr.left().accept(this);
	final BooleanMatrix right = binExpr.right().accept(this);
	final ExprOperator op = binExpr.op();

	switch (op) {
		case UNION :
			ret = left.or(right);
			break;
		case INTERSECTION :
			ret = left.and(right);
			break;
		case DIFFERENCE :
			ret = left.difference(right);
			break;
		case OVERRIDE :
			ret = left.override(right);
			break;
		case JOIN :
			ret = left.dot(right);
			break;
		case PRODUCT :
			ret = left.cross(right);
			break;
		default :
			throw new IllegalArgumentException("Unknown operator: " + op);
	}

	return cache(binExpr, ret);
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/**
 * @ensures appends the tokenization of the given node to this.tokens
 */
public void visit(BinaryExpression node) {
	final ExprOperator op = node.op();
	visitChild(node.left(), parenthesize(op, node.left()));
	infix(op);
	visitChild(node.right(), parenthesize(op, node.right()));
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(BinaryExpression x) {
	String newname = makename(x);
	if (newname == null)
		return;
	String left = make(x.left());
	String right = make(x.right());
	switch (x.op()) {
		case DIFFERENCE :
			file.printf("Expression %s=%s.difference(%s);%n", newname, left, right);
			break;
		case INTERSECTION :
			file.printf("Expression %s=%s.intersection(%s);%n", newname, left, right);
			break;
		case JOIN :
			file.printf("Expression %s=%s.join(%s);%n", newname, left, right);
			break;
		case OVERRIDE :
			file.printf("Expression %s=%s.override(%s);%n", newname, left, right);
			break;
		case PRODUCT :
			file.printf("Expression %s=%s.product(%s);%n", newname, left, right);
			break;
		case UNION :
			file.printf("Expression %s=%s.union(%s);%n", newname, left, right);
			break;
		default :
			throw new RuntimeException("Unknown kodkod operator \"" + x.op() + "\" encountered");
	}
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/**
 * If x = SOMETHING->RELATION where SOMETHING.arity==1, then return the
 * RELATION, else return null.
 */
private static Relation right(Expression x) {
	if (!(x instanceof BinaryExpression))
		return null;
	BinaryExpression bin = (BinaryExpression) x;
	if (bin.op() != ExprOperator.PRODUCT)
		return null;
	if (bin.left().arity() == 1 && bin.right() instanceof Relation)
		return (Relation) (bin.right());
	else
		return null;
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(BinaryExpression x) {
    String newname=makename(x); if (newname==null) return;
    String left=make(x.left());
    String right=make(x.right());
    switch(x.op()) {
       case DIFFERENCE: file.printf("Expression %s=%s.difference(%s);%n", newname, left, right); break;
       case INTERSECTION: file.printf("Expression %s=%s.intersection(%s);%n", newname, left, right); break;
       case JOIN: file.printf("Expression %s=%s.join(%s);%n", newname, left, right); break;
       case OVERRIDE: file.printf("Expression %s=%s.override(%s);%n", newname, left, right); break;
       case PRODUCT: file.printf("Expression %s=%s.product(%s);%n", newname, left, right); break;
       case UNION: file.printf("Expression %s=%s.union(%s);%n", newname, left, right); break;
       default: throw new RuntimeException("Unknown kodkod operator \""+x.op()+"\" encountered");
    }
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/** If x = SOMETHING->RELATION where SOMETHING.arity==1, then return the RELATION, else return null. */
private static Relation right(Expression x) {
    if (!(x instanceof BinaryExpression)) return null;
    BinaryExpression bin = (BinaryExpression)x;
    if (bin.op() != ExprOperator.PRODUCT) return null;
    if (bin.left().arity()==1 && bin.right() instanceof Relation) return (Relation)(bin.right()); else return null;
}
 

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

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
/** 
 * Calls lookup(binExpr) 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(binExpr) | 
 *          x != null => x,  
 *          cache(binExpr, binExpr.left.accept(this) + binExpr.right.accept(this)) 
 */
public Set<T> visit(BinaryExpression binExpr) {
	Set<T> ret = lookup(binExpr);
	if (ret!=null) return ret;		
	ret = newSet();
	ret.addAll(binExpr.left().accept(this));
	ret.addAll(binExpr.right().accept(this));
	return cache(binExpr, ret);
}
 

import kodkod.ast.BinaryExpression; //导入依赖的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.BinaryExpression; //导入依赖的package包/类
/** @ensures appends the tokenization of the given node to this.tokens */
public void visit(BinaryExpression node) {
	final ExprOperator op = node.op();
	visitChild(node.left(), parenthesize(op, node.left()));
	infix(op);
	visitChild(node.right(), parenthesize(op, node.right()));
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
public Expression visit(BinaryExpression expr) { 
	Expression ret = lookup(expr);
	if (ret!=null) return ret;
	final ExprOperator op = expr.op();
	final Expression left = expr.left().accept(this);
	final Expression right = expr.right().accept(this);
	
	ret = simplify(op, left, right);
	
	if (ret==null) {
	
		final int hash = hash(op, left, right);
		for(Iterator<PartialCannonicalizer.Holder<Expression>> itr = exprs.get(hash); itr.hasNext(); ) {
			final Expression next = itr.next().obj;
			if (next instanceof BinaryExpression) { 
				final BinaryExpression hit = (BinaryExpression) next;
				if (hit.op()==op && hit.left()==left && hit.right()==right) { 
					return cache(expr, hit);
				}
			}
		}

		ret = left==expr.left()&&right==expr.right() ? expr : left.compose(op, right);
		exprs.add(new PartialCannonicalizer.Holder<Expression>(ret, hash));
	}
	
	return cache(expr,ret);
}
 

import kodkod.ast.BinaryExpression; //导入依赖的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.BinaryExpression; //导入依赖的package包/类
public Expression visit(BinaryExpression expr) { 
	Expression ret = lookup(expr);
	if (ret!=null) return ret;
	final ExprOperator op = expr.op();
	final Expression left = expr.left().accept(this);
	final Expression right = expr.right().accept(this);
	
	ret = simplify(op, left, right);
	
	if (ret==null) {
		ret = left==expr.left()&&right==expr.right() ? expr : left.compose(op, right);
	}
	
	return cache(expr,ret);
}
 

import kodkod.ast.BinaryExpression; //导入依赖的package包/类
@SuppressWarnings("unchecked")
private Formula makeReadable(Formula formula) { 
	final List<Formula> replacements = new ArrayList<Formula>();
	final Map<Expression, Integer> levels = new LinkedHashMap<Expression, Integer>();
	final AbstractReplacer replacer = new AbstractReplacer(Collections.EMPTY_SET) { 
		protected <N extends Node> N cache(N node, N replacement) {
			cache.put(node, replacement);
			return replacement;
		}
		public Expression visit(BinaryExpression expr) { 
			Expression ret = lookup(expr);
			if (ret!=null) return ret;
			final Expression left = expr.left().accept(this);
			final Expression right = expr.right().accept(this);
			if (expr.op()==ExprOperator.OVERRIDE && left instanceof Relation) { 
				final int level = levels.containsKey(left) ? levels.get(left) : 0;
				final Relation r = Relation.nary(((Relation)left).name()+"'", expr.arity());
				replacements.add(r.eq(left.compose(expr.op(), right)));
				levels.put(left, level+1);
				return cache(expr, r);
			}
			return cache(expr, left.compose(expr.op(), right));
		}
	};
	
	int size;
	do {
		size = replacements.size();
		formula = formula.accept(replacer);
	} while (size < replacements.size());
	
	return formula.and(Formula.and(replacements));
}