1 package org.sat4j.minisat.core;
2
3 import static org.junit.Assert.assertEquals;
4 import static org.junit.Assert.assertFalse;
5 import static org.junit.Assert.assertTrue;
6
7 import org.junit.Test;
8 import org.sat4j.core.VecInt;
9 import org.sat4j.minisat.SolverFactory;
10 import org.sat4j.opt.MaxSatDecorator;
11 import org.sat4j.specs.ContradictionException;
12 import org.sat4j.specs.ISolver;
13 import org.sat4j.specs.IVecInt;
14 import org.sat4j.specs.TimeoutException;
15 import org.sat4j.tools.ModelIterator;
16 import org.sat4j.tools.OptToSatAdapter;
17
18 public class Bug275101 {
19
20 @Test
21 public void testMaxSAtIteratorIfSat() throws ContradictionException,
22 TimeoutException {
23 ISolver solver = new ModelIterator(new OptToSatAdapter(
24 new MaxSatDecorator(SolverFactory.newDefault())));
25 solver.newVar(3);
26 IVecInt literals = new VecInt();
27 literals.push(-1).push(-2).push(3);
28 solver.addClause(literals);
29 literals.clear();
30 literals.push(-1).push(2);
31 solver.addClause(literals);
32 literals.clear();
33 literals.push(-1).push(-3);
34 solver.addClause(literals);
35 literals.clear();
36 assertTrue(solver.isSatisfiable());
37 assertEquals(3, solver.model().length);
38 System.out.println("" + solver.model(1) + solver.model(2)
39 + solver.model(3));
40 assertTrue(solver.isSatisfiable());
41 assertEquals(3, solver.model().length);
42 System.out.println("" + solver.model(1) + solver.model(2)
43 + solver.model(3));
44 assertTrue(solver.isSatisfiable());
45 assertEquals(3, solver.model().length);
46 System.out.println("" + solver.model(1) + solver.model(2)
47 + solver.model(3));
48 assertTrue(solver.isSatisfiable());
49 assertEquals(3, solver.model().length);
50 System.out.println("" + solver.model(1) + solver.model(2)
51 + solver.model(3));
52 assertFalse(solver.isSatisfiable());
53 }
54
55 @Test
56 public void testMaxSAtIterator() throws ContradictionException,
57 TimeoutException {
58 ISolver solver = new ModelIterator(new OptToSatAdapter(
59 new MaxSatDecorator(SolverFactory.newDefault())));
60 solver.newVar(2);
61 IVecInt literals = new VecInt();
62 literals.push(-1).push(-2);
63 solver.addClause(literals);
64 literals.clear();
65 literals.push(-1).push(2);
66 solver.addClause(literals);
67 literals.clear();
68 literals.push(1).push(-2);
69 solver.addClause(literals);
70 literals.clear();
71 literals.push(1).push(2);
72 solver.addClause(literals);
73 assertTrue(solver.isSatisfiable());
74 assertEquals(2, solver.model().length);
75 System.out.println("" + solver.model(1) + solver.model(2));
76 assertTrue(solver.isSatisfiable());
77 assertEquals(2, solver.model().length);
78 System.out.println("" + solver.model(1) + solver.model(2));
79 assertTrue(solver.isSatisfiable());
80 assertEquals(2, solver.model().length);
81 System.out.println("" + solver.model(1) + solver.model(2));
82 assertTrue(solver.isSatisfiable());
83 assertEquals(2, solver.model().length);
84 System.out.println("" + solver.model(1) + solver.model(2));
85 assertFalse(solver.isSatisfiable());
86 }
87 }