java-smt icon indicating copy to clipboard operation
java-smt copied to clipboard

Published 20 hours ago • verified publisher icon sosy-lab

Succeed CVC4 by CVC5

Open baierd opened this issue 3 years ago • 4 comments

CVC4 was succeeded by CVC5 and as a consequence support for CVC4 stopped. We should also update to CVC5 as a consequence. This issue tracks the status and problems of this update.

  • CVC5 provides its own Java wrapper again.
  • CVC5 uses the same license as CVC4: BSD 3-Clause.
  • CVC5 can be used on Unix systems, MacOS and Windows.
  • Windows can be cross-compiled on Unix with Mingw-w64, MacOS using Homebrew seemingly only on a MacOS system.
  • CVC5 supports cross-compilation for ARM64.
  • CVC5 comes with several optional background SAT solvers and other helpful libraries.
  • I could not find concrete information about reentrance, but it seems like it supports it from the code.
  • API seems to reflect CVC4s, meaning problems like parsing and dumping (fixed in our code) still persist. Maybe we should ask them if they would add parsing?

baierd avatar Jan 28 '22 11:01 baierd

CVC5 currently does not provide API for formula translation between distinct solver contexts, but they are working on a solution for that.

Further, CVC5 does not provide a termination callback and it seems like they will not in the future. Also some convenience functions like getting a max signed bit vector are also missing, but that's fixable from our side.

baierd avatar Feb 04 '22 16:02 baierd

Hi!

I am a JavaSMT user, and would like to try out cvc5. Can I help you making the switch from CVC4 to cvc5?

Best, Lorenz

lorenzleutgeb avatar Aug 10 '22 18:08 lorenzleutgeb

Greetings @lorenzleutgeb, the implementation is done except for the interpolation prover. We are currently communicating with the CVC5 devs about some problems there. We just need to upload the binary into Ivy/Maven.

@kfriedberger could you compile/upload CVC5 version 1.0.1 (current) into Ivy/Maven? The compile/publish script is done and up to date for this version. (1.0.0 would need a rollback of the script)

baierd avatar Aug 11 '22 08:08 baierd

There are a few things remaining from JavaSMT's side. I am working on them:

  • build-scipts updated (nearly done)
  • loading mechanism fixed (see https://github.com/cvc5/cvc5/pull/9047, or we apply it directly internally before compiling CVC5 for JavaSMT, second way used so far)
  • code for CVC5 in JavaSMT updated (in progress)

kfriedberger avatar Aug 15 '22 21:08 kfriedberger