Java ParseFormatException类代码示例

OStack程序员社区-中国程序员成长平台 › 门户 › 编程› Java›Java编程经验

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

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

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

示例1: verifySatICPL_2

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test
public void verifySatICPL_2() throws IOException, ParseFormatException, ContradictionException, org.sat4j.specs.TimeoutException, CSVException{
	ISolver solver = SolverFactory.newDefault();
	Reader reader = new LecteurDimacs(solver);
	IProblem problem = reader.parseInstance("TestData/Realistic/freebsd-icse11.dimacs");
	assertTrue(problem.isSatisfiable());
	
	CNF cnf = new CNF("TestData/Realistic/freebsd-icse11.dimacs", CNF.type.dimacs);
	
	CoveringArray ca = new CoveringArrayFile("reports/bestcoverages/freebsd-icse11-size78-1thread.dimacs.ca2.csv");
	for(int n = 0; n < ca.getRowCount(); n++){
		// Convert
		Integer[] solinteger = ca.getRow(n);
		int[] sol = new int[solinteger.length];
		for(int i = 0; i < sol.length; i++){
			sol[i] = cnf.getNr(ca.getId(i+1));
			if(solinteger[i]==1) sol[i] = -sol[i];
		}
		IVecInt assumps = new VecInt(sol);
		
		// Test
		assertTrue(problem.isSatisfiable(assumps));
	}
}

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

示例2: verifySatICPL_3

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test
public void verifySatICPL_3() throws IOException, ParseFormatException, ContradictionException, org.sat4j.specs.TimeoutException, CSVException{
	ISolver solver = SolverFactory.newDefault();
	Reader reader = new LecteurDimacs(solver);
	IProblem problem = reader.parseInstance("TestData/Realistic/2.6.28.6-icse11.dimacs");
	assertTrue(problem.isSatisfiable());
	
	CNF cnf = new CNF("TestData/Realistic/2.6.28.6-icse11.dimacs", CNF.type.dimacs);
	
	CoveringArray ca = new CoveringArrayFile("reports/bestcoverages/2.6.28.6-icse11-size469-1thread.dimacs.ca2.csv");
	for(int n = 0; n < ca.getRowCount(); n++){
		// Convert
		Integer[] solinteger = ca.getRow(n);
		int[] sol = new int[solinteger.length];
		for(int i = 0; i < sol.length; i++){
			sol[i] = cnf.getNr(ca.getId(i+1));
			if(solinteger[i]==1) sol[i] = -sol[i];
		}
		IVecInt assumps = new VecInt(sol);
		//System.out.println(n + ", " + assumps.size());
		
		// Test
		assertTrue(problem.isSatisfiable(assumps));
	}
}

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

示例3: runSatSolver

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
private int[] runSatSolver(Path path){
    ISolver solver = SolverFactory.newDefault();
    solver.setTimeout(TIMEOUT_MINUTES);
    Reader reader = new DimacsReader(solver);

    IProblem problem = null;
    try {
        problem = reader.parseInstance(path.toString());
        if (problem.isSatisfiable()) {
            return problem.model();
        } else {
            logger.error("Problem described in " + path.getFileName() + " is unsatisfiable");
        }
    } catch (ContradictionException | TimeoutException | ParseFormatException | IOException e) {
        logger.error("Error during SAT-solver processing", e);
    }
    return null;
}

开发者ID:Vapsel，项目名称:social-media-analytic-system，代码行数:19，代码来源:SATSolverManagerImpl.java

示例4: setUp

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Before
public void setUp() throws FileNotFoundException, ParseFormatException,
		IOException, ContradictionException {
	xplain = new Xplain<ISolver>(SolverFactory.newDefault());
	xplain.setTimeout(3600); // 1 hour timeout
	Reader reader = new DimacsReader(xplain);
	String dimacs = "src/test/testfiles/eb42.dimacs";
	reader.parseInstance(dimacs);
}

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

