Z3 - 주어진 수식에서 변수를 추출하는 방법?

Question

Z3 C++ API (버전 4.3.1)를 사용 중이고 수식의 변수 (유형이 expr 인 개체)를 추출하고 싶습니다. similar question을 찾았지만 Z3py에 있습니다. Z3 C/C++ API에 expr 개체에서 변수를 추출하는 메서드가 있는지 궁금합니다. 감사! 예를 들어

(일부 생략 된 상세)

expr fs = implies(x + y == 0, z * x < 15); 
    std::vector<expr> varlist = get_vars(fs); 

그럼 varlist는 X, Y, Z를 포함한다.

Answer 1

배포본 (examples/C++/example.cpp)의 C++ 예제는 샘플 방문자 패턴을 보여줍니다. 매우 단순하지만 아이디어를 줄 것입니다.

void visit(expr const & e) { 
if (e.is_app()) { 
    unsigned num = e.num_args(); 
    for (unsigned i = 0; i < num; i++) { 
     visit(e.arg(i)); 
    } 
    // do something 
    // Example: print the visited expression 
    func_decl f = e.decl(); 
    std::cout << "application of " << f.name() << ": " << e << "\n"; 
} 
else if (e.is_quantifier()) { 
    visit(e.body()); 
    // do something 
} 
else { 
    assert(e.is_var()); 
    // do something 
} 
} 

방문자 기능이 있기 때문에 일반적으로 Z3에서 이전에 방문한 표현의 캐시 하위 표현식을 공유 사용합니다 를 사용하여 개선 될 수있다 :

나는 아래 여기를 반복합니다. 이것은 파이썬 예제와 비슷합니다.

희망이 있습니다.