使用 z3py 的全局参数

【问题标题】：Using global parameters of z3py使用 z3py 的全局参数
【发布时间】：2023-01-23 01:10:08
【问题描述】：

我正在尝试使用 SMT 求解器解决调度问题，但在文档中找不到任何帮助。

似乎使用以下设置参数的方式对求解器没有任何影响。

from z3 import *

set_param(logic="QF_UFIDL")
s = Optimize() # or even Solver()

甚至

from z3 import *

s = Optimize()
s.set("parallel.enable", True)

那么如何在 z3py 中有效地设置 [global] 参数。最具体地说，我需要在下面设置参数：

【问题讨论】：

标签： python z3py

【解决方案1】：

在创建 Solver 或 Optimize 对象之前，在单独的行中使用如下全局参数语句：

set_param('parallel.enable', True)
set_param('parallel.threads.max', 4)   #  default 10000

要设置特定于 Solver 或 Optimize 对象的非全局参数，您可以使用 help() 函数来显示可用参数：

o = Optimize()
o.help()

s = Solver()
s.help()

以下示例显示如何设置 Optimize 参数：

opt = Optimize()
opt.set(priority='pareto')

【讨论】：