public static Instance check(UniverseFactory uf,
		SATFactory sat,
		Pair<Formula, Pair<Formula, Formula>> answer)
		throws URISyntaxException {
	Formula qf = answer.fst;		
	if (answer.snd.fst != null) {
		qf = qf.and(answer.snd.fst);
	}

	Formula cf = answer.fst;
	if (answer.snd.snd != null) {
		cf = cf.and(answer.snd.snd);
	}
	
	Set<Relation> liveRelations = ASTUtils.gatherRelations(qf.and(cf));
			
	Bounds b = uf.boundUniverse(liveRelations);
	
	Solver solver = new Solver();
	solver.options().setSolver(sat);
	solver.options().setIntEncoding(IntEncoding.TWOSCOMPLEMENT);
	solver.options().setBitwidth(bitWidth);
	//solver.options().setSkolemDepth(-1);
	solver.options().setSymmetryBreaking(0);
	solver.options().setSharing(1);
	Formula f = Nodes.simplify(qf, b);

	if (DEBUG) System.err.println(f);
	
	Solution s = solver.solve(f, b);
	
	if (s.outcome() == Outcome.SATISFIABLE || s.outcome() == Outcome.TRIVIALLY_SATISFIABLE) {
		Instance instance = s.instance();
			
		if (DEBUG) System.err.println(instance);
		return instance;
	} else {
		if (answer.snd.snd != null) {				
			Solution diff = solver.solve(Nodes.simplify(cf, b), b);

			if (diff.sat()) {
				Evaluator eval = new Evaluator(diff.instance());

				for(Relation rl : diff.instance().relations()) {
					if ("extra_solutions".equals(rl.name()) || "missing_solutions".equals(rl.name())) {
						System.err.println(rl.name() + ":\n" + eval.evaluate(rl));
					}
				}
			}
		}
		return null;
	}
}
 

/**
 * Returns the encoding used by this factory to represent integers.
 *
 * @return this.intEncoding
 */
public abstract Options.IntEncoding intEncoding();
 

/**
 * Returns TWOSCOMPLEMENT.
 *
 * @return TWOSCOMPLEMENT
 * @see kodkod.engine.bool.BooleanFactory#intEncoding()
 */
@Override
public IntEncoding intEncoding() {
    return IntEncoding.TWOSCOMPLEMENT;
}
 

/**
 * Returns the encoding used by this factory to represent integers.
 * @return this.intEncoding
 */
public abstract Options.IntEncoding intEncoding();
 

/**
 * Returns TWOSCOMPLEMENT.
 * @return TWOSCOMPLEMENT
 * @see kodkod.engine.bool.BooleanFactory#intEncoding()
 */
@Override
public IntEncoding intEncoding() {
	return IntEncoding.TWOSCOMPLEMENT;
}