转储 z3 的配置？答案

【问题标题】：Dump z3's configuration?转储 z3 的配置？
【发布时间】：2023-02-26 19:53:02
【问题描述】：

从 CLI 和 Python 运行时，有没有办法让 Z3 转储所有设置？

我有一个大型优化器 (maxsat) 程序，它从 CLI 以 2m 的距离运行，但在 Python 中运行时从未完成，我想了解它们之间的区别。对于此测试，我在 Python 中创建程序，然后使用“opt.sexpr()”将 smt 转储到我随后在 CLI 中测试的文件。

看起来“z3 -p”显示了默认的 CLI 设置。除了 (set-option) 行的明显差异之外，这些是否与加载脚本时的设置相同？

如何从 Python 内部得到同样的东西？

【问题讨论】：

这真的很奇怪；您是否可以分享一些展示此行为的代码，以便我们自己进行实验？据我所知，只要您不在 CLI 上传递任何自定义参数，在 Python 内部运行或通过 opt.sexpr() 保存到文件并从 CLI 运行它应该不会有什么不同。如果您确定是这种情况，请在 z3 问题跟踪器上报告：github.com/Z3Prover/z3/issues

标签： z3 z3py

【解决方案1】：

您可以设置或检索全局参数，如下所示：

#  Demo how to set global parameters
#  Run with a non-existent parameter to get a list of legal parameters
set_param("timeout", 60000 * 1000)  # milliseconds
v = z3.get_param('timeout')
print(f"timeout = {v}")

set_param("verbose", 0)
v = z3.get_param('verbose')
print(f"verbose = {v}")

set_param("sat.phase", "always_false")
v = z3.get_param('sat.phase')
print(f"sat.phase = {v}")

我还没有找到检索Solver参数的方法：

#  Demo how to set Solver parameters
s = Solver()
#  Display supported solver parameters
#  s.help()
s.set('shuffle_vars', True)
s.set('threads', 4)

v = s.sexpr()  # does not show any options
print(f"sexpr: {v}")

#  Display parameter reference descriptions
pr = s.param_descrs()
prLen = len(pr)
print(f"prLen = {prLen}")
prSize = pr.size()   #  alias for len(pr)
print(f"prSize = {prSize}")

for i in range(10):   #  not all 413 but only 10 ...
    v = pr.get_name(i)
    print(f"name {i}: {v}")
    v = pr.get_kind(i)
    print(f"kind {i}: {v}")
    v = pr[i]   #  returns the parameter name like get_name(i)
    print(f"{i}: {v}")

与 Solver 不同，Optimize 确实在 sexpr() 中显示参数。

#  Parameter handling of Optimize()
o = Optimize()
# o.help()
o.set("timeout", 123456)

v = o.sexpr()  # shows all options like (set-option :opt.timeout 123456)
print(f"sexpr: {v}")

使用 Python 检查器，我将默认的 Z3 参数与实际的 z3py 参数值进行了比较：

import subprocess

def show_non_default_parameters():
    result = subprocess.run('z3 -p', capture_output=True, text=True)
    lines = result.stdout.split('
')
    for line in lines:
        if line.startswith('Global'):
            prefix = ""
        elif line.startswith('[module]'):
            prefix = line.split(', ')[0][9:] + '.'
        elif "(default: " in line:
            name = prefix + line[:line.find(' (')].strip()
            dflt = line[line.find('(default: '):][9:-1].strip()
            if dflt != "":
                val = get_param(name)
                if val != dflt:
                    print(f"{name} = {val} (default: {dflt})")

发现以下默认偏差：
（Z3Py 版本 4.12.1 - 64 位 Windows 针对 Z3 4.11.2 二进制文件进行了检查）

rewriter.ite_extra_rules = true (default: false)
smt.bv.delay = false (default: true)

与 Z3 4.12.1 二进制文件的比较没有产生任何差异。

【讨论】：