如何使用pickle保存pyprover逻辑表达式对象？

问题场景 #

尝试用pickle保存pyprover生成的逻辑表达式时，反序列化阶段出现AttributeError: 'Top' object has no attribute 'elems'错误，代码及报错如下：

测试代码 #

!pip install pyprover
import pickle
from pyprover import *

logic = ~A & B

print(1,logic)
print(2,type(logic))
print(3,type(A))

with open("test.pickle","wb") as f:
  pickle.dump(logic,f)

with open("test.pickle","rb") as f:
  logic2 = pickle.load(f) # error

print(logic2)

运行报错 #

1 ~A & B
2 <class 'pyprover.logic.And'>
3 <class 'pyprover.logic.Prop'>
---------------------------------------------------------------------------
AttributeError                            Traceback (most recent call last)
<ipython-input-27-4cd4fe38fcb4> in <module>
     12 
     13 with open("test.pickle","rb") as f:
---> 14   logic2 = pickle.load(f) # error
     15 
     16 print(logic2)

AttributeError: 'Top' object has no attribute 'elems'

解决方案 #

方法一：字符串中转序列化（推荐，无需修改库） #

利用pyprover逻辑表达式可转为字符串、且字符串可通过eval还原的特性，先将表达式转为字符串再序列化，加载时反向解析：

!pip install pyprover
import pickle
from pyprover import *

logic = ~A & B

# 保存：将表达式转为字符串后pickle
with open("test.pickle","wb") as f:
  pickle.dump(str(logic), f)

# 加载：读取字符串后用eval还原
with open("test.pickle","rb") as f:
  logic_str = pickle.load(f)
  logic2 = eval(logic_str)

print(logic2)  # 输出：~A & B
print(type(logic2))  # 输出：<class 'pyprover.logic.And'>

方法二：为Top类添加pickle支持（从根源修复） #

报错原因是pyprover的Top类未实现pickle所需的序列化方法，导致反序列化时误将其当作包含elems属性的对象处理。可手动为Top类添加__getstate__和__setstate__方法：

!pip install pyprover
import pickle
from pyprover import *
from pyprover.logic import Top

# 为Top类添加pickle支持
def top_getstate(self):
    return {}  # Top是单例，无需保存状态

def top_setstate(self, state):
    pass  # 加载时直接使用单例实例

Top.__getstate__ = top_getstate
Top.__setstate__ = top_setstate

logic = ~A & B

# 正常序列化/反序列化
with open("test.pickle","wb") as f:
  pickle.dump(logic,f)

with open("test.pickle","rb") as f:
  logic2 = pickle.load(f)

print(logic2)  # 输出：~A & B

内容的提问来源于stack exchange，提问作者ryoryon66