-
Notifications
You must be signed in to change notification settings - Fork 2
Description
The Simulator is a bit slow. There are many calls to Z3 that aren't necessary.
For example, the simulator is also called when there is no Update in the modifiers chain.
No update -> no timed change -> don't run Z3
Also:
If dt is not part of any modifier constraint -> no timed change -> don't run Z3
Also:
Only add the modifiers backwards until the update. any influence before the update can be ignored, since their behaviour (output value) will not change
This reduces the size of modifiers.
fewer constraints -> faster Z3 (I guess).
The problem lies in the efficient discovery of these conditions.
For example, how can we find out if dt is used in an update function without converting its constraints to string (slow), accessing its source code (slow) or going through the constraint ASTs (also slow, maybe?).
There should be some great caching somewhere (e.g. the source code's?)