SMT解算器Z3引入了一个扩展(ΓZ(来支持优化目标的求解。我正在寻找其他支持软断言和字符串理论的SMT求解器。
据我所知，其他支持软约束的SMT解算器只有SMT-RAT和用于SMT的Barcelogic。然而，他们似乎都不支持弦理论。
据我所知，z3是唯一一个同时支持字符串和最大sat(即优化(的求解器。
Optimathsat(https://optimathsat.disi.unitn.it)支持优化，但看起来不支持字符串。或者，CVC5支持字符串，但不支持max-sat。(https://cvc5.github.io)
构建一个支持所有感兴趣理论的最大sat求解器并不是一项容易的任务；所以我不确定是否会有其他的解决方案来支持这个组合。希望将来会有，但就目前而言，z3似乎是你对这个特定组合的唯一选择。