import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/**
 * Calls lookup(compFormula) and returns the cached value, if any. If a
 * translation has not been cached, translates the formula, calls cache(...)
 * on it and returns it.
 * 
 * @return let t = lookup(compFormula) | some t => t, let op =
 *         (binExpr.op).(SUBSET->subset + EQUALS->eq) | cache(compFormula,
 *         op(compFormula.left.accept(this),
 *         compFormula.right.accept(this)))
 */
public final BooleanValue visit(ComparisonFormula compFormula) {
	BooleanValue ret = lookup(compFormula);
	if (ret != null)
		return ret;

	final BooleanMatrix left = compFormula.left().accept(this);
	final BooleanMatrix right = compFormula.right().accept(this);
	final ExprCompOperator op = compFormula.op();

	switch (op) {
		case SUBSET :
			ret = left.subset(right, env);
			break;
		case EQUALS :
			ret = left.eq(right, env);
			break;
		default :
			throw new IllegalArgumentException("Unknown operator: " + compFormula.op());
	}
	return cache(compFormula, ret);
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(ComparisonFormula x) {
	String newname = makename(x);
	if (newname == null)
		return;
	String left = make(x.left());
	String right = make(x.right());
	switch (x.op()) {
		case EQUALS :
			file.printf("Formula %s=%s.eq(%s);%n", newname, left, right);
			break;
		case SUBSET :
			file.printf("Formula %s=%s.in(%s);%n", newname, left, right);
			break;
		default :
			throw new RuntimeException("Unknown kodkod operator \"" + x.op() + "\" encountered");
	}
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/**
 * Calls lookup(compFormula) and returns the cached value, if any.  
 * If a translation has not been cached, translates the formula,
 * calls cache(...) on it and returns it.
 * @return let t = lookup(compFormula) | some t => t, 
 *      let op = (binExpr.op).(SUBSET->subset + EQUALS->eq) | 
 *       cache(compFormula, op(compFormula.left.accept(this), compFormula.right.accept(this)))
 */
public final BooleanValue visit(ComparisonFormula compFormula) {
	BooleanValue ret = lookup(compFormula);
	if (ret!=null) return ret;

	final BooleanMatrix left = compFormula.left().accept(this);
	final BooleanMatrix right = compFormula.right().accept(this);
	final ExprCompOperator op = compFormula.op();

	switch(op) {
	case SUBSET	: ret = left.subset(right, env); break;
	case EQUALS	: ret = left.eq(right, env); break;
	default : 
		throw new IllegalArgumentException("Unknown operator: " + compFormula.op());
	}
	return cache(compFormula,ret);
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/**
 * Calls lookup(compFormula) and returns the cached value, if any.  
 * If a translation has not been cached, translates the formula,
 * calls cache(...) on it and returns it.
 * @return let t = lookup(compFormula) | some t => t, 
 *      let op = (binExpr.op).(SUBSET->subset + EQUALS->eq) | 
 *       cache(compFormula, op(compFormula.left.accept(this), compFormula.right.accept(this)))
 */
public final BooleanValue visit(ComparisonFormula compFormula) {
	BooleanValue ret = lookup(compFormula);
	if (ret!=null) return ret;

	final BooleanMatrix left = compFormula.left().accept(this);
	final BooleanMatrix right = compFormula.right().accept(this);
	final ExprCompOperator op = compFormula.op();

	switch(op) {
	case SUBSET	: ret = left.subset(right); break;
	case EQUALS	: ret = left.eq(right); break;
	default : 
		throw new IllegalArgumentException("Unknown operator: " + compFormula.op());
	}
	return cache(compFormula,ret);
}
 

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

	ret = left==formula.left()&&right==formula.right() ? formula : left.compare(op, right);
	formulas.add(new PartialCannonicalizer.Holder<Formula>(ret, hash));
	return cache(formula,ret);
}
 

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

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

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

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

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/**
 * Calls super.visit(cf) after disabling skolemization and returns the
 * result.
 * 
 * @return super.visit(cf)
 **/
public final Formula visit(ComparisonFormula cf) {
	final int oldDepth = skolemDepth;
	skolemDepth = -1; // cannot skolemize inside a comparison formula
	final Formula ret = super.visit(cf);
	skolemDepth = oldDepth;
	return source(ret, cf);
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(ComparisonFormula x) {
    String newname=makename(x); if (newname==null) return;
    String left=make(x.left());
    String right=make(x.right());
    switch(x.op()) {
       case EQUALS: file.printf("Formula %s=%s.eq(%s);%n", newname, left, right); break;
       case SUBSET: file.printf("Formula %s=%s.in(%s);%n", newname, left, right); break;
       default: throw new RuntimeException("Unknown kodkod operator \""+x.op()+"\" encountered");
    }
}
 

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

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

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/** 
 * Calls super.visit(cf) after disabling skolemization and returns the result. 
 * @return super.visit(cf) 
 **/
public final Formula visit(ComparisonFormula cf) {
	final int oldDepth = skolemDepth;
	skolemDepth = -1; // cannot skolemize inside a comparison formula
	final Formula ret = super.visit(cf);
	skolemDepth = oldDepth;
	return source(ret,cf);
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/** @effects this.tokens' = concat[ this.tokens, tokenize[node.left], node.op, tokenize[node.right] */
public void visit(ComparisonFormula node) {
	if (displayed(node)) return;
	final boolean oldTop = notTop();
	visitChild(node.left(), parenthesize(node.left()));
	infix(node.op());
	visitChild(node.right(), parenthesize(node.right()));
	top = oldTop;
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
public Formula visit(ComparisonFormula formula) { 
	Formula ret = lookup(formula);
	if (ret!=null) return ret;
	
	final ExprCompOperator op = formula.op();
	final Expression left = formula.left().accept(this);
	final Expression right = formula.right().accept(this);
	
	if (left==right) return cache(formula,Formula.TRUE);
	
	ret = left==formula.left()&&right==formula.right() ? formula : left.compare(op, right);
	return cache(formula,ret);
}
 

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

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
public void visit(ComparisonFormula compFormula) {
	if (visited(compFormula))
		return;
	relevant.add(compFormula);
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/** @see #visitFormula(Formula) */
public final void visit(ComparisonFormula cf) {
	visitFormula(cf);
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
@Override
public Proc visit(ComparisonFormula cf) {
	return new Proc.FOL(bounds, cf);
}
 

import kodkod.ast.ComparisonFormula; //导入依赖的package包/类
/**
 * @ensures this.tokens' = concat[ this.tokens, tokenize[node.left],
 *          node.op, tokenize[node.right]
 */
public void visit(ComparisonFormula node) {
	visitChild(node.left(), parenthesize(node.left()));
	infix(node.op());
	visitChild(node.right(), parenthesize(node.right()));
}