import kodkod.instance.Instance; //导入依赖的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.instance.Instance; //导入依赖的package包/类
public final void testEmina_01232006() {
	final List<String> atoms = new ArrayList<String>(5);
	for (int i = 0; i < 5; i++)
		atoms.add("a" + i);
	final Universe u = new Universe(atoms);
	final TupleFactory tf = u.factory();

	final Relation r1 = Relation.unary("r1"), r2 = Relation.binary("r2"), r3 = Relation.ternary("r3");
	final Bounds b = new Bounds(u);
	final TupleSet r2Bound = tf.noneOf(2);
	for (int i = 0; i < 4; i++)
		r2Bound.add(tf.tuple(atoms.get(i), atoms.get(i)));
	r2Bound.add(tf.tuple("a4", "a1"));
	r2Bound.add(tf.tuple("a4", "a2"));
	b.bound(r2, r2Bound);
	b.bound(r1, tf.setOf("a0", "a3"), tf.setOf("a0", "a3", "a4"));
	b.bound(r3, tf.setOf(tf.tuple("a0", "a0", "a0"), tf.tuple("a3", "a3", "a3")));
	final Formula f = r1.product(r2).in(r3);

	final Instance instance = solver.solve(f, b).instance();
	assertTrue((new Evaluator(instance)).evaluate(f));
	// System.out.println(instance);
	// System.out.println((new Evaluator(instance)).evaluate(f ));

}
 

import kodkod.instance.Instance; //导入依赖的package包/类
/**
	 * If this.solver.solve() is true, returns 
	 * an interpretation of the cnf solution as a 
	 * mapping from Relations to sets of Tuples.  The Relations
	 * mapped by the returned instance are either leaves
	 * of this.formula with different lower and upper
	 * bounds (i.e. {r: this.formula.*children & Relation | 
	 * this.bounds.upperBound[r] != this.bounds.lowerBound[r]}), 
	 * or skolem constants.
	 * @return an interpretation of the cnf solution as
	 * a mapping from (this.variableUsage().keySet() & Relation) to sets of Tuples.
	 * @throws IllegalStateException - this.solver.solve() has not been called or the 
	 * outcome of the last call was not <code>true</code>.
	 */
	public Instance interpret() {
		final TupleFactory f = bounds.universe().factory();
		final Instance instance = new Instance(bounds.universe());
//		System.out.println(varUsage);
		for(Relation r : bounds.relations()) {
			TupleSet lower = bounds.lowerBound(r);
			IntSet indeces = Ints.bestSet(lower.capacity());
			indeces.addAll(lower.indexView());
			IntSet vars = primaryVarUsage.get(r);
			if (vars!=null) {
				int lit = vars.min();
				for(IntIterator iter = bounds.upperBound(r).indexView().iterator(); iter.hasNext();) {
					final int index = iter.next();
					if (!indeces.contains(index) && solver.valueOf(lit++))
						indeces.add(index);
				}
			}
			instance.add(r, f.setOf(r.arity(), indeces));
		}
		return instance;
	}
 

import kodkod.instance.Instance; //导入依赖的package包/类
/**
	 * Prints the given solution using the given options to the console
	 */
	void print(Instance instance, Options options) {
		final Evaluator eval = new Evaluator(instance, options);
		final int n = instance.universe().size();
		for(int i = 0; i < n; i++) { 
			Expression x = IntConstant.constant(i).toExpression();
			for(int j = 0; j < n; j++) { 
				Expression y = IntConstant.constant(j).toExpression();
				if (eval.evaluate(x.product(y).in(queen))) { 
					System.out.print(" Q");
				} else {
					System.out.print(" .");
				}
			}
			System.out.println();
		}
//		System.out.println(instance); 
	}
 

import kodkod.instance.Instance; //导入依赖的package包/类
/**
	 * Prints the given solution using the given options to the console
	 */
	void print(Instance instance, Options options) {
		final Evaluator eval = new Evaluator(instance, options);
		final int n = instance.tuples(queen).size();
		for(int i = 0; i < n; i++) { 
			Expression ci = IntConstant.constant(i).toExpression();
			for(int j = 0; j < n; j++) { 
				Expression cj = IntConstant.constant(j).toExpression();
				if (eval.evaluate(x.join(ci).intersection(y.join(cj)).some())) { 
					System.out.print(" Q");
				} else {
					System.out.print(" .");
				}
			}
			System.out.println();
		}
//		System.out.println(instance); 
	}
 

import kodkod.instance.Instance; //导入依赖的package包/类
/**
		 * Prints the given solution
		 */
		void print(Instance instance, Options options) {
			final Evaluator eval = new Evaluator(instance, options);
			for(int i = 0; i < n; i++) { 
				Expression ci = IntConstant.constant(i).toExpression();
				for(int j = 0; j < n; j++) { 
					Expression cj = IntConstant.constant(j).toExpression();
					if (eval.evaluate(x.join(ci).intersection(y.join(cj)).some())) { 
						System.out.print(" Q");
					} else {
						System.out.print(" .");
					}
				}
				System.out.println();
			}
//			System.out.println(instance); 
		}
 

