z3에서 해결해야 할 몇 가지 제약이 있습니다. 통계를 출력하는 "--st"명령 행 플래그를 알고 있지만, 결국에는 내부 데이터 구조 값을 출력하기위한 TRACE 기능을 알고 있습니다. z3에서 진단 정보를 얻는 방법이 있습니까 (예 : 메모리 사용을 지속적으로 모니터) (ps와 같은 외부 도구는 항상 편리하지 않고 항상 목적을 수행하지는 못합니다). 명령 줄? 감사.z3 메모리 사용 특성 모니터링
-v:100 옵션을 사용할 수 있으며 자세한 표시 수준을 100으로 설정합니다. 원하는만큼 자주 메모리 사용량을 표시하지 못할 수 있습니다. 또 다른 옵션은 적절한 위치에 다음 코드 줄을 추가하는 것입니다.
timeit tt(get_verbosity_level() >= 3, "report");
자세한 표시 수준이 >= 3이면 메모리 사용이 표시됩니다. 예를 들어, 좋은 방법은 lbool context::bounded_search()src/smt/smt_context.cpp에있는 방법의 시작 부분에 있습니다. 이 메소드는 다시 시작할 때마다 실행됩니다.