由于可用问题需要大量技巧和预处理技术与决策程序无直接关系,因此很多时候对SMT求解器进行新的研究.这些通常是未发表的或需要时间来适当地实施和优化,此外使得对不同解算器的比较和理解非常困难.
是否可以使用Z3作为预处理器来解决问题并将其转储为预处理形式(z3本身用来解决问题)？
我没有看到任何命令行选项,但我猜测可能有一些方法可以实现这一点,通过策略,通过python接口,甚至编写一些额外的代码.
是的，Z3可以用作预处理器。该命令apply允许用户应用策略并将其转储为 SMT 2.0 基准。下面是一个示例（也可以在http://rise4fun.com/Z3/eutO在线获取）：
(declare-const x Real)
(declare-const y Real)
(assert (forall ((n Real)) (or (< x n) (< n y))))
(assert (= (< x y) (< x 100.0)))
(apply (then qe nnf) :print false :print-benchmark true)
在上面的示例中，qe（量词消除）和 nnf（否定范式）策略应用于输入问题。
一些补充要点：
几种策略只能产生同等令人满意的结果。因此，所得基准的模型不一定是原始公式的模型。我们可以要求 Z3 转储关联的“模型转换器”（选项:print-model-converter true）。模型转换器对 Z3 用于将结果公式的模型转换为原始公式的模型的步骤进行编码。然而，打印模型转换器没有标准，Z3无法读取这些描述。当然，我们可以使用编程 API 将所有内容粘合在一起。
一小部分策略会产生低于（只有 sat 结果可信）或高于（只有 unsat 结果可信）的近似值。它们通常用于模型或证明查找。当Z3显示结果目标时，它会告知结果是准确的（sat和unsat可以信任）。