z3 - 测试 Z3 的（完整）实例化策略

Question

我有兴趣测试 [1] 中讨论的决策/实例化过程（包括其实施）的“实际”影响。

我需要：

1) 一个“工具”，它采用 SMT 基准并返回它的（可能完整的）实例化版本，应用该策略。如果这是不可能的，

2) Z3 版本实现了这个策略和一个打开和关闭它的选项。

你能帮我吗？

[1] Satisfiabiliby Modulo Theories 中量化公式的完整实例化

Answer 1

据我所知，没有工具可以返回 SMT 基准测试的实例化版本。Z3 使用 [1] 第 6 节中描述的基于模型的量词实例化 (MBQI) 按需实例化量词。最新 Z3 中的实际循环比本节中描述的更复杂。

以下是有关如何启用/禁用 MBQI 模块的一些说明。

• 首先，我们应该使用命令禁用自动配置

（设置选项：自动配置假）

• Z3 4.x 使用 MBQI 和 E-Matching 来处理量词。我们应该使用以下命令来禁用它们：

(set-option :ematching false)
(set-option :mbqi false)

• 要启用它们，我们应该使用：

(set-option :ematching true)
(set-option :mbqi true)

使用这些选项，您可以检查 MBQI 和 E-Matching 在不同问题中的效果。请注意，如果我们仅使用 E 匹配，则 Z3 将返回unknown任何包含量词的可满足问题。

MBQI 模块在文件src/smt/smt_model_finder.cpp和src/smt/smt_model_checker.cpp. 该文件src/smt/smt_model_finder.cpp本质上是转换为模型中的无量词公式生成的模型，该模型可能潜在地满足普遍量化的公式。请注意，该类auf_solver实际上是“解决”集合约束并“构建”[1] 中描述的投影函数的类。

如果我们想跟踪 MBQI 模块生成的实际实例，我们可以修改void model_checker::assert_new_instances(). src/smt/smt_model_checker.cpp请注意，这些方法已经有一些跟踪命令将数据发送到tout（跟踪输出）。我们可以替换tout为std::cout来获取标准输出的信息。例如，如果我们添加以下代码，那么每当q（通过 MBQI 模块）使用一些绑定实例化一个通用量词时，Z3 将在标准输出中显示信息：

std::cout << "[New-instance]\n" << mk_pp(q, m_manager) << "\n";
std::cout << "[Bindings]\n";
for (unsigned i = 0; i < num_decls; i++) {
    expr * b = inst->m_bindings[i];
    std::cout << mk_pp(b, m_manager) << "\n";
}
std::cout << "[End-New-Instance]\n";