import kodkod.instance.Tuple; //导入依赖的package包/类
public final void testEvalUnion() {
	// Hilary + Hilary = Hilary
	assertEquals(eval(hilary.union(hilary)), value(hilary));
	// Hilary + Jocelyn + Person = Person
	assertEquals(eval(hilary.union(jocelyn).union(person)), value(person));
	// spouse + shaken = spouse + shaken
	Set<Tuple> spousePlusShaken = new HashSet<Tuple>();
	spousePlusShaken.addAll(value(spouse));
	spousePlusShaken.addAll(value(shaken));
	assertEquals(eval(spouse.union(shaken)), spousePlusShaken);
	// shaken + spouse = spouse + shaken
	assertEquals(eval(shaken.union(spouse)), spousePlusShaken);
	// spouse + Person = arity mismatch
	try {
		eval(spouse.union(person));
		fail("Expected IllegalArgumentException");
	} catch (IllegalArgumentException iae) {}

}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
public final void testEvalProduct() {
	// Hilary->Jocelyn = Hilary->Jocelyn
	final Set<Tuple> hilaryAndJocelyn = eval(hilary.product(jocelyn));
	final Tuple hj = hilaryAndJocelyn.iterator().next();
	assertEquals(hilaryAndJocelyn.size(), 1);
	assertEquals(hj.atom(0), value(hilary).iterator().next().atom(0));
	assertEquals(hj.atom(1), value(jocelyn).iterator().next().atom(0));

	// Person->(spouse->shaken) = (Person->spouse)->shaken
	assertEquals(eval(person.product(spouse.product(shaken))), eval(person.product(spouse).product(shaken)));
	// Person->(spouse + shaken) = Person->spouse + Person->shaken
	assertEquals(eval(person.product(spouse.union(shaken))),
			eval(person.product(spouse).union(person.product(shaken))));
	// arity(spouse->shaken) = 4
	assertEquals(spouse.product(shaken).arity(), 4);
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/** Parse tuple. */
private Tuple parseTuple(XMLNode tuple, int arity) throws Err {
	Tuple ans = null;
	try {
		for (XMLNode sub : tuple)
			if (sub.is("atom")) {
				Tuple x = factory.tuple(sub.getAttribute("label"));
				if (ans == null)
					ans = x;
				else
					ans = ans.product(x);
			}
		if (ans == null)
			throw new ErrorFatal("Expecting: <tuple> <atom label=\"..\"/> .. </tuple>");
		if (ans.arity() != arity)
			throw new ErrorFatal("Expecting: tuple of arity " + arity + " but got tuple of arity " + ans.arity());
		return ans;
	} catch (Throwable ex) {
		throw new ErrorFatal("Expecting: <tuple> <atom label=\"..\"/> .. </tuple>", ex);
	}
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/**
 * Returns a read-only iterator that iterates over each tuple in this
 * TupleSet.
 */
public Iterator<A4Tuple> iterator() {
	return new Iterator<A4Tuple>() {
		private final Iterator<Tuple> it = tuples.iterator();

		public final boolean hasNext() {
			return it.hasNext();
		}

		public final A4Tuple next() {
			if (!it.hasNext())
				throw new NoSuchElementException();
			return new A4Tuple(it.next(), sol);
		}

		public final void remove() {
			throw new UnsupportedOperationException();
		}
	};
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/**
 * Computes the lowerbound from bottom-up; it will also set a suitable
 * initial value for each sig's upperbound. Precondition: sig is not a
 * builtin sig
 */
private TupleSet computeLowerBound(List<Tuple> atoms, final PrimSig sig) throws Err {
	int n = sc.sig2scope(sig);
	TupleSet lower = factory.noneOf(1);
	for (PrimSig c : sig.children())
		lower.addAll(computeLowerBound(atoms, c));
	TupleSet upper = lower.clone();
	boolean isExact = sc.isExact(sig);
	if (isExact || sig.isTopLevel())
		for (n = n - upper.size(); n > 0; n--) {
			Tuple atom = atoms.remove(atoms.size() - 1);
			// If MUST<SCOPE and s is exact, then add fresh atoms to both
			// LOWERBOUND and UPPERBOUND.
			// If MUST<SCOPE and s is inexact but toplevel, then add fresh
			// atoms to the UPPERBOUND.
			if (isExact)
				lower.add(atom);
			upper.add(atom);
		}
	lb.put(sig, lower);
	ub.put(sig, upper);
	return lower;
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/** Print the tupleset using the name n. */
private void printTupleset(String n, TupleSet ts, Map<Object,String> atomMap) {
	file.printf("TupleSet %s = factory.noneOf(%d);%n", n, ts.arity());
	for (Tuple t : ts) {
		file.printf("%s.add(", n);
		for (int i = 0; i < ts.arity(); i++) {
			if (i != 0)
				file.printf(".product(");
			Object a = t.atom(i);
			String b = atomMap == null ? null : atomMap.get(a);
			file.printf("factory.tuple(\"%s\")", (b == null ? a.toString() : b));
			if (i != 0)
				file.printf(")");
		}
		file.printf(");%n");
	}
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/** Computes the lowerbound from bottom-up; it will also set a suitable initial value for each sig's upperbound.
 * Precondition: sig is not a builtin sig
 */
private TupleSet computeLowerBound(List<Tuple> atoms, final PrimSig sig) throws Err {
    int n = sc.sig2scope(sig);
    TupleSet lower = factory.noneOf(1);
    for(PrimSig c:sig.children()) lower.addAll(computeLowerBound(atoms, c));
    TupleSet upper = lower.clone();
    boolean isExact = sc.isExact(sig);
    if (isExact || sig.isTopLevel()) for(n=n-upper.size(); n>0; n--) {
       Tuple atom = atoms.remove(atoms.size()-1);
       // If MUST<SCOPE and s is exact, then add fresh atoms to both LOWERBOUND and UPPERBOUND.
       // If MUST<SCOPE and s is inexact but toplevel, then add fresh atoms to the UPPERBOUND.
       if (isExact) lower.add(atom);
       upper.add(atom);
    }
    lb.put(sig, lower);
    ub.put(sig, upper);
    return lower;
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/**
 * Returns a pretty-printed string of the given sudoku solution.
 * @requires solution is a valid sudoku solution
 * @requires some r: int | solution.universe = { i: Integer | 1 <= i.intValue() <= r*r }
 * @return a pretty-printed string of the given sudoku solution
 */
public static final String prettyPrint(TupleSet solution) { 
	final StringBuilder str = new StringBuilder();
	final int n = solution.universe().size();
	final int r = (int)Math.sqrt(n);
	appendDivider(str, r);
	final Iterator<Tuple> psol = solution.iterator();
	for(int i = 1; i <= n; i++) {
		str.append("| ");
		for(int j = 0; j < r; j++) {
			for(int k = 0; k < r; k++) {
				final int atom = (Integer)psol.next().atom(2);
				if (atom<10&&r>3) str.append(" ");
				str.append(atom);
				str.append(" ");
			}
			str.append("| ");
		}
		str.append("\n");
		if (i%r==0)	appendDivider(str, r);		
	}
	return str.toString();
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
@Test
public final void testEvalUnion() {
	// Hilary + Hilary = Hilary
	assertEquals(eval(hilary.union(hilary)), value(hilary));
	// Hilary + Jocelyn + Person = Person
	assertEquals(eval(hilary.union(jocelyn).union(person)), value(person));
	// spouse + shaken = spouse + shaken
	Set<Tuple> spousePlusShaken = new HashSet<Tuple>();
	spousePlusShaken.addAll(value(spouse));
	spousePlusShaken.addAll(value(shaken));
	assertEquals(eval(spouse.union(shaken)), spousePlusShaken);
	// shaken + spouse = spouse + shaken
	assertEquals(eval(shaken.union(spouse)), spousePlusShaken);
	// spouse + Person = arity mismatch
	try {
		eval(spouse.union(person));
		fail("Expected IllegalArgumentException");
	} catch (IllegalArgumentException iae) {}

}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
@Test
public final void testEvalProduct() {
	// Hilary->Jocelyn = Hilary->Jocelyn
	final Set<Tuple> hilaryAndJocelyn = eval(hilary.product(jocelyn));
	final Tuple hj = hilaryAndJocelyn.iterator().next();
	assertEquals(hilaryAndJocelyn.size(), 1);
	assertEquals(hj.atom(0), value(hilary).iterator().next().atom(0));
	assertEquals(hj.atom(1), value(jocelyn).iterator().next().atom(0));

	// Person->(spouse->shaken) = (Person->spouse)->shaken
	assertEquals(eval(person.product(spouse.product(shaken))),
			eval(person.product(spouse).product(shaken)));
	// Person->(spouse + shaken) = Person->spouse + Person->shaken
	assertEquals(eval(person.product(spouse.union(shaken))),
			eval(person.product(spouse).union(person.product(shaken))));
	// arity(spouse->shaken) = 4
	assertEquals(spouse.product(shaken).arity(), 4);
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
private static void displayOp(Instance instance, Relation op) {
	System.out.println("\n" + op + ":");
	final Iterator<Tuple> iter = instance.tuples(op).iterator();
	for (int i = 0; i < 7; i++) {
		for (int j = 0; j < 7; j++) {
			System.out.print(iter.next().atom(2));
			System.out.print("\t");
		}
		System.out.println();
	}
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/**
 * Returns the bounds the problem (axioms 1, 4, 9-11, last formula of 14-15,
 * and first formula of 16-22).
 * 
 * @return the bounds for the problem
 */
public final Bounds bounds() {
	final Bounds b = super.bounds();
	final TupleFactory f = b.universe().factory();

	final TupleSet op1h = b.upperBound(op1).clone();
	final TupleSet op2h = b.upperBound(op2).clone();

	final TupleSet op1l = f.setOf(f.tuple("e16", "e16", "e15")); // axiom
																	// 14,
																	// line
																	// 6
	final TupleSet op2l = f.setOf(f.tuple("e26", "e26", "e25")); // axiom
																	// 15,
																	// line
																	// 6

	op1h.removeAll(f.area(f.tuple("e16", "e16", "e10"), f.tuple("e16", "e16", "e16")));
	op1h.addAll(op1l);

	op2h.removeAll(f.area(f.tuple("e26", "e26", "e20"), f.tuple("e26", "e26", "e26")));
	op2h.addAll(op2l);

	b.bound(op1, op1l, op1h);
	b.bound(op2, op2l, op2h);

	final TupleSet high = f.area(f.tuple("e10", "e20"), f.tuple("e15", "e26"));

	// first line of axioms 16-22
	for (int i = 0; i < 7; i++) {
		Tuple t = f.tuple("e16", "e2" + i);
		high.add(t);
		b.bound(h[i], f.setOf(t), high);
		high.remove(t);
	}

	return b;
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
private final void testIntersectionMultiplicity(Multiplicity mult, Relation p, Relation q, Tuple intersection) {
	final Instance m = solve(p.intersection(q).apply(mult));
	assertNotNull(m);
	final Set<Tuple> ps = m.tuples(p), qs = m.tuples(q);
	assertFalse(ps.isEmpty());
	assertFalse(qs.isEmpty());
	assertTrue(ps.contains(intersection));
	assertTrue(qs.contains(intersection));
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/**
 * This constructs a Kodkod Tuple from the list of atoms, and returns null
 * if no such Tuple can be constructed.
 */
private static Tuple t_tuple(TupleFactory factory, Object... atoms) {
	try {
		if (atoms.length <= 0)
			return null;
		return factory.tuple(atoms);
	} catch (Throwable ex) {
		return null;
	}
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
private TupleSet convert(TupleFactory factory, Expr f) throws Err {
	TupleSet old = ((A4TupleSet) (partial.eval(f))).debugGetKodkodTupleset();
	TupleSet ans = factory.noneOf(old.arity());
	for (Tuple oldT : old) {
		Tuple newT = null;
		for (int i = 0; i < oldT.arity(); i++) {
			if (newT == null)
				newT = factory.tuple(oldT.atom(i));
			else
				newT = newT.product(factory.tuple(oldT.atom(i)));
		}
		ans.add(newT);
	}
	return ans;
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/** Parse tuple. */
private Tuple parseTuple(XMLNode tuple, int arity) throws Err {
    Tuple ans = null;
    try {
        for(XMLNode sub:tuple) if (sub.is("atom")) {
            Tuple x = factory.tuple(sub.getAttribute("label"));
            if (ans==null) ans=x; else ans=ans.product(x);
        }
        if (ans==null) throw new ErrorFatal("Expecting: <tuple> <atom label=\"..\"/> .. </tuple>");
        if (ans.arity()!=arity) throw new ErrorFatal("Expecting: tuple of arity "+arity+" but got tuple of arity "+ans.arity());
        return ans;
    } catch(Throwable ex) {
        throw new ErrorFatal("Expecting: <tuple> <atom label=\"..\"/> .. </tuple>", ex);
    }
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/** Returns a read-only iterator that iterates over each tuple in this TupleSet. */
public Iterator<A4Tuple> iterator() {
    return new Iterator<A4Tuple>() {
        private final Iterator<Tuple> it = tuples.iterator();
        public final boolean hasNext() { return it.hasNext(); }
        public final A4Tuple next() {
            if (!it.hasNext()) throw new NoSuchElementException();
            return new A4Tuple(it.next(), sol);
        }
        public final void remove() { throw new UnsupportedOperationException(); }
    };
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/** This constructs a Kodkod Tuple from the list of atoms, and returns null if no such Tuple can be constructed. */
private static Tuple t_tuple (TupleFactory factory, Object... atoms) {
    try {
        if (atoms.length <= 0) return null;
        return factory.tuple(atoms);
    } catch(Throwable ex) {
        return null;
    }
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
/** Print the tupleset using the name n. */
private void printTupleset(String n, TupleSet ts, Map<Object,String> atomMap) {
    file.printf("TupleSet %s = factory.noneOf(%d);%n", n, ts.arity());
    for(Tuple t:ts) {
        file.printf("%s.add(",n);
        for(int i=0; i<ts.arity(); i++) {
            if (i!=0) file.printf(".product(");
            Object a=t.atom(i);
            String b=atomMap==null ? null : atomMap.get(a);
            file.printf("factory.tuple(\"%s\")" , (b==null ? a.toString() : b) );
            if (i!=0) file.printf(")");
        }
        file.printf(");%n");
    }
}
 

import kodkod.instance.Tuple; //导入依赖的package包/类
private TupleSet convert(TupleFactory factory, Expr f) throws Err {
    TupleSet old = ((A4TupleSet) (partial.eval(f))).debugGetKodkodTupleset();
    TupleSet ans = factory.noneOf(old.arity());
    for(Tuple oldT: old) {
        Tuple newT = null;
        for(int i=0; i<oldT.arity(); i++) {
            if (newT==null) newT=factory.tuple(oldT.atom(i)); else newT=newT.product(factory.tuple(oldT.atom(i)));
        }
        ans.add(newT);
    }
    return ans;
}