1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20 package org.sat4j.pb;
21
22 import static org.junit.Assert.assertEquals;
23 import static org.junit.Assert.assertFalse;
24 import static org.junit.Assert.assertTrue;
25 import static org.sat4j.pb.tools.WeightedObject.newWO;
26
27 import java.util.ArrayList;
28 import java.util.Arrays;
29 import java.util.Iterator;
30 import java.util.List;
31 import java.util.Set;
32
33 import org.junit.Before;
34 import org.junit.Test;
35 import org.sat4j.pb.tools.DependencyHelper;
36 import org.sat4j.pb.tools.StringNegator;
37 import org.sat4j.pb.tools.WeightedObject;
38 import org.sat4j.specs.ContradictionException;
39 import org.sat4j.specs.IVec;
40 import org.sat4j.specs.TimeoutException;
41
42 public class TestDependencyHelper {
43 private static final String profile = "profile";
44 private static final String junit3 = "junit_3";
45 private static final String junit4 = "junit_4";
46
47 private DependencyHelper<String, String> helper;
48
49 @Before
50 public void setUp() {
51 helper = new DependencyHelper<String, String>(SolverFactory
52 .newEclipseP2());
53
54
55 }
56
57 @Test
58 public void testBasicRequirements() throws ContradictionException,
59 TimeoutException {
60 helper.implication("A").implies("B").and("C").and("D").named("I1");
61 helper.implication("B").impliesNot("C").named("I2");
62 helper.setTrue("A", "User selection");
63 assertFalse(helper.hasASolution());
64
65 Set<String> cause = helper.why();
66 assertEquals(3, cause.size());
67 Iterator<String> it = cause.iterator();
68 assertEquals("I1", it.next());
69 assertTrue(it.hasNext());
70 assertEquals("I2", it.next());
71 assertTrue(it.hasNext());
72 assertEquals("User selection", it.next());
73 }
74
75 @Test
76 public void testBasicRequirementsDetailedExplanation()
77 throws ContradictionException, TimeoutException {
78 helper.implication("A").implies("B").named("I1b");
79 helper.implication("A").implies("C").named("I1c");
80 helper.implication("A").implies("D").named("I1d");
81 helper.implication("B").impliesNot("C").named("I2");
82 helper.setTrue("A", "User selection");
83 assertFalse(helper.hasASolution());
84
85 Set<String> cause = helper.why();
86 assertEquals(4, cause.size());
87 Iterator<String> it = cause.iterator();
88 assertEquals("I1b", it.next());
89 assertEquals("I1c", it.next());
90 assertEquals("I2", it.next());
91 assertEquals("User selection", it.next());
92 }
93
94 @Test
95 public void testDisjunctions() throws ContradictionException,
96 TimeoutException {
97 helper.implication("A").implies("B").and("C").and("D").named("I1");
98 helper.implication("C").implies("C1", "C2", "C3").named("C versions");
99 helper.atMost(1, "C1", "C2", "C3").named("Singleton on C");
100 helper.setTrue("A", "User selection");
101 assertTrue(helper.hasASolution());
102 IVec<String> solution = helper.getSolution();
103 assertTrue(solution.contains("A"));
104 assertTrue(solution.contains("B"));
105 assertTrue(solution.contains("C"));
106 assertTrue(solution.contains("D"));
107 if (solution.contains("C1")) {
108 assertFalse(solution.contains("C2"));
109 assertFalse(solution.contains("C3"));
110 }
111 if (solution.contains("C2")) {
112 assertFalse(solution.contains("C1"));
113 assertFalse(solution.contains("C3"));
114 }
115 if (solution.contains("C3")) {
116 assertFalse(solution.contains("C1"));
117 assertFalse(solution.contains("C2"));
118 }
119 }
120
121 @Test
122 public void testDisjunctionExplanation() throws ContradictionException,
123 TimeoutException {
124 helper.implication("A").implies("B").and("C").and("D").named("I1");
125 helper.implication("B").impliesNot("C1").named("I2");
126 helper.implication("D").impliesNot("C2").named("I3");
127 helper.implication("C").implies("C1", "C2").named("C versions");
128 helper.atMost(1, "C1", "C2", "C3").named("Singleton on C");
129 helper.setTrue("A", "User selection");
130 assertFalse(helper.hasASolution());
131
132 Set<String> cause = helper.why();
133 assertEquals(5, cause.size());
134 Iterator<String> it = cause.iterator();
135 assertEquals("C versions", it.next());
136 assertEquals("I1", it.next());
137 assertEquals("I2", it.next());
138 assertEquals("I3", it.next());
139 assertEquals("User selection", it.next());
140 }
141
142 @Test
143 public void testExplanationForASolution() throws ContradictionException,
144 TimeoutException {
145 helper.implication("A").implies("B").and("C").and("D").named("I1");
146 helper.implication("C").implies("C1", "C2", "C3").named("C versions");
147 helper.atMost(1, "C1", "C2", "C3").named("Singleton on C");
148 helper.setTrue("A", "User selection");
149 assertTrue(helper.hasASolution());
150 IVec<String> solution = helper.getSolution();
151 assertTrue(solution.contains("A"));
152 assertTrue(solution.contains("B"));
153 assertTrue(solution.contains("C"));
154 assertTrue(solution.contains("D"));
155 Set<String> cause = helper.why("D");
156 assertEquals(2, cause.size());
157 Iterator<String> it = cause.iterator();
158 assertEquals("I1", it.next());
159 assertEquals("User selection", it.next());
160 }
161
162 @Test
163 public void testObjectiveFunction() throws ContradictionException,
164 TimeoutException {
165 helper.implication("A").implies("B").and("C").and("D").named("I1");
166 helper.implication("C").implies("C1", "C2", "C3").named("C versions");
167 helper.atMost(1, "C1", "C2", "C3").named("Singleton on C");
168 helper.setTrue("A", "User selection");
169 helper.setObjectiveFunction(newWO("C1", 4), newWO("C2", 2), newWO("C3",
170 1));
171 assertTrue(helper.hasASolution());
172 IVec<String> solution = helper.getSolution();
173 assertTrue(solution.contains("A"));
174 assertTrue(solution.contains("B"));
175 assertTrue(solution.contains("C"));
176 assertTrue(solution.contains("C3"));
177 assertFalse(solution.contains("C2"));
178 assertFalse(solution.contains("C1"));
179 assertTrue(solution.contains("D"));
180 }
181
182 @Test
183 public void testJunitExample() throws ContradictionException,
184 TimeoutException {
185 helper.implication(profile).implies(junit3).named("profile->junit_3");
186 helper.implication(profile).implies(junit4).named("profile->junit_4");
187 helper.setObjectiveFunction(WeightedObject.newWO(junit4, 1),
188 WeightedObject.newWO(junit3, 2));
189 helper.setTrue(profile, "profile must exist");
190 assertTrue(helper.hasASolution());
191 List<String> expected = new ArrayList<String>(Arrays.asList(profile,
192 junit3, junit4));
193 IVec<String> solution = helper.getSolution();
194 for (Iterator<String> i = solution.iterator(); i.hasNext();) {
195 String variable = i.next();
196 assertTrue(variable + " was not part of the solution", expected
197 .remove(variable));
198 }
199 assertTrue("solution contained too many variables: " + expected,
200 expected.isEmpty());
201 }
202
203 @Test
204 public void testJunitSingletonObjectiveExample()
205 throws ContradictionException, TimeoutException {
206 helper.implication(profile).implies(junit3, junit4).named(
207 "profile->junit");
208 helper.atMost(1, junit4, junit3);
209 helper.setObjectiveFunction(WeightedObject.newWO(junit4, 1),
210 WeightedObject.newWO(junit3, 2));
211 helper.setTrue(profile, "profile must exist");
212 assertTrue(helper.hasASolution());
213 List<String> expected = new ArrayList<String>(Arrays.asList(profile,
214 junit4));
215 IVec<String> solution = helper.getSolution();
216 for (Iterator<String> i = solution.iterator(); i.hasNext();) {
217 String variable = i.next();
218 assertTrue(variable + " was not part of the solution", expected
219 .remove(variable));
220 }
221 assertTrue("solution contained too many variables: " + expected,
222 expected.isEmpty());
223 }
224
225 @Test
226 public void testEquivalency() throws ContradictionException,
227 TimeoutException {
228 helper.implication("A").implies("B").named("C1");
229 helper.iff("C2", "B", "C");
230 helper.setTrue("A", "C3");
231 assertTrue(helper.hasASolution());
232 helper.setFalse("C", "C4");
233 assertFalse(helper.hasASolution());
234 }
235
236 @Test
237 public void testDisjunction() throws ContradictionException,
238 TimeoutException {
239
240 helper.disjunction("A", "B").implies("C", "D").named("C1");
241
242 helper.implication().implies("A", "B").named("C2");
243 helper.setFalse("C", "C3");
244 assertTrue(helper.hasASolution());
245 helper.setFalse("D", "C4");
246 assertFalse(helper.hasASolution());
247
248 }
249
250 @Test
251 public void testCathyExamples() throws ContradictionException,
252 TimeoutException {
253 helper.setNegator(StringNegator.instance);
254
255 helper.and("C1", "A", "B", "C", "D");
256
257 helper.implication("-A", "B").implies("E").named("C2");
258 helper.setFalse("D", "InitState");
259 helper.setTrue("B", "InitState");
260 helper.setFalse("E", "InitState");
261 helper.atMost(1, "A", "B", "C", "D", "E").named("C5");
262 assertFalse(helper.hasASolution());
263 assertEquals(3, helper.why().size());
264 }
265 }