1

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

我需要:

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

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

你能帮我吗?

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

4

1 回答 1

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.cppsrc/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(跟踪输出)。我们可以替换toutstd::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";
于 2012-11-19T19:15:15.137 回答