python – Z3可以用来预处理问题吗?
由于可用问题需要大量技巧和预处理技术与决策程序无直接关系,因此很多时候对SMT求解器进行新的研究.这些通常是未发表的或需要时间来适当地实施和优化,此外使得对不同解算器的比较和理解非常困难. 是否可以使用Z3作为预处理器来解决问题并将其转储为预处理形式(z3本身用来解决问题)? 我没有看到任何命令行选项,但我猜测可能有一些方法可以实现这一点,通过策略,通过python接口,甚至编写一些额外的代码. 最佳答案
是的,Z3可以用作预处理器.命令apply允许用户应用策略并将其转储为SMT 2.0基准.这是一个例子(也可在http://rise4fun.com/Z3/eutO在线获得):
在上面的例子中,qe(量词消除)和nnf(否定 – 正规形式)策略应用于输入问题. 一些额外的要点: >几种策略只能产生令人满意的结果.因此,所得基准的模型不一定是原始公式的模型.我们可以要求Z3转储相关的“模型转换器”(选项:print-model-converter true).模型转换器对Z3用于将结果公式的模型转换为原始公式的模型的步骤进行编码.但是,打印模型转换器没有标准,Z3无法读取这些描述.当然,我们可以使用程序化API将所有内容粘合在一起. (编辑:李大同) 【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容! |