由于可用问题需要大量技巧和预处理技术与决策程序无直接关系,因此很多时候对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将所有内容粘合在一起.
>一小部分策略产生(只有坐姿结果可以信任)或结束(只有不满意的结果可以信任)近似值.它们通常用于模型或证据查找.当Z3显示结果目标时,它将通知结果是精确的(sat和不可信任).