如何使用 z3 库将经过优化的 SMT 模型转换为由 cvc4 等不同求解器识别的 .smt2 文件？

Question

我想使用文件 .smt2 中的 z3 库转换用 python 编写的 SMT 模型，以获得可以从不同求解器（例如 cvc4-solver）运行的文件。 问题是我的模型进行了优化，当从 z3 文件转换为 smt2 文件时，cvc4（其他 SMT 求解器）无法识别指令（最大化 x）。
这里有一个例子可以更好地理解这个问题：
型号：

o = Optimize()
i = Int('x')
o.add (i > 5)
o.add (i < 10)
o.maximize(i)
to_write= "(set-option :produce-models true)\n(set-info :status unknown)\n(set-logic QF_UFLIA)\n" 
to_write += o.sexpr() 
with open('/content/file1.smt2', "w") as f:   
   f.write(to_write)

现在我的文件的输出是：

(set-option :produce-models true)
(set-info :status unknown)
(set-logic QF_UFLIA)
(declare-fun x () Int)
(assert (> x 5))
(assert (< x 10))
(maximize x)
(check-sat)

如果我在 CMD 中运行此文件 smt2，使用 z3，求解器会返回 sat，但如果我使用 cvc4，求解器会给出此错误

(error "Parse Error: /content/file1.smt2:7.9: expected SMT-LIBv2 command, got `maximize'.
  (maximize x)
   ^
")

cvc4 无法识别该命令（最大化 x），还有另一种方法可以为 cvc4 求解器编写此指令吗？哪些 SMT 求解器可以识别 smt2 文件中的最大化/最小化指令？

我期待一个文件 smt2 可用于每个能够进行优化的求解器。

Answer 1

并非所有 SMT 求解器都会进行优化。事实上，据我所知，支持优化的只有 z3 和 optimathsat：https://optimathsat.disi.unitn.it

事实上，SMTLib 标准根本没有真正标准化优化。 （https://smtlib.cs.uiowa.edu）

因此，对于涉及优化的问题，我建议尝试使用 optimathsat 作为替代方案。据我所知，它理解相同的优化指令（即

maximize

/

minimize

等），因此脚本可能可以开箱即用。不过，检索结果的方式可能会有所不同，因此，如果您在那里遇到麻烦，请随时提出具体问题。

Answer 2

由于 Z3 支持优化类，而 CVC5（或旧版本的 CVC）目前不支持优化类，因此我们无法导出 SMT-LIB2 格式约束以进行优化并在 CVC SMT 求解器中使用。

但根据一位 CVC5 开发人员最近的评论，优化类和 softConstraint 功能的添加正在开发中，并将在 6 个月左右的时间内推出。

附上参考和评论链接： https://github.com/cvc5/cvc5/issues/10007#issuecomment-1715705938