Z3의 C++ API를 사용하여 긴 disjunction을 만드시겠습니까?

Question

가변 길이의 분리 문자로 긴 분리를 만드는 데 선호되는 방법은 무엇입니까?

내 생각 엔 이런 일이 (가) expr_vector 최초의 동적 push_back 모든 disjuncts의 다음 어떻게 든 내 분리를 구축하는 Z3_mk_or를 사용하여 사용 가능해야한다는 것입니다.

Z3_ast의 배열을 expr_vector에서 Z3_mk_or의 세 번째 인수로 전달하려면 어떻게해야합니까?

Btw, 하나의 긴 n-ary 분리가 아닌 긴 이진 분리 시퀀스를 만드는 경우 효율성이 저하됩니까?

Answer 1

Z3 C++ API는 expr_vector 개체로부터의 n-ary 분리를 지원하지 않습니다. 이것이 유용한 기능이라는 데 동의하며 다음 Z3 버전에서 추가 할 예정입니다. 다음 코드를 사용하여이 기능을 시뮬레이션 할 수 있습니다. 다음 코드는 expr_vector의 "복사본"을 생성하므로 완벽하지는 않지만 임시 해결 방법으로 사용할 수 있습니다. 앞에서 말했듯이 다음 버전에서는 이러한 종류의 작업에 대한 지원 기능이 내장되어 있으므로 사본을 피할 수 있습니다. 하나 대신 하나의 n 차 하나의 바이너리 disjunctions의 긴 시퀀스를 생성하면 두 번째 질문에 대해서는

는

#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- 차원 형식을 매우 효율적으로 변환 할 수 있습니다.