3

我正在尝试优化从我的模型生成的 z3 python 输入。我能够在具有 15k 约束（200 个状态）的模型上运行它，然后 z3 在合理的时间（<10 分钟）内停止完成。有没有办法优化从我的模型生成的约束？

3 种状态的模型：

http://pastebin.com/EHZ1P20C

4

1 回答 1

2

使用自定义策略可以提高脚本http://pastebin.com/F5iuhN42的性能。Z3 允许用户定义自定义策略/求解器。本教程展示了如何使用 Z3 Python API 定义策略/策略。在脚本http://pastebin.com/F5iuhN42中，如果我们替换该行

s = Solver()

和

s = Then('simplify', 'elim-term-ite', 'solve-eqs', 'smt').solver()

运行时间将从 30 秒减少到 1 秒（在我的机器上）。

该过程Then正在创建由 4 个步骤组成的策略/策略：

  • 简化器（即，应用规则的重写器，例如x + 1 - x + y==>1 + y

  • 消除If(a, b, c)whereb和cnot Boolean 形式的表达式。脚本大量使用了这种表达方式。该策略elim-term-ite将应用消除这种表达的转换。

  • 方程求解器。它应用了诸如x = a And F[x]==>之类的转换F[a]。在上面的脚本中，这种策略可以消除 1000 多个变量。

  • 该策略smt调用 Z3 中的通用 SMT 求解器。

该方法将 Z3 战术/策略转换为提供和方法.solver()的求解器对象。我在消息开头包含的教程有更多详细信息。addcheck

于 2013-01-13T15:41:23.810 回答