Issue454 - move computation of negated axioms to search component

[salome-eriksson]

No description provided.

[salome-eriksson]

I added some comments on the code where I try to explain why I implemented certain things the way I did.

[roeger]

First round of comments. I haven't looked at everything, yet.

[roeger]

Hi @salome-eriksson,

I added another round of comments.

For the record, we talked about two more general aspects in person:

• it is a bit confusing that parts of the implementation have a perspective of a fact that can be true or false (e.g. "needed negatively") and other parts use the perspective of a binary finite-domain variable that has a default value and the other value.
• @speckdavid suggested to add an option to the affected heuristics to use the overapproximation for all derived variables that are needed negatively (weakening the heuristic but saving the time for the transformation).

Best,
Gabi

[FlorianPommerening]

I did a light review on the auxiliary parts of the code (CMake, Options, etc.) I didn't look at the actual implementation in src/search/tasks and src/translate.

What I didn't quite get from the documentation is what happens if I don't use the option simple_default_value_axioms. Will axioms just behave "correctly" (whatever this means) without the option and once I set this option, I approximate this behavior in a way that can only weaken heuristics?

[salome-eriksson]

I did a light review on the auxiliary parts of the code (CMake, Options, etc.) I didn't look at the actual implementation in src/search/tasks and src/translate.

What I didn't quite get from the documentation is what happens if I don't use the option simple_default_value_axioms. Will axioms just behave "correctly" (whatever this means) without the option and once I set this option, I approximate this behavior in a way that can only weaken heuristics?

The negated axioms are always "correct" in the sense that the heuristic will be safe and stay admissible if it should be (for example hmax). But sometimes the conditions under which a derived variable achieves its default value are just (over)approximated, making the heuristic weaker. If the option is set, then all negated axioms are just overapproximated, which is much faster to compute, but can lose a lot of information. If the option is not set, then the overapproximation is only done for some axioms (those whose derived variables have cyclic dependencies, see issue453 for details).

[roeger]

Hi @salome-eriksson,

I had another look at the changes and only left a few comments on cosmetics. From my side, the code in principle is ready to merge.

Best,
Gabi