优化z3输入

Question

我正在尝试优化从我的模型中生成的z3 python输入。我能够在15k约束的模型上运行它(200个状态)，然后z3停止在合理的时间内完成(<10分钟)。是否有一种方法来优化从我的模型生成的约束？

三个国家的模式：

http://pastebin.com/EHZ1P20C

Answer 1

使用自定义策略可以提高脚本http://pastebin.com/F5iuhN42的性能。Z3允许用户定义自定义策略/解决器。本教程展示了如何使用Z3 Python定义策略/策略。在脚本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)的表达式，其中b和c不是布尔表达式。脚本广泛使用了这种表达方式。策略elim-term-ite将应用消除这种表达式的转换。
• 等式求解器。它应用诸如x = a And F[x] ==> F[a]之类的转换。在上面的脚本中，这种策略可以消除1000多个变量。
• 战术smt在Z3中调用一个通用的SMT求解器。

方法.solver()将Z3策略/策略转换为提供add和check方法的求解器对象。我在邮件开头包含的教程包含了更多细节。