Java ModelIterator类代码示例

OGeek|极客世界-中国程序员成长平台 › 门户 › 编程› Java›Java编程经验

原作者: [db:作者] 来自: [db:来源] 收藏邀请

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

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

示例1: countValidConfigurations

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
/****************************************************************************************************************
 *  Count feature model valid configurations
 ****************************************************************************************************************/
// Important: Performance of this operation is very poor as expected for a SAT solver, use a BDD instead
@Override
public double countValidConfigurations() throws FMReasoningException {
	if ( isConsistent() ) {
		ISolver solver = new ModelIterator(satSolver);
		double countSat = 0;
		long start = System.nanoTime();
		try {
			while (solver.isSatisfiable()) {
				solver.model();
				countSat++;				
				if ( (System.nanoTime()-start)/1E6 > timeout ) return -1;
			 }
		} catch (Exception e) {
			throw new FMReasoningException(e);
		}
		return countSat;
	}
	throw new FMReasoningException("Operation does not apply to inconsistent feature models");
}

开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:24，代码来源:ReasoningWithSAT.java

示例2: testModelIterator

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testModelIterator() throws ContradictionException,
        TimeoutException {
    ModelIterator iterator = new ModelIterator(SolverFactory.newDefault());
    iterator.addClause(new VecInt(new int[] { 1, 2 }));
    iterator.addClause(new VecInt(new int[] { -1, -2 }));
    iterator.addClause(new VecInt(new int[] { -3, -4 }));
    iterator.addClause(new VecInt(new int[] { 5, 6 }));
    iterator.addClause(new VecInt(new int[] { -5, -6 }));
    iterator.addClause(new VecInt(new int[] { -1, 3 }));
    int counter = 0;
    int[] sub = new int[0];
    while (iterator.isSatisfiable()) {
        sub = iterator.model();
        counter++;
    }
    assertEquals(8, counter);
    assertEquals(6, sub.length);
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:20，代码来源:BugSAT109.java

示例3: testSubModelIterator

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testSubModelIterator() throws ContradictionException,
        TimeoutException {
    IVecInt subset = new VecInt(new int[] { 1, 2, 3, 4 });
    ModelIterator iterator = new SubModelIterator(
            SolverFactory.newDefault(), subset);
    iterator.addClause(new VecInt(new int[] { 1, 2 }));
    iterator.addClause(new VecInt(new int[] { -1, -2 }));
    iterator.addClause(new VecInt(new int[] { -3, -4 }));
    iterator.addClause(new VecInt(new int[] { 5, 6 }));
    iterator.addClause(new VecInt(new int[] { -5, -6 }));
    iterator.addClause(new VecInt(new int[] { -1, 3 }));
    int counter = 0;
    int[] sub = new int[0];
    while (iterator.isSatisfiable()) {
        sub = iterator.model();
        counter++;
    }
    assertEquals(4, counter);
    assertEquals(4, sub.length);
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:22，代码来源:BugSAT109.java

示例4: setUp

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Before
public void setUp() throws ContradictionException {
    PseudoOptDecorator pbsolver = new PseudoOptDecorator(
            SolverFactory.newDefault());
    IVecInt clause = new VecInt();
    pbsolver.newVar(1000);
    for (int i = 1; i <= 1000; i++) {
        clause.push(-i);
    }
    pbsolver.addClause(clause);
    Vec<BigInteger> weights = new Vec<BigInteger>();
    for (int i = 1; i <= 1000; i++) {
        weights.push(BigInteger.valueOf(5));
    }
    pbsolver.setObjectiveFunction(new ObjectiveFunction(clause, weights));
    this.solver = new ModelIterator(pbsolver);
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:18，代码来源:TestGlobalTimeoutForOptimalModelEnumeration.java

示例5: testIteratingWithObjectiveFunctionWithDecorator

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testIteratingWithObjectiveFunctionWithDecorator() {
    IPBSolver solver = buildSolver2();

    IProblem problem = new ModelIterator(solver);
    int nbModel = 0;
    try {
        while (problem.isSatisfiable()) {
            problem.model(); // needed to discard that model
            nbModel++;
        }
    } catch (TimeoutException e) {
        fail();
    }
    assertEquals(4, nbModel);
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:17，代码来源:TestLonca.java

示例6: testMaxSAtIteratorIfSat

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testMaxSAtIteratorIfSat() throws ContradictionException,
		TimeoutException {
	ISolver solver = new ModelIterator(new OptToSatAdapter(
			new MaxSatDecorator(SolverFactory.newDefault())));
	solver.newVar(3);
	IVecInt literals = new VecInt();
	literals.push(-1).push(-2).push(3);
	solver.addClause(literals);
	literals.clear();
	literals.push(-1).push(2);
	solver.addClause(literals);
	literals.clear();
	literals.push(-1).push(-3);
	solver.addClause(literals);
	literals.clear();
	assertTrue(solver.isSatisfiable());
	assertEquals(3, solver.model().length);
	System.out.println("" + solver.model(1) + solver.model(2)
			+ solver.model(3));
	assertTrue(solver.isSatisfiable());
	assertEquals(3, solver.model().length);
	System.out.println("" + solver.model(1) + solver.model(2)
			+ solver.model(3));
	assertTrue(solver.isSatisfiable());
	assertEquals(3, solver.model().length);
	System.out.println("" + solver.model(1) + solver.model(2)
			+ solver.model(3));
	assertTrue(solver.isSatisfiable());
	assertEquals(3, solver.model().length);
	System.out.println("" + solver.model(1) + solver.model(2)
			+ solver.model(3));
	assertFalse(solver.isSatisfiable());
}

开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:35，代码来源:Bug275101.java

示例7: testMaxSAtIterator

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testMaxSAtIterator() throws ContradictionException,
		TimeoutException {
	ISolver solver = new ModelIterator(new OptToSatAdapter(
			new MaxSatDecorator(SolverFactory.newDefault())));
	solver.newVar(2);
	IVecInt literals = new VecInt();
	literals.push(-1).push(-2);
	solver.addClause(literals);
	literals.clear();
	literals.push(-1).push(2);
	solver.addClause(literals);
	literals.clear();
	literals.push(1).push(-2);
	solver.addClause(literals);
	literals.clear();
	literals.push(1).push(2);
	solver.addClause(literals);
	assertTrue(solver.isSatisfiable());
	assertEquals(2, solver.model().length);
	System.out.println("" + solver.model(1) + solver.model(2));
	assertTrue(solver.isSatisfiable());
	assertEquals(2, solver.model().length);
	System.out.println("" + solver.model(1) + solver.model(2));
	assertTrue(solver.isSatisfiable());
	assertEquals(2, solver.model().length);
	System.out.println("" + solver.model(1) + solver.model(2));
	assertTrue(solver.isSatisfiable());
	assertEquals(2, solver.model().length);
	System.out.println("" + solver.model(1) + solver.model(2));
	assertFalse(solver.isSatisfiable());
}

开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:33，代码来源:Bug275101.java

示例8: tearDDown

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Before
public void tearDDown() throws ContradictionException {
	solver = new ModelIterator(SolverFactory.newDefault());
	IVecInt clause = new VecInt();
	for (int i = 1; i <= 1000; i++)
		clause.push(-i);
	solver.addClause(clause);
}

开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:9，代码来源:TestGroupedTimeoutModelEnumeration.java

示例9: testBugReport

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testBugReport() throws ContradictionException, TimeoutException {
	ISolver theSolver = SolverFactory.newDefault();
	ModelIterator solver = new ModelIterator(new OptToSatAdapter(
			new MaxSatDecorator(SolverFactory.newDefault())));
	System.out.println("Taille de voc : " + solver.nVars());
	solver.newVar(3);
	solver.setExpectedNumberOfClauses(3);
	solver.addClause(new VecInt(new int[] { 1, 2 }));
	solver.addClause(new VecInt(new int[] { 1, 3 }));
	solver.addClause(new VecInt(new int[] { 2, 3 }));
	System.out.println("Taille de voc : " + solver.nVars());
	if (solver.isSatisfiable()) {
		System.out.println("Taille du modèle : " + solver.model().length);
		for (int i = 1; i <= solver.model().length; i++) {
			System.out.print(solver.model(i) + " ");
		}
		System.out.println();
	}

	solver.reset();
	System.out.println("Taille de voc : " + solver.nVars());
	solver.newVar(2);
	solver.setExpectedNumberOfClauses(2);
	solver.addClause(new VecInt(new int[] { 1, 2 }));
	solver.addClause(new VecInt(new int[] { 2 }));
	System.out.println("Taille de voc : " + solver.nVars());
	if (solver.isSatisfiable()) {
		System.out.println("Taille du modèle : " + solver.model().length);
		for (int i = 1; i <= solver.model().length; i++) {
			System.out.print(solver.model(i) + " ");
		}
		System.out.println();
	}
	System.out.println("The End.");

}

开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:38，代码来源:BugFatih.java

示例10: getSolutions

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
public String getSolutions(int number) throws TimeoutException {
	if (contradiction)
           return "contradiction\n";

	StringBuffer out = new StringBuffer();
       IProblem problem = new ModelIterator(solver);
       int[] lastModel = null;
   	for (int i = 0; i < number; i++) {
		if (!problem.isSatisfiable(i > 0)) {
			out.append("only " + i + " solutions\n");
			break;
		}
		int[] model = problem.model();
		if (lastModel != null) {
			boolean same = true;
			for (int j = 0; j < model.length; j++)
				if (model[j] != lastModel[j])
					same = false;
			if (same) {
				out.append("only " + i + " solutions\n");
				break;
			}
		}
		lastModel = model;
		StringBuilder pos = new StringBuilder();
		StringBuilder neg = new StringBuilder();
		for (int var : model)
			if (var > 0)
				pos.append(intToVar.get(Math.abs(var)) + " ");
			else
				neg.append(intToVar.get(Math.abs(var)) + " ");
		out.append("true: " + pos + "    false: " + neg + "\n");
	}
   	return out.toString();
}

开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:36，代码来源:SatSolver.java

示例11: getSolution

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
public String getSolution() throws TimeoutException {
	if (contradiction)
           return null;

	StringBuilder out = new StringBuilder();
       IProblem problem = new ModelIterator(solver);
	if (!problem.isSatisfiable())
		return null;
	int[] model = problem.model();
	for (int var : model)
		if (var > 0)
			out.append(intToVar.get(Math.abs(var)) + "\n");
   	return out.toString();
}

开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:15，代码来源:SatSolver.java

示例12: testMaxSAtIterator

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testMaxSAtIterator() throws ContradictionException,
        TimeoutException {
    ISolver solver = new ModelIterator(new OptToSatAdapter(
            new MaxSatDecorator(SolverFactory.newDefault())));
    solver.newVar(2);
    IVecInt literals = new VecInt();
    literals.push(-1).push(-2);
    solver.addClause(literals);
    literals.clear();
    literals.push(-1).push(2);
    solver.addClause(literals);
    literals.clear();
    literals.push(1).push(-2);
    solver.addClause(literals);
    literals.clear();
    literals.push(1).push(2);
    solver.addClause(literals);
    assertTrue(solver.isSatisfiable());
    assertEquals(2, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2));
    assertTrue(solver.isSatisfiable());
    assertEquals(2, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2));
    assertTrue(solver.isSatisfiable());
    assertEquals(2, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2));
    assertTrue(solver.isSatisfiable());
    assertEquals(2, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2));
    assertFalse(solver.isSatisfiable());
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:33，代码来源:Bug275101.java

示例13: setUp

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Before
public void setUp() throws ContradictionException {
    this.solver = new ModelIterator(SolverFactory.newDefault());
    IVecInt clause = new VecInt();
    for (int i = 1; i <= 15; i++) {
        clause.push(-i);
    }
    this.solver.addClause(clause);
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:10，代码来源:TestGroupedTimeoutModelEnumeration.java

示例14: testBugReport

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testBugReport() throws ContradictionException, TimeoutException {
    ModelIterator solver = new ModelIterator(new OptToSatAdapter(
            new MaxSatDecorator(SolverFactory.newDefault())));
    System.out.println("Taille de voc : " + solver.nVars());
    solver.newVar(3);
    solver.setExpectedNumberOfClauses(3);
    solver.addClause(new VecInt(new int[] { 1, 2 }));
    solver.addClause(new VecInt(new int[] { 1, 3 }));
    solver.addClause(new VecInt(new int[] { 2, 3 }));
    System.out.println("Taille de voc : " + solver.nVars());
    if (solver.isSatisfiable()) {
        System.out.println("Taille du modèle : " + solver.model().length);
        for (int i = 1; i <= solver.model().length; i++) {
            System.out.print(solver.model(i) + " ");
        }
        System.out.println();
    }

    solver.reset();
    System.out.println("Taille de voc : " + solver.nVars());
    solver.newVar(2);
    solver.setExpectedNumberOfClauses(2);
    solver.addClause(new VecInt(new int[] { 1, 2 }));
    solver.addClause(new VecInt(new int[] { 2 }));
    System.out.println("Taille de voc : " + solver.nVars());
    if (solver.isSatisfiable()) {
        System.out.println("Taille du modèle : " + solver.model().length);
        for (int i = 1; i <= solver.model().length; i++) {
            System.out.print(solver.model(i) + " ");
        }
        System.out.println();
    }
    System.out.println("The End.");

}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:37，代码来源:BugFatih.java

示例15: testBugReport

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testBugReport() throws ContradictionException, TimeoutException {
	ModelIterator solver = new ModelIterator(new OptToSatAdapter(
			new MaxSatDecorator(SolverFactory.newDefault())));
	// MaxSatDecorator solver = new
	// MaxSatDecorator(SolverFactory.newDefault());
	System.out.println("Taille de voc : " + solver.nVars());
	solver.newVar(13);
	solver.setExpectedNumberOfClauses(24);
	solver.addClause(new VecInt(new int[] { -1 }));
	solver.addClause(new VecInt(new int[] { -2 }));
	solver.addClause(new VecInt(new int[] { -3, 4 }));
	solver.addClause(new VecInt(new int[] { -3, 5 }));
	solver.addClause(new VecInt(new int[] { -3, 6 }));
	solver.addClause(new VecInt(new int[] { -1, 7 }));
	solver.addClause(new VecInt(new int[] { -2, 6 }));
	solver.addClause(new VecInt(new int[] { -4, 3 }));
	solver.addClause(new VecInt(new int[] { -5, 3 }));
	solver.addClause(new VecInt(new int[] { -6, 3, 2 }));
	solver.addClause(new VecInt(new int[] { -7, 1 }));
	solver.addClause(new VecInt(new int[] { 3, -1, 8 }));
	solver.addClause(new VecInt(new int[] { -3, 1, 8 }));
	solver.addClause(new VecInt(new int[] { -3, -1, 9 }));
	solver.addClause(new VecInt(new int[] { -9 }));
	solver.addClause(new VecInt(new int[] { 1, -2, 10 }));
	solver.addClause(new VecInt(new int[] { -1, 2, 10 }));
	solver.addClause(new VecInt(new int[] { -1, -2, 11 }));
	solver.addClause(new VecInt(new int[] { -10 }));
	solver.addClause(new VecInt(new int[] { -11 }));
	solver.addClause(new VecInt(new int[] { 3, -1, 12 }));
	solver.addClause(new VecInt(new int[] { -3, 1, 12 }));
	solver.addClause(new VecInt(new int[] { -3, -1, 13 }));
	solver.addClause(new VecInt(new int[] { -13 }));
	System.out.println("Taille de voc : " + solver.nVars());
	if (solver.isSatisfiable()) {
		System.out.println("Taille du modèle : " + solver.model().length);
		for (int i = 1; i <= solver.model().length; i++) {
			System.out.print(solver.model(i) + " ");
		}
		System.out.println();
	}
}

开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:43，代码来源:BugFatih2.java

示例16: testThatItWorksWithTwoDecorators

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testThatItWorksWithTwoDecorators() {
    ModelIterator it = new ModelIterator(new GateTranslator(solver));
    assertEquals(solver, it.getSolvingEngine());
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:6，代码来源:TestSolverEngine.java

示例17: testBugReport

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testBugReport() throws ContradictionException, TimeoutException {
    ModelIterator solver = new ModelIterator(new OptToSatAdapter(
            new MaxSatDecorator(SolverFactory.newDefault())));
    // MaxSatDecorator solver = new
    // MaxSatDecorator(SolverFactory.newDefault());
    System.out.println("Taille de voc : " + solver.nVars());
    solver.newVar(13);
    solver.setExpectedNumberOfClauses(24);
    solver.addClause(new VecInt(new int[] { -1 }));
    solver.addClause(new VecInt(new int[] { -2 }));
    solver.addClause(new VecInt(new int[] { -3, 4 }));
    solver.addClause(new VecInt(new int[] { -3, 5 }));
    solver.addClause(new VecInt(new int[] { -3, 6 }));
    solver.addClause(new VecInt(new int[] { -1, 7 }));
    solver.addClause(new VecInt(new int[] { -2, 6 }));
    solver.addClause(new VecInt(new int[] { -4, 3 }));
    solver.addClause(new VecInt(new int[] { -5, 3 }));
    solver.addClause(new VecInt(new int[] { -6, 3, 2 }));
    solver.addClause(new VecInt(new int[] { -7, 1 }));
    solver.addClause(new VecInt(new int[] { 3, -1, 8 }));
    solver.addClause(new VecInt(new int[] { -3, 1, 8 }));
    solver.addClause(new VecInt(new int[] { -3, -1, 9 }));
    solver.addClause(new VecInt(new int[] { -9 }));
    solver.addClause(new VecInt(new int[] { 1, -2, 10 }));
    solver.addClause(new VecInt(new int[] { -1, 2, 10 }));
    solver.addClause(new VecInt(new int[] { -1, -2, 11 }));
    solver.addClause(new VecInt(new int[] { -10 }));
    solver.addClause(new VecInt(new int[] { -11 }));
    solver.addClause(new VecInt(new int[] { 3, -1, 12 }));
    solver.addClause(new VecInt(new int[] { -3, 1, 12 }));
    solver.addClause(new VecInt(new int[] { -3, -1, 13 }));
    solver.addClause(new VecInt(new int[] { -13 }));
    System.out.println("Taille de voc : " + solver.nVars());
    if (solver.isSatisfiable()) {
        System.out.println("Taille du modèle : " + solver.model().length);
        for (int i = 1; i <= solver.model().length; i++) {
            System.out.print(solver.model(i) + " ");
        }
        System.out.println();
    }
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:43，代码来源:BugFatih2.java

示例18: testMaxSAtIteratorIfSat

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
@Test
public void testMaxSAtIteratorIfSat() throws ContradictionException,
        TimeoutException {
    ISolver solver = new ModelIterator(new OptToSatAdapter(
            new MaxSatDecorator(SolverFactory.newDefault())));
    solver.newVar(3);
    IVecInt literals = new VecInt();
    literals.push(-1).push(-2).push(3);
    solver.addClause(literals);
    literals.clear();
    literals.push(-1).push(2);
    solver.addClause(literals);
    literals.clear();
    literals.push(-1).push(-3);
    solver.addClause(literals);
    literals.clear();
    assertTrue(solver.isSatisfiable());
    assertEquals(3, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2)
            + solver.model(3));
    assertTrue(solver.isSatisfiable());
    assertEquals(3, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2)
            + solver.model(3));
    assertTrue(solver.isSatisfiable());
    assertEquals(3, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2)
            + solver.model(3));
    assertTrue(solver.isSatisfiable());
    assertEquals(3, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2)
            + solver.model(3));
    assertTrue(solver.isSatisfiable());
    assertEquals(3, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2)
            + solver.model(3));
    assertTrue(solver.isSatisfiable());
    assertEquals(3, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2)
            + solver.model(3));
    assertTrue(solver.isSatisfiable());
    assertEquals(3, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2)
            + solver.model(3));
    assertTrue(solver.isSatisfiable());
    assertEquals(3, solver.model().length);
    System.out.println("" + solver.model(1) + solver.model(2)
            + solver.model(3));
    assertFalse(solver.isSatisfiable());
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:51，代码来源:Bug275101.java

