Spawned from issue335. I'm attaching Patrik's example from that issue. With the
current translator version, we quickly run out of memory on this example unless
we comment out all but two objects. This is probably caused by
axiom_rules.compute_negative_axioms, which does a CNF-to-DNF-style conversion.
There are two separate aspects here. Firstly, we could avoid the exponential
blowup by introducing auxiliary axioms.
Secondly, it's not clear why we need to compute these negated axioms at all. I
think they were originally added for "extended DTGs", and I'm not sure if they
are really used except perhaps by a few optional parts of the planner (CG
heuristic, possibly cea heuristic, possibly some landmark generation methods).
If this is an optional computation, it doesn't belong in the translator.
(However, I did a quick test that simply removed this line of code, and this
didn't work well, claiming Patrik's example is unsolvable. It may be that the
simplification later on in the translator then decides that the variable is
unnecessary or something like that.)
|