'Any other MAX-SMT solvers that support string theory besides Z3?
The SMT solver Z3 has introduced an extension (νZ) to support the solving of optimization objectives. I'm looking for other SMT solvers that support both soft assertions and string theory.
The only other SMT solvers that support soft constraints I'm aware of are SMT-RAT and Barcelogic for SMT. However, neither of them seem to support string theory.
Solution 1:[1]
As far as I know z3 is the only solver that supports both strings and max-sat, i.e., optimization.
Optimathsat (https://optimathsat.disi.unitn.it) supports optimization, but doesn't look like it supports strings. Alternatively, CVC5 supports strings, but not max-sat. (https://cvc5.github.io)
Building a max-sat solver that supports all the theories of interest is not an easy task; so I'm not sure if there'll be any other solver anytime soon that'll support this combo. Hopefully there'll be in the future, but for the time being z3 seems to be your only choice for this particular combination.
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|---|
| Solution 1 | alias |