search

CatarinaGamboa / liquidjava

32 stars 1 forks source link

cvc5 support #18

Open FrogOfJuly opened 2 years ago

FrogOfJuly commented 2 years ago

In this branch I plan to implement support for cvc5 alongside with z3 smt solver. It is necessary as cvc5 has java API for separation logic. I will log problems I am concoutering here

FrogOfJuly commented 2 years ago

Since here it is possible to access cvc5 API

alcides commented 2 years ago

A maven integration would be helpful for other systems. Would this not work, even if we skip the JavaSMT API usage? https://mvnrepository.com/artifact/org.sosy-lab/javasmt-solver-cvc5/1.0.1-g8c2b8db17

FrogOfJuly commented 2 years ago

A maven integration would be helpful for other systems. Would this not work, even if we skip the JavaSMT API usage? https://mvnrepository.com/artifact/org.sosy-lab/javasmt-solver-cvc5/1.0.1-g8c2b8db17

I thought it only had cvc5 support for Linux.

Screenshot 2022-10-29 at 19 02 20

My initial aim was to make cvc5 available first and then later fix the building process. The best option was to build cvc5 separately and install it as a local package via maven install:install-file. But I stumbled on the problem that maven search for cvc5 in spoon repository instead of a local one. After some tries, I decided to fix it later, when it will be clear that using cvc5 API is a good way to introduce separation logic.

But if you think that it is ok to use javaSMT despite platform issues, there is not much work to be lost.

FrogOfJuly commented 2 years ago

Now cvc5 dependecy is a local package. See here for the details.