首页 文章

Z3理论插件错误

提问于
浏览 次
2

我创建了一个自定义理论插件，目前什么都不做 . 回调都是实现和注册的，但它们只是返回 . 然后，我使用Z3_parse_smtlib2_string读取了一堆declare-consts，declare-funs和asserts，并将结果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

z3

1 回答

  • 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模块 . 您可以通过在创建 Z3_context 时设置 MBQI=false 来实现 . 在C中，您可以使用以下代码片段执行此操作 .

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

    这也解释了为什么你的插件适用于无量词的公式 . MBQI模块不用于此类公式 .

    回复于

相关问题