其他数学求解器，例如 z3 或 cplex，能够求解具有多个约束的数学模型，目的是最小化/最大化表达式，例如：
a+b=10； 2<=b<=6
目标：最小化(a)=> a:=4
但是，我在cvc5规范中似乎找不到任何这样的选项。我错过了什么，还是这个功能根本不存在？
目前我们正在使用 cplex 来实现此类应用程序，但我们正在尝试找到一个不太昂贵且具有确定性的求解器（与 z3 不同）
据我所知，CVC5 不支持优化。为了优化位向量，您可以通过从最高有效位到最低有效位来使用增量接口。对于其他理论，您可以使用量化公式。但没有内置的优化支持。
由于 z3 似乎不适合您，您可能需要看看 OptiMathSAT，它是专为优化模理论而构建的：https://optimathsat.disi.unitn.it
我应该注意 OptiMathSat（以下为 MathSat）具有限制性许可证。 （仅免费用于研究和评估目的。）