java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
I have two Maven packages: In `project1` I use `java-smt` with native solvers (specifically Z3). I then install `project1` to my local Maven repository, and use it in `project2` (where...
This PR extends the compile script for the Yices2j JNI-wrapper to support a Darwin-based system. The wrapper is statically linked with its dependencies to produce the single file `libyices2j.dylib`. I...
When running tests, such as in [this case](https://gitlab.com/sosy-lab/software/java-smt/-/jobs/7816950900), some of the tests seem to print warnings like the following: - `Unexpected logic for quantifier elimination ALL` - `WARNING: optimization with...
## Objective This PR aims to expose proofs produced by supported solvers through the API, primarily via a `getProof()` method. ## Key Changes - Introduced `ProofNode`, `ProofDag`, and `ProofRule` as...
Most solvers allow either re-usable shutdown or we use shared environments that are created per prover, making them isolated enough to be shut down without stopping the context. This PR...
While trying to parse the String output from the method `printResolutionProofSMT2` from the OpenSMT API I could not find a way to recover the formulas from their name used in...
Yices2 supports parsing on our currently main branch. But the tests are still disabled for it and it fails many basic tests. This should be investigated and solved before the...
Applying light quantifier elimination `applyQELightImpl()` is only implemented for Z3. While returning the original formula is valid, we should tell users that this only works for Z3. Otherwise they expect...
Hi, I am facing problems during the installation of JavaSMT. Could anyone please help me with appropriate build.xml and ivy.xml? You can find my current attempts [attached](https://github.com/user-attachments/files/19393124/IvyxmlBuildxml.zip), but they do...
I found a problem when asking for a model iterator in Mathsat5 using CPAchecker. It takes about 600s to get to the error and this was executed using [this branch](https://gitlab.com/sosy-lab/software/cpachecker/-/tree/symex-pathbased-solver-context?ref_type=heads)...