Fixing #856 and some light refactoring

[marcoeilers]

Fixing #856 and #327 by making two changes:

• Inverse function and snapshot map definitions are marked as global only if they do not depend on relevant quantified variables in the current state (previously, they were always marked as global)
• Some relevant quantified variables were already added as arguments to these functions, but some that were relevant for the QP's condition were omitted here. That is fixed now.

In the process, I merged the two functions summarise_field and summarise_predicate_or_wand that largely did the same and only differed in a few places into one function.