import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
private final void testProofExtractor(Class<?>[] probs, Class<? extends ReductionStrategy> strategy, int maxScope) { 
	for(Class<?> prob : probs) { 
		Object instance = instance(prob);
		Map<Method, Formula> checks = invokeAll(instance, checks(prob));
		for(Formula check : checks.values()) { 
			for(int scope = 1; scope <= maxScope; scope++ ) { 
				Bounds bounds = bounds(instance, scope);
				Solution sol = solver.solve(check, bounds);
				if (sol.outcome()==Solution.Outcome.UNSATISFIABLE) {
					minimizeAndVerify(check, bounds, sol.proof(), strategy(strategy, sol.proof().log()));
				} 
			}
		}
		
	}
}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * @return strategy with the given name
 */
@SuppressWarnings("unchecked")
private static Class< ? extends ReductionStrategy> findStrategy(String className) {
	try {
		final Class< ? > c = Class.forName(className);
		if (ReductionStrategy.class.isAssignableFrom(c))
			return (Class<ReductionStrategy>) c;
		else {
			throw new IllegalArgumentException(className + " is not a known strategy.");
		}
	} catch (ClassNotFoundException e) {
		throw new IllegalArgumentException(className + " is not a known strategy.");
	}
}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * Runs the minimal core finder using the specified strategy (with the given
 * resolution depth, if applicable) on the given methods, bounds, and prints
 * out results using the given results printer.
 */
