Z3理论插入式误差

Question

我已经创建了一个定制的理论插件，它目前什么都不做。回调都是实现和注册的，但它们只是返回。然后，我阅读了一堆使用Z3_parse_smtlib2_string进行声明、声明-funs和断言的内容，并将生成的ast传递给Z3_assert_cnstr。随后对Z3_check_and_get_model的调用失败，出现以下错误：

mk_fresh_ext_data回调不是为用户理论设置的，必须使用Z3_theory_set_mk_fresh_ext_data_callback

据我所知，Z3_theory_set_mk_fresh_ext_data_callback并不存在。

使用相同的字符串，但没有注册理论插件，Z3_check_and_get_model返回sat，并给出了一个预期的模型。

我使用的是版本4和Linux 64位库。

完整的示例如下：http://pastebin.com/hLJ8hFf1

Answer 1

问题是基于模型的量词实例化模块(MBQI).此模块尝试创建主逻辑引擎的副本。要创建副本，Z3必须复制每个理论插件。它可以为所有的内在理论，但不能为外部理论。

最初的理论插件API不支持复制自己，因为它是在MBQI模块之前实现的。API Z3_theory_set_mk_fresh_ext_data_callback就是为此而设计的。然而，由于几个原因，它还没有暴露出来。主要问题是Z3 4.0为解决程序提供了一个新的API。当前的理论插件API与新的解决程序API不兼容。我们正在研究如何将它们结合起来。在Z3 4.0中，理论插件只适用于旧的(不推荐的)解决程序API。

为了避免您描述的问题，只需禁用MBQI模块即可。您可以通过在创建MBQI=false时设置Z3_context来做到这一点。在C中，您可以使用下面的代码片段来实现这一点。

Z3_config cfg; 
Z3_context ctx;
cfg = Z3_mk_config();
Z3_set_param_value(cfg, "MBQI", "false");
ctx = Z3_mk_context(cfg);

这也解释了为什么你的插件在没有量词的公式上工作.这种公式不使用MBQI模块。