I merged the change.

> I'd be interested in seeing if we see a positive effect in the citycar domain
> in the planner, so I'll run some informal experiments there and then write
> again.

I tried the following command before and after this change:

$ ./fast-downward.py --validate 
~/downward/benchmarks/citycar-sat14-adl/p4-3-3-0-1.pddl --evaluator "h=cg()"
--search "lazy_greedy([h],preferred=[h])"

(The CG heuristic is one of the ones that is quite sensitive to a good encoding.)

With the new code, this is solved in 10 seconds (not counting translator time).
With the old code, this runs out of 32-bit address space after around 4:20
minutes on my machine, so it is not solved.

I did similar, less complete, tests for the five p3-*... instances of
citycar-sat14-adl. The new code solves all of them more or less instantaneously.
The old code takes a substantial amount of time or fails to solve them altogether.


So this looks not just like a good bugfix, but also like a performance
improvement at least in this domain. In any case, it's ready to merge.

> (There are unexplained errors for every task because originally I had the
> access rights for an additional md5-sum-parser wrong. You can ignore them.)

Ah, I must have overlooked that.

The pull request makes sense to me. :-)

Regarding the experimental results, I assume the "unexplained errors" where
mainly experiment parsing isuses that were later resolved. I didn't look through
them in detail because there is so many and it's clear that the change makes sense.

I'd be interested in seeing if we see a positive effect in the citycar domain in
the planner, so I'll run some informal experiments there and then write again.

Experiment data is at
https://ai.dmi.unibas.ch/_tmp_files/pommeren/issue874-v1-issue874-base-issue874-v1-compare.html

(There are unexplained errors for every task because originally I had the access
rights for an additional md5-sum-parser wrong. You can ignore them.)

The issue can be reviewed (and probably merged).

Do you have an experimental results file that we can link to this issue?

For trucks-strips, the translator files often change even without a code change
because we hit the internal invariant synthesis timeout, and the number of
invariants found until this point can vary based on how "lucky" we are with
process speed. If the change in trucks-strips only happens for larger instances,
it is probably related to that.

In the spider domain, the previously detected invariant {clear 0, on 1 [0]} was
wrong because there can be several cards on discard (a constant).

I had a look at the impact of this change:

- the overall translation time gets sometimes faster, sometimes slower. The
change is worst in organic-synthesis-split-sat18-strips, where task 12 takes 14
seconds longer (but e.g. task 13 is 20 seconds faster)
- the number of variables is only affected in very few domains (citycar and
trucks-strips). For trucks-p25 it decreases by 169 variables and for the other
trucks tasks it is either equivalent or increased by one. In citycar it gets
significantly lower throughout all tasks.
- in the spider domain, we loose the mutex between clear and on but this does
not have an impact on the encoding.

While looking into issue810, I noticed that ensure_inequality reads Atom.parts
(which is always an empty tuple) instead of Atom.args (containing the terms). As
a result, it never generates any constraints on the renaming that make sure that
the atoms are indeed different.

As a result, we might unnecessarily consider an action as too heavy (not
threatening correctness) but also might accept an unbalanced add effect as
balanced (a problem regarding correctness).