Skip to content

Draft: MR for code review of branch 'interpolation-model-checking-refactor'

Po-Chun Chien requested to merge interpolation-model-checking-refactor into trunk

This branch includes the following updates:

  • Move the interpolation-related operations of IMC and ISMC into a separate class InterpolationManager
  • Reuse the InterpolationManager in the package util.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

Merge request reports