Decomposed interpolants

Experiments

We experimented with application of decomposed interpolants in a model checking algorithm PDKIND [1], implemented in SALLY.

The version of SALLY used in the experiments currently lives in a forked repository. The precise commit is tagged as tacas19. The version of OpenSMT used in these experiments is also tagged with the same tag, tacas19. Follow these instructions to compile and install OpenSMT. To print the statistics about the decomposed interpolants, set the cmake option PRINT_DECOMPOSED_STATS to ON. Yices2 is also required.

The benchmarks were run with the following command:

sally --solver y2o2 --solver-logic QF_LRA --engine pdkind -i <input_file> --opensmt2-simplify_itp 2 --opensmt2-itp N

where N can be:

  • 0 for Farkas interpolation
  • 2 for dual Farkas interpolation
  • 4 for decomposed interpolants
  • 5 for dual decomposed interpolants

 

For the runs with MathSAT we used the following command:

sally --solver y2m5 --solver-logic QF_LRA --engine pdkind -i <input_file> --y2m5-mathsat5-flatten

The set of benchmarks can be found here. It is a combination of benchmarks provided by SALLY from here and here.

The results per benchmark can be found here.

The results for running the same benchmark with different random seed for OpenSMT can be found here.

 


1. Jovanović, D., Dutertre, B.: Property-directed k-induction. In: 2016 Formal Methods in Computer-Aided Design (FMCAD). pp. 85–92 (Oct 2016).