Z3上下文序列化/反序列化？

Question

是否可以序列化/反序列化Z3上下文（來自C＃）？ 如果沒有，該功能是否計劃？

我認爲這個功能對真實世界的應用很重要。

Answer 1

這在當前API中不直接支持。下一個版本將支持多個求解器，我們將提供命令將斷言從一個求解器複製到另一個求解器，並檢索斷言。使用這些命令，可以通過將表達式轉儲到文件中（以SMT 2.0格式）來實現序列化。要反序列化，我們只是讀迴文件。 請注意，如果您跟蹤您斷言的邏輯上下文中的斷言，則可以使用當前API實現此解決方案。

這就是說，我見過以下方法在許多使用Z3的項目中使用。他們有自己的公式表示。當他們調用Z3時，他們將它們的表示轉換爲Z3的表示。在大多數情況下，性能開銷很小。這種方法給了他們很大的靈活性。序列化就是一個很好的例子。一些編程環境（例如Python）已經爲序列化提供了一些內置支持。