z3 - 使用 Z3 的配置 API

Question

使用最新的(不稳定的)Z3 运行 z3 -p 显示按模块分组的参数列表。说明如下:

To set a module parameter, use <module-name>.<parameter-name>=value
Example:  pp.decimal=true

一般来说，这些指令如何转换为 C API？在当前文档中，似乎有一组处理“全局”配置的 API 调用，例如 Z3_set_param_value，以及围绕 Z3_params 构建的另一组特定于对象的调用> 类型，例如 Z3_solver_set_params。

特别是，我想知道我是否可以使用 Z3_set_param_value 在任何模块中全局设置任何参数。 Other StackOverflow answers宣传 Z3_params 对象的使用，甚至用于全局参数，如 timeout(或者是 :timeout？)，但我不清楚如何此 API 映射到 module.parameter=value 语法。

Answer 1

module/name参数主要针对Z3的命令行版本。

全局参数意味着在开始时设置一次，然后对所有后续调用都有效。我们将此参数设置方案与新的策略/目标/求解器/策略/探针接口(interface)一起引入，因为我们需要不同的策略配置，而 Z3_params 对象主要用于此。例如，Z3_tactic_using_params 创建一个新策略，它是基于 Z3_params 对象中的选项重新配置另一个策略。

但是请注意，当通过 API 创建策略时，没有模块(您创建的策略不存在于 Z3 内部的“参数模块”中)。例如，在策略教程(参见 here)中，一个策略的构造和应用如下:

(check-sat-using (then (using-params simplify :arith-lhs true :som true)
                        normalize-bounds
                        lia2pb  
                        pb2bv                       
                        bit-blast                       
                        sat))

因此，简化器启用了参数“arith-lhs”和“som”。在命令行上，“重写器”模块中有相同的选项，即 rewriter.arith_lhs=true 如果在命令行上启用它，则每次简化器时都会启用它叫做。

可以通过运行(在 Windows、Linux 上)获得策略列表和它识别的参数列表

echo (help-tactic) | z3 -in -smt2
echo "(help-tactic)" | z3 -in -smt2

另一件需要注意的事情是 Z3_params 对象中的参数不会以任何方式进行检查，也就是说，有可能提供虚假的参数名称并且 Z3 不会提示或发出警告，策略会简单地忽略该参数。

参数名前面的:是Lisp的遗留物，是SMT2格式的基础。参见，例如，此处:Why colons precede variables in Common Lisp .只有在使用 SMT2 输入语言时才需要它们。所以，SMT2命令

(set-option :timeout 2000)

相当于命令行参数

timeout=2000

由于问题明确提到了超时参数:我们最近在 OSX 上处理超时时遇到了一些问题，可能需要获取最新的修复程序，当然可能还有更多我们尚未发现的错误。

在C API 中，函数Z3_global_param_set 用于设置全局参数，也用于设置默认模块参数。这些参数将由之后创建的所有 Z3_context 对象共享(即 pp.decimal)，如果应用其中一种内置策略，将使用它们。