Currently, a commit is performed by first running propagate (in order to set all tmp values) and then iterating over all variables and invariants and committing them. This is very slow.
There should be some special propagation mode for committing, where variables and invariants are committed on the fly, and where invariants and variables that are not modified are not committed.
I am not sure if it makes sense to have a flag in the propagate algorithm or if it is better to have two implementations. If we have a flag then that might actually be much slower as we will be needlessly checking if we are committing or not, in the code the flag is always const so to speak.
Maybe this can be done using templates so that one calls propagate()? For committing?
Currently, a commit is performed by first running propagate (in order to set all tmp values) and then iterating over all variables and invariants and committing them. This is very slow.
There should be some special propagation mode for committing, where variables and invariants are committed on the fly, and where invariants and variables that are not modified are not committed.
I am not sure if it makes sense to have a flag in the propagate algorithm or if it is better to have two implementations. If we have a flag then that might actually be much slower as we will be needlessly checking if we are committing or not, in the code the flag is always const so to speak. Maybe this can be done using templates so that one calls propagate()? For committing?