search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Instructions and fixes for a 64-bit Windows build #88

Closed jix closed 4 years ago

jix commented 4 years ago

This adds a COMPILING_WIN64.md file, adapted from COMPILING_WIN32.md, containing updated instructions for a 64-bit Windows build using Python 3.

It also adds a workaround for building CaDiCaL on Windows. CaDiCaL's source tar contains a symlink that cannot be extracted on Windows. The build script now ignores that file when extracting on Windows, it isn't required for a successful build.

The resulting build hasn't been tested extensively, but it successfully runs the included Python API examples.

Signed-off-by: Jannis Harder me@jix.one

aytey commented 4 years ago

Hi!

I think we should just merge the Win32/Win64 steps -- maybe even update them to be Python3?

Also, I've never had the issue about CaDiCaL not extracting under MSYS -- can you provide some more details on that?

Cheers,

Andrew

aytey commented 4 years ago

Ha! Probably should have looked closer ... these are already Python3 -- which is awesome!

I wonder if we should just replace the Win32 instructions with your undated Win64 ones? I no longer "need" Win32 instructions, and Win64 is good for me (I just hadn't got around to updating the repo).

Cheers,

Andrew

aytey commented 4 years ago

Another question, I haven't tried it recently, but:

python examples/api/python/api_usage_examples.py

Used to hang on Windows when doing the quantifier stuff (right at the bottom of the script). Does this script now terminate "quickly" for you?

jix commented 4 years ago

During untar I get this error message:

tar: cadical-cb89cbfa16f47cb7bf1ec6ad9855e7b6d5203c18/src/makefile: Cannot create symlink to ‘../makefile’: No such file or directory
tar: Exiting with failure status due to previous errors

I don't need win32 either, and don't have time to test that currently, so I didn't merge them as I didn't want to accidentally break the instructions for 32-bit builds, so replacing them would be fine for me too.

It does hang when I use lingeling, it works fine when using cadical (which seems to be the default when cadical is compiled in).

mpreiner commented 4 years ago

Yes, let's just switch over to win64 and get rid of win32 if no one needs it anymore.

jix commented 4 years ago

I've updated the commit to replace the 32-bit build guide with a 64-bit one. Let me know if any other changes are required.

mpreiner commented 4 years ago

@andrewvaughanj since you needed the initial 32-bit build, would you mind testing the 64-bit version?

aytey commented 4 years ago

I've opened-up this PR to clean-up these instructions: https://github.com/jix/boolector/pull/1

Important commits:

jix commented 4 years ago

I'm not working with Windows anymore (I only did so for a previous job), so I'm probably not the right person to continue with this.

If you want I could merge your changes into my pull request as is, but to me it seems better if you'd open a pull request to the upstream repository directly and I just close this pull request.

aytey commented 4 years ago

@jix I opened-up https://github.com/Boolector/boolector/pull/138 which is a PR I am the author of this. Can you close this one?

Just to confirm: your initial commit is included in my PR :)