Draft: MR for code review of branch 'interpolation-model-checking-refactor'
This branch includes the following updates:
Move the interpolation-related operations of IMC and ISMC into a separate classInterpolationManager
- Reuse the
InterpolationManager
in the packageutil.predicates.interpolation
for interpolation-related operations of IMC and ISMC - Unify the internal formula representation of IMC and ISMC into
PartitionedFormulas
- Add a new IMC config
assertTargetsAtEveryIteration
No regression seems to be introduced by these changes (cf. the experimental comparison of IMC and ISMC), thus it should be safe to merge.
EDIT: update the experimental results to the latest revision r39914
(5a57b705).
This merge request is for code review and discussions only. Merge must be done with svn merge
.
Edited by Po-Chun Chien