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

Published 20 hours ago • verified publisher icon sosy-lab

CVC5 integration

Open kfriedberger opened this issue 3 years ago • 3 comments

This PR integrates the new CVC5 (successor of CVC4) into JavaSMT.

kfriedberger avatar Aug 15 '22 21:08 kfriedberger

We have now an initial working version of CVC5 1.0.1 available via Ivy. We can now take a look at the API and bugs related to its usage.

kfriedberger avatar Aug 16 '22 20:08 kfriedberger

If you make the new solver available via maven, I would be happy to give it a try and report any issues I encounter :D

hernanponcedeleon avatar Aug 16 '22 20:08 hernanponcedeleon

The following bugs in the JavaSMT-bindings for CVC5 are currently known and will be analyzed in the next days:

  • Formulas from model evaluation are cleaned up when closing the model. This causes a Segfault. We need to copy the internals to keep the references.
  • Model evaluation can cause exponential overhead on CVC4 and CVC5 due to bad formula traversal.
  • CVC5 crashes when using timeout in JUnit tests, instantly when creating the first formula. This looks like an internal problem of CVC5.

kfriedberger avatar Aug 25 '22 21:08 kfriedberger

Update for the last comment:

  • Formulas from model need to be converted from one solver instance to another one. This is not easily doable from JavaSMT-ide, because we would do this recursively on arbitrary formulas.
  • The exponential overhead from model generation can be avoided by using the better model-evaluation for variables and UFs from CVC5 directly. This would be near-linear. However, for UFs (and maybe also arrays), CVC5 does return an nested ITE-structure that does have an else-case without proper condition. This else-value can not be converted to a proper assignment in JavaSMT, because of missing parameter assignments. For example, a formula foo(1)=2 AND foo(3)=4 has a model ITE(arg1=1; 2; 4) where the value 3 is not available. We asked the developers for a proper parameter listing, but got no solution yet (cf. https://github.com/cvc5/cvc5-projects/issues/20).
  • The crash when using timeout in JUnit test is unsolved yet.

kfriedberger avatar Oct 03 '22 10:10 kfriedberger

The current status of this branch is that most solver functionality should work as expected and there are some minor issues, mostl performance-related. I suggest to merge this PR and make an official release (with a hint on beta-status in the Changelog :wrench: ), and then continue further development and bugfixing in the master-branch.

kfriedberger avatar Oct 03 '22 11:10 kfriedberger