1 package org.sat4j;
2
3 import static org.junit.Assert.assertEquals;
4
5 import org.junit.Before;
6 import org.junit.Test;
7 import org.sat4j.core.VecInt;
8 import org.sat4j.minisat.SolverFactory;
9 import org.sat4j.specs.ContradictionException;
10 import org.sat4j.specs.ISolver;
11 import org.sat4j.specs.IVecInt;
12
13 public class TestFreeId {
14
15 private ISolver solver;
16
17 @Before
18 public void setUp() {
19 solver = SolverFactory.newDefault();
20 }
21
22 @Test
23 public void testEmptySolver() {
24 assertEquals(1,solver.nextFreeVarId(false));
25 solver.newVar(100);
26 assertEquals(101,solver.nextFreeVarId(false));
27 }
28
29 @Test
30 public void testIncrementalFeed() throws ContradictionException {
31 assertEquals(1,solver.nextFreeVarId(false));
32 IVecInt clause = new VecInt();
33 clause.push(3).push(-5);
34 solver.addClause(clause);
35 assertEquals(6,solver.nextFreeVarId(false));
36 clause.clear();
37 clause.push(1).push(-2);
38 solver.addClause(clause);
39 assertEquals(6,solver.nextFreeVarId(false));
40 clause.clear();
41 clause.push(1000).push(-31);
42 solver.addClause(clause);
43 assertEquals(1001,solver.nextFreeVarId(false));
44 }
45
46 @Test
47 public void testReserveParameter() {
48 assertEquals(1,solver.nextFreeVarId(false));
49 assertEquals(1,solver.nextFreeVarId(false));
50 assertEquals(1,solver.nextFreeVarId(false));
51 assertEquals(1,solver.nextFreeVarId(false));
52 assertEquals(1,solver.nextFreeVarId(true));
53 assertEquals(2,solver.nextFreeVarId(true));
54 assertEquals(3,solver.nextFreeVarId(false));
55 assertEquals(3,solver.nextFreeVarId(false));
56 }
57 }