Improve DSML to SMT transformation performance for repeated calls
Current status
The DMSLtoSMTTransformator recalculates all Z3 expressions when the transformation is called. For successive calls, this has a major performance impact since the transformation is costly. It even takes much longer than solving medium sized problems in Z3.
Proposed solution
Cache previous transformation results such that they can be reused in
case only a few constraints/objectives are replaced. This automatically
includes the sets of implicitly generated constraints.
This stateful transformator comes at no cost, since it is written
already that way. In this ticket, this approach shall be commonly used
in that class (currently inconsistent) such that all transformation
results have to be queried in additional calls after a transform(…)
call.
(from redmine: issue id 3741, created on 2019-05-30, closed on 2019-06-05)
- Uploads: