Open stklik opened 5 years ago
Another one: Replace get_modifier_map
in the simulator with the networkx
approach.
The graphs will be created for the dependency order anyway, so we might as well use these operations instead of creating the graph it manually.
I also hope this is faster, but we'll see.
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 Z3Also: 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?)