Rerelease CVC4 to add JavaDocs and sources#640
Conversation
|
CVC4, Boolector, and OptiMathSAT are no longer actively maintained by their authors, i.e., since at least 2021 for CVC4, since 2018 for OptiMathSAT. This PR does quite some work for updating the solver once again. However, it might not be worth the effort for maintainance and re-compilation on JavaSMT-side. It is more like "nice to have". Fine for me. |
| } else { | ||
| throw new AssertionError( | ||
| "Unhandled type '%s' with base type '%s'.".formatted(t, t.getBaseType())); | ||
| return FormulaType.fromSMTLIBString(t.toString()); |
There was a problem hiding this comment.
Type-check might be slightly more expensive that way. However, it is simpler in code. So let's keep it that way.
|
Looks like the memory management is not yet sufficient (broken CI-job in master-branch) and we might need to track all formulas/terms and avoid any cleanup. This implies tracking all Java-object from Java-side (requires even more memory, because Java objects are kept alive forever) or remove the finalizers once again (as done before). |
Sorry about that. It seemed to be working when I tested it locally I'll look into how to remove the finalizers again |
|
No problem at all. I ran some local tests as well, and it worked well on my machine. That’s the classic headache with garbage collection: nondeterministic nature makes these issues quite hard to find and fix. The old fork of CVC4 that contains some commits for disbled finalizers can be found here: https://github.com/kfriedberger/CVC4 (last commit is from 2019). We could try to rebase or merge with the latest CVC4-Archived. The difference is just a few commits. |
Yes, finalizers were deprecated for a reason.. 😅
Thanks! I've already extended the build script to remove the finalizers here. But using your branch should also work. I don't think there have been any important commits since then |
2 participants
Hello,
this PR adds sources and JavaDocs to the CVC4 release. The CVC4 bindings haven't been compiled in a while, and we were previously using a modified version of CVC4. Because of this, some larger changes were needed, and I decided to split this off into a separate PR. JavaDoc for all other solvers and JavaSMT itself will be handled in #639