我有兴趣测试 [1] 中讨论的决策/实例化过程(包括其实施)的“实际”影响。
我需要:
1) 一个“工具”,它采用 SMT 基准并返回它的(可能完整的)实例化版本,应用该策略。如果这是不可能的,
2) Z3 版本实现了这个策略和一个打开和关闭它的选项。
你能帮我吗?
[1] Satisfiabiliby Modulo Theories 中量化公式的完整实例化
据我所知,没有工具可以返回 SMT 基准测试的实例化版本。Z3 使用 [1] 第 6 节中描述的基于模型的量词实例化 (MBQI) 按需实例化量词。最新 Z3 中的实际循环比本节中描述的更复杂。
以下是有关如何启用/禁用 MBQI 模块的一些说明。
(设置选项:自动配置假)
(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";