• 设为首页
  • 点击收藏
  • 手机版
    手机扫一扫访问
    迪恩网络手机版
  • 关注官方公众号
    微信扫一扫关注
    迪恩网络公众号

Java Reader类代码示例

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

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



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

示例1: verifySatICPL_2

import org.sat4j.reader.Reader; //导入依赖的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.Reader; //导入依赖的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: solve

import org.sat4j.reader.Reader; //导入依赖的package包/类
public void solve(IProblem problem, Reader reader, ILogAble logger,
        PrintWriter out, long beginTime) {
    this.exitCode = ExitCode.UNKNOWN;
    this.out = out;
    this.nbSolutionFound = 0;
    this.beginTime = beginTime;
    try {
        if (problem.isSatisfiable()) {
            if (this.exitCode == ExitCode.UNKNOWN) {
                this.exitCode = ExitCode.SATISFIABLE;
            }
        } else {
            if (this.exitCode == ExitCode.UNKNOWN) {
                this.exitCode = ExitCode.UNSATISFIABLE;
            }
        }
    } catch (TimeoutException e) {
        logger.log("timeout");
    }

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


示例4: runSatSolver

import org.sat4j.reader.Reader; //导入依赖的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


示例5: createReader

import org.sat4j.reader.Reader; //导入依赖的package包/类
@Override
protected Reader createReader(ISolver theSolver, String problemname) {
	if (highLevel) {
		return new GroupedCNFReader((HighLevelXplain<ISolver>) theSolver);
	}
	return new LecteurDimacs(theSolver);
}
 
开发者ID:axel-halin,项目名称:Thesis-JHipster,代码行数:8,代码来源:MUSLauncher.java


示例6: setUp

import org.sat4j.reader.Reader; //导入依赖的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


示例7: verifySatICPL_1

import org.sat4j.reader.Reader; //导入依赖的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


示例8: createReader

import org.sat4j.reader.Reader; //导入依赖的package包/类
@Override
protected Reader createReader(ISolver theSolver, String problemname) {
    if (this.highLevel) {
        return new GroupedCNFReader(
                (GroupClauseSelectorSolver<ISolver>) theSolver);
    }
    return new LecteurDimacs(theSolver);
}
 
开发者ID:TakehideSoh,项目名称:Scarab,代码行数:9,代码来源:MUSLauncher.java


示例9: testIterativeAssumptionCallsWithSet

import org.sat4j.reader.Reader; //导入依赖的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);
        // Check
        if (satSolver.isSatisfiable(assumps)) {
            sol.add(varnr);
        }

        assertEquals(satSolverOracle.isSatisfiable(assumps),
                satSolver.isSatisfiable(assumps));
    }
}
 
开发者ID:TakehideSoh,项目名称:Scarab,代码行数:41,代码来源:TestSatAssumps.java


示例10: setUp

import org.sat4j.reader.Reader; //导入依赖的package包/类
@Before
public void setUp() throws FileNotFoundException, ParseFormatException,
        IOException, ContradictionException {
    this.xplain = new Xplain<ISolver>(SolverFactory.newDefault());
    this.xplain.setTimeout(3600); // 1 hour timeout
    Reader reader = new DimacsReader(this.xplain);
    String dimacs = "src/test/testfiles/eb42.dimacs";
    reader.parseInstance(dimacs);
}
 
开发者ID:TakehideSoh,项目名称:Scarab,代码行数:10,代码来源:BugSAT26.java


示例11: getDefaultOPBReader

import org.sat4j.reader.Reader; //导入依赖的package包/类
private Reader getDefaultOPBReader() {
    if (this.opb == null) {
        this.opb = new OPBReader2012(new PBSolverHandle(
                new PseudoOptDecorator(solver)));
    }
    return this.opb;
}
 
开发者ID:TakehideSoh,项目名称:Scarab,代码行数:8,代码来源:PBInstanceReader.java


示例12: handleFileName

