使用 Z3 的 C++ API 创建长析取

Create a long disjunction using the C++ api of Z3?

本文关键字：创建 API Z3 C++ 使用      更新时间：2023-10-16
创建

具有可变数量的析取的长析取的首选方法是什么？

我的猜测是，使用expr_vector首先动态push_back所有析取，然后以某种方式使用Z3_mk_or来构建我的析取，应该可以像这样的事情

。

但是我怎样才能从expr_vector中获取Z3_ast数组作为第三个参数传递给Z3_mk_or？

顺便说一句，如果创建一个长序列的二进制析取，而不是一个长 n 元析取，是否有任何效率损失？

Z3 C++ API 不支持从expr_vector对象创建 n 元析取。我同意这是一个有用的功能，我将在下一个 Z3 版本中添加它。可以使用以下代码段模拟此功能。以下代码并不完美，因为它创建了expr_vector的"副本"，但它可以用作临时解决方法。正如我上面所说，下一个版本将内置对这种操作的支持，并且将避免复制。

#include<vector>
#include<z3++.h>
using namespace z3;
expr mk_or(expr_vector args) {
    std::vector<Z3_ast> array;
    for (unsigned i = 0; i < args.size(); i++) 
        array.push_back(args[i]);
    return to_expr(args.ctx(), Z3_mk_or(args.ctx(), array.size(), &(array[0])));
}
int main() {
    context      c;
    expr_vector  args(c);
    args.push_back(c.bool_const("p"));
    args.push_back(c.bool_const("q"));
    args.push_back(c.bool_const("r"));
    std::cout << mk_or(args) << std::endl;
    return 0;
}

关于你的第二个问题，如果创建一个长序列的二进制析取而不是单个n元析取，则不会有明显的性能损失。在内部，Z3 可以非常有效地在二进制和 n 元格式之间进行转换。

相关文章：