Review grounder transformations to reduce context switches, to prevent unnecessary Tseitins

[Broes De Cat]

Partial function unnesting does not always have to introduce existential quantification. E.g., !x: P(f(x)) => R(x) can be transformed into !x y: f(x)=y & P(y) => R(x).

More?

[Bart Bogaerts]

Disagree with the second point:

!x: P(f(x)) => R(x)

should be unnested to !x: (?y: y=f(x) & P(y)) => R(x) This is the semantics and we should not complicate code by taking context into account.

However, after unnesting, we might (should) call another pushnegation (and flatten) to obtain the formula you wanted

[Broes De Cat]

Agree with the correction ;)