Windows x64 port

[sfiruch]

Officially-provided windows binaries would be nice. In the meantime, I hacked together a port to Windows (and VC++), and released x64 binaries here:
https://github.com/deiruch/kissat/releases/

The port uses the same PAL as my CaDiCaL port. I replaced the VLAs by alloca, because VLAs are unfortunately still not supported by VC++. Additionally, I had to change some struct members from bool to unsigned to work around the annoying struct packing behavior of VC++.

[a1880]

Porting to Windows might be easier with gcc as compiler under Msys64/MinGW64 in this case. gcc allows for dynamic arrays. To get around bit-field packing problems in watch.h, I had to use the -mno-ms-bitfields compile flag. The resulting binary is about 8% faster than the VC++ binary, at least for my example.

[arminbiere]

It is unlikely that I will support binaries soon (particularly for MacOS / Windows) but I will have a look at the changes you did to make VC++ happy and see whether I can address those issues in a simple way.

[benjaminbartsch]

@deiruch Thank you very much for the executable file, its the only one that worked. I tried to compile kissat and gimsatul myself using cygwin+gcc. It seemed to work but the tests failed.

Would you be so kind and try to compile https://github.com/arminbiere/gimsatul too?

[anhpham197]

@deiruch Can you please add a README file to guide how to use your Kissat version on Windows?

[sfiruch]

@deiruch Can you please add a README file to guide how to use your Kissat version on Windows?

There are no Windows-specific instructions. The Windows port works exactly the same way as the Linux version. If you have specific usage questions, I suggest you create new issues in this repo. If you have Windows-specific questions then you should create an issue in the repo of my Windows port.

[a1880]

Using the wsl2 environment of Windows, many Unix tools can be built without changes.

An overview of how to call Kissat can be found here.

[anhpham197]

Thanks @deiruch , I have some problems with your Windows version, could you please open add issues feature?

[sfiruch]

Thanks @deiruch , I have some problems with your Windows version, could you please open add issues feature?

Ha, stupid me! I only realized now that Issues were disabled in my fork. I enabled the feature. Feel free to create an issue describing the problem here: https://github.com/deiruch/kissat/issues

[anhpham197]

Thanks @deiruch , I have some problems with your Windows version, could you please open add issues feature?

Ha, stupid me! I only realized now that Issues were disabled in my fork. I enabled the feature. Feel free to create an issue describing the problem here: https://github.com/deiruch/kissat/issues

Dear @deiruch , I've opened a new issue on your repo. Hope to receive your ans!

[benjaminbartsch]

@sfiruch : May I ask you, if it would be possible of you to add the exe/dll file of the newest Version (4.0.0)? That would be really really nice.

[sfiruch]

@sfiruch : May I ask you, if it would be possible of you to add the exe/dll file of the newest Version (4.0.0)? That would be really really nice.

There you go: https://github.com/sfiruch/kissat/releases/tag/rel-4.0.0

[benjaminbartsch]

@sfiruch: Thank you sooo much!

[benjaminbartsch]

@sfiruch: The Windows-EXE seems to have a bug (at least in my Windows 10 Version) ... I will open an Issue.

[sfiruch]

@sfiruch: The Windows-EXE seems to have a bug (at least in my Windows 10 Version) ... I will open an Issue.

I think it'd make sense to discuss Windows-specific bugs in the repo of the fork. Also, can you test whether disabling shrinking helps?

[benjaminbartsch]

I opened an Issue in the fork.

But maybe this Information is relevant for further "ports" or other people trying to compile it themselves on windows:

Before crashing (on Windows) verbose shows:

And after using this
--congruence=false

The Windows port does not crash.

After some testing - this also works:
--congruencebinaries=false