3

使用最新（不稳定）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全局设置任何模块中的任何参数。其他 StackOverflow 答案甚至宣传Z3_params对象的使用，即使是全局参数，比如timeout（或者是:timeout？），但我不清楚这个 API 如何映射到module.parameter=value语法。

4

1 回答 1

4

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

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

但是请注意，通过 API 创建策略时，没有模块（您创建的策略不存在于 Z3 内部的“参数模块”中）。例如，在策略教程（参见此处）中，构建和应用策略如下：

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

因此，为简化器启用了参数“arith-lhs”和“som”。在命令行上，相同的选项在“rewriter”模块中，也就是说，rewriter.arith_lhs=true如果它在命令行上启用，它将在每次调用简化器时启用。

可以通过运行（分别在 Windows、Linux 上）获得战术列表和它识别的参数列表

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

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

:参数名称前面是 Lisp 的剩余部分，它是 SMT2 格式的基础。参见，例如，这里：为什么冒号在 Common Lisp 中的变量之前。只有在使用 SMT2 输入语言时才需要它们。所以，SMT2 命令

(set-option :timeout 2000)

相当于命令行参数

timeout=2000

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

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

于 2014-07-03T12:50:14.653 回答