|Re: [p2-dev] Planner explanation question|
|What is returned by the slicer is not an explanation, but just a "bunch of notes" collected along the way as it was slicing. The information collected is very vague and here is an example why. I have the following IUs|
A requires B [0, 3.0)
B-1 requires C
B-1.1 requires E
B-2 requires D
When the slicer is slicing for A, it will include B-1, B-1.1 and B-2 in the slice. Now when it slices B-1 it will fail at finding a C and will create a log. Same will go for B-1.1 with E. When it comes to B-2 it will find D. In this case, the resolution of A will have a solution. Now if I take B-2 out of the set of available IUs, then the slicer will return 2 warnings but really only one of those warnings would have to be "fixed" for a solution to be found. Of course this is a small example, if you follow all the possibilities of all the versions you can get a lot of noise from which it may be hard for you to figure out what is really missing.
Computing an explanation is done by the core SAT solver and will sort through the noise to figure out something that you can act upon.
I will let Daniel explain if more can actually be done.
I have released the test you provided, but it is not enabled as part of the global test suite.
On 2011-05-12, at 2:45 PM, Todorova, Katya wrote: