Создайте длинную дизъюнкцию, используя C++ api Z3?

Question

Что было бы предпочтительным способом создания длинной дизъюнкции с переменным количеством дизъюнкций?

Я думаю, что что-то подобное должно быть возможным с помощью expr_vector на первый динамически push_back все дизъюнктов, а затем каким-то образом использовать Z3_mk_or строить свою дизъюнкции.

Но как я могу получить массив Z3_ast с expr_vector, чтобы передать третий аргумент Z3_mk_or?

Btw, есть ли штраф эффективности, если вы создаете длинную последовательность двоичных дизъюнкций, а не одну длинную n-арную дизъюнкцию?

Answer 1

Z3 API C++ не поддерживает создание n-арной дизъюнкции от объекта expr_vector. Я согласен, что это полезная функция, и я добавлю ее в следующую версию 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; 
} 

Что касается вашего второго вопроса, то есть нет значительного снижения производительности, если один создает длинную последовательность двоичных дизъюнкции вместо одного п-арной один. Внутренне Z3 может эффективно конвертировать между бинарными и n-арными форматами.