import kodkod.instance.Instance; //导入依赖的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.instance.Instance; //导入依赖的package包/类
/**
 * Constructs a new Evaluator for the given instance and options
 * 
 * @ensures this.instance' = instance && this.options' = options
 * @throws NullPointerException instance = null || options = null
 */
public Evaluator(Instance instance, Options options) {
	if (instance == null || options == null)
		throw new NullPointerException();
	this.instance = instance;
	this.options = options;
}
 

import kodkod.instance.Instance; //导入依赖的package包/类
@Override
public void holFixpointIncrementingOutcome(HOLTranslation tr, Instance next) {
	if (next != null)
		System.out.println(String.format("  [%s]   climbed one step", tr));
	else
		System.out.println(String.format("  [%s]   fixpoint reached", tr));
}
 

import kodkod.instance.Instance; //导入依赖的package包/类
/**
 * Constructs a Solution from the given values.
 * 
 * @requires outcome != null && stats != null
 * @requires outcome = SATISFIABLE || TRIVIALLY_SATISFIABLE => instance !=
 *           null
 */
private Solution(Outcome outcome, Statistics stats, Instance instance, Proof proof) {
	assert outcome != null && stats != null;
	this.outcome = outcome;
	this.stats = stats;
	this.instance = instance;
	this.proof = proof;
}
 

import kodkod.instance.Instance; //导入依赖的package包/类
/**
 * Displays an instance obtained with the given options.
 * 
 * @requires inst != null and opt != null
 */
private final void display(Instance inst, Options opt) {
	final Universe univ = inst.universe();
	final Evaluator eval = new Evaluator(inst, opt);
	final TupleFactory factory = univ.factory();
	final List<TupleSet> subnets = new ArrayList<TupleSet>();

	System.out.println("address\t\tnetwork id\tmask\tdevice-interface");
	for (int i = 0, ports = univ.size() - 32; i < ports; i++) {
		final Object atom = univ.atom(i);
		final Relation p = Relation.unary(atom.toString());
		inst.add(p, factory.setOf(atom));

		System.out.print(toQuad(eval.evaluate(addr(p))) + "\t");
		System.out.print(toQuad(eval.evaluate(netid(p))) + "\t");
		System.out.print(eval.evaluate(implicitMask(p)) + "\t");
		System.out.println(p);

		final TupleSet members = eval.evaluate(subnet(p));
		if (!members.isEmpty())
			subnets.add(members);
	}

	System.out.println("\nsubnets:");
	for (TupleSet sub : subnets) {
		System.out.println(sub);
	}

}
 

import kodkod.instance.Instance; //导入依赖的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.Instance; //导入依赖的package包/类
/**
 * Prints the values of the op1, op2, and h1-h7 relations to standard out.
 */
void display(Instance instance) {
	displayOp(instance, op1);
	displayOp(instance, op2);
	for (int i = 0; i < 7; i++) {
		System.out.println("\n" + h[i] + ":");
		System.out.println(instance.tuples(h[i]));
	}
}
 

import kodkod.instance.Instance; //导入依赖的package包/类
private final void display(Instance instance, Options options) {
	final Evaluator eval = new Evaluator(instance, options);
	for (int i = 0; i < 2; i++) {
		System.out.print("                      | ");
		System.out.print(instance.tuples(x[i]).indexView().min());
		System.out.println(" |");
	}

	for (int i = 0; i < rows; i++) {
		System.out.print("| ");
		for (int j = 0; j < cols; j++) {
			System.out.print(instance.tuples(a[i][j]).isEmpty() ? 0 : 1);
			System.out.print(" ");
		}
		System.out.print(i == 1 ? "| * | " : "|   | ");
		System.out.print(instance.tuples(x[i + 2]).indexView().min());
		System.out.print(i == 1 ? " | = | " : " |   | ");
		System.out.print(eval.evaluate(b[i]));
		System.out.println(" |");
	}

	for (int i = 5; i < 8; i++) {
		System.out.print("                      | ");
		System.out.print(instance.tuples(x[i]).indexView().min());
		System.out.println(" |");
	}

	// for(int i = 0; i < 3; i++)
	// System.out.println(b[i]);
	//
	// for(int i = 0; i < rows; i++) {
	// for(int j = 0 ; j < 8; j++) {
	// IntExpression e0 = x[j].sum();
	// IntExpression e1 = a[i][j].some().thenElse(e0,
	// IntConstant.constant(0));
	// System.out.println(e0 + " : " + eval.evaluate(e0));
	// System.out.println(e1 + " : " + eval.evaluate(e1));
	// }
	// }
}
 

