See meta-issue: issue924.

We want to simplify the translator output format by only allowing binary derived
variables whose default value is always false, and only allowing axioms setting
a derived variable to true. "Negated axioms" should instead be computed in the
search component when needed (for example in cg/landmarks/relaxation heuristics).

See msg8204 of issue862 for an overview of how the axiom code currently works.
(May become out of date while we're working on the axiom code further.)
(the axiom code was heavily reworked with issue453)

Check for references to "issue454" in the code, specifically axiom_rules.py and
sas_tasks.py. (Best look for references to issue454 in the whole codebase.)

Further TODOs/plans moved from issue862:
- Try moving the computation of axiom layers earlier, having everything related
  to negated axiom rules at the end. Then simplify the layer computation code
  to take into account that it no longer has to deal with negated heads, and
  enable the test that verifies the layering condition properly, removing all
  the hacks that are currently there because of the negated rules.
  Add assertions that there are no negated heads. Then rerun the experiments.
- Open an issue for the bug with compute_necessary_axiom_literals
  (see msg8204). (this was resolved as part of issue453)
- Make a plan for further steps for the axiom code. See the various notes etc.
  in msg8204.

While working on issue453, we changed the handling of axioms in the translator to
set the default value of derived variables to false. We can now continue to clean
up the translator output format and move the computation of negated axioms rules
into the search component. I updated the summary accordingly.

I added the remaining TODOs from the resolved issue862 to the summary because
they fit this issue better.

Add a pointer to msg8204 to the summary.

BTW, I'm no longer convinced that changing this would only affect a few parts of
the code. It looks like at least most of our relaxation heuristics (h^FF, h^add,
h^max) make use of the axioms provided by the code, and ripping out the negated
axiom versions can have a strong negative impact on them.

I don't mean this as an excuse to leave this issue unfixed, of course. But it
does mean we need to tread a bit carefully. In particular, we should make sure
not to ruin performance in cases without cyclic dependencies, which includes all
cases where derived variables are currently artificially introduced by the
translator.

Made the summary more comprehensive.

I'm reclassifying this as a bug because the negated axiom rules mean that we can
currently have axiom rules with heads (v=0) and (v=1) for the same variable. (At
least I think that this can happen.)

This is not necessarily a problem due to the way the axioms are actually
constructed, but it does not agree with how we specified the layering condition
in the AIJ paper on the translator and elsewhere. So at the very least, we
should make the semantics and the behaviour of the translator clear.

One reasonable place where this could be documented (in addition to the code
itself) is http://www.fast-downward.org/TranslatorOutputFormat, in particular
sections "Variables section" and "Axiom section" and section "Evaluation axioms"
at the end.

The proposed fix for issue862 interacts with this issue.

I've added code comments to axiom_rules.py which explain the interaction. All
relevant comments mention the keyword "issue454", so searching for this keyword
in axiom_rules.py while working on this issue should be enough to find all of
them. I've added a reminder of this to the summary.

Note to self: when fixing this, search the code (in particular the translator)
for references to issue454. The work-in-progress code for issue533 has a code
comment related to this issue.

We currently generate "negated forms" of axiom rules in certain cases. This can
be very expensive, is only used in few contexts, and is apparently currently
buggy (see issue453).

This issue is about getting rid of these negated-form axioms. The most difficult
part in this is probably detecting all the places where they are implicitly used
(e.g. in relevance analysis?). We should also evaluate the performance impact on
planner configurations that make use of these negated axiom rules (such as the
CG heuristic and possibly some of the landmark generators) and possibly
reintroduce them locally for planner configurations that use them.