import org.sat4j.reader.Reader; //导入依赖的package包/类
@Override
protected Reader handleFileName(String fname, String prefix) {
    if (fname.endsWith(".opb") || "PB".equals(prefix)) {
        return getDefaultOPBReader();
    }
    return super.handleFileName(fname, prefix);
}
 
开发者ID:TakehideSoh,项目名称:Scarab,代码行数:8,代码来源:PBInstanceReader.java


示例13: parseInstance

import org.sat4j.reader.Reader; //导入依赖的package包/类
@Override
public IProblem parseInstance(final java.io.Reader input)
        throws ParseFormatException, ContradictionException {
    IProblem problem = parseInstance(new LineNumberReader(input));
    this.solver.setObjectiveFunction(getObjectiveFunction());
    return problem;
}
 
开发者ID:TakehideSoh,项目名称:Scarab,代码行数:8,代码来源:OPBReader2005.java


示例14: testReserveVarsButUseLess

import org.sat4j.reader.Reader; //导入依赖的package包/类
@Test
public void testReserveVarsButUseLess() throws ContradictionException,
        TimeoutException, FileNotFoundException, ParseFormatException,
        IOException {
    IPBSolver solver = SolverFactory.newEclipseP2();
    Reader reader = new OPBEclipseReader2007(solver);
    reader.parseInstance(PREFIX + "bug247567.opb");
    assertTrue(solver.isSatisfiable());
    assertTrue(solver.model(1));
    assertTrue(solver.model(2));
    assertTrue(solver.model(3));
    assertFalse(solver.model(4));
    assertFalse(solver.model(5));
    assertFalse(solver.model(6));
}
 
开发者ID:TakehideSoh,项目名称:Scarab,代码行数:16,代码来源:TestEclipseBug247567.java


示例15: testReserveVarsButUseLess

import org.sat4j.reader.Reader; //导入依赖的package包/类
@Test
public void testReserveVarsButUseLess() throws ContradictionException,
        TimeoutException, FileNotFoundException, ParseFormatException,
        IOException {
    IPBSolver solver = SolverFactory.newEclipseP2();
    Reader reader = new OPBEclipseReader2007(solver);
    reader.parseInstance(PREFIX + "bug275101.opb");
    assertTrue(solver.isSatisfiable());
}
 
开发者ID:TakehideSoh,项目名称:Scarab,代码行数:10,代码来源:TestEclipseBug275101.java


示例16: createReader

import org.sat4j.reader.Reader; //导入依赖的package包/类
@Override
protected Reader createReader(ISolver theSolver, String problemname) {
	return new InstanceReader(theSolver);
}
 
开发者ID:axel-halin,项目名称:Thesis-JHipster,代码行数:5,代码来源:BasicLauncher.java


示例17: testIterativeAssumptionCallsWithSet

import org.sat4j.reader.Reader; //导入依赖的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


示例18: testIterativeAssumptionCallsWithList

import org.sat4j.reader.Reader; //导入依赖的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


示例19: testIterativeCorrectWay

import org.sat4j.reader.Reader; //导入依赖的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


示例20: createInstanceReader

import org.sat4j.reader.Reader; //导入依赖的package包/类
protected Reader createInstanceReader(T aSolver) {
	return new InstanceReader(aSolver);
}
 
开发者ID:axel-halin,项目名称:Thesis-JHipster,代码行数:4,代码来源:AbstractAcceptanceTestCase.java



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


鲜花

握手

雷人

路过

鸡蛋
该文章已有0人参与评论

请发表评论

全部评论

专题导读
上一篇:
Java ReaderCallback类代码示例发布时间:2022-05-22
下一篇:
Java Animation类代码示例发布时间:2022-05-22
热门推荐
阅读排行榜

扫描微信二维码

查看手机版网站

随时了解更新最新资讯

139-2527-9053

在线客服(服务时间 9:00~18:00)

在线QQ客服
地址:深圳市南山区西丽大学城创智工业园
电邮:jeky_zhao#qq.com
移动电话:139-2527-9053

Powered by 互联科技 X3.4© 2001-2213 极客世界.|Sitemap