0

那里当我从 smtlib2 实例中获得 unsat cores 时，我将它们拆分为一个子句，例如（not (>=::Int x1))。然后我尝试将该子句添加到 z3 以再次解决。但是问题发生了被遵守后。

警告：无效的函数应用，位置 1 的参数排序不匹配警告：（定义非 Bool Bool）应用于：（非（<= 0::Int x6））排序 Bool

expr F = to_expr(ctx,f);
solver s(ctx);`
expr_vector todo(c);
vector<expr> u;
todo.push_back(F);
while (!todo.empty()) {
    expr current = todo.back();
    todo.pop_back();
    if (current.decl().decl_kind() == Z3_OP_AND) {
         for (unsigned i = 0; i < current.num_args(); i++) {
             u.push_back(current.arg(i));
          }
    }
}
for(i=0;i<u.size();i++){
    expr r = to_expr(ct.,Z3_mk_not(ctx,u[i]));
    s.add(r);
}
if(s.check() == sat){
    model m = s.get_model();
}else if(s.check() == unsat){
    expr_vector core = s.unsat_core();
}

你能帮帮我吗？非常感谢。

4

1 回答 1

2

你没有提供完整的例子。所以，很难准确。我的猜测是您正在混合来自不同 Z3 上下文的表达式。下面这段代码非常可疑：

solver s(ctx);
expr_vector todo(c);

看来您有两个 Z3 上下文：ctx和c. 一个上下文中的表达式和公式不能用于不同的上下文。我们必须将它们从一种上下文翻译到另一种上下文（API: Z3_translate）。这是一个“高级”功能。大多数用户不需要多个上下文。我强烈建议您使用单一上下文。

此外，您似乎正在尝试从 Stackoverflow 上可用的不同现有帖子中“粘合”代码片段。但是，生成的代码似乎很奇怪。你基本上得到了一个公式f，在 -loop 中提取它的合取词while，然后在 -loop 中断言它们中的每一个的否定for。也就是说，如果f是公式

A and B and C

您的程序在求解器中断言以下文字s:(Not A)和. 那是你真正想要的吗？(Not B)(Not C)

为什么要使用双循环？您可以在 -loop 中断言否定while，并避免使用辅助向量u。

check另一个问题，您在不提供假设的情况下调用。因此，该unsat_core方法将返回空向量。请查看examples/c++/example.cppZ3 发行版文件中的 unsat-core 示例。

请记住，Z3 具有适用于 Python 和 .Net 等托管语言的 API。它们比 C++ 更容易使用。我们有几个Z3 Python API教程。

于 2012-12-10T17:17:17.063 回答