Z3 컨텍스트 직렬화/직렬화 해제?

Question

(C#에서) Z3 컨텍스트를 직렬화/비 직렬화 할 수 있습니까? 그렇지 않은 경우이 기능이 계획되어 있습니까?

이 기능은 실제 응용 프로그램에서 중요하다고 생각합니다.

Answer 1

현재 API에서는 직접 지원되지 않습니다. 다음 릴리스에서는 여러 솔버를 지원하며 하나의 솔버에서 다른 솔버로 어설 션을 복사하고 어설 션을 검색하는 명령을 제공합니다. 이러한 명령을 사용하면 표현식을 파일 (SMT 2.0 형식)에 덤프하여 직렬화를 구현할 수 있습니다. 비 직렬화하려면 파일을 다시 읽습니다. 논리적 컨텍스트에 어설 션 된 어설 션을 추적하는 경우이 솔루션은 이미 현재 API를 사용하여 구현할 수 있습니다.

Z3을 사용하는 많은 프로젝트에서 다음과 같은 접근 방식을 사용했습니다. 그들에는 공식을위한 그들의 자신의 대표가있다. 그들이 Z3을 호출 할 때, 그들은 그들의 표현을 Z3의 표현으로 변환합니다. 대부분의 경우 성능 오버 헤드가 최소화됩니다. 이러한 접근 방식은 많은 유연성을 제공합니다. 직렬화가 좋은 예입니다. 일부 프로그래밍 환경 (예 : Python)은 이미 직렬화에 대한 일부 내장 지원을 제공합니다.