本文整理汇总了Java中org.sat4j.specs.IVecInt类的典型用法代码示例。如果您正苦于以下问题：Java IVecInt类的具体用法？Java IVecInt怎么用？Java IVecInt使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
IVecInt类属于org.sat4j.specs包，在下文中一共展示了IVecInt类的20个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的Java代码示例。
示例1: testWithMin
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
@Test
public void testWithMin() throws ContradictionException {
IPBSolver solver = new OPBStringSolver();
solver.newVar(3);
IVecInt clause = new VecInt();
clause.push(1).push(2).push(3);
solver.addClause(clause);
IVecInt vars = new VecInt();
vars.push(2).push(3);
IVec<BigInteger> coeffs = new Vec<BigInteger>();
coeffs.push(BigInteger.TEN).push(BigInteger.valueOf(32));
ObjectiveFunction obj = new ObjectiveFunction(vars, coeffs);
solver.setObjectiveFunction(obj);
assertEquals(STRING2, solver.toString());
}
开发者ID:Vapsel，项目名称:social-media-analytic-system，代码行数:17，代码来源:PbmOPBStringSolver.java
示例2: addClause
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
@Override
public IConstr addClause(IVecInt literals) throws ContradictionException {
if (literals.equals(lastClause)) {
// System.err.println("c Duplicated entry: " + literals);
return null;
}
lastClause.clear();
literals.copyTo(lastClause);
int newvar = createNewVar(literals);
literals.push(newvar);
lastConstr = super.addClause(literals);
if (lastConstr == null) {
discardLastestVar();
} else {
constrs.put(newvar, lastConstr);
}
return lastConstr;
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:19，代码来源:Xplain.java
示例3: testHasASingleSolutionIVecInt
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
public void testHasASingleSolutionIVecInt() throws ContradictionException,
TimeoutException {
IVecInt clause = new VecInt();
clause.push(1).push(2);
detector.addClause(clause);
IVecInt assumptions = new VecInt();
assumptions.push(1);
assertTrue(detector.isSatisfiable(assumptions));
assertFalse(detector.hasASingleSolution(assumptions));
clause.clear();
clause.push(-1).push(2);
detector.addClause(clause);
assertTrue(detector.isSatisfiable(assumptions));
assertTrue(detector.hasASingleSolution(assumptions));
clause.clear();
clause.push(-1).push(-2);
detector.addClause(clause);
assertFalse(detector.isSatisfiable(assumptions));
try {
assertFalse(detector.hasASingleSolution(assumptions));
fail();
} catch (UnsupportedOperationException e) {
// OK
}
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:26，代码来源:SingleSolutionTest.java
示例4: testEclipseTestCase2
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
@Test
public void testEclipseTestCase2() throws ContradictionException,
TimeoutException {
solver.newVar(4);
IVecInt clause = new VecInt();
clause.push(-1).push(2);
solver.addClause(clause);
clause.clear();
clause.push(-1).push(3);
solver.addClause(clause);
clause.clear();
clause.push(-2).push(-3);
solver.addClause(clause);
clause.clear();
clause.push(-4).push(1);
solver.addClause(clause);
clause.clear();
IVecInt assump = new VecInt();
assump.push(4);
assertFalse(solver.isSatisfiable(assump));
Collection<IConstr> explanation = solver.explain();
assertEquals(4, explanation.size());
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:24，代码来源:AbstractXplainTest.java
示例5: test4Unsat
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
public void test4Unsat() throws TimeoutException {
try {
solver.reset();
// 2 variables
solver.newVar(2);
// premi?re contrainte de cardinalit?
// a + not b >=3
IVecInt vecLit = new VecInt();
vecLit.push(1);
vecLit.push(-2);
solver.addAtLeast(vecLit, 3);
solver.isSatisfiable();
fail();
} catch (ContradictionException e) {
}
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:20，代码来源:TestAtMost.java
示例6: test5Sat
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
public void test5Sat() throws TimeoutException {
try {
solver.reset();
// 2 variables
solver.newVar(2);
// premi\x{FFFD}re contrainte de cardinalit\x{FFFD}
// a + not b <=0
IVecInt vecLit = new VecInt();
vecLit.push(1);
vecLit.push(-2);
solver.addAtMost(vecLit, 0);
boolean isSat = solver.isSatisfiable();
assertTrue(isSat);
} catch (ContradictionException e) {
assertTrue(false);
}
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:21，代码来源:TestAtMost.java
示例7: testTrivialUnsat
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
public void testTrivialUnsat() {
solver.newVar(1);
IVecInt vec = new VecInt();
vec.push(1);
try {
solver.addClause(vec);
} catch (ContradictionException e) {
fail();
}
vec.clear();
vec.push(-1);
try {
solver.addClause(vec);
fail();
} catch (ContradictionException e1) {
}
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:18，代码来源:TestsFonctionnels.java
示例8: simpleSimplification
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
private void simpleSimplification(IVecInt conflictToReduce) {
int i, j;
final boolean[] seen = mseen;
for (i = j = 1; i < conflictToReduce.size(); i++) {
IConstr r = voc.getReason(conflictToReduce.get(i));
if (r == null) {
conflictToReduce.moveTo(j++, i);
} else {
for (int k = 0; k < r.size(); k++)
if (voc.isFalsified(r.get(k)) && !seen[r.get(k) >> 1]
&& (voc.getLevel(r.get(k)) != 0)) {
conflictToReduce.moveTo(j++, i);
break;
}
}
}
conflictToReduce.shrink(i - j);
stats.reducedliterals += (i - j);
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:20，代码来源:Solver.java
示例9: verifySatICPL_2
import org.sat4j.specs.IVecInt; //导入依赖的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
示例10: checkTheExpectedWayToDealWithUnitClausesToRemove
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
@Test
public void checkTheExpectedWayToDealWithUnitClausesToRemove() throws ContradictionException, TimeoutException {
ISolver solver = SolverFactory.newDefault();
ConstrGroup g1 = new ConstrGroup();
IVecInt clause = new VecInt(new int[] { 1 });
solver.addClause(clause);
// starting group
clause.clear();
clause.push(2).push(-3);
g1.add(solver.addClause(clause));
clause.clear();
clause.push(-2).push(4);
g1.add(solver.addClause(clause));
IVecInt unitClauses = new VecInt(new int[] {3,-4});
assertFalse(solver.isSatisfiable(unitClauses));
g1.removeFrom(solver);
assertTrue(solver.isSatisfiable(unitClauses));
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:25，代码来源:TestConstrGroup.java
示例11: testGlobalInconsistency
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
@Test
public void testGlobalInconsistency() throws ContradictionException,
TimeoutException {
solver.newVar(2);
IVecInt clause = new VecInt();
clause.push(1).push(2);
solver.addClause(clause);
clause.clear();
clause.push(1).push(-2);
solver.addClause(clause);
clause.clear();
clause.push(-1).push(2);
solver.addClause(clause);
clause.clear();
clause.push(-1).push(-2);
solver.addClause(clause);
clause.clear();
assertFalse(solver.isSatisfiable());
Collection<IConstr> explanation = solver.explain();
assertEquals(4, explanation.size());
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:22，代码来源:AbstractXplainTest.java
示例12: testIncrementalFeed
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
@Test
public void testIncrementalFeed() throws ContradictionException {
assertEquals(1,solver.nextFreeVarId(false));
IVecInt clause = new VecInt();
clause.push(3).push(-5);
solver.addClause(clause);
assertEquals(6,solver.nextFreeVarId(false));
clause.clear();
clause.push(1).push(-2);
solver.addClause(clause);
assertEquals(6,solver.nextFreeVarId(false));
clause.clear();
clause.push(1000).push(-31);
solver.addClause(clause);
assertEquals(1001,solver.nextFreeVarId(false));
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:17，代码来源:TestFreeId.java
示例13: and
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
/**
* Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
*
* @param y
* @param literals
* the x1 ... xn literals.
* @throws ContradictionException
* @since 2.1
*/
public IConstr[] and(int y, IVecInt literals) throws ContradictionException {
// y <=> AND x1 ... xn
IConstr[] constrs = new IConstr[literals.size() + 1];
// y <= x1 .. xn
IVecInt clause = new VecInt(literals.size() + 2);
clause.push(y);
for (int i = 0; i < literals.size(); i++) {
clause.push(-literals.get(i));
}
constrs[0] = processClause(clause);
clause.clear();
for (int i = 0; i < literals.size(); i++) {
// y => xi
clause.clear();
clause.push(-y);
clause.push(literals.get(i));
constrs[i + 1] = processClause(clause);
}
return constrs;
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:30，代码来源:GateTranslator.java
示例14: or
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
/**
* translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
*
* @param y
* @param literals
* @throws ContradictionException
* @since 2.1
*/
public IConstr[] or(int y, IVecInt literals) throws ContradictionException {
// y <=> OR x1 x2 ...xn
// y => x1 x2 ... xn
IConstr[] constrs = new IConstr[literals.size() + 1];
IVecInt clause = new VecInt(literals.size() + 2);
literals.copyTo(clause);
clause.push(-y);
constrs[0] = processClause(clause);
clause.clear();
for (int i = 0; i < literals.size(); i++) {
// xi => y
clause.clear();
clause.push(y);
clause.push(-literals.get(i));
constrs[i + 1] = processClause(clause);
}
return constrs;
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:27，代码来源:GateTranslator.java
示例15: xor2Clause
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
private void xor2Clause(int[] f, int prefix, boolean negation,
IVec<IConstr> constrs) throws ContradictionException {
if (prefix == f.length - 1) {
IVecInt clause = new VecInt(f.length + 1);
for (int i = 0; i < f.length - 1; ++i) {
clause.push(f[i]);
}
clause.push(f[f.length - 1] * (negation ? -1 : 1));
constrs.push(processClause(clause));
return;
}
if (negation) {
f[prefix] = -f[prefix];
xor2Clause(f, prefix + 1, false, constrs);
f[prefix] = -f[prefix];
xor2Clause(f, prefix + 1, true, constrs);
} else {
xor2Clause(f, prefix + 1, false, constrs);
f[prefix] = -f[prefix];
xor2Clause(f, prefix + 1, true, constrs);
f[prefix] = -f[prefix];
}
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:27，代码来源:GateTranslator.java
示例16: copyTo
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
public void copyTo(IVecInt arg0) {
int argLength = arg0.size();
final int[] workArray = vec; // faster access
arg0.ensure(argLength + workArray.length);
for (int i : workArray) {
arg0.set(argLength++, i);
}
}
开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:9，代码来源:SAT4J.java
示例17: testNoMin
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
@Test
public void testNoMin() throws ContradictionException {
IPBSolver solver = new OPBStringSolver();
solver.newVar(3);
IVecInt clause = new VecInt();
clause.push(1).push(2).push(3);
solver.addClause(clause);
assertEquals(STRING1, solver.toString());
}
开发者ID:Vapsel，项目名称:social-media-analytic-system，代码行数:10，代码来源:PbmOPBStringSolver.java
示例18: copyTo
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
public void copyTo(IVecInt arg0) {
int argLength = arg0.size();
arg0.ensure(argLength + vec.length);
for(int i : vec) {
arg0.set(argLength++, i);
}
}
开发者ID:ModelWriter，项目名称:Tarski，代码行数:8，代码来源:SAT4J.java
示例19: tearDDown
import org.sat4j.specs.IVecInt; //导入依赖的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
示例20: atLeastNew
import org.sat4j.specs.IVecInt; //导入依赖的package包/类
/**
* @since 2.1
*/
public static Constr atLeastNew(UnitPropagationListener s, ILits voc,
IVecInt ps, int n) throws ContradictionException {
int degree = niceParameters(s, voc, ps, n);
if (degree == 0)
return new UnitClauses(ps);
return new AtLeast(voc, ps, degree);
}
开发者ID:axel-halin，项目名称:Thesis-JHipster，代码行数:11，代码来源:AtLeast.java
注：本文中的org.sat4j.specs.IVecInt类示例整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。 |
客服电话
APP下载
官方微信
请发表评论