【发布时间】：2015-06-11 18:31:15
【问题描述】：
我正在尝试提高我的 z3py 代码的性能以进行推理。您认为更改添加到求解器的逻辑约束的顺序可能会有所帮助吗？
【问题讨论】：
标签： performance z3 smt z3py
【发布时间】：2015-06-11 18:31:15
【问题描述】：
可能，但切换求解器或建立专门的策略可能会产生更大的影响。
【讨论】：
-
谢谢。您是否知道任何解释选择什么求解器以及如何编写自定义策略的好教程？我努力搜索但失败了。
-
从 Z3Py 中，您可以打印一组可用的策略。然后你可能想以某种方式组合然后（例如使用 AndThen() ）。 Z3Py 中的有用函数： 战术（） - 返回战术列表；战术描述（名称）； describe_tactics() - 结合其他 2 个函数