• 如果您觉得本站非常有看点，那么赶紧使用Ctrl+D 收藏吧
> java > Java ResolutionTrace类的典型用法和代码示例

Java ResolutionTrace类的典型用法和代码示例

java 1次浏览

本文整理汇总了Java中kodkod.engine.satlab.ResolutionTrace类的典型用法代码示例。如果您正苦于以下问题：Java ResolutionTrace类的具体用法？Java ResolutionTrace怎么用？Java ResolutionTrace使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。

ResolutionTrace类属于kodkod.engine.satlab包，在下文中一共展示了ResolutionTrace类的26个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的Java代码示例。

示例1: next

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (varsToTry.isEmpty())
		return Ints.EMPTY_SET;
	// if the last attempt at reduction was unsuccessful,
	// add the unit clauses that we tried to discard back to coreVars
	coreVars.addAll(StrategyUtils.coreTailUnits(trace));
	final int first = varsToTry.iterator().next();// varsToTry.min();
	varsToTry.remove(first);
	coreVars.remove(first);
	// get all axioms corresponding to the clauses that
	// form the translations of formulas identified by coreVars
	final IntSet relevantClauses = StrategyUtils.clausesFor(trace, coreVars);
	assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size() - 1);
	return relevantClauses;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:21，
代码来源:NCEStrategy.java

示例2: coreVars

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns relevant core variables; that is, all variables that occur both
 * in the positive and negative phase in trace.core.
 * 
 * @return { v: [1..) | (some p, n: trace.core | v in trace.elts[p].literals
 *         and -v in trace.elts[n].literals) }
 */
public static IntSet coreVars(ResolutionTrace trace) {

	final IntSet posVars = new IntTreeSet(), negVars = new IntTreeSet();

	for (Iterator<Clause> iter = trace.iterator(trace.core()); iter.hasNext();) {
		Clause clause = iter.next();
		for (IntIterator lits = clause.literals(); lits.hasNext();) {
			int lit = lits.next();
			if (lit > 0)
				posVars.add(lit);
			else
				negVars.add(-lit);
		}
	}

	posVars.retainAll(negVars);

	assert !posVars.isEmpty();
	final IntSet ret = new IntBitSet(posVars.max() + 1);
	ret.addAll(posVars);

	return ret;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:31，
代码来源:StrategyUtils.java

示例3: coreUnits

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns the set of all variables in the core of the given trace that form
 * unit clauses.
 * 
 * @return { v: [1..) | some c: trace.core | c.size() = 1 and
 *         c.maxVariable() = v }
 */
public static IntSet coreUnits(ResolutionTrace trace) {
	final IntSet units = new IntTreeSet();

	for (Iterator<Clause> itr = trace.reverseIterator(trace.core()); itr.hasNext();) {
		Clause c = itr.next();
		if (c.size() == 1) {
			units.add(c.maxVariable());
		}
	}

	if (units.isEmpty())
		return Ints.EMPTY_SET;

	return Ints.asSet(units.toArray());
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:23，
代码来源:StrategyUtils.java

示例4: clausesFor

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns the indices of all axioms in the given trace that form the
 * translations of the formulas identified by the given variables. This
 * method assumes that the axioms in the given trace were generated by the
 * Kodkod {@linkplain Translator}.
 * 
 * @return let C = { c: trace.prover.clauses | c.maxVariable() in
 *         relevantVars }, T = { c1, c2: C | c2.maxVariable() in
 *         abs(c1.literals) } | C.*T
 */
static IntSet clausesFor(ResolutionTrace trace, IntSet relevantVars) {
	// System.out.println("relevant: " + relevantVars);
	final IntSet axioms = trace.axioms();

	final IntSet reachableVars = new IntBitSet(relevantVars.max() + 1);
	reachableVars.addAll(relevantVars);

	final IntSet relevantAxioms = new IntBitSet(axioms.size());

	final Iterator<Clause> itr = trace.reverseIterator(axioms);
	for (int i = axioms.max(); i >= 0; i--) {
		Clause clause = itr.next();
		int maxVar = clause.maxVariable();
		if (reachableVars.contains(maxVar)) {
			for (IntIterator lits = clause.literals(); lits.hasNext();) {
				reachableVars.add(StrictMath.abs(lits.next()));
			}
			relevantAxioms.add(i);
		}
	}

	return relevantAxioms;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:34，
代码来源:StrategyUtils.java

示例5: next

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (varsToTry.isEmpty())
		return Ints.EMPTY_SET; // tried everything
	final IntSet relevantVars = StrategyUtils.coreTailUnits(trace);

	for (IntIterator varItr = varsToTry.iterator(); varItr.hasNext();) {
		final int var = varItr.next();
		varItr.remove();
		if (relevantVars.remove(var)) { // remove maxVar from the set of
										// relevant variables
			if (relevantVars.isEmpty())
				break; // there was only root formula left
			// get all axioms and resolvents corresponding to the clauses
			// that
			// form the translations of formulas identified by relevant vars
			final IntSet relevantClauses = clausesFor(trace, relevantVars);
			assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size() - 1);
			return relevantClauses;
		}
	}

	varsToTry.clear();
	return Ints.EMPTY_SET;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:30，
代码来源:RCEStrategy.java

示例6: clausesFor

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns the indices of all axioms and resolvents in the given trace that
 * form the translations of the formulas identified by the given variables.
 * This method assumes that the axioms in the given trace were generated by
 * the Kodkod {@linkplain Translator}.
 * 
 * @return let C = { c: trace.prover.clauses | c.maxVariable() in
 *         relevantVars }, T = { c1, c2: C | c2.maxVariable() in
 *         abs(c1.literals) }, A = C.*T | trace.backwardReachable(A) -
 *         trace.backwardReachable(trace.axioms() - A)
 */
private IntSet clausesFor(ResolutionTrace trace, IntSet relevantVars) {

	final IntSet relevantAxioms = StrategyUtils.clausesFor(trace, relevantVars);

	if (dist < trace.resolvents().size()) {
		IntSet relevant = relevantAxioms;
		for (int i = 0, lastSize = 0; lastSize < relevant.size() && i < dist; i++) {
			lastSize = relevant.size();
			relevant = trace.directlyLearnable(relevant);
		}
		return relevant;
	} else {
		return trace.learnable(relevantAxioms); // return all resolvents
	}

	// System.out.println("level 1 resolvents " +
	// (relevant.size()-relevantAxioms.size()) + ", axioms " +
	// relevantAxioms.size());

}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:32，
代码来源:RCEStrategy.java

示例7: next

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (varsToTry.isEmpty())
		return Ints.EMPTY_SET; // tried everything
	final IntSet relevantVars = StrategyUtils.coreTailUnits(trace);

	for (IntIterator varItr = varsToTry.iterator(); varItr.hasNext();) {
		final int var = varItr.next();
		varItr.remove();
		if (relevantVars.remove(var)) { // remove maxVar from the set of
										// relevant variables
			if (relevantVars.isEmpty())
				break; // there was only root formula left
			// get all axioms corresponding to the clauses that
			// form the translations of formulas identified by relevant vars
			final IntSet relevantClauses = StrategyUtils.clausesFor(trace, relevantVars);
			assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size() - 1);
			return relevantClauses;
		}
	}
	varsToTry.clear();
	return Ints.EMPTY_SET;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:28，
代码来源:SCEStrategy.java

示例8: coreVars

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns relevant  core variables; that is, all variables that occur both in the positive and
 * negative phase in trace.core.
 * @return { v: [1..) | (some p, n: trace.core | v in trace.elts[p].literals and -v in trace.elts[n].literals) }
 */
public static IntSet coreVars(ResolutionTrace trace) { 

	final IntSet posVars = new IntTreeSet(), negVars = new IntTreeSet();
	
	for(Iterator<Clause> iter = trace.iterator(trace.core()); iter.hasNext();) {
		Clause clause = iter.next();
		for(IntIterator lits = clause.literals(); lits.hasNext(); ) {
			int lit = lits.next();
			if (lit > 0) posVars.add(lit);
			else negVars.add(-lit);
		}
	}
	
	posVars.retainAll(negVars);
	
	assert !posVars.isEmpty();
	final IntSet ret = new IntBitSet(posVars.max()+1);
	ret.addAll(posVars);
	
	return ret;
}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:27，
代码来源:StrategyUtils.java

示例9: clausesFor

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
	 * Returns the indices of all axioms
	 * in the given trace that form the translations of the formulas
	 * identified by the given variables.  This method assumes that
	 * the axioms in the given trace were generated by the Kodkod
	 * {@linkplain Translator}.
	 * @return 
	 * let C = { c: trace.prover.clauses | c.maxVariable() in relevantVars },
	 *     T = { c1, c2: C | c2.maxVariable() in abs(c1.literals) } |
	 *     C.*T 
	 */
	static IntSet clausesFor(ResolutionTrace trace, IntSet relevantVars) { 
//		System.out.println("relevant: " + relevantVars);
		final IntSet axioms = trace.axioms();

		final IntSet reachableVars = new IntBitSet(relevantVars.max()+1);
		reachableVars.addAll(relevantVars);

		final IntSet relevantAxioms = new IntBitSet(axioms.size());
		
		final Iterator<Clause> itr = trace.reverseIterator(axioms);
		for(int i = axioms.max(); i >= 0; i--) {
			Clause clause = itr.next();
			int maxVar = clause.maxVariable();
			if (reachableVars.contains(maxVar)) {
				for(IntIterator lits = clause.literals(); lits.hasNext(); ) {
					reachableVars.add(StrictMath.abs(lits.next()));
				}
				relevantAxioms.add(i);
			} 
		}
		
		return  relevantAxioms;
	}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:35，
代码来源:StrategyUtils.java

示例10: next

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (varsToTry.isEmpty()) return Ints.EMPTY_SET; // tried everything
	final IntSet relevantVars = StrategyUtils.coreTailUnits(trace);
	
	for(IntIterator varItr = varsToTry.iterator(); varItr.hasNext();) {
		final int var = varItr.next();
		varItr.remove();
		if (relevantVars.remove(var)) { // remove maxVar from the set of relevant variables
			if (relevantVars.isEmpty()) break; // there was only root formula left
			// get all axioms and resolvents corresponding to the clauses that
			// form the translations of formulas identified by relevant vars
			final IntSet relevantClauses = clausesFor(trace, relevantVars); 
			assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size()-1);
			return relevantClauses;
		}
	}
	
	varsToTry.clear();		
	return Ints.EMPTY_SET;
}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:25，
代码来源:RCEStrategy.java