示例19: BugSAT117ModelIterator

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
public BugSAT117ModelIterator() {
    solver = SolverFactory.newLight();
    gateTranslator = new GateTranslator(solver);
    modelIterator = new ModelIterator(solver);
}

开发者ID:TakehideSoh，项目名称:Scarab，代码行数:6，代码来源:BugSAT117ModelIterator.java

示例20: answer

import org.sat4j.tools.ModelIterator; //导入依赖的package包/类
public PerformanceResult answer(Reasoner r) {
	int iteration = 0;
	if (r == null) {
		throw new FAMAParameterException("Reasoner :Not specified");
	}

	features = new String[((Sat4jReasoner) r).getVariables().size()];
	cnfvalues = new String[((Sat4jReasoner) r).getVariables().size()];

	int i = 0;
	for (Entry<String, String> entry : ((Sat4jReasoner) r).getVariables().entrySet()) {
		features[i] = entry.getKey();
		cnfvalues[i] = entry.getValue();
		i++;
	}

	// prepare the reasoning mechanism
	String cnfmodel = ((Sat4jReasoner) r).getPartialCNF(1);
	solver = SolverFactory.newDefault();
	ModelIterator mi = new ModelIterator(solver);
	solver.setTimeout(3600); // 1 hour timeout
	Reader reader = new DimacsReader(mi);

	try {
		reader.parseInstance(new ByteArrayInputStream((cnfmodel).getBytes(StandardCharsets.UTF_8)));

		// First iteration
		PrintWriter out = new PrintWriter(outputDirectory + "/" + iteration + ".out");
		for (i = 0; i < features.length; i++) {
			if (isValidConf(i + 1)) {
				out.println((i + 1) + "\t" + features[i]);
			}
		}
		out.flush();
		out.close();

		// whatever it remains
		File file = new File(outputDirectory + "/" + iteration + ".out");
		while (file.length() > 0) {
			iteration++;

			try (BufferedReader br = new BufferedReader(new FileReader(file))) {
				String line;
				while ((line = br.readLine()) != null) {
					// process the line.

					String key = line.substring(0, line.indexOf('\t'));
					String value = line.substring(line.indexOf('\t') + 1, line.length());
					map(key, value, iteration);

				}
			}

			file = new File(outputDirectory + "/" + iteration + ".out");
		}

	} catch (ParseFormatException | ContradictionException | IOException e) {
		e.printStackTrace();
	}
	return null;
}

