The translator gets stuck on the "Completing instantiation" step on the attached
instance. Adding some diagnostic output shows that progress is made, but very
very slowly.
My initial incomplete examination suggests that the reason for the slowness is
that our grounding of universally quantified effects is implemented much more
naively than the other parts of the grounding algorithm (possibly because that
part was tacked on at a late point), by exhaustively trying out a large number
of object combinations. Most of these are unnecessary because they fail static
predicates.
The grounding of universally quantified effects should be integrated into the
Horn grounding algorithm in a more elegant fashion. This isn't too hard
conceptually, but it'd be some implementation work. If there's anyone interested
in implementing this, I'm happy to provide some guidance on how I think this
should be implemented.
Split off from issue292.
|