remove_unused transformation incorrect with some orderings
Based on my experience, and reading the source code, I think the remove_unused
transformation is currently incorrect (removes used axioms) if declarations are ordered as follows:
<declaration of id>
<use of id>
<axiom which depends on id>
The algorithm goes backwards in the task and when it encounters the axiom, sees that the symbol id
isn't used (yet) and doesn't register the axiom in the used_ids
. But id
is used before the axiom (the algorithm processes it after the axiom).
I think the algorithm needs to be improved, probably some kind of dependency map needs to be maintained and then used to rebuild the task.
@marche do you agree? If so, who should do it? I could probably try.