java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
The team of Boolector developed a new SMT solver [Bitwuzla](https://bitwuzla.github.io/) that seems to be quite fast for bitvector logic (see [results of SMT-COMP 2020](https://bitwuzla.github.io/smt-comp.html)). Bitwuzla seems to be the successor...
Since a few months, Boolector has new features that might be helpful for us. ### Global Declarations JavaSMT actually only support global declarations, and Boolector [provides now an option for...
Princess supports more theories than the ones currently announced in `java-smt`. The goal of this PR is to support them: - [X] String theory via naïve theory - [ ]...
JavaSMT when used via Ivy or Maven depends on an SMTInterpol JAR that contains not only classes from SMTInterpol, but instead also from several libraries of the Ultimate project (e.g.,...
The newest (not yet released) version of Yices2 seems to support interpolation: [Interpolation in the Yices2 API](https://github.com/SRI-CSL/yices2/blob/141154bfaa0a46d79b8e602dfad11edefdcfdf8a/src/api/yices_api.c#L9244) Additionally, they seem to provide their own Java bindings, which might be worth...
I just pushed some non-code change, and unit tests failed on Travis and AppVeyor with crashes: - `InterpolatingProverTest` on Windows with OpenJDK 14 ([log](https://ci.appveyor.com/project/sosy-lab/java-smt/builds/39260203#L185)) - `SolverStackTest`, `VariableNamesEscaperTest`, and `VariableNamesTest` on...
We should test the performance of basic operations like: - push, pop, addConstraint - creating large amounts of variables - creating large (but cheap) formulas - creating and closing several...
https://github.com/ultimate-pa/smtinterpol/pull/23 seems to add solving under assumptions for SMTInterpol, so JavaSMT should make use of it. It even seems to support what we call `unsatCoreOverAssumptions` (with `get-unsat-assumptions`).
Since we have a working MathSAT5 binary for ARM, we should incorporate the possibility to use this automatically. This means that our build systems either need to detected the architecture...
This PR covers the Windows support for Yices2. The JNI-wrapper was changed to conform to Windows pointer standards. A bash script is provided that explains how to build Yices2 for...