c++ - 使用 Z3 的 C++ api 创建长析取？

Question

用可变数量的析取创建长析取的首选方法是什么？

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

但是我怎样才能得到Z3_ast's的数组expr_vector作为第三个参数传递给Z3_mk_or？

顺便说一句，如果创建一个长序列的二元析取而不是一个长的 n 元析取，是否会降低效率？

Answer 1

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 元格式之间进行转换。