XplainTests xref

View Javadoc

1   package org.sat4j.pb;
2   
3   import java.util.List;
4   import java.util.Set;
5   
6   import org.junit.Before;
7   import org.junit.Test;
8   import static org.junit.Assert.*;
9   import org.sat4j.pb.SolverFactory;
10  import org.sat4j.pb.tools.DependencyHelper;
11  import org.sat4j.specs.ContradictionException;
12  import org.sat4j.specs.TimeoutException;
13  
14  import static org.sat4j.pb.tools.WeightedObject.newWO;
15  
16  public class XplainTests {
17  	private static final int EXTRA_IMPLICATIONS_PER_LEVEL = 10;
18  	private DependencyHelper<String, String> helper;
19  
20  	@Before
21  	public void setUp() {
22  		// TODO: We would like to use SolverFactory.newEclipseP2();
23  		// currently this throws a class cast exception in the DependencyHelper
24  		// DLB: FIXED
25  		helper = new DependencyHelper<String, String>(SolverFactory.newEclipseP2());
26  	}
27  
28  	@Test(timeout = 10000)
29  	public void testRequiredSoftwareDependsOnOlderVersion() throws ContradictionException, TimeoutException {
30  		helper.setTrue("profile", "profile must exist");
31  		helper.implication("profile").implies("a_1").named("profile->a_1");
32  		addExtraImplications("profile");
33  		helper.implication("a_1").implies("b_1").named("a_1->b_1");
34  		addExtraImplications("a_1");
35  		helper.implication("b_1").implies("c_[2,3)").named("b_1->c_[2,3)");
36  		addExtraImplications("b_1");
37  		helper.implication("c_[2,3)").implies("p(c_[2,3))").named("c_[2,3) does not exist");
38  		helper.setFalse("p(c_[2,3))", "placeholder(c_[2,3))");
39  
40  		Explanation<String> explanation = new Explanation<String>();
41  		explanation.newFalseRoot("profile must exist").newChild("profile->a_1").newChild("a_1->b_1").newChild("b_1->c_[2,3)").newChild("c_[2,3) does not exist")
42  				.newChild("placeholder(c_[2,3))");
43  		checkExplanationForMissingRequirement(explanation);
44  	}
45  
46  	@Test(timeout = 10000)
47  	public void testRequiredSoftwareDependsOnOlderVersionDeepTree() throws ContradictionException, TimeoutException {
48  		helper.setTrue("profile", "profile must exist");
49  		helper.implication("profile").implies("a_1").named("profile->a_1");
50  		addExtraImplications("profile");
51  
52  		Explanation<String> explanation = new Explanation<String>();
53  		DepdendenyNode<String> node = explanation.newFalseRoot("profile must exist").newChild("profile->a_1");
54  
55  		String lastThing = "a_1";
56  		for(int i = 0 ; i < 10; i++) {
57  			String newThing = "newThing" + i;
58  			String name = lastThing+"->" + newThing;
59  			helper.implication(lastThing).implies(newThing).named(name);
60  			node = node.newChild(name);
61  			addExtraImplications(lastThing);
62  			lastThing = newThing;
63  		}
64  		helper.implication(lastThing).implies("c_[2,3)").named("b_1->c_[2,3)");
65  		node = node.newChild("b_1->c_[2,3)");
66  		addExtraImplications(lastThing);
67  		helper.implication("c_[2,3)").implies("p(c_[2,3))").named("c_[2,3) does not exist");
68  		node = node.newChild("c_[2,3) does not exist");
69  		helper.setFalse("p(c_[2,3))", "placeholder(c_[2,3))");
70  		node = node.newChild("placeholder(c_[2,3))");
71  
72  		checkExplanationForMissingRequirement(explanation);
73  	}
74  
75  	// Currently expected to fail, need weighting rules on a_1, a_2, b_1, and
76  	// b_2
77  	@Test(timeout = 10000)
78  	public void testUseWeightToOrderSolutions() throws ContradictionException, TimeoutException {
79  		helper.setTrue("profile", "profile must exist");
80  		helper.implication("profile").implies("a_1").named("profile->a_1");
81  		helper.implication("profile").implies("a_2").named("profile->a_2");
82  		addExtraImplications("profile");
83  		helper.implication("a_1").implies("b_1").named("a_1->b_1");
84  		helper.implication("a_1").implies("b_2").named("a_1->b_2");
85  		addExtraImplications("a_1");
86  		helper.implication("a_2").implies("b_1").named("a_2->b_1");
87  		helper.implication("a_2").implies("b_2").named("a_2->b_2");
88  		addExtraImplications("a_2");
89  		helper.implication("b_1").implies("c_[2,3)").named("b_1->c_[2,3)");
90  		addExtraImplications("b_1");
91  		helper.implication("b_2").implies("c_[2,3)").named("b_2->c_[2,3)");
92  		addExtraImplications("b_2");
93  
94  		// Need some way to weight a_2 > a_1 & b_2 > b_1
95  		helper.setObjectiveFunction(newWO("a_1",2),newWO("a_2",1),newWO("b_1",8),newWO("b_2",4));
96  		helper.implication("c_[2,3)").implies("p(c_[2,3))").named("c_[2,3) does not exist");
97  		helper.setFalse("p(c_[2,3))", "placeholder(c_[2,3))");
98  
99  		Explanation<String> explanation = new Explanation<String>();
100 		explanation.newFalseRoot("profile must exist").newChild("profile->a_2").newChild("a_2->b_2").newChild("b_2->c_[2,3)").newChild("c_[2,3) does not exist")
101 				.newChild("placeholder(c_[2,3))");
102 		checkExplanationForMissingRequirement(explanation);
103 	}
104 
105 	@Test(timeout = 10000)
106 	public void testUseNumberOfMissingVariablesToOrderExplanations() throws ContradictionException, TimeoutException {
107 		helper.setTrue("profile", "profile must exist");
108 		helper.implication("profile").implies("a_1").named("profile->a_1");
109 		helper.implication("profile").implies("a_2").named("profile->a_2");
110 		addExtraImplications("profile");
111 		helper.implication("a_1").implies("b_1").named("a_1->b_1");
112 		addExtraImplications("a_1");
113 		helper.implication("a_2").implies("b_1").named("a_2->b_1");
114 		helper.implication("a_2").implies("d").named("a_2->d");
115 		addExtraImplications("a_2");
116 		helper.implication("b_1").implies("c_[2,3)").named("b_1->c_[2,3)");
117 		addExtraImplications("b_1");
118 
119 		// Need some way to weight a_2 > a_1 & b_2 > b_1
120 		helper.setObjectiveFunction(newWO("a_1",2),newWO("a_2",1),newWO("b_1",8),newWO("b_2",4));
121 		helper.implication("c_[2,3)").implies("p(c_[2,3))").named("c_[2,3) does not exist");
122 		helper.setFalse("p(c_[2,3))", "placeholder(c_[2,3))");
123 		helper.implication("d").implies("p(d)").named("d does not exist");
124 		helper.setFalse("p(d)", "placeholder(d)");
125 
126 		Explanation<String> explanation = new Explanation<String>();
127 		explanation.newFalseRoot("profile must exist").newChild("profile->a_1").newChild("a_1->b_1").newChild("b_1->c_[2,3)").newChild("c_[2,3) does not exist")
128 				.newChild("placeholder(c_[2,3))");
129 		checkExplanationForMissingRequirement(explanation);
130 	}
131 
132 	// Expected to fail, need some way to weight a_2 > a_1 & b_2 > b_1
133 	@Test(timeout = 10000)
134 	public void testUseNumberOfMissingVariablesAndWeightToOrderExplanations() throws ContradictionException, TimeoutException {
135 		helper.setTrue("profile", "profile must exist");
136 		helper.implication("profile").implies("a_1").named("profile->a_1");
137 		helper.implication("profile").implies("a_2").named("profile->a_2");
138 		addExtraImplications("profile");
139 		helper.implication("a_1").implies("b_1").named("a_1->b_1");
140 		helper.implication("a_1").implies("b_2").named("a_1->b_2");
141 		addExtraImplications("a_1");
142 		helper.implication("a_2").implies("b_1").named("a_2->b_1");
143 		helper.implication("a_2").implies("b_2").named("a_2->b_2");
144 		helper.implication("a_2").implies("d").named("a_2->d");
145 		addExtraImplications("a_2");
146 		helper.implication("b_1").implies("c_[2,3)").named("b_1->c_[2,3)");
147 		addExtraImplications("b_1");
148 		helper.implication("b_2").implies("c_[2,3)").named("b_2->c_[2,3)");
149 		addExtraImplications("b_2");
150 
151 		// Need some way to weight a_2 > a_1 & b_2 > b_1
152 		helper.setObjectiveFunction(newWO("a_1",2),newWO("a_2",1),newWO("b_1",8),newWO("b_2",4));
153 		helper.implication("c_[2,3)").implies("p(c_[2,3))").named("c_[2,3) does not exist");
154 		helper.setFalse("p(c_[2,3))", "placeholder(c_[2,3))");
155 		helper.implication("d").implies("p(d)").named("d does not exist");
156 		helper.setFalse("p(d)", "placeholder(d)");
157 
158 		Explanation<String> explanation = new Explanation<String>();
159 		explanation.newFalseRoot("profile must exist").newChild("profile->a_1").newChild("a_1->b_2").newChild("b_2->c_[2,3)").newChild("c_[2,3) does not exist")
160 				.newChild("placeholder(c_[2,3))");
161 		checkExplanationForMissingRequirement(explanation);
162 	}
163 	
164 	@Test
165 	public void testConflictingRequirements() throws ContradictionException, TimeoutException {
166 		helper.setTrue("profile", "profile must exist");
167 		helper.implication("profile").implies("a_1").named("profile->a_1");
168 		helper.implication("profile").implies("b_1").named("profile->b_1");
169 		addExtraImplications("profile");
170 		helper.implication("a_1").implies("c_1").named("a_1->c_1");
171 		addExtraImplications("a_1");
172 		helper.implication("b_1").implies("d_1").named("b_1->d_1");
173 		addExtraImplications("b_1");
174 		helper.implication("c_1").implies("d_2").named("c_1->d_2");
175 		addExtraImplications("c_1");
176 		helper.setTrue("d_1", "d_1 exists");
177 		helper.setTrue("d_2", "d_2 exists");
178 		helper.atMost(1, "d_1", "d_2").named("singleton on d");
179 
180 		Explanation<String> explanation = new Explanation<String>();
181 		Conflict<String> conflict = explanation.newConflict();
182 		conflict.newRoot("profile must exist").newChild("profile->a_1").newChild("a_1->c_1").newChild("c_1->d_2");
183 		conflict.newRoot("profile must exist").newChild("profile->b_1").newChild("b_1->d_1");
184 		checkExplanationForConflict(explanation);
185 	}
186 	
187 	private void checkExplanationForConflict(Explanation<String> explanation) throws TimeoutException {
188 		assertFalse(helper.hasASolution());
189 		
190 		// TODO: would like all conflicting elements
191 		// This throws an ArrayIndexOutOfBounds
192 		// DLB: this is a real bug. I still need to work on that issue :(
193 		// String conflictingElement = helper.getConflictingElement();
194 		
195 		List<Conflict<String>> conflicts = explanation.getConflicts();
196 		
197 		// TODO: why throws an NPE
198 		// DLB: fixed.
199 		Set<String> cause = helper.why();
200 
201 		// TODO: Change this logic to actually use the tree of dependencies
202 		for (Conflict<String> conflict : conflicts) {
203 			List<DepdendenyNode<String>> roots = conflict.getRoots();
204 			for (DepdendenyNode<String> node : roots) {
205 				while(node != null) {
206 					assertTrue("Could not find " + node.getName(), cause.remove(node.getName()));
207 					node = node.getOnlyChild();
208 				}
209 			}
210 		}
211 		assertTrue(cause.isEmpty());
212 	}
213 
214 	private void checkExplanationForMissingRequirement(Explanation<String> explanation) throws TimeoutException {
215 		assertFalse(helper.hasASolution());
216 
217 		Set<String> cause = helper.why();
218 		List<DepdendenyNode<String>> roots = explanation.getRoots();
219 		assertEquals(1, roots.size());
220 
221 		// TODO: Fix this logic to actually investigate the tree returned
222 		DepdendenyNode<String> root = roots.get(0);
223 		assertFalse(root.hasBranches());
224 		assertEquals(root.getMaxDepth(), cause.size());
225 
226 		DepdendenyNode<String> node = root;
227 		while (node != null) {
228 			assertTrue("Could not find " + node.getName() + " in " + cause, cause.contains(node.getName()));
229 			node = node.getOnlyChild();
230 		}
231 	}
232 
233 	/**
234 	 * Creates extra rules for the given dependent. This allows us to prove that
235 	 * the explanation doesn't contain unnecessary rules.
236 	 * 
237 	 * @param variable
238 	 *            the variable that will have extra implications added to it
239 	 * @throws ContradictionException
240 	 */
241 	private void addExtraImplications(String variable) throws ContradictionException {
242 		for (int i = 0; i < EXTRA_IMPLICATIONS_PER_LEVEL; i++) {
243 			String newVariable = variable + "Extra" + i;
244 			helper.setTrue(newVariable, newVariable + " exists");
245 			helper.implication(variable).implies(newVariable).named(variable + "->" + newVariable);
246 		}
247 	}
248 }