Failed to load objects of pyprover

Question

Failed to load objects of pyprover

Closed this issue 2 years ago · 4 comments

Hi, this issue is a detailed explanation of my question stackoverflow.
I followed the following advise.

Can you (a) try again, but with dill.detect.trace(True) and print out the traceback? (b) also try changing dill.settings['recurse'] = True to use a serialization variant?

I tryied to use dill to save and load a logical expression of pyprover. However, it failed.
Below is the code I used.

# !pip install pyprover

import dill 
from pyprover import *

logic = ~A & B

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

dill.detect.trace(True)
dill.settings['recurse'] = True

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

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

print(logic2)

And, the output is below.

T4: <class 'pyprover.logic.And'>
INFO:dill:T4: <class 'pyprover.logic.And'>
# T4
INFO:dill:# T4
D2: <dict object at 0x7fc757dba7d0>
INFO:dill:D2: <dict object at 0x7fc757dba7d0>
T4: <class 'pyprover.logic.Not'>
INFO:dill:T4: <class 'pyprover.logic.Not'>
# T4
INFO:dill:# T4
D2: <dict object at 0x7fc757d87f00>
INFO:dill:D2: <dict object at 0x7fc757d87f00>
T4: <class 'pyprover.logic.Prop'>
INFO:dill:T4: <class 'pyprover.logic.Prop'>
# T4
INFO:dill:# T4
D2: <dict object at 0x7fc757d8faf0>
INFO:dill:D2: <dict object at 0x7fc757d8faf0>
# D2
INFO:dill:# D2
# D2
INFO:dill:# D2
D2: <dict object at 0x7fc757d9b190>
INFO:dill:D2: <dict object at 0x7fc757d9b190>
# D2
INFO:dill:# D2
# D2
INFO:dill:# D2
1 ~A & B
2 <class 'pyprover.logic.And'>
3 <class 'pyprover.logic.Prop'>
---------------------------------------------------------------------------
AttributeError                            Traceback (most recent call last)
[<ipython-input-15-9e6a64c3b2be>](https://localhost:8080/#) in <module>
     16 
     17 with open("test.pickle","rb") as f:
---> 18   logic2 = dill.load(f) # error
     19 
     20 print(logic2)

1 frames
[/usr/local/lib/python3.7/dist-packages/dill/_dill.py](https://localhost:8080/#) in load(file, ignore, **kwds)
    371     See :func:`loads` for keyword arguments.
    372     """
--> 373     return Unpickler(file, ignore=ignore, **kwds).load()
    374 
    375 def loads(str, ignore=None, **kwds):

[/usr/local/lib/python3.7/dist-packages/dill/_dill.py](https://localhost:8080/#) in load(self)
    644 
    645     def load(self): #NOTE: if settings change, need to update attributes
--> 646         obj = StockUnpickler.load(self)
    647         if type(obj).__module__ == getattr(_main_module, '__name__', '__main__'):
    648             if not self._ignore:

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

The environment I used is google colabratory.

And the following is the versions of libraries imported in the code and python.

!pip list | grep pyprover  -> 0.6.2
!pip list | grep dill -> 0.3.5.1

import sys
print(sys.version)
# 3.7.13 (default, Apr 24 2022, 01:04:09) 
# [GCC 7.5.0]

I tried to import modules like this but it didn't solve the problem.

import dill 
import pyprover
from pyprover import *
from pyprover.logic import *
from pyprover.parser import *
from pyprover.constants import *
from pyprover.atoms import *
from pyprover.util import *
from pyprover.tools import *
from pyprover.__coconut__ import *
from pyprover.__init__ import *

If any information is missing, please let me know.

Answer 1 · 2022-09-19T12:10:35.000Z

Two observations:

This types of objects are unpickleable (actually "non-loadable") in general, i.e. both for dill and for pickle. Using the object from your example:
```
>>> import pickle
>>> pickle.loads(pickle.dumps(logic))
AttributeError: 'Top' object has no attribute 'elems'
```

The class BinaryOp in pyprover.logic implements a non-trivial __new__() method and should also implement a __reduce_ex__() method to be pickleable. The pickled object's elems attribute should be passed to it as arguments, but the default object.__reduce_ex__() doesn't do it.

How it is with object.__reduce_ex__():

>>> logic.__reduce_ex__(pickle.DEFAULT_PROTOCOL)
(<function copyreg.__newobj__(cls, *args)>,
 (pyprover.logic.And,),
 (None, {'elems': (Not(Prop("A")), Prop("B"))}),
 None,
 None)

How it should be with a custom BinaryOp.__reduce_ex__() method (the two None items at the end are irrelevant):

>>> logic.__reduce_ex__(pickle.DEFAULT_PROTOCOL)
(<function copyreg.__newobj__(cls, *args)>,
 (pyprover.logic.And, Not(Prop("A")), Prop("B")),  <---
 (None, {'elems': (Not(Prop("A")), Prop("B"))}),
 None,
 None)

See how the change fixes it. Reconstructing the object manually as the function load(s) would do:

>>> rv = logic.__reduce_ex__(pickle.DEFAULT_PROTOCOL)
>>> rv = (rv[0], rv[1] + rv[2][1]['elems'], *rv[2:])  # change second item
>>> # below is how pickle processes the reduced value in this case
>>> cls, *args = rv[1]
>>> obj = cls.__new__(cls, *args)
>>> state, slotstate = rv[2]
>>> for name, value in slotstate.items():
...     setattr(obj, name, value)
>>> obj
And(Not(Prop("A")), Prop("B"))

It's really easy to make this class and its subclasses pickleable. You should ask the pyprover devs to implement this or propose it yourself. See https://docs.python.org/3/library/pickle.html#object.__reduce__ for details. But this should suffice (not tested):

class BinaryOp(Expr):
    # __new__(), __init__(), etc.
    def __reduce_ex__(self, protocol):
        if protocol < 2:
            raise NotImplementedError  # legacy format, not covered here
        rv = super().__reduce_ex__(protocol)
        return (rv[0], rv[1] + self.elems, rv[2])

Answer 2 · 2022-09-21T04:01:36.000Z

Thank you very much for the swift reply.
I think I've learned a lot.

Answer 3 · 2022-09-21T20:20:36.000Z

@ryoryon66 Great! I think I just forgot to tell you how I found out that the problem was with the class BinaryOp... Using the logic object from your example:

>>> # First, let inspect the object and its type:
>>> logic
And(Not(Prop("A")), Prop("B"))
>>> cls = type(logic)
>>> cls
pyprover.logic.And
>>> # The object is pickled by calling its __reduce_ex__() method
>>> # (falling back to __reduce__() if the other is not defined).
>>> # What classes 'And' descends from and which one implements it?
>>> cls.__mro__
(pyprover.logic.And,
 pyprover.logic.BoolOp,
 pyprover.logic.BinaryOp,
 pyprover.logic.Expr,
 object)
>>> cls.__reduce_ex__
<method '__reduce_ex__' of 'object' objects>
>>> # So it uses the default __reduce_ex__() from the base class 'object',
>>> # that's why it pickles successfully. Let's see what it returns:
>>> logic.__reduce_ex_(3)
(<function copyreg.__newobj__(cls, *args)>,
 (pyprover.logic.And,),
 (None, {'elems': (Not(Prop("A")), Prop("B"))}),
 None,
 None)
>>> # It uses __newobj__() to recreate the object, which we know, by the
>>> # documentation, that will call And.__new__(). Let's look at it:
>>> cls.__new__
<function pyprover.logic.BinaryOp.__new__(cls, *elems)>

Bingo! There it is: And inherits its __new__() method from the class BynaryOp, which receives elems as expanded arguments. This is missing from the second tuple returned from __reduce_ex__().

I actually inspected the module's source code to understand the problem, but didn't need to in this case.

Answer 4 · 2022-09-22T08:25:10.000Z

Thank you very much for your detailed explanation. I really learned a lot of things I didn't know such as mro. I also learned a lot about analysis methods.