开发者ID:isa-group，项目名称:FaMA，代码行数:62，代码来源:Sat4jAllConfigurationsQuestion.java

注：本文中的org.sat4j.tools.ModelIterator类示例整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。

鲜花

握手

雷人

路过

鸡蛋

该文章已有0人参与评论

请发表评论

全部评论

专题导读

More+

10-27 六六分期app的软件客服如何联系？(六六分期

11-06 可心卡盟:win10系统火狐flash插件崩溃怎么

11-06 亲亲特价:怎么删除回收站图标

11-06 济南大学虚拟社区:鲁大师节能降温的具体办

11-06 xlueops.exe:无线网络安装向导

11-06 女斗合众国:win7系统cf与主机连接不稳定怎

11-06 0xc000022-[cf烟雾头]cf怎么调烟雾头

11-06 qizideyouhuo:应用程序无法正常启动0xc0000

11-06 ipz-185:win7系统vcf文件怎么打开

11-06 傻哥蹦迪:win10系统s4怎么打开usb调试

11-06 八神浩树gtaste:回收站清空了怎么恢复

11-06 妖尾之黑色守护:win10系统电脑没有1440x900

11-06 校园至尊魔王小说:win7系统浏览网页时字体

11-06 女斗合众国:win10系统访问共享文件夹提示请

11-06 tokyo hot n0654:恢复win7系统默认字体一招

11-06 雨酷仙境:设置win7系统转移临时文件夹腾出

11-06 阿穆纳伊之杖:win7系统开始菜单在右边还原

11-06 tunespotting:win10系统火狐flash插件总是

11-06 甘尔葛分析师：计谋网站seo关键词暴涨有什

11-06 蔡贵霖: 计谋网站seo关键词暴涨有什么秘密

11-06 博益网首页:ao3网页版进入不了解决方法

11-06 漏斗子专栏: 网站数据分析小白易懂精华篇

11-06 见证双虹怎么做:win7系统开启telnet命令的

11-06 颾狐蝶蜋:系统资源不足无法完成请求的服务

11-06 国光中学校歌:提交网站到alexa查询详细步骤

11-06 西安有情天:静态网页和动态网页的区别

11-06 红木雅尚斋:外部链接构造对网站的好处

11-06 前官礼遇：防止域名劫持–增强域安全性的10

11-06 密传二转答案: 中文分词算法有哪些

11-06 金泉家园邮编:百度快照劫持的表现及应对方

Java Range类代码示例发布时间：2022-05-22

Java RuntimeOperatorException类代码示例发布时间：2022-05-22

剪的笔顺,诠释剪的笔画,认识剪的部首

1 六六分期app的软件客服如何联系？(六六分期

六六分期app的软件客服如何联系？不知道吗？加qq群【895510560】即可！标题：六六分期

阅读：18175|2023-10-27

2 可心卡盟:win10系统火狐flash插件崩溃怎么

今天小编告诉大家如何处理win10系统火狐flash插件总是崩溃的问题，可能很多用户都不知

阅读：9643|2022-11-06

3 亲亲特价:怎么删除回收站图标

今天小编告诉大家如何对win10系统删除桌面回收站图标进行设置，可能很多用户都不知道

阅读：8166|2022-11-06

4 济南大学虚拟社区:鲁大师节能降温的具体办

今天小编告诉大家如何对win10系统电脑设置节能降温的设置方法，想必大家都遇到过需要

阅读：8542|2022-11-06

5 xlueops.exe:无线网络安装向导

我们在使用xp系统的过程中,经常需要对xp系统无线网络安装向导设置进行设置，可能很多

阅读：8444|2022-11-06

6 女斗合众国:win7系统cf与主机连接不稳定怎

今天小编告诉大家如何处理win7系统玩cf老是与主机连接不稳定的问题，可能很多用户都不

阅读：9368|2022-11-06

7 0xc000022-[cf烟雾头]cf怎么调烟雾头

电脑对日常生活的重要性小编就不多说了，可是一旦碰到win7系统设置cf烟雾头的问题，很

阅读：8415|2022-11-06

8 qizideyouhuo:应用程序无法正常启动0xc0000

我们在日常使用电脑的时候，有的小伙伴们可能在打开应用的时候会遇见提示应用程序无法

阅读：7852|2022-11-06

9 ipz-185:win7系统vcf文件怎么打开

今天小编告诉大家如何对win7系统打开vcf文件进行设置，可能很多用户都不知道怎么对win

阅读：8400|2022-11-06

10 傻哥蹦迪:win10系统s4怎么打开usb调试

今天小编告诉大家如何对win10系统s4开启USB调试模式进行设置，可能很多用户都不知道怎

阅读：7391|2022-11-06

客服电话

电子邮件

Java ModelIterator类代码示例

示例1: countValidConfigurations

示例2: testModelIterator

示例3: testSubModelIterator

示例4: setUp

示例5: testIteratingWithObjectiveFunctionWithDecorator

示例6: testMaxSAtIteratorIfSat

示例7: testMaxSAtIterator

示例8: tearDDown

示例9: testBugReport

示例10: getSolutions

示例11: getSolution

示例12: testMaxSAtIterator

示例13: setUp

示例14: testBugReport

示例15: testBugReport

示例16: testThatItWorksWithTwoDecorators

示例17: testBugReport

示例18: testMaxSAtIteratorIfSat

示例19: BugSAT117ModelIterator

示例20: answer

请发表评论

全部评论

上一篇：

下一篇：

bradtraversy/iweather: Ionic 3 mobile we

CVE-2022-35882

joaomh/curso-de-matlab

断牙刷新位置时间（断牙属性及刷新位置介绍

rugk/mastodon-simplified-federation: Sim

剪的笔顺,诠释剪的笔画,认识剪的部首

六六分期app的软件客服如何联系？(六六分期

florent37/ViewAnimator: A fluent Android

florent37/Shrine-MaterialDesign2: implem

CVE-2020-36276

SimpleSoftwareIO/simple-sms: Send and re

关于我们

产品与服务

解决方案

139-2527-9053