Z3禁用数组模型输出lambda函数的配置方法咨询

问题背景 #

使用Z3处理数组相关问题时，4.8.12及之后的版本会默认将部分数组模型以lambda函数的形式返回，而4.8.6版本则使用as const的常量数组格式返回，两种返回示例如下：

4.8.6版本返回示例：

((tmp_array2 ((as const (Array (_ BitVec 4) Bool)) false))
 (tmp_bv3 #x0)
 (tmp_bool0 false)
 (tmp_bool3 false))

4.8.12版本返回示例：

((tmp_array2 (lambda ((x!1 (_ BitVec 4))) (= x!1 #x0)))
 (tmp_bv3 #x0)
 (tmp_bool0 false)
 (tmp_bool3 false))

解决方法 #

Z3提供了对应的配置选项，可直接禁用lambda形式的数组模型输出，恢复旧版本的常量数组格式，只需要在SMT脚本的头部添加两行配置即可：

(set-option :model.compact false)
(set-option :pp.model_lambda false)

两个参数的作用分别为：

• :model.compact false：强制Z3生成模型时优先构造as const加store的显式数组结构，不使用压缩的lambda表达式表示数组
• :pp.model_lambda false：关闭模型打印阶段的lambda输出语法，即使内部临时使用了lambda表示，打印时也会转换为显式的数组常量形式

将上述配置添加到测试脚本中，在4.8.12及后续版本运行即可得到和4.8.6版本完全一致的输出结果。如果是通过Python、C++等API调用Z3，在创建Context或Solver对象时传入这两个参数即可达到相同效果。

内容的提问来源于stack exchange，提问作者olibeck