import kodkod.instance.Instance; //导入依赖的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.Instance; //导入依赖的package包/类
private Instance solve(Formula f, Bounds b) {

		final Solution sol = solver.solve(f, b);
		final Statistics stats = sol.stats();
		pVars = stats.primaryVariables();
		iVars = stats.variables() - pVars;
		clauses = stats.clauses();
		return sol.instance();

	}
 

import kodkod.instance.Instance; //导入依赖的package包/类
private final void testNoSkolems(Decls d, Formula f) {
	Instance inst = solve(f.not());
	assertEquals(bounds.relations(), inst.relations());

	inst = solve(f.or(r2a.in(r2b)));
	assertEquals(bounds.relations(), inst.relations());

	inst = solve(f.iff(r2a.in(r2b)));
	assertEquals(bounds.relations(), inst.relations());

	inst = solve(r2a.in(r2b).implies(f));
	assertEquals(bounds.relations(), inst.relations());

}
 

import kodkod.instance.Instance; //导入依赖的package包/类
public final void testVincent_02162006() {
	// set ups universe of atoms [1..257]
	final List<Integer> atoms = new ArrayList<Integer>();

	// change this to 256, and the program works
	for (int i = 0; i < 257; i++) {
		atoms.add(i + 1);
	}

	final Universe universe = new Universe(atoms);
	final Bounds bounds = new Bounds(universe);
	final TupleFactory factory = universe.factory();

	// oneRel is bounded to the Integer 1
	final Relation oneRel = Relation.unary("oneRel");

	// rel can contain anything
	final Relation rel = Relation.unary("rel");

	bounds.bound(oneRel, factory.setOf(factory.tuple(atoms.get(0))), factory.setOf(factory.tuple(atoms.get(0))));
	bounds.bound(rel, factory.allOf(1));

	// constraint: oneRel in rel
	Formula formula = oneRel.in(rel);

	// solve

	final Instance instance = solver.solve(formula, bounds).instance();
	assertNotNull(instance);
	// System.out.println(instance);

}
 

import kodkod.instance.Instance; //导入依赖的package包/类
public final void testGreg_11232005() {
	final List<String> atoms = new ArrayList<String>(3);
	atoms.add("-1");
	atoms.add("0");
	atoms.add("1");
	final Universe u = new Universe(atoms);
	final TupleFactory t = u.factory();

	final Relation inc = Relation.binary("inc"), add = Relation.ternary("add"), one = Relation.unary("1"),
			param0 = Relation.unary("param0"), ints = Relation.unary("int");

	// (one param0 && ((1 . (param0 . add)) in (param0 . ^inc)))
	final Formula f = param0.one().and((one.join(param0.join(add))).in(param0.join(inc.closure())));

	final Bounds b = new Bounds(u);

	b.bound(param0, t.allOf(1));
	b.boundExactly(one, t.setOf(t.tuple("1")));
	b.boundExactly(ints, t.allOf(1));
	b.boundExactly(inc, t.setOf(t.tuple("-1", "0"), t.tuple("0", "1")));
	// [1, 1, -1], [1, -1, 0], [1, 0, 1], [-1, 1, 0], [-1, -1, 1],
	// [-1, 0, -1], [0, 1, 1], [0, -1, -1], [0, 0, 0]]
	b.boundExactly(add,
			t.setOf(t.tuple("1", "1", "-1"), t.tuple("1", "-1", "0"), t.tuple("1", "0", "1"),
					t.tuple("-1", "1", "0"), t.tuple("-1", "-1", "1"), t.tuple("-1", "0", "-1"),
					t.tuple("0", "1", "1"), t.tuple("0", "-1", "-1"), t.tuple("0", "0", "0")));

	// System.out.println(f);
	// System.out.println(b);

	final Instance instance = solver.solve(f, b).instance();
	assertTrue((new Evaluator(instance)).evaluate(f));
	// System.out.println(instance);
	// System.out.println((new Evaluator(instance)).evaluate(f ));

}
 

import kodkod.instance.Instance; //导入依赖的package包/类
private final void testBinOp(IntOperator op, IntExpression ei, IntExpression ej, int i, int j, int result,
		int realResult, int mask) {
	final IntExpression e = ei.compose(op, ej);
	final Formula f = ei.eq(constant(i)).and(ej.eq(constant(j))).and(e.eq(constant(result)));
	final Solution s = solve(f);
	Instance inst = s.instance();
	if (overflows(op, ei, ej, i, j, realResult)) {
		assertNull(f.toString(), inst);
	} else {
		assertNotNull(f.toString(), inst);
		final Evaluator eval = new Evaluator(inst, solver.options());
		assertEquals(f.toString(), result & mask, eval.evaluate(e) & mask);
	}
}