import kodkod.ast.Expression; //导入依赖的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.Expression; //导入依赖的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.Expression; //导入依赖的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.Expression; //导入依赖的package包/类
/**
 * Returns the application of the AbTransferOkay predicate.
 * 
 * @return application of the AbTransferOkay predicate.
 */
public Formula AbTransferOkay(Expression s, Expression sprime, Expression a_in, Expression a_out) {
	final Expression e0 = a_in.join(from);
	final Expression e1 = a_in.join(to);

	final Formula f0 = AbWorldSecureOp(s, sprime, a_in, a_out);
	final Formula f1 = Authentic(s, e0);
	final Formula f2 = Authentic(s, e1);
	final Formula f3 = SufficientFundsProperty(s, a_in);
	final Formula f4 = e0.intersection(e1).no();

	final Formula f5 = e0.join(abBalance).join(sprime).eq(e0.join(abBalance).join(s).difference(a_in.join(value)));
	final Formula f6 = e0.join(abLost).join(sprime).eq(e0.join(abLost).join(s));
	final Formula f7 = e1.join(abBalance).join(sprime).eq(e1.join(abBalance).join(s).union(a_in.join(value)));
	final Formula f8 = e1.join(abLost).join(sprime).eq(e1.join(abLost).join(s));

	final Formula f9 = Authentic(sprime, e0);
	final Formula f10 = Authentic(sprime, e1);

	return Formula.and(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10);

}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/** Allocate relations for SubsetSig top-down. */
private Expression allocateSubsetSig(SubsetSig sig) throws Err {
    // We must not visit the same SubsetSig more than once, so if we've been here already, then return the old value right away
    Expression sum = sol.a2k(sig);
    if (sum!=null && sum!=Expression.NONE) return sum;
    // Recursively form the union of all parent expressions
    TupleSet ts = factory.noneOf(1);
    for(Sig parent:sig.parents) {
       Expression p = (parent instanceof PrimSig) ? sol.a2k(parent) : allocateSubsetSig((SubsetSig)parent);
       ts.addAll(sol.query(true, p, false));
       if (sum==null) sum=p; else sum=sum.union(p);
    }
    // If subset is exact, then just use the "sum" as is
    if (sig.exact) { sol.addSig(sig, sum); return sum; }
    // Allocate a relation for this subset sig, then bound it
    rep.bound("Sig "+sig+" in "+ts+"\n");
    Relation r = sol.addRel(sig.label, null, ts);
    sol.addSig(sig, r);
    // Add a constraint that it is INDEED a subset of the union of its parents
    sol.addFormula(r.in(sum), sig.isSubset);
    return r;
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/** Returns the corresponding Kodkod expression for the given expression, or null if it is not associated with anything. */
Expression a2k(Expr expr) throws ErrorFatal {
    while(expr instanceof ExprUnary) {
        if (((ExprUnary)expr).op==ExprUnary.Op.NOOP) { expr = ((ExprUnary)expr).sub; continue; }
        if (((ExprUnary)expr).op==ExprUnary.Op.EXACTLYOF) { expr = ((ExprUnary)expr).sub; continue; }
        break;
    }
    if (expr instanceof ExprConstant && ((ExprConstant)expr).op==ExprConstant.Op.EMPTYNESS) return Expression.NONE;
    if (expr instanceof ExprConstant && ((ExprConstant)expr).op==ExprConstant.Op.STRING) return s2k.get(((ExprConstant)expr).string);
    if (expr instanceof Sig || expr instanceof Field || expr instanceof ExprVar) return a2k.get(expr);
    if (expr instanceof ExprBinary) {
        Expr a=((ExprBinary)expr).left, b=((ExprBinary)expr).right;
        switch(((ExprBinary)expr).op) {
          case ARROW: return a2k(a).product(a2k(b));
          case PLUS: return a2k(a).union(a2k(b));
          case MINUS: return a2k(a).difference(a2k(b));
          //TODO: IPLUS, IMINUS???
        }
    }
    return null; // Current only UNION, PRODUCT, and DIFFERENCE of Sigs and Fields and ExprConstant.EMPTYNESS are allowed in a defined field's definition.
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/**
 * Returns the invariants predicate.
 * 
 * @return invariants
 */
public Formula invariants() {
	final Variable t = Variable.unary("t");

	final Expression losAtT = lineOfSight.join(t);
	final Expression satAtT = satellite.join(t);
	final Formula symNonRefl = symmNonRefl(losAtT).and(symmNonRefl(satAtT));
	final Formula noSatAndLos = satAtT.intersection(losAtT).no();

	final Variable r1 = Variable.unary("r1");
	final Variable r2 = Variable.unary("r2");
	final Expression productUnion = r1.product(r2).union(r2.product(r1));
	final Formula someSatAtT = productUnion.eq(satAtT).forSome(r1.oneOf(Router).and(r2.oneOf(Router)));
	final Formula loneSatAtT = satellite.no().or(someSatAtT);

	return symNonRefl.and(noSatAndLos).and(loneSatAtT).forAll(t.oneOf(Time));
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/**
 * Returns the connectedSites predicate.
 * 
 * @return pred connectedSites(sites: set Site) { -- all sites in the given
 *         set are connected to each other all s: sites | sites - s in
 *         ((site.s).^link).site }
 */
public Formula connectedSites(Expression sites) {
	final Variable s = Variable.unary("s");
	Expression closed;
	if (closureApprox > 0) {
		closed = link;
		for (int i = 1; i < closureApprox; i *= 2) {
			closed = closed.union(closed.join(closed));
		}
	} else {
		closed = link.closure();
	}

	final Expression sreachable = site.join(s).join(closed).join(site);
	final Formula f = sites.difference(s).in(sreachable);
	return f.forAll(s.oneOf(sites));
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/**
 * Parametrization of axioms 14 and 15.
 * 
 * @requires e's are unary, op is ternary
 */
Formula ax14and15(Relation[] e, Relation op) {
	final Expression expr0 = e[5].join(op); // op(e5,...)
	final Expression expr1 = e[5].join(expr0); // op(e5,e5)
	final Expression expr2 = expr1.join(expr0); // op(e5,op(e5,e5))
	final Expression expr3 = expr2.join(expr2.join(op)); // op(op(e5,op(e5,e5)),op(e5,op(e5,e5)))
	final Expression expr3a = expr3.join(op); // op(op(op(e5,op(e5,e5)),op(e5,op(e5,e5))),...)
	final Expression expr4 = e[5].join(expr3a); // op(op(op(e5,op(e5,e5)),op(e5,op(e5,e5))),e5)
	// e0 = op(op(op(e5,op(e5,e5)),op(e5,op(e5,e5))),op(e5,op(e5,e5)))
	final Formula f0 = e[0].eq(expr2.join(expr3a));
	// e1 = op(e5,e5)
	final Formula f1 = e[1].eq(expr1);
	// e2 = op(op(e5,op(e5,e5)),op(e5,op(e5,e5)))
	final Formula f2 = e[2].eq(expr3);
	// e3 = op(op(op(e5,op(e5,e5)),op(e5,op(e5,e5))),e5)
	final Formula f3 = e[3].eq(expr4);
	// e4 = op(e5,op(e5,e5))
	final Formula f4 = e[4].eq(expr2);
	// e6 =
	// op(op(op(op(e5,op(e5,e5)),op(e5,op(e5,e5))),e5),op(e5,op(e5,e5)))
	final Formula f6 = e[6].eq(expr2.join(expr4.join(op)));
	return f0.and(f1).and(f2).and(f3).and(f4).and(f6);
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/**
 * Return the A4TupleSet for the given field (if solution not yet solved, or
 * unsatisfiable, or field not found, then return an empty tupleset)
 */
public A4TupleSet eval(Field field) {
	try {
		if (!solved || eval == null)
			return new A4TupleSet(factory.noneOf(field.type().arity()), this);
		A4TupleSet ans = evalCache.get(field);
		if (ans != null)
			return ans;
		TupleSet ts = eval.evaluate((Expression) TranslateAlloyToKodkod.alloy2kodkod(this, field));
		ans = new A4TupleSet(ts, this);
		evalCache.put(field, ans);
		return ans;
	} catch (Err er) {
		return new A4TupleSet(factory.noneOf(field.type().arity()), this);
	}
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/**
 * Parametrization of axioms 16-22.
 * 
 * @requires e is unary, h is binary
 */
Formula ax16_22(Relation e, Relation h) {
	final Expression expr0 = e.join(op2); // op2(e,...)
	final Expression expr1 = e.join(expr0); // op2(e,e)
	final Expression expr2 = expr1.join(expr1.join(op2)); // op2(op2(e,e),op2(e,e))
	final Expression expr3 = expr2.join(expr0); // op2(e,op2(op2(e,e),op2(e,e)))
	// h(e10) = op2(e,op2(e,e))
	final Formula f0 = e1[0].join(h).eq(expr1.join(expr0));
	// h(e11) = op2(op2(e,e),op2(e,e))
	final Formula f1 = e1[1].join(h).eq(expr2);
	// h(e12) = op2(op2(op2(e,e),op2(e,e)),op2(e,e))
	final Formula f2 = e1[2].join(h).eq(expr1.join(expr2.join(op2)));
	// h(e13) = op2(e,op2(op2(e,e),op2(e,e)))
	final Formula f3 = e1[3].join(h).eq(expr3);
	// h(e14) = op2(e,op2(e,op2(op2(e,e),op2(e,e))))
	final Formula f4 = e1[4].join(h).eq(expr3.join(expr0));
	// h(e15) = op2(e,e)
	final Formula f5 = e1[5].join(h).eq(expr1);
	return Formula.and(f0, f1, f2, f3, f4, f5);
}
 

import kodkod.ast.Expression; //导入依赖的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.Expression; //导入依赖的package包/类
/**
 * Returns the sn_cure_2 axiom.
 * 
 * @return sn_cure_2
 */
public final Formula sn_cure_2() {
	final Variable x0 = Variable.unary("X0");
	final Expression x1 = UNIV.difference(x0.join(gt));
	final Formula f0 = x1.in(releaselg).not().and(x0.in(bcapacitysn)).and(x0.in(qilt27).not()).and(
			x0.join(gt).in(conditionhyper));
	return f0.implies(x1.in(conditionnormo)).forAll(x0.oneOf(UNIV));
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/**
 * Returns the ex_cure axiom.
 * 
 * @return ex_cure
 */
public final Formula ex_cure() {
	final Variable x0 = Variable.unary("X0");
	final Expression x1 = UNIV.difference(x0.join(gt));
	final Formula f0 = x1.in(uptakelg).and(x1.in(uptakepg)).and(x0.in(bcapacityex).not()).and(
			x0.join(gt).in(conditionhyper));
	return f0.implies(x1.in(conditionnormo.union(conditionhypo))).forAll(x0.oneOf(UNIV));
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/**
 * all s : set univ | (some s) iff #s > 0
 */
@Test
public void testCardinality1() {
	Variable s = Variable.unary("s");
	Formula f = s.some().iff(s.count().gt(IntConstant.constant(0))).forAll(s.setOf(Expression.UNIV));
	checkTrue(f);
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/**
 * Returns the associativity axiom.
 * 
 * @return associativity
 */
public final Formula associativity() {
	// all w, x, y, z: A | f[f[x][w][y]][w][z] = f[x][w][f[y][w][z]]
	final Variable w = Variable.unary("w");
	final Variable x = Variable.unary("x");
	final Variable y = Variable.unary("y");
	final Variable z = Variable.unary("z");
	final Expression e0 = y.join(w.join(x.join(f)));
	final Expression e1 = z.join(w.join(e0.join(f)));
	final Expression e2 = z.join(w.join(y.join(f)));
	final Expression e3 = e2.join(w.join(x.join(f)));
	return e1.eq(e3).forAll(w.oneOf(UNIV).and(x.oneOf(UNIV)).and(y.oneOf(UNIV)).and(z.oneOf(UNIV)));
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/** Add a new field to this solution and associate it with the given expression.
 * <br> The expression must contain only constant Relations or Relations that are already bound in this solution.
 * <br> (If the field was already added by a previous call to addField(), then this call will return immediately without altering what it is associated with)
 */
void addField(Field f, Expression expr) throws ErrorFatal {
   if (solved) throw new ErrorFatal("Cannot add an additional field since solve() has completed.");
   if (expr.arity()!=f.type().arity()) throw new ErrorFatal("Field "+f+" must be associated with an "+f.type().arity()+"-ary relational value.");
   if (a2k.containsKey(f)) return;
   a2k.put(f, expr);
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
/** If ex is a simple combination of Relations, then return that combination, else return null. */
private Expression sim(Expr ex) {
    while(ex instanceof ExprUnary) {
       ExprUnary u = (ExprUnary)ex;
       if (u.op!=ExprUnary.Op.NOOP && u.op!=ExprUnary.Op.EXACTLYOF) break;
       ex = u.sub;
    }
    if (ex instanceof ExprBinary) {
       ExprBinary b = (ExprBinary)ex;
       if (b.op==ExprBinary.Op.ARROW || b.op==ExprBinary.Op.PLUS || b.op==ExprBinary.Op.JOIN) {
          Expression left = sim(b.left);  if (left==null) return null;
          Expression right = sim(b.right); if (right==null) return null;
          if (b.op==ExprBinary.Op.ARROW) return left.product(right);
          if (b.op==ExprBinary.Op.PLUS) return left.union(right); else return left.join(right);
       }
    }
    if (ex instanceof ExprConstant) {
       switch(((ExprConstant)ex).op) {
          case EMPTYNESS: return Expression.NONE;
       }
    }
    if (ex==Sig.NONE) return Expression.NONE;
    if (ex==Sig.SIGINT) return Expression.INTS;
    if (ex instanceof Sig) return sol.a2k((Sig)ex);
    if (ex instanceof Field) return sol.a2k((Field)ex);
    return null;
}
 

import kodkod.ast.Expression; //导入依赖的package包/类
protected int exeKodkodDef(int i, int j) {
	IntExpression kkIntExpr = kodkodOpExpr(IntConstant.constant(i), IntConstant.constant(j));
	Expression kkExpr = kkIntExpr.toExpression();
	Formula f = ret
			.eq(kkExpr.some().thenElse(kkIntExpr.toExpression(), IntConstant.constant(DEF_VAL).toExpression()));
	Solution sol = solve(f);
	return eval(sol.instance());
}
 

import kodkod.ast.Expression; //导入依赖的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);
}