-
Sylvain Dailler authored
The idea is to change the pairing so that it is better when only axioms change. In the extreme case, the goal is unchanged. The first idea is to add a separator when printing the shape so that goal and hypothesis are separated. When pairing shape, the first sorting is done only on goals. Then, we try to add to the PQ all the elements that have the same goal shape. I say that some goals that are very close would not be directly next to each other with the current algorithm: we give them a chance to evaluate their measure (lcp) before elements are withdrawn. Then, we also tried to change lcp in case the goal is slightly changed but an hypothesis is changed too. If the goal change slightly in the same way for a lot of tasks, currently the (lcp Old New) value is always the same. The idea is to transform the lcp into a lcp_list which compare the goal like lcp and then compare each hypothesis like lcp. So, we hope that when the goal differs the same for two New goals compared to one Old, the right one will be taken because it differs the same way on the hypothesis.
8511e56d