java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
Z3 supports interpolation again (using model-based interpolants) by utilizing their CHC backend (Spacer). It has to be compiled with a special flag for that. We can add this back in...
`FunctionDeclarationKind` is an enum with quite a lot of cases that belong to different categories. When using this enum, e.g., in a visitor, it is likely common that one wants...
1. Added dependencies for UltimateEliminator in ivy.xml 2. Integrated classes needed for UltimateEliminator in JavaSMT 3. Created UltimateEliminatorWrapper class and equipped with a utility class UltimateEliminatorParser 4. Created options in...
# Optimization API and Resource Management Improvements ## Description This PR addresses the inconsistent optimization support across SMT solvers by implementing a robust fallback mechanism and standardizing the optimization API....
Quantification with bound boolean variables is currently not working in Princess. We should investigate and fix this if possible.
SMTInterpol is available in version 2.5-1388 while we still use the 3 year old version 2.5-1242. I don't know the details of changes, but the new version does include changes...
Hello, this PR will add support for parsing to CVC5. The approach taken is very similar to what we're doing in the Bitwuzla code as we again have to carefully...
This PR extends JavaSMT with an independent SMTLib2 parser/generator layer. Every solver can use the layer to generate or parse SMTLib2, independent of their own implementation. The parsing directly uses...
# Inconsistent Optimization Support Across Solvers ## Description The optimization API in JavaSMT has inconsistent implementation across different solvers, leading to unpredictable behavior when applications switch between solver backends. Currently,...
Hello, the [Getting-started](https://github.com/sosy-lab/java-smt/blob/463-problems-with-installation/doc/Getting-started.md) guide recommends users to use Ivy to install JavaSMT, but we currently don't have an example project for this. This PR adds adds the missing project template...