[Z3] Rebase Quantifier unfolding based on a per-quantifier basis
Current status
The switch to perform a quantifier unfolding (or not) is currently done on the level ExplorationTargets, res its expression. For large constraint sets this differentiation may be to rough such that a no-longer understandable amount of Z3 expressions may be generated if unfolding must be used for some of them (acc. to Tiziano)
Ideas
After a short discussion, we came to the following conclusions:
- The benefit might be worth the effort (performance + readability), since the required technical modifications should be quite limited.
- Quantifiers would need an additional attribute “unfold” and the one from the constraints should be removed.
- The primary citizen for the transformation should be the quantified transformator that calls the unquantified one when needed.
- It may be required to pass around the Set->ModelElement “Stack”-Set when switching between the quantified and unquantified transformators.
(from redmine: issue id 3698, created on 2019-03-28, closed on 2019-07-23)