示例5: testReaderFromDimacsReader

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test
public void testReaderFromDimacsReader() throws ParseFormatException,
		ContradictionException, IOException, TimeoutException {
	String cnfString = "p cnf 3 4\n1 2 3 0\n-1 -2 0\n-1 -3 0\n-2 -3 0";
	DimacsReader reader = new DimacsReader(SolverFactory.newDefault());
	IProblem problem = reader.parseInstance(new ByteArrayInputStream(
			cnfString.getBytes()));
	assertNotNull(problem);
	assertTrue(problem.isSatisfiable());
}

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

示例6: testReaderFromLecteurDimacs

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test
public void testReaderFromLecteurDimacs() throws ParseFormatException,
		ContradictionException, IOException, TimeoutException {
	String cnfString = "p cnf 3 4\n1 2 3 0\n-1 -2 0\n-1 -3 0\n-2 -3 0";
	LecteurDimacs reader = new LecteurDimacs(SolverFactory.newDefault());
	IProblem problem = reader.parseInstance(new ByteArrayInputStream(
			cnfString.getBytes()));
	assertNotNull(problem);
	assertTrue(problem.isSatisfiable());
}

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

示例7: testReaderFromInstanceReader

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test(expected = UnsupportedOperationException.class)
public void testReaderFromInstanceReader() throws ParseFormatException,
		ContradictionException, IOException {
	String cnfString = "p cnf 3 4\n1 2 3 0\n-1 -2 0\n-1 -3 0\n-2 -3 0";
	InstanceReader reader = new InstanceReader(SolverFactory.newDefault());
	reader.parseInstance(new ByteArrayInputStream(cnfString.getBytes()));
	fail();
}

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

示例8: verifySatICPL_1

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test
public void verifySatICPL_1() throws IOException, ParseFormatException, ContradictionException, org.sat4j.specs.TimeoutException, CSVException{
	ISolver solver = SolverFactory.newDefault();
	Reader reader = new LecteurDimacs(solver);
	IProblem problem = reader.parseInstance("TestData/Realistic/ecos-icse11.dimacs");
	assertTrue(problem.isSatisfiable());
	
	CNF cnf = new CNF("TestData/Realistic/ecos-icse11.dimacs", CNF.type.dimacs);
	
	CoveringArray ca = new CoveringArrayFile("reports/bestcoverages/ecos-icse11-size66-1thread.dimacs.ca2.csv");
	for(int n = 0; n < ca.getRowCount(); n++){
		// Convert
		Integer[] solinteger = ca.getRow(n);
		int[] sol = new int[solinteger.length];
		for(int i = 0; i < sol.length; i++){
			//System.out.println(i+1 + ", " + ca.nrid.get(i+1));
			sol[i] = cnf.getNr(ca.getId(i+1));
			if(solinteger[i]==1) sol[i] = -sol[i];
		}
		IVecInt assumps = new VecInt(sol);
		//System.out.println(assumps);
		//System.out.println(n + ", " + assumps.size());
		
		// Test
		assertTrue(problem.isSatisfiable(assumps));
	}
}

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

示例9: testIterativeAssumptionCallsWithSet

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test
public void testIterativeAssumptionCallsWithSet()
		throws FileNotFoundException, ParseFormatException, IOException,
		ContradictionException, TimeoutException {
	ISolver satSolver = SolverFactory.newDefault();
	Reader reader = new LecteurDimacs(satSolver);
	IProblem p = reader.parseInstance("src/test/testfiles/Eshop-fm.dimacs");

	List<Integer> vars = new ArrayList<Integer>();
	for (int i = 1; i <= p.nVars(); i++) {
		vars.add(-i);
		vars.add(i);
	}

	Set<Integer> sol = new HashSet<Integer>();

	for (int i = 0; i < vars.size(); i++) {
		ISolver satSolverOracle = SolverFactory.newDefault();
		Reader readerOracle = new LecteurDimacs(satSolverOracle);
		readerOracle.parseInstance("src/test/testfiles/Eshop-fm.dimacs");

		int varnr = vars.get(i);

		int assumpsArray[] = new int[sol.size() + 1];
		int c = 0;
		for (int a : sol) {
			assumpsArray[c] = a;
			c++;
		}
		assumpsArray[assumpsArray.length - 1] = varnr;
		IVecInt assumps = new VecInt(assumpsArray);

		System.out.println(assumps);

		// Check
		if (satSolver.isSatisfiable(assumps)) {
			sol.add(varnr);
		} else {
			System.out.println("unsat: " + varnr);
		}

		assertEquals(satSolverOracle.isSatisfiable(assumps),
				satSolver.isSatisfiable(assumps));
	}
}

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

