java-smt

java-smt copied to clipboard

SMTLib2 Output Consistency for Quantified Terms

1

I noticed that quantified formulas are dumped in many different ways, some of which are inconsistent with SMTLib2 and can not be parsed by other solvers. We should add I/O...

baierd

Java 11 premier support ended in September 2023. We should update to Java 17 as our basis to keep up with the support and new developments. I would suggest to...

baierd

MathSAT5 can create quantified formulas, but not solve them. However, they can be dumped with `msat_to_smtlib2_ext()` and `msat_to_smtlib2_term()`. `msat_to_smtlib2_ext()` exports a full SMTLib2 program, while `msat_to_smtlib2_term()` exports only the formula...

baierd

Hello, this MR patches several minor issues remaining after #422: * When escaping a String we now also escape `\` to make sure the backslash is preserved and doesn't get...

daniel-raffler

Blacklist more SMTLIB keywords as variable/uf names and automatically escape all variable names that would be illegal

2

Hello, this will update the list of forbidden variable/uf names to include all SMTLIB commands, such as `check-sat` or `assert`, and all predefined function names, like `mod` or `fp.add`. While...

daniel-raffler

CVC5 timeout implementation

6

Hi! I am trying to implement timeout on query to CVC5 solver. I am aware of non-existence of such interface in library (there is `ShutdownManager`, but it does not implement...

Avgor46

Use the partial model for formula evaluation in Princess

2

Hello, We stopped using the partial model in Princess [here](https://github.com/sosy-lab/java-smt/pull/391) as there were several solver issues when using it with rational formulas. Most of these issues have now been resolved...

daniel-raffler

Bitwuzla: Fix handling of quoted symbol names while parsing SMTLIB formulas

3

This addresses an issue in the Bitwuzla backend where quoted SMTLIB symbols like `|var|` were added to the variable cache without removing the quotes first. As a result there could...

daniel-raffler

Update CVC4 to the Last Release Version 1.8

2

We are currently using prerelease version 1.8 of CVC4. But 1.8 has been release as the last version of CVC4 and is roughly a year younger than our version. We...

baierd

Inconsistent handling of Unicode characters in String theory

4

Different solvers return different results when using Unicode characters in String theory. This should be analyzed. Maybe we need to fix JavaSMT or report to the solvers' developers. Details: https://github.com/sosy-lab/java-smt/pull/391#discussion_r1847998043

kfriedberger