private static void findMinCore(final Class< ? extends ReductionStrategy> strategy, final int depth,
		final Map<Method,Formula> checks, final Bounds bounds, final ResultPrinter out) {

	try {

		final Solver solver = solver();
		final ThreadMXBean bean = ManagementFactory.getThreadMXBean();
		bean.setThreadCpuTimeEnabled(true);
		for (Map.Entry<Method,Formula> check : checks.entrySet()) {
			// System.out.println(PrettyPrinter.print(check.getValue(), 1));
			Solution sol = solver.solve(check.getValue(), bounds);

			if (sol.outcome() == Solution.Outcome.UNSATISFIABLE) {

				final long start = bean.getCurrentThreadUserTime() / 1000000;
				final Set<Formula> initialCore = Nodes.minRoots(check.getValue(),
						sol.proof().highLevelCore().values());
				final Set<Formula> minCore;

				if (strategy == null) { // no strategy -- one-step
					minCore = initialCore;
				} else {
					if (strategy.getSimpleName().startsWith("RCE")) {
						sol.proof().minimize(strategy(strategy, sol.proof().log(), depth));
					} else {
						sol.proof().minimize(strategy(strategy, sol.proof().log()));
					}
					minCore = Nodes.minRoots(check.getValue(), sol.proof().highLevelCore().values());
				}
				final long end = bean.getCurrentThreadUserTime() / 1000000;

				out.printUnsat(check.getKey().getName(), check.getValue(), bounds, sol.stats(), initialCore,
						minCore, end - start);
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
private final void minimizeAndVerify(Formula formula, Bounds bounds, Proof proof, ReductionStrategy strategy) { 
	proof.minimize(strategy);
	final Set<Formula> core = Nodes.allRoots(formula, proof.highLevelCore().values());
	final Set<Formula> tcore = proof.highLevelCore().keySet();
	verify(tcore, proof.log().bounds());
	if (solver.options().coreGranularity()==0) { 
		assertEquals(tcore.size(), core.size());
		verify(core, bounds);
	} else {
		assertNull(vSolver.solve(Formula.and(core), bounds).instance());
	}
}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
@Override
public String unsatCore() {
    Proof proof = solution.proof();
    if (proof == null)
        return "unknown";
    ReductionStrategy strategy = new AdaptiveRCEStrategy(proof.log()); 
    proof.minimize(strategy);
    int minCore = proof.highLevelCore().size();
    StringBuilder sb = new StringBuilder(); 
    sb.append("Core (size="+minCore+"):\n");
    for(Node n : proof.highLevelCore().values()) { 
        sb.append(PrettyPrinter.print(n, 0)).append("\n");
    }
    return sb.toString();
}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.Proof#minimize(kodkod.engine.satlab.ReductionStrategy)
 */
public void minimize(ReductionStrategy strategy) {
	solver.reduce(strategy);
	coreFilter = null;
	coreRoots = null;
}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * Minimizes the current core using the trivial strategy that does one of
 * the following: (1) if there is a root that simplified to FALSE, sets the
 * minimal core to that root; or (2) if not, there must be two roots that
 * translated to x and -x, where x is a boolean literal, so we pick those
 * two as the minimal core. The strategy argument is ignored (it can be
 * null).
 * 
 * @see Proof#minimize(ReductionStrategy)
 */
@Override
public void minimize(ReductionStrategy strategy) {
	final Map<Formula,int[]> rootLits = new LinkedHashMap<Formula,int[]>();
	final Map<Formula,Node> rootNodes = new LinkedHashMap<Formula,Node>();
	final Set<Formula> roots = log().roots();

	for (Iterator<TranslationRecord> itr = core(); itr.hasNext();) {
		final TranslationRecord rec = itr.next();
		if (roots.contains(rec.translated())) {
			// simply record the most recent output value for each formula:
			// this is guaranteed to be the final output value for that
			// formula because of the translation log guarantee that the
			// log is replayed in the order of translation: i.e. a child's
			// output value is always recorded before the parent's
			int[] val = rootLits.get(rec.translated());
			if (val == null) {
				val = new int[1];
				rootLits.put(rec.translated(), val);
			}
			val[0] = rec.literal();
			rootNodes.put(rec.translated(), rec.node());
		}
	}

	final SparseSequence<Formula> lits = new TreeSequence<Formula>();
	for (Map.Entry<Formula,int[]> entry : rootLits.entrySet()) {
		final int lit = entry.getValue()[0];
		if (lit == -Integer.MAX_VALUE) {
			coreRoots = Collections.singletonMap(entry.getKey(), rootNodes.get(entry.getKey()));
			break;
		} else if (lits.containsIndex(-lit)) {
			final Formula f0 = lits.get(-lit);
			final Formula f1 = entry.getKey();
			coreRoots = new LinkedHashMap<Formula,Node>(3);
			coreRoots.put(f0, rootNodes.get(f0));
			coreRoots.put(f1, rootNodes.get(f1));
			coreRoots = Collections.unmodifiableMap(coreRoots);
			break;
		} else {
			lits.put(lit, entry.getKey());
		}
	}

	coreFilter = null;
	assert coreRoots.size() == 1 && rootLits.get(coreRoots.keySet().iterator().next())[0] == -Integer.MAX_VALUE
			|| coreRoots.size() == 2;
}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * Usage: java tests.benchmarks.UCoreStats <class> <scope> [-m method] [-s
 * strategy | oce] [-d depth] [-o (user | stats) ]
 */
public static void main(String[] args) {
	if (args.length < 2)
		usage();
	final Class< ? > problem = findClass(args[0]);
	final Map<String,String> optional = processOptionalArgs(args);

	final Object instance = instance(problem);
	final Bounds bounds = bounds(instance, scope(args[1]));
	final Map<Method,Formula> checks = invokeAll(instance,
			optional.containsKey("-m") ? Collections.singleton(formulaCreator(problem, optional.get("-m")))
					: checks(problem));

	if (checks.isEmpty()) {
		usage();
	}

	final String extractor;
	final Class< ? extends ReductionStrategy> strategy;
	if (optional.containsKey("-s")) {
		extractor = optional.get("-s");
		if (extractor.equals("rce")) {
			strategy = findStrategy("kodkod.engine.ucore.RCEStrategy");
		} else if (extractor.equals("sce")) {
			strategy = findStrategy("kodkod.engine.ucore.SCEStrategy");
		} else if (extractor.equals("nce")) {
			strategy = findStrategy("kodkod.engine.ucore.NCEStrategy");
		} else if (!extractor.equals("oce")) {
			strategy = findStrategy(optional.get("-s"));
		} else {
			strategy = null;
		}
	} else {
		extractor = "oce";
		strategy = null;
	}

	final ResultPrinter out = "stats".equals(optional.get("-o")) ? ResultPrinter.STATS : ResultPrinter.USER;

	if (optional.containsKey("-d")) {
		try {
			// findMinCore(strategy, Integer.parseInt(optional.get("-d")),
			// checks, bounds(instance, 2), out);
			findMinCore(strategy, Integer.parseInt(optional.get("-d")), checks, bounds, out);
		} catch (NumberFormatException nfe) {
			usage();
		}
	} else {
		findMinCore(strategy, Integer.MAX_VALUE, checks, bounds, out);
	}

}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * @see kodkod.engine.Proof#minimize(kodkod.engine.satlab.ReductionStrategy)
 */
public void minimize(ReductionStrategy strategy) {
	solver.reduce(strategy);
	coreFilter = null;
	coreRoots = null;
}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * Minimizes the current core using the trivial strategy
 * that does one of the following: (1) if there is a 
 * root that simplified to FALSE, sets the minimal core
 * to that root; or (2) if not, there must be two
 * roots that translated to x and -x, where x is a boolean 
 * literal, so we pick those two as the minimal core.
 * The strategy argument is ignored (it can be null).
 * @see Proof#minimize(ReductionStrategy)
 */
@Override
public void minimize(ReductionStrategy strategy) {	
	final Map<Formula, int[]> rootLits = new LinkedHashMap<Formula,int[]>();
	final Map<Formula, Node> rootNodes = new LinkedHashMap<Formula, Node>();
	final Set<Formula> roots = log().roots();
	
	for(Iterator<TranslationRecord> itr = core(); itr.hasNext();) { 
		final TranslationRecord rec = itr.next();
		if (roots.contains(rec.translated())) { 
			// simply record the most recent output value for each formula:
			// this is guaranteed to be the final output value for that 
			// formula because of the translation log guarantee that the
			// log is replayed in the order of translation:  i.e. a child's
			// output value is always recorded before the parent's
			int[] val = rootLits.get(rec.translated());
			if (val==null) { 
				val = new int[1]; 
				rootLits.put(rec.translated(), val);
			}
			val[0] = rec.literal();
			rootNodes.put(rec.translated(), rec.node());
		}
	}
	
	final SparseSequence<Formula> lits = new TreeSequence<Formula>();
	for(Map.Entry<Formula,int[]> entry : rootLits.entrySet()) { 
		final int lit = entry.getValue()[0];
		if (lit==-Integer.MAX_VALUE) { 
			coreRoots = Collections.singletonMap(entry.getKey(), rootNodes.get(entry.getKey()));
			break;
		} else if (lits.containsIndex(-lit)) { 
			final Formula f0 = lits.get(-lit);
			final Formula f1 = entry.getKey();
			coreRoots = new LinkedHashMap<Formula, Node>(3);
			coreRoots.put(f0, rootNodes.get(f0));
			coreRoots.put(f1, rootNodes.get(f1));
			coreRoots = Collections.unmodifiableMap(coreRoots);
			break;
		} else {
			lits.put(lit, entry.getKey());
		}
	}
	
	coreFilter = null;
	assert coreRoots.size()==1 && rootLits.get(coreRoots.keySet().iterator().next())[0]==-Integer.MAX_VALUE || coreRoots.size()==2;
}
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * Minimizes the proof of this.log.formula's unsatisfiability using the
 * specified proof reduction strategy. The strategy argument is ignored (it
 * can be null) if this.formula is trivially unsatisfiable with respect to
 * this.bounds. In that case, the core is reduced using the trivial strategy
 * that does one of the following: (1) if there is a root that simplified to
 * FALSE, sets the minimal core to that root; or (2) if not, then there must
 * be two roots that translated to x and -x, where x is a boolean literal,
 * so we pick those two as the minimal core.
 * <p>
 * <b>Note:</b> the core minimization is performed at the level of the
 * transformed formula, not the original formula if the problem was
 * translated with a non-zero {@linkplain Options#coreGranularity() core
 * granularity} setting. In other words, after this method has been called,
 * {@linkplain #highLevelCore() highLevelCore()} returns a map M such that
 * M.keySet() is a minimal core with respect to this.log.bounds. In
 * contrast, {@linkplain Nodes#allRoots(Formula, java.util.Collection)
 * Nodes.roots(this.log.originalFormula, M.values())} is unsatisfiable with
 * respect this.log.originalBounds. These formulas, however, do not
 * necessarily form a minimal core of this.log.originalFormula if the
 * original problem was translated with a non-zero
 * {@linkplain Options#coreGranularity() core granularity} setting.
 * </p>
 * 
 * @ensures minimizes the proof of this.log.formula's unsatisfiability using
 *          the specified proof reduction strategy (or the trivial strategy
 *          if this.formula is trivially unsatisfiable with respect to
 *          this.bounds).
 * @see kodkod.engine.satlab.ReductionStrategy
 */
public abstract void minimize(ReductionStrategy strategy);
 

import kodkod.engine.satlab.ReductionStrategy; //导入依赖的package包/类
/**
 * Minimizes the proof of this.log.formula's unsatisfiability
 * using the specified proof reduction strategy.  The strategy
 * argument is ignored (it can be null) if this.formula is 
 * trivially unsatisfiable with respect to this.bounds.  In that
 * case, the core is reduced using the trivial strategy
 * that does one of the following: (1) if there is a 
 * root that simplified to FALSE, sets the minimal core
 * to that root; or (2) if not, then there must be two
 * roots that translated to x and -x, where x is a boolean 
 * literal, so we pick those two as the minimal core. 
 * 
 * <p><b>Note:</b> the core minimization is performed at the level of the 
 * transformed formula, not the original formula if the problem was translated
 * with a non-zero {@linkplain Options#coreGranularity() core granularity} setting.
 * In other words, after this method has been called, {@linkplain #highLevelCore() highLevelCore()} 
 * returns a map M such that M.keySet() is a minimal core with respect to this.log.bounds. In contrast,
 * {@linkplain Nodes#allRoots(Formula, java.util.Collection) Nodes.roots(this.log.originalFormula, M.values())} is 
 * unsatisfiable with respect this.log.originalBounds.  These formulas, however, do not necessarily form a 
 * minimal core of this.log.originalFormula if the original problem was translated
 * with a non-zero {@linkplain Options#coreGranularity() core granularity} setting.  </p>
 * 
 * @ensures minimizes the proof of this.log.formula's unsatisfiability
 * using the specified proof reduction strategy (or the trivial 
 * strategy if this.formula is trivially unsatisfiable with respect
 * to this.bounds). 
 * 
 * @see kodkod.engine.satlab.ReductionStrategy
 */
public abstract void minimize(ReductionStrategy strategy);