z3py：如何设置名称包含“.”的战术配置选项？答案

【问题标题】：z3py: How to set Tactic configuration options whose names contain "."?z3py：如何设置名称包含“.”的战术配置选项？
【发布时间】：2015-08-07 05:39:12
【问题描述】：

在z3.py中配置战术的正确方法是使用“With”。例如

t = With(Tactic('simplify'), som=True)

但是，某些选项名称包含“。”在其中，例如策略“qflia”中的“arith.solver”。如果我们用同样的方式编码

t = With(Tactic('qflia'), arith.solver=1)

系统给出错误“SyntaxError：keyword can't be an expression”。我猜这违反了python中关键字的语法规则。

如何配置名称中包含“.”的选项？或者我指的是错误的战术配置选项列表？我使用的是z3而不是z3.py上的命令“（help-tactic）”输出。

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

诀窍是不要使用“With”，而应该使用“set_param”或“set_option”。例如。 set_param('smt.phase_selection',5)

【讨论】：