import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Calls lookup(decls) and returns the cached value, if any. If a
 * replacement has not been cached, visits each of the children's variable
 * and expression. If nothing changes, the argument is cached and returned,
 * otherwise a replacement Decls object is cached and returned.
 * 
 * @return { d: Decls | d.size = decls.size && all i: [0..d.size) |
 *         d.declarations[i] = decls.declarations[i].accept(delegate) }
 */
public Decls visit(Decls decls) {
	Decls ret = lookup(decls);
	if (ret != null)
		return ret;

	Decls visitedDecls = null;
	boolean allSame = true;
	for (Decl decl : decls) {
		Decls newDecl = visit(decl);
		if (newDecl != decl)
			allSame = false;
		visitedDecls = (visitedDecls == null) ? newDecl : visitedDecls.and(newDecl);
	}
	ret = allSame ? decls : visitedDecls;
	return cache(decls, ret);
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Returns a formula that properly constrains the given skolem's domain.
 * 
 * @requires !nonSkolems.isEmpty()
 * @return a formula that properly constrains the given skolem's domain.
 */
private Formula domainConstraint(Decl skolemDecl, Relation skolem) {
	final Iterator<DeclInfo> itr = nonSkolems.iterator();
	Decls rangeDecls = null;
	while (itr.hasNext()) {
		Decl d = itr.next().decl;
		Decl dd = d.variable().oneOf(d.expression());
		rangeDecls = rangeDecls != null ? rangeDecls.and(dd) : dd;
	}
	// System.out.println(skolemDecl.expression());
	Expression skolemDomain = skolem;
	for (int i = 0, max = skolemDecl.variable().arity(); i < max; i++) {
		skolemDomain = skolemDomain.join(Expression.UNIV);
	}
	return skolemDomain.in(Formula.TRUE.comprehension(rangeDecls));
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Translates the given comprehension as follows (where A_0...A_|A| stand
 * for boolean variables that represent the tuples of the expression A,
 * etc.): let comprehension = "{ a: A, b: B, ..., x: X | F(a, b, ..., x) }"
 * | { a: A, b: B, ..., x: X | a in A && b in B && ... && x in X && F(a, b,
 * ..., x) }.
 * 
 * @param decls the declarations comprehension
 * @param param formula the body of the comprehension
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations;
 *            should be Boolean.TRUE intially
 * @param partialIndex partial index into the provided matrix; should be 0
 *            initially
 * @param matrix boolean matrix that will retain the final results; should
 *            be an empty matrix of dimensions universe.size^decls.length
 *            initially
 * @ensures the given matrix contains the translation of the comprehension
 *          "{ decls | formula }"
 */
private final void comprehension(Decls decls, Formula formula, int currentDecl, BooleanValue declConstraints,
		int partialIndex, BooleanMatrix matrix) {
	final BooleanFactory factory = interpreter.factory();

	if (currentDecl == decls.size()) {
		// TODO: what about this and overflow???
		matrix.set(partialIndex, factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final int position = (int) StrictMath.pow(interpreter.universe().size(), decls.size() - currentDecl - 1);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for (IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		comprehension(decls, formula, currentDecl + 1, factory.and(entry.value(), declConstraints),
				partialIndex + entry.index() * position, matrix);
		groundValue.set(entry.index(), BooleanConstant.FALSE);
	}
	env = env.parent();
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Translates the given sum expression as follows (where A_0...A_|A| stand
 * for boolean variables that represent the tuples of the expression A,
 * etc.): let sum = "sum a: A, b: B, ..., x: X | IE(a, b, ..., x) " | sum a:
 * A, b: B, ..., x: X | if (a in A && b in B && ... && x in X) then IE(a, b,
 * ..., x) else 0 }.
 * 
 * @param decls intexpr declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations;
 *            should be Boolean.TRUE intially
 * @param values integer values computed so far
 */
private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,
		List<Int> values) {
	final BooleanFactory factory = interpreter.factory();
	if (decls.size() == currentDecl) {
		Int intExpr = expr.accept(this);
		Int newInt = intExpr.choice(declConstraints, factory.integer(0));
		values.add(newInt);
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for (IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		sum(decls, expr, currentDecl + 1, factory.and(entry.value(), declConstraints), values);
		groundValue.set(entry.index(), BooleanConstant.FALSE);
	}
	env = env.parent();
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Visits the given comprehension, quantified formula, or sum
 * expression. The method returns TRUE if the creator body contains any
 * variable not bound by the decls; otherwise returns FALSE.
 */
private Boolean visit(Node creator, Decls decls, Node body) {
	Boolean ret = lookup(creator);
	if (ret != null)
		return ret;
	boolean retVal = false;
	for (Decl decl : decls) {
		retVal = decl.expression().accept(this) || retVal;
		varsInScope.push(decl.variable());
	}
	retVal = ((Boolean) body.accept(this)) || retVal;
	for (int i = decls.size(); i > 0; i--) {
		varsInScope.pop();
	}
	return cache(creator, retVal);
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
public final void testDeepSkolems() {
	solver.options().setSkolemDepth(3);
	testDeepSkolems(Multiplicity.ONE);
	testDeepSkolems(Multiplicity.LONE);
	testDeepSkolems(Multiplicity.SOME);
	testDeepSkolems(Multiplicity.SET);
	final Variable va = Variable.unary("va");
	final Variable vb = Variable.unary("vb");
	Decl da1 = va.oneOf(r1a);
	Decl db = vb.oneOf(r1b);
	final Formula f0 = va.in(vb.join(r2b));
	final Formula f1 = f0.forAll(db).not().forAll(da1);
	final Formula f2 = f0.forSome(db).forSome(da1);
	Instance inst = solve(f1.and(f2));
	assertEquals(bounds.relations().size() + 3, inst.relations().size());
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
public final void testQuantifiedFormula() {

		final Variable p = Variable.unary("p"), q = Variable.unary("q");
		final Decl pdecl = p.oneOf(person), qdecl = q.oneOf(person);
		final Decls pqdecls = pdecl.and(qdecl);
		// all p: Person | some p.spouse = true
		assertTrue(eval(p.join(spouse).some().forAll(pdecl)));
		// all p, q: Person | (p.spouse = q) => ! (q in p.shaken) = true
		assertTrue(eval((p.join(spouse).eq(q).implies(q.in(p.join(shaken)).not()).forAll(pqdecls))));
		// some p: Person | no p.shaken = true
		assertTrue(eval(p.join(shaken).no().forSome(pdecl)));
		// all p: Person | some q: Person | p.shaken = q = false
		assertFalse(eval((p.join(shaken).eq(q).forSome(qdecl)).forAll(pdecl)));
		// some p, q: Person | !(p = q) && (p.shaken = q.shaken) = true
		assertTrue(eval(p.eq(q).not().and(p.join(shaken).eq(q.join(shaken))).forSome(pqdecls)));
		// some p: Person | all q: Person-p | p in q.shaken = false
		assertFalse(eval((p.in(q.join(shaken)).forAll(q.oneOf(person.difference(p)))).forSome(pdecl)));
	}
 

import kodkod.ast.Decl; //导入依赖的package包/类
public final void testComprehension() {
	final Variable[] vars = new Variable[3];
	final Decl[] decls = new Decl[3];
	for (int i = 0; i < 3; i++) {
		Variable v = Variable.unary("v" + i);
		Decl d = v.oneOf(person);
		vars[i] = v;
		decls[i] = d;
	}

	// {v0: Person | no v0.shaken} = univ - shaken.Person
	assertEquals(eval(vars[0].join(shaken).no().comprehension(decls[0])),
			eval(univ.difference(shaken.join(person))));
	// {v0, v1: Person | v1 in v0.shaken} = shaken
	assertEquals(eval(vars[1].in(vars[0].join(shaken)).comprehension(decls[0].and(decls[1]))), value(shaken));
	// {v0, v1, v2: Person | no v1.shaken} = Person->(univ -
	// shaken.Person)->Person
	assertEquals(eval(vars[1].join(shaken).no().comprehension(decls[0].and(decls[1]).and(decls[2]))),
			eval(person.product(univ.difference(shaken.join(person))).product(person)));
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/** {@inheritDoc} */
public void visit(Decl x) {
	String newname = makename(x);
	if (newname == null)
		return;
	String v = make(x.variable());
	String e = make(x.expression());
	switch (x.multiplicity()) {
		case LONE :
			file.printf("Decls %s=%s.loneOf(%s);%n", newname, v, e);
			break;
		case ONE :
			file.printf("Decls %s=%s.oneOf(%s);%n", newname, v, e);
			break;
		case SOME :
			file.printf("Decls %s=%s.someOf(%s);%n", newname, v, e);
			break;
		case SET :
			file.printf("Decls %s=%s.setOf(%s);%n", newname, v, e);
			break;
		default :
			throw new RuntimeException("Unknown kodkod multiplicity \"" + x.multiplicity() + "\" encountered");
	}
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/** 
 * Calls lookup(decls) and returns the cached value, if any.  
 * If a replacement has not been cached, visits each of the children's 
 * variable and expression.  If nothing changes, the argument is cached and
 * returned, otherwise a replacement Decls object is cached and returned.
 * @return { d: Decls | d.size = decls.size && 
 *                      all i: [0..d.size) | d.declarations[i] = decls.declarations[i].accept(this) } 
 */
public Decls visit(Decls decls) { 
	Decls ret = lookup(decls);
	if (ret!=null) return ret;
	
	Decls visitedDecls = null;
	boolean allSame = true;
	for(Decl decl : decls) {
		Decls newDecl = visit(decl);
		if (newDecl != decl) 
			allSame = false;
		visitedDecls = (visitedDecls==null) ? newDecl : visitedDecls.and(newDecl);
	}
	ret = allSame ? decls : visitedDecls;
	return cache(decls, ret);
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Translates the given comprehension as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let comprehension = "{ a: A, b: B, ..., x: X | F(a, b, ..., x) }" |
 *     { a: A, b: B, ..., x: X | a in A && b in B && ... && x in X && F(a, b, ..., x) }.
 * @param decls the declarations comprehension
 * @param param formula the body of the comprehension
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param partialIndex partial index into the provided matrix; should be 0 initially
 * @param matrix boolean matrix that will retain the final results; should be an empty matrix of dimensions universe.size^decls.length initially
 * @ensures the given matrix contains the translation of the comprehension "{ decls | formula }"
 */
private final void comprehension(Decls decls, Formula formula, int currentDecl, 
		BooleanValue declConstraints, int partialIndex, BooleanMatrix matrix) {
	final BooleanFactory factory = interpreter.factory();

	if (currentDecl==decls.size()) {
	    //TODO: what about this and overflow???
		matrix.set(partialIndex, factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final int position = (int)StrictMath.pow(interpreter.universe().size(), decls.size()-currentDecl-1);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		comprehension(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints), 
				partialIndex + entry.index()*position, matrix);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Translates the given sum expression as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let sum = "sum a: A, b: B, ..., x: X | IE(a, b, ..., x) " |
 *     sum a: A, b: B, ..., x: X | if (a in A && b in B && ... && x in X) then IE(a, b, ..., x) else 0 }.
 * @param decls intexpr declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param values integer values computed so far
 */
private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,
		List<Int> values) {
	final BooleanFactory factory = interpreter.factory();
	if (decls.size()==currentDecl) {
		Int intExpr = expr.accept(this);
           Int newInt = intExpr.choice(declConstraints, factory.integer(0));
           values.add(newInt);
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		sum(decls, expr, currentDecl+1, factory.and(entry.value(), declConstraints), values);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Translates the given comprehension as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let comprehension = "{ a: A, b: B, ..., x: X | F(a, b, ..., x) }" |
 *     { a: A, b: B, ..., x: X | a in A && b in B && ... && x in X && F(a, b, ..., x) }.
 * @param decls the declarations comprehension
 * @param param formula the body of the comprehension
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param partialIndex partial index into the provided matrix; should be 0 initially
 * @param matrix boolean matrix that will retain the final results; should be an empty matrix of dimensions universe.size^decls.length initially
 * @ensures the given matrix contains the translation of the comprehension "{ decls | formula }"
 */
private final void comprehension(Decls decls, Formula formula, int currentDecl, 
		BooleanValue declConstraints, int partialIndex, BooleanMatrix matrix) {
	final BooleanFactory factory = interpreter.factory();

	if (currentDecl==decls.size()) {
		matrix.set(partialIndex, factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final int position = (int)StrictMath.pow(interpreter.universe().size(), decls.size()-currentDecl-1);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		comprehension(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints), 
				partialIndex + entry.index()*position, matrix);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Translates the given universally quantified formula as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let quantFormula = "all a: A, b: B, ..., x: X | F(a, b, ..., x)" |
 *     (A_0 && B_0 && ... && X_0 => translate(F(A_0, B_0, ..., X_0))) && ... && 
 *     (A_|A| && B_|B| && ... && X_|X| => translate(F(A_|A|, B_|B|, ..., X_|X|))
 * @param decls formula declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.FALSE intially
 * @param acc the accumulator that contains the top level conjunction; should be an empty AND accumulator initially
 * @ensures the given accumulator contains the translation of the formula "all decls | formula"
 */
private void all(Decls decls, Formula formula, int currentDecl, BooleanValue declConstraints, BooleanAccumulator acc) {
	if (acc.isShortCircuited()) return;
	final BooleanFactory factory = interpreter.factory();

	if (decls.size()==currentDecl) {
		acc.add(factory.or(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		all(decls, formula, currentDecl+1, factory.or(factory.not(entry.value()), declConstraints), acc);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
	
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Translates the given existentially quantified formula as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let quantFormula = "some a: A, b: B, ..., x: X | F(a, b, ..., x)" |
 *     (A_0 && B_0 && ... && X_0 && translate(F(A_0, B_0, ..., X_0))) || ... || 
 *     (A_|A| && B_|B| && ... && X_|X| && translate(F(A_|A|, B_|B|, ..., X_|X|))
 * @param decls formula declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param acc the accumulator that contains the top level conjunction; should be an empty OR accumulator initially
 * @ensures the given accumulator contains the translation of the formula "some decls | formula"
 */
private void some(Decls decls, Formula formula, int currentDecl, BooleanValue declConstraints, BooleanAccumulator acc) {
	if (acc.isShortCircuited()) return;
	final BooleanFactory factory = interpreter.factory();

	if (decls.size()==currentDecl) {
		acc.add(factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		some(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints), acc);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();

}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Translates the given sum expression as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let sum = "sum a: A, b: B, ..., x: X | IE(a, b, ..., x) " |
 *     sum a: A, b: B, ..., x: X | if (a in A && b in B && ... && x in X) then IE(a, b, ..., x) else 0 }.
 * @param decls intexpr declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param values integer values computed so far
 */
private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,
		List<Int> values) {
	final BooleanFactory factory = interpreter.factory();
	if (decls.size()==currentDecl) {
		values.add( expr.accept(this).choice(declConstraints, factory.integer(0)) );
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		sum(decls, expr, currentDecl+1, factory.and(entry.value(), declConstraints), values);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
@Test
public final void testDeepSkolems() {
	solver.options().setSkolemDepth(3);
	testDeepSkolems(Multiplicity.ONE);
	testDeepSkolems(Multiplicity.LONE);
	testDeepSkolems(Multiplicity.SOME);
	testDeepSkolems(Multiplicity.SET);
	final Variable va = Variable.unary("va");
	final Variable vb = Variable.unary("vb");
	Decl da1 = va.oneOf(r1a);
	Decl db = vb.oneOf(r1b);
	final Formula f0 = va.in(vb.join(r2b));
	final Formula f1 = f0.forAll(db).not().forAll(da1);
	final Formula f2 = f0.forSome(db).forSome(da1);
	Instance inst = solve(f1.and(f2));
	assertEquals(bounds.relations().size()+3, inst.relations().size());
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
@Test
public final void testQuantifiedFormula() {

	final Variable p = Variable.unary("p"), q = Variable.unary("q");
	final Decl pdecl = p.oneOf(person), qdecl = q.oneOf(person);
	final Decls pqdecls = pdecl.and(qdecl);
	// all p: Person | some p.spouse                            = true
	assertTrue(eval(p.join(spouse).some().forAll(pdecl)));
	// all p, q: Person | (p.spouse = q) => ! (q in p.shaken)   = true
	assertTrue(eval((p.join(spouse).eq(q).implies(q.in(p.join(shaken)).not()).forAll(pqdecls))));
	// some p: Person | no p.shaken                             = true
	assertTrue(eval(p.join(shaken).no().forSome(pdecl)));
	// all p: Person | some q: Person | p.shaken = q            = false
	assertFalse(eval((p.join(shaken).eq(q).forSome(qdecl)).forAll(pdecl)));
	// some p, q: Person | !(p = q) && (p.shaken = q.shaken)    = true
	assertTrue(eval(p.eq(q).not().and(p.join(shaken).eq(q.join(shaken))).forSome(pqdecls)));
	// some p: Person | all q: Person-p | p in q.shaken         = false
	assertFalse(eval((p.in(q.join(shaken)).forAll(q.oneOf(person.difference(p)))).forSome(pdecl)));
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
@Test
public final void testComprehension() {
	final Variable[] vars = new Variable[3];
	final Decl[] decls = new Decl[3];
	for (int i = 0; i < 3; i++) {
		Variable v = Variable.unary("v"+i);
		Decl d = v.oneOf(person);
		vars[i] = v;
		decls[i] = d;
	}

	// {v0: Person | no v0.shaken} = univ - shaken.Person
	assertEquals(eval(vars[0].join(shaken).no().comprehension(decls[0])), eval(univ.difference(shaken.join(person))));
	// {v0, v1: Person | v1 in v0.shaken} = shaken
	assertEquals(eval(vars[1].in(vars[0].join(shaken)).comprehension(decls[0].and(decls[1]))),
			value(shaken));
	// {v0, v1, v2: Person | no v1.shaken} = Person->(univ - shaken.Person)->Person
	assertEquals(eval(vars[1].join(shaken).no().comprehension(decls[0].and(decls[1]).and(decls[2]))),
			eval(person.product(univ.difference(shaken.join(person))).product(person)));
}
 

import kodkod.ast.Decl; //导入依赖的package包/类
/**
 * Visits all the children of the given declarations node if
 * this.visited(decls) returns false. Otherwise does nothing.
 * 
 * @ensures all d: declarations.declarations | d.variable.accept(this) &&
 *          d.expression.accept(this)
 */
public void visit(Decls decls) {
	if (visited(decls))
		return;
	for (Decl decl : decls) {
		decl.accept(this);
	}
}