示例11: clausesFor

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
	 * Returns the indices of all axioms and resolvents
	 * in the given trace that form the translations of the formulas
	 * identified by the given variables.  This method assumes that
	 * the axioms in the given trace were generated by the Kodkod
	 * {@linkplain Translator}.
	 * @return 
	 * let C = { c: trace.prover.clauses | c.maxVariable() in relevantVars },
	 *     T = { c1, c2: C | c2.maxVariable() in abs(c1.literals) },
	 *     A = C.*T | 
	 *     trace.backwardReachable(A) - trace.backwardReachable(trace.axioms() - A)
	 */
	private IntSet clausesFor(ResolutionTrace trace, IntSet relevantVars) { 

		final IntSet relevantAxioms = StrategyUtils.clausesFor(trace, relevantVars);

		if (dist<trace.resolvents().size()) { 
			IntSet relevant = relevantAxioms;
			for(int i = 0, lastSize = 0; lastSize < relevant.size() && i < dist; i++) { 
				lastSize = relevant.size();
				relevant = trace.directlyLearnable(relevant);
			}
			return relevant;
		} else {
			return trace.learnable(relevantAxioms); // return all resolvents
		}
		
	
//		System.out.println("level 1 resolvents " + (relevant.size()-relevantAxioms.size()) + ",  axioms " + relevantAxioms.size());
		
	}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:32，
代码来源:RCEStrategy.java

示例12: next

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (varsToTry.isEmpty()) return Ints.EMPTY_SET; // tried everything

	final IntSet relevantVars = StrategyUtils.coreTailUnits(trace);

	
	for(IntIterator varItr = varsToTry.iterator( ); varItr.hasNext();) {
		final int var = varItr.next();
		varItr.remove();
		if (relevantVars.remove(var)) {	// remove maxVar from the set of relevant variables
			if (relevantVars.isEmpty()) break; // there was only one root formula left
			// get all axioms and resolvents corresponding to the clauses that
			// form the translations of formulas identified by relevant vars
			final IntSet relevantClauses = clausesFor(trace, relevantVars); 
			assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size()-1);
			
			if (DBG) System.out.println("relevant clauses: " + relevantClauses.size() + ", removed " + var);
			
			return relevantClauses;
		}
	}
	
	varsToTry.clear();		
	return Ints.EMPTY_SET;
}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:30，
代码来源:AdaptiveRCEStrategy.java

示例13: next

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (varsToTry.isEmpty()) return Ints.EMPTY_SET; // tried everything
	final IntSet relevantVars = StrategyUtils.coreTailUnits(trace);
			
	for(IntIterator varItr = varsToTry.iterator(); varItr.hasNext();) {
		final int var = varItr.next();
		varItr.remove();
		if (relevantVars.remove(var)) { // remove maxVar from the set of relevant variables
			if (relevantVars.isEmpty()) break; // there was only root formula left
			// get all axioms corresponding to the clauses that
			// form the translations of formulas identified by relevant vars
			final IntSet relevantClauses = StrategyUtils.clausesFor(trace, relevantVars); 
			assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size()-1);
			return relevantClauses;
		}
	}
	varsToTry.clear();		
	return Ints.EMPTY_SET;
}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:24，
代码来源:SCEStrategy.java

示例14: next

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (topVars.isEmpty()) return Ints.EMPTY_SET; // tried everything
	final IntSet core = trace.core();
	
	for(Iterator<Clause> iter = trace.iterator(core); iter.hasNext();) {
		Clause clause = iter.next();
		int maxVar = clause.maxVariable();
		if (topVars.remove(maxVar)) {
			// get all core clauses with the given maximum variable
			IntSet exclude = coreClausesWithMaxVar(trace, maxVar);
			assert !exclude.isEmpty();
			//	get all clauses reachable from the conflict clause
			IntSet next = trace.reachable(Ints.singleton(trace.size()-1)); 
			// remove all clauses backward reachable from the clauses with the given maxVar
			next.removeAll(trace.backwardReachable(exclude));
			if (!next.isEmpty()) {
				return next;
			}
		}
	}
	
	topVars.clear();
	return Ints.EMPTY_SET;
}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:29，
代码来源:HybridStrategy.java

示例15: testProofOfNthEmptyClauseCNF

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
@Test
public void testProofOfNthEmptyClauseCNF() {
	for(SATFactory factory : solvers) {
		if (!factory.prover()) continue;
		final SATProver solver = (SATProver) factory.instance();
		solver.addVariables(1);
		solver.addClause(new int[]{1});
		solver.addVariables(1);
		solver.addClause(new int[]{-2});
		solver.addVariables(2);
		solver.addClause(new int[]{2, 3, 4});
		solver.addClause(new int[0]);
		solver.addClause(new int[]{4});
		solver.addClause(new int[]{3});
		assertFalse(solver.solve());
		final ResolutionTrace proof = solver.proof();
		assertEquals(4, proof.size());
		assertEquals(Ints.singleton(3), proof.core());
		assertEquals(Ints.EMPTY_SET, proof.resolvents());
		assertEquals(0, proof.get(3).size());
	}
}