示例10: testIterativeAssumptionCallsWithList

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test
public void testIterativeAssumptionCallsWithList()
		throws FileNotFoundException, ParseFormatException, IOException,
		ContradictionException, TimeoutException {
	ISolver satSolver = SolverFactory.newDefault();
	Reader reader = new LecteurDimacs(satSolver);
	IProblem p = reader.parseInstance("src/test/testfiles/Eshop-fm.dimacs");

	List<Integer> vars = new ArrayList<Integer>();
	for (int i = 1; i <= p.nVars(); i++) {
		vars.add(-i);
		vars.add(i);
	}

	List<Integer> sol = new ArrayList<Integer>();

	for (int i = 0; i < vars.size(); i++) {
		ISolver satSolverOracle = SolverFactory.newDefault();
		Reader readerOracle = new LecteurDimacs(satSolverOracle);
		readerOracle.parseInstance("src/test/testfiles/Eshop-fm.dimacs");

		int varnr = vars.get(i);

		int assumpsArray[] = new int[sol.size() + 1];
		int c = 0;
		for (int a : sol) {
			assumpsArray[c] = a;
			c++;
		}
		assumpsArray[assumpsArray.length - 1] = varnr;
		IVecInt assumps = new VecInt(assumpsArray);

		System.out.println(assumps);

		// Check
		if (satSolver.isSatisfiable(assumps)) {
			sol.add(varnr);
		} else {
			System.out.println("unsat: " + varnr);
		}

		assertEquals(satSolverOracle.isSatisfiable(assumps),
				satSolver.isSatisfiable(assumps));
	}
}

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

示例11: testIterativeCorrectWay

import org.sat4j.reader.ParseFormatException; //导入依赖的package包/类
@Test
public void testIterativeCorrectWay() throws FileNotFoundException,
		ParseFormatException, IOException, ContradictionException,
		TimeoutException {
	ISolver satSolver = SolverFactory.newDefault();
	Reader reader = new LecteurDimacs(satSolver);
	IProblem p = reader.parseInstance("src/test/testfiles/Eshop-fm.dimacs");

	Set<Integer> sol = new HashSet<Integer>();

	for (int i = 1; i <= p.nVars(); i++) {
		ISolver satSolverOracle = SolverFactory.newDefault();
		Reader readerOracle = new LecteurDimacs(satSolverOracle);
		readerOracle.parseInstance("src/test/testfiles/Eshop-fm.dimacs");

		int assumpsArray[] = new int[sol.size() + 1];
		int c = 0;
		for (int a : sol) {
			assumpsArray[c] = a;
			c++;
		}
		assumpsArray[assumpsArray.length - 1] = -i;
		IVecInt assumps = new VecInt(assumpsArray);

		System.out.println(assumps);

		// Check
		assertEquals(satSolverOracle.isSatisfiable(assumps),
				satSolver.isSatisfiable(assumps));
		if (satSolver.isSatisfiable(assumps)) {
			sol.add(-i);
			continue;
		}
		assumpsArray[assumpsArray.length - 1] = i;
		System.out.println(assumps);
		satSolverOracle = SolverFactory.newDefault();
		readerOracle = new LecteurDimacs(satSolverOracle);
		readerOracle.parseInstance("src/test/testfiles/Eshop-fm.dimacs");
		assertEquals(satSolverOracle.isSatisfiable(assumps),
				satSolver.isSatisfiable(assumps));
		if (satSolver.isSatisfiable(assumps)) {
			sol.add(i);
		} else {
			System.out.println("unsat: " + i);
		}
	}
}

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