Z3 솔버에서 C API를 사용하여 메모리 사용량 받기

Question

Z3에서 -st 플래그를 사용하면 Z3의 메모리 소비가 발생합니다. 그러나 나는 C/C++ API을 사용하여 같은 것을 얻고 싶습니다. 누군가 어떻게 할 수 있을까요? API Z3_solver_get_statistics()을 사용한 다음 Z3_stats_to_string()을 사용해 보았습니다. 그러나 결과 문자열에는 메모리에 대한 정보가 없습니다.

감사합니다.

Answer 1

이 기능은 Z3 API에서 노출되지 않습니다. 이 정보는

static unsigned long long get_allocation_size(); 

memory 클래스로 얻을 수 있습니다. 이 방법은 src/util/memory_manager.h 파일에 정의되어 있습니다. 아이디어는이 값을 반환하는 Z3 API에 새로운 함수를 추가하는 것입니다. Z3 정적 라이브러리를 사용하는 경우 memory_manager.h을 포함하여이 방법에 직접 액세스 할 수 있다고 생각합니다.