msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
815 stars 178 forks source link

Adding Special Flags for windows environment. #760

Open deepeshchugh opened 2 months ago

deepeshchugh commented 2 months ago

Hi, Im facing difficulty modifying the setup.py for the python port on a windows machine since an install of the dependency gmp (gmpxx.h linked with gmp.h) is not straightforward.

Additionally. Even on taking roundabout ways to install it like using WSL, im getting this error (and similar ones): error C2039: 'end_getting_small_clauses': is not a member of 'CMSat::SATSolver'

Not sure how to approach debugging this, any advice is appreciated.

Thanks,

deepeshchugh commented 2 months ago

Hi,

I have resolved the issue on my end, The main problem was me attempting to build the github repo directly and not the corresponding release tar like in the root folder readme.

Would recommend adding two things to simplify for future users:

  1. External readme has first step as download corresponding tarball from Releases section in repo
  2. Adding prerequisite of building a release in the python installation/build readme.

Thanks,

msoos commented 2 months ago

Ah, glad you managed to compile under Windows! Can you maybe create a pull request for the changes you mention? I'd be happy to merge it :)

deepeshchugh commented 2 months ago

Raised the pull request like mentioned above ^

For future windows users Ill mention the sequence I use for building using wsl here (tried and tested) although a simpler way is likely to exist:

  1. Download the Tarball to your local system
  2. In WSL navigate to the project directory you want to build cryptominisat in using the windows directory mount.
  3. Follow the root readme instructions to build and install (I had gmp externally installed if you face any issues there you can download it into one of your source directories from: https://gmplib.org/ prior to the cmake*). Additionally i moved the tarball to the folder to unpack using windows.
  4. Do the python build using windows command line (I use pip install -e . in the directory with setup.py). For me the linux build didnt work as expected but I didnt attempt any debugging since the windows build worked off the bat.

* - edit after more building

deepeshchugh commented 2 months ago

Hi @msoos ,

I tried recompiling after pulling for the other memory issue : https://github.com/msoos/cryptominisat/issues/761

After failing there I tried using the new release you recently put up. But got the same error both times (similar to the one mentioned in this issue):

python/src/pycryptosat.cpp(232): error C2039: 'start_getting_small_clauses': is not a member of 'CMSat::SATSolver' C:\Users\deepe\OneDrive\Documents\Notes\Personal_Project\new-try\cryptominisat-5.11.22\python\src../../src/cryptominisat.h(38): note: see declaration of 'CMSat::SATSolver' python/src/pycryptosat.cpp(250): error C2039: 'get_next_small_clause': is not a member of 'CMSat::SATSolver'
C:\Users\deepe\OneDrive\Documents\Notes\Personal_Project\new-try\cryptominisat-5.11.22\python\src../../src/cryptominisat.h(38): note: see declaration of 'CMSat::SATSolver' python/src/pycryptosat.cpp(281): error C2039: 'end_getting_small_clauses': is not a member of 'CMSat::SATSolver'
C:\Users\deepe\OneDrive\Documents\Notes\Personal_Project\new-try\cryptominisat-5.11.22\python\src../../src/cryptominisat.h(38): note: see declaration of 'CMSat::SATSolver'

I retried the same steps as above with release 5.11.21 and it works, not sure what change is breaking.

Thanks, Deepesh

P.S. Can you tell me the last release without the memory bug you fixed recently so I can use that for my project in the meantime.?

msoos commented 2 months ago

I am working on this. Will be done by today. Sorry.

msoos commented 2 months ago

Hi,

I have now uploaded a pypi package. However, I cannot make Windows work. CaDiCaL and Cadiback would need to somehow work on windows, and then the GMP bignum library would need to be compiled for windows, too. All of these are SUPPOSED to work, but it'd take me several days to do it, and I don't have the Windows environment to be able to do that. If you'd like to experiment and make it work, you are more than welcome. If you have a look at the latest pypi build script, it's actually VERY simple. So it may be very easy to fix for windows:

https://github.com/msoos/cryptominisat/blob/5a30185ab6319aa937d43d5fa3c44f2111be808a/.github/workflows/python-wheel-build.yml#L13

msoos commented 2 months ago

The changes relative to the old one are:

With Linux this is fine. Windows and Mac are always special in their ways :)

msoos commented 2 months ago

I have very little time left to do things. So if you create a Pull Request that fixes the issue with Windows, I'd be super happy. However, I can't do this myself, it's just too much work. I hope that's understandable,

Mate

deepeshchugh commented 2 months ago

Thanks for the quick response as always, I noticed you fixed the import issue in another issue here: https://github.com/msoos/cryptominisat/issues/763

I think thats likely similar to what im facing since the build was previously working in windows (with Cadical and Cadiback built using wsl) and I'm having the same error. Ill try that one the coming Tuesday. I'll close this issue once I verify its working as expected

ill check the pypi thing then as well, however I'm also busy with a project (the one where im using this library) so it might take me a while to get to the actual solution. I recommend recording the last known stable version for windows being 5.11.21 in the meanwhile.

Thanks, Deepesh