开发者ID:emina，
项目名称:kodkod，
代码行数:23，
代码来源:NativeSolverTest.java

示例16: testProofOfLastEmptyClauseCNF

​ 点赞 3 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
@Test
public void testProofOfLastEmptyClauseCNF() {
	for(SATFactory factory : solvers) {
		if (!factory.prover()) continue;
		final SATProver solver = (SATProver) factory.instance();
		solver.addVariables(1);
		solver.addClause(new int[]{1});
		solver.addVariables(1);
		solver.addClause(new int[]{-2});
		solver.addVariables(2);
		solver.addClause(new int[]{2, 3, 4});
		solver.addClause(new int[0]);
		assertFalse(solver.solve());
		final ResolutionTrace proof = solver.proof();
		assertEquals(4, proof.size());
		assertEquals(Ints.singleton(3), proof.core());
		assertEquals(Ints.EMPTY_SET, proof.resolvents());
		assertEquals(0, proof.get(3).size());
	}
}

开发者ID:emina，
项目名称:kodkod，
代码行数:21，
代码来源:NativeSolverTest.java

示例17: coreTailUnits

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns the consecutive variables at the tail of the core of the given
 * trace that form unit clauses.
 * 
 * @return the consecutive variables at the tail of the core of the given
 *         trace that form unit clauses
 */
static IntSet coreTailUnits(ResolutionTrace trace) {
	final IntSet units = new IntTreeSet();

	for (Iterator<Clause> itr = trace.reverseIterator(trace.core()); itr.hasNext();) {
		Clause c = itr.next();
		if (c.size() == 1) {
			units.add(c.maxVariable());
		} else {
			break;
		}
	}

	return units;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:22，
代码来源:StrategyUtils.java

示例18: next

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (hits.isEmpty())
		return Ints.EMPTY_SET; // tried everything
	final IntSet relevantVars = StrategyUtils.coreTailUnits(trace);

	final long[] byRelevance = sortByRelevance(trace, relevantVars);
	if (DBG)
		printRelevant(byRelevance);
	for (int i = byRelevance.length - 1; i >= 0; i--) {
		final int var = (int) byRelevance[i];
		if (hits.remove(var) != null) {
			// remove maxVar from the set of relevant variables
			relevantVars.remove(var);
			if (relevantVars.isEmpty())
				break; // there was only one root formula left
			// get all axioms and resolvents corresponding to the clauses
			// that
			// form the translations of formulas identified by relevant vars
			final IntSet relevantClauses = clausesFor(trace, relevantVars);
			assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size() - 1);

			if (DBG)
				System.out.println("relevant clauses: " + relevantClauses.size() + ", removed " + var);

			return relevantClauses;
		}
	}

	hits.clear();
	return Ints.EMPTY_SET;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:37，
代码来源:DynamicRCEStrategy.java

示例19: clausesFor

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns the indices of all axioms and resolvents in the given trace that
 * form the translations of the formulas identified by the given variables.
 * This method assumes that the axioms in the given trace were generated by
 * the Kodkod {@linkplain Translator}.
 * 
 * @return let C = { c: trace.prover.clauses | c.maxVariable() in
 *         relevantVars }, T = { c1, c2: C | c2.maxVariable() in
 *         abs(c1.literals) }, A = C.*T | trace.backwardReachable(A) -
 *         trace.backwardReachable(trace.axioms() - A)
 */
