z3 和 νz (z3opt)：使用 Python API 设置逻辑

Question

我知道我们可以选择像AUFLIRA这样的逻辑供Z3或νZ（或z3opt，Z3的优化分支）使用

(set-logic AUFLIRA)

在输入.smt2 文件中。

但是如果我们需要使用 Python API 设置这个逻辑呢？我们可以使用哪些方法来做到这一点？

我检查了一些documentation，我注意到z3 模块中有一个SolverFor(logicName) 用于基于给定逻辑创建求解器（例如通过调用SolverFor('AUFLIRA')），但我有以下问题：

1. νZ 呢？ z3 模块也有 Optimize 对象，其工作方式类似于 Solver 对象，但我没有看到任何 OptimizeFor() 方法来获取给定逻辑的 Optimize 对象。

   李>

2. z3 模块中的SolverFor() 方法从不引发异常，即使我通过调用SolverFor('abcd') 指定了不存在 逻辑。文档说如果 Z3 不支持该逻辑，那么它将使用默认设置，但是我怎么知道它是否使用我提供的逻辑（例如 AUFLIRA 逻辑） ?

谢谢

Answer 1

nuZ 不公开可定制的策略/求解器，因为它非常专业地使用求解器来找到最佳值。

我们绝对应该解决 SolverFor('abc') 不会产生任何警告/异常的事实。我现在在不同的用户代码示例中看到了这个问题，如果没有警告/异常，用户可能不会意识到他们的设置没有效果。