Project

General

Profile

Skype meeting 2016-05-17

Updates from last meeting:
- OpenSMT2 can now be compiled as a shared object library
- FunFrog has a git repository
- The repository includes the version history from svn

Things we agreed to do this week:
- Antti will make a git repository for OpenSMT2
- Antti and Leo will make sure that interpolation will be available in OpenSMT2 as a library
- The API for interpolation should look more or less like the one for PeRIPLO in what comes to propositional interpolation (unless there's a reason to change it)
- The encoding will be worked on separately without the need of integration to OpenSMT2 by Karine
- Grisha will check compiling OpenSMT2 without the interpolation to the extent that it is reasonable
- Regression tests run for the old FunFrog+PeRIPLO combination is not critical to fix right now
- it will be important to have these running later
- Matteo will have ideas on how to enable seamless parallelisation with FunFrog. This could be a longer-term goal
- We'll work more on Grisha's example of parallelising model-checking.

Next meeting will be next Tuesday, May 24, at 17.00 CET.