Это не поддерживается напрямую в текущем API. Следующий выпуск будет поддерживать несколько решателей, и мы предоставим команды для копирования утверждений из одного решателя в другой и извлечения утверждений. С помощью этих команд можно реализовать сериализацию, выгружая выражения в файл (в формате SMT 2.0). Для десериализации мы просто читаем файл обратно.
Обратите внимание, что это решение уже может быть реализовано с использованием текущего API, если вы отслеживаете утверждения, которые вы утверждали в логическом контексте.
При этом я видел следующий подход, используемый во многих проектах, использующих Z3. У них есть собственное представление для формул. Когда они вызывают Z3, они переводят свое представление в представление Z3. В большинстве случаев издержки производительности минимальны. Такой подход дает им большую гибкость. Сериализация является хорошим примером. Некоторые среды программирования (например, Python) уже предоставляют некоторую встроенную поддержку сериализации.