z3 :: expr이 할당되었는지 확인하는 방법

Question

나는 C++ 인터페이스를 통해 z3을 사용하고 있습니다. z3 :: expr은 기본 변수/상수 (c.real_const, c.real_val) 또는 표현식이 될 수 있습니다. 나는 종종 z3 :: expr을 사용하여 발생하는 오류가 발생했습니다. 문제는 다음 코드에 의해 설명 될 수 있습니다 : 루프가 전혀 실행되지

z3::context c; 
z3::expr exp(c); 
for(...){ 
    exp=...; 
} 
cout<<exp; 

경우에, 나는 오류가 발생합니다. 그 이유는 특급이 할당되지 않는다는 것입니다. z3 :: expr 변수가 할당되었는지 여부를 어떻게 확인할 수 있습니까?

Answer 1

expr 클래스는이 목적으로 사용할 수있는 bool() 연산자가있는 ast에서 파생됩니다. 이것은 우리가 단순히

if (exp) 
    cout << exp; 

을 (: return m_ast != 0; 내부적으로 표현하고하는 AST는 단순히 포인터, 포인터가 0이 될 때마다 그들이 유효해야하므로 부울() 연산자는 단순히 제로가 아닌 포인터를 확인합니다) 쓸 수 있다는 것을 의미합니다.