Z3理论插件错误

我已经创建了一个自定义理论插件，目前它什么都不做。回调都是实现和注册的，但他们只是返回。然后，我读了一堆declare-consts，declare-funs，并使用Z3_parse_smtlib2_string进行断言，并将生成的ast传递给Z3_assert_cnstr。到Z3_check_and_get_model的后续调用失败，出现以下错误：Z3理论插件错误

The mk_fresh_ext_data callback was not set for user theory, you must use 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

来源

2012-07-25 zanderso

简化示例[链接]（http://pastebin.com/rGB6jX2a） – zanderso 2012-07-25 12:46:29

与使用API构建而不是解析调用的断言相同：[link]（http://pastebin.com/ytzsbzpF）。此外，这个问题似乎与使用forall有关。当断言没有完成时，事情按预期工作。 – zanderso 2012-07-25 13:46:23

的问题是基于模型的量词情境化模块（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模块不用于这种公式。

来源

2012-07-25 16:46:25

谢谢！所以现在看来，我可以使用理论插件或量词，但不能同时使用。这是否准确？（将MBQI设置为false后，上面的示例不再导致错误，但是我用量词尝试过的任何内容都返回“unknown”。）另外，是否有适用于新解算器/战术API的教程？ – zanderso 2012-07-25 17:43:34

您仍然可以使用量词，但它们将仅使用电子匹配引擎进行处理。只需使用E匹配，Z3仍然可以显示许多公式为“不合格”。但是，E匹配引擎将返回“unknown”，以表示可以满足的任何问题。你的例子就是这种情况吗？ – 2012-07-25 18:10:41

这里是一个链接在线教程战术：http://rise4fun.com/z3/tutorial/strategies，http://rise4fun.com/z3py/tutorial/strategies – 2012-07-25 18:13:06

Z3理论插件错误

回答

相关问题