private IntSet clausesFor(ResolutionTrace trace, IntSet relevantVars) {
	final double hardness = (double) trace.size() / (double) trace.axioms().size();
	final double coreRatio = ((double) trace.core().size() / (double) trace.axioms().size());

	if (DBG)
		System.out.println("trace size: " + trace.size() + ", axioms: " + trace.axioms().size() + ", core: "
				+ trace.core().size() + ", resolvents: " + trace.resolvents().size());
	if (DBG)
		System.out.println("hardness: " + hardness + ", coreRatio: " + coreRatio);

	final IntSet relevantAxioms = StrategyUtils.clausesFor(trace, relevantVars);
	if (DBG)
		System.out.println("relevant axioms:  " + relevantAxioms.size());

	if (coreRatio < noRecycleRatio) {
		return relevantAxioms;
	} else if (hardness < hardnessCutOff) {
		return trace.learnable(relevantAxioms);
	} else {
		IntSet current = relevantAxioms, last;
		final int maxRelevant = (int) Math.rint(relevantAxioms.size() * recycleLimit);
		do {
			last = current;
			current = trace.directlyLearnable(current);
		} while (last.size() < current.size() && current.size() < maxRelevant);

		if (DBG)
			System.out.println(
					"last: " + last.size() + ", current: " + current.size() + ", maxRelevant: " + maxRelevant);

		return current.size() < maxRelevant ? current : last;
	}

}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:46，
代码来源:DynamicRCEStrategy.java

示例20: next

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(final ResolutionTrace trace) {
	final IntSet core = trace.core();
	if (lastCore > core.size()) {
		lastCore = core.size();
		return core;
	} else {
		lastCore = Integer.MIN_VALUE;
		return Ints.EMPTY_SET;
	}
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:16，
代码来源:ECFPStrategy.java

示例21: next

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (varsToTry.isEmpty())
		return Ints.EMPTY_SET; // tried everything

	final IntSet relevantVars = StrategyUtils.coreTailUnits(trace);

	for (IntIterator varItr = varsToTry.iterator(); varItr.hasNext();) {
		final int var = varItr.next();
		varItr.remove();
		if (relevantVars.remove(var)) { // remove maxVar from the set of
										// relevant variables
			if (relevantVars.isEmpty())
				break; // there was only one root formula left
			// get all axioms and resolvents corresponding to the clauses
			// that
			// form the translations of formulas identified by relevant vars
			final IntSet relevantClauses = clausesFor(trace, relevantVars);
			assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size() - 1);

			if (DBG)
				System.out.println("relevant clauses: " + relevantClauses.size() + ", removed " + var);

			return relevantClauses;
		}
	}

	varsToTry.clear();
	return Ints.EMPTY_SET;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:35，
代码来源:AdaptiveRCEStrategy.java

示例22: clausesFor

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns the indices of all axioms and resolvents in the given trace that
 * form the translations of the formulas identified by the given variables.
 * This method assumes that the axioms in the given trace were generated by
 * the Kodkod {@linkplain Translator}.
 * 
 * @return let C = { c: trace.prover.clauses | c.maxVariable() in
 *         relevantVars }, T = { c1, c2: C | c2.maxVariable() in
 *         abs(c1.literals) }, A = C.*T | trace.backwardReachable(A) -
 *         trace.backwardReachable(trace.axioms() - A)
 */
private IntSet clausesFor(ResolutionTrace trace, IntSet relevantVars) {
	final double hardness = (double) trace.size() / (double) trace.axioms().size();
	final double coreRatio = ((double) trace.core().size() / (double) trace.axioms().size());

	if (DBG)
		System.out.println("\ntrace size: " + trace.size() + ", axioms: " + trace.axioms().size() + ", core: "
				+ trace.core().size() + ", resolvents: " + trace.resolvents().size());
	if (DBG)
		System.out.println("hardness: " + hardness + ", coreRatio: " + coreRatio);

	final IntSet relevantAxioms = StrategyUtils.clausesFor(trace, relevantVars);
	if (DBG)
		System.out.println("relevant axioms:  " + relevantAxioms.size());

	if (coreRatio < noRecycleRatio) {
		return relevantAxioms;
	} else if (hardness < hardnessCutOff) {
		return trace.learnable(relevantAxioms);
	} else {
		IntSet current = relevantAxioms, last;
		final int maxRelevant = (int) Math.rint(relevantAxioms.size() * recycleLimit);
		do {
			last = current;
			current = trace.directlyLearnable(current);
		} while (last.size() < current.size() && current.size() < maxRelevant);

		if (DBG)
			System.out.println(
					"last: " + last.size() + ", current: " + current.size() + ", maxRelevant: " + maxRelevant);

		return current.size() < maxRelevant ? current : last;
	}

}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:46，
代码来源:AdaptiveRCEStrategy.java

示例23: next

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * 
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (topVars.isEmpty())
		return Ints.EMPTY_SET; // tried everything
	final IntSet core = trace.core();

	for (Iterator<Clause> iter = trace.iterator(core); iter.hasNext();) {
		Clause clause = iter.next();
		int maxVar = clause.maxVariable();
		if (topVars.remove(maxVar)) {
			// get all core clauses with the given maximum variable
			IntSet exclude = coreClausesWithMaxVar(trace, maxVar);
			assert !exclude.isEmpty();
			// get all clauses reachable from the conflict clause
			IntSet next = trace.reachable(Ints.singleton(trace.size() - 1));
			// remove all clauses backward reachable from the clauses with
			// the given maxVar
			next.removeAll(trace.backwardReachable(exclude));
			if (!next.isEmpty()) {
				return next;
			}
		}
	}

	topVars.clear();
	return Ints.EMPTY_SET;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:32，
代码来源:HybridStrategy.java

示例24: coreClausesWithMaxVar

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns the indices of the clauses in the unsatisfiable core of the given
 * trace that have the specified maximum variable.
 * 
 * @return { i: trace.core() | trace[i].maxVariable() = maxVariable }
 */
private static IntSet coreClausesWithMaxVar(ResolutionTrace trace, int maxVariable) {
	final IntSet core = trace.core();
	final IntSet restricted = new IntBitSet(core.max() + 1);
	final Iterator<Clause> clauses = trace.iterator(core);
	final IntIterator indices = core.iterator();
	while (clauses.hasNext()) {
		Clause clause = clauses.next();
		int index = indices.next();
		if (clause.maxVariable() == maxVariable)
			restricted.add(index);
	}
	return restricted;
}

开发者ID:AlloyTools，
项目名称:org.alloytools.alloy，
代码行数:20，
代码来源:HybridStrategy.java

示例25: next

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * {@inheritDoc}
 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
 */
public IntSet next(ResolutionTrace trace) {
	if (varsToTry.isEmpty()) return Ints.EMPTY_SET;
	// if the last attempt at reduction was unsuccessful,
	// add the unit clauses that we tried to discard back to coreVars
	coreVars.addAll(StrategyUtils.coreTailUnits(trace));
	final int first = varsToTry.iterator().next();//varsToTry.min();
	varsToTry.remove(first);
	coreVars.remove(first);
	// get all axioms corresponding to the clauses that
	// form the translations of formulas identified by coreVars
	final IntSet relevantClauses = StrategyUtils.clausesFor(trace, coreVars); 
	assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size()-1);
	return relevantClauses;
}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:19，
代码来源:NCEStrategy.java

示例26: coreUnits

​ 点赞 2 ​ 

import kodkod.engine.satlab.ResolutionTrace; //导入依赖的package包/类
/**
 * Returns the set of all variables in the core of the given trace
 * that form unit clauses.
 * @return { v: [1..) | some c: trace.core | c.size() = 1 and c.maxVariable() = v }
 */
public static IntSet coreUnits(ResolutionTrace trace) { 
	final IntSet units = new IntTreeSet();
	
	for(Iterator<Clause> itr = trace.reverseIterator(trace.core()); itr.hasNext(); ) { 	
		Clause c = itr.next();
		if (c.size()==1) { 
			units.add(c.maxVariable());
		}
	}
	
	if (units.isEmpty()) return Ints.EMPTY_SET;
	
	return Ints.asSet(units.toArray());
}

开发者ID:ModelWriter，
项目名称:Tarski，
代码行数:20，
代码来源:StrategyUtils.java

版权声明：本文转自网络文章，转载此文章仅为分享知识，如有侵权，请联系管理员进行删除。
喜欢 (0)