latest release gives importerror

[Wout4]

The latest release gives an importerror when trying to use the package on linux:

from pycryptosat import Solver

ImportError: undefined symbol: _ZN5CMSat6Solver12oracle_vivifERb

[msoos]

Hi,

Thanks. Oopps. I am at odds with this python thing. I am not 100% sure I want to have it at all.... I'll think about it. It's extremely painful to build and maintain. I'll keep this issue open for now and think about what to do..

Mate

[msoos]

Ah, I think I managed to fix this! Sorry, it's late so it'll have to wait until tomorrow night to have the new package on pypi. But it'll be there and working, yay! Also for mac it seems :)

[GregoryMorse]

Just to note that as of 5.11.23, which as of the time of this message is still in PyPI, this import bug persists, meaning the current version is essentially unusable on Linux at least. Maybe should roll this back to 5.11.21 or update it.

For now the suggested work around is:

python -m pip install pycryptosat==5.11.21

[GregoryMorse]

The problem seems to be that in setup.py there is no reference to src/oracle_use.cpp and hence the bool Solver::oracle_vivif(bool& finished) is not found in the shared library.

[msoos]

Ah okay. I'll look into this tonight!

[msoos]

Oh no, I just spent another evening without realizing and I have no idea what I'm doing. I'm sorry, I just can't. It would take me years to understand the python system. Someone must understand it, but it sure isn't me. I can help write a symbolic execution framework, write a model counter, a SAT solver, but I swear it feels like I have spent effort trying to fix this python project than I have spent on any of those projects. It's incredibly exhausting and I can't find a way to make it work in a sane way. I'm sorry.

I would kindly like to ask you to help. Can you please send a PR to fix this? Or ask someone knowledgeable to help? I can't seem to understand even the problem, and the solutions is waaaay beyond me.

Thanks,

Mate