This is a link » History » Version 1
Antti Hyvärinen, 17/05/2016 18:11
| 1 | 1 | Antti Hyvärinen | h1. Skype meeting 2016-05-17 |
|---|---|---|---|
| 2 | |||
| 3 | Updates from last meeting: |
||
| 4 | - OpenSMT2 can now be compiled as a shared object library |
||
| 5 | - FunFrog has a git repository |
||
| 6 | - The repository includes the version history from svn |
||
| 7 | |||
| 8 | Things we agreed to do this week: |
||
| 9 | - Antti will make a git repository for OpenSMT2 |
||
| 10 | - Antti and Leo will make sure that interpolation will be available in OpenSMT2 as a library |
||
| 11 | - 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) |
||
| 12 | - The encoding will be worked on separately without the need of integration to OpenSMT2 by Karine |
||
| 13 | - Grisha will check compiling OpenSMT2 without the interpolation to the extent that it is reasonable |
||
| 14 | - Regression tests run for the old FunFrog+PeRIPLO combination is not critical to fix right now |
||
| 15 | - it will be important to have these running later |
||
| 16 | - Matteo will have ideas on how to enable seamless parallelisation with FunFrog. This could be a longer-term goal |
||
| 17 | - We'll work more on Grisha's example of parallelising model-checking. |
||
| 18 | |||
| 19 | Next meeting will be next Tuesday, May 24, at 17.00 CET. |