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

Linking MinGW build with MSVC #151

Closed rafaelsamenezes closed 2 years ago

rafaelsamenezes commented 3 years ago

I followed the instruction to build Boolector in Windows and was able to generate the .a files. However, I wish to use both MSVC and Clang (on Windows), can I do this or I will have to use MinGW when using Boolector?

aytey commented 3 years ago

What are you trying to do? Do you mean you want to link in Boolector (statically) into a project compiled with MSVC?

Can you do something like this: https://stackoverflow.com/a/2139061 ?

aytey commented 3 years ago

... or, do you want to build Boolector itself "natively" with MSVC?

rafaelsamenezes commented 3 years ago

What are you trying to do? Do you mean you want to link in Boolector (statically) into a project compiled with MSVC?

Yes, it doesn't need to be static.

Can you do something like this: https://stackoverflow.com/a/2139061 ?

This helped me to compile it, but it crashes when running I am assuming that the runtime library from mingw does not have the same memory model than MSVC.

Another approach that I tested was this: http://www.mingw.org/wiki/msvc_and_mingw_dlls I made some changes on src/CMakeLists.txt to add the linker flags into boolector and managed to export both .def and converted it into .dll but still had some issues when linking.

I also tried to build boolector as a shared library (by replacing EXTRA_FLAGS with shared) but the build process fails.

aytey commented 3 years ago

So, this process must be possible because I can compile pyboolector.pyd (which is a DLL!) and load it against the MSVC-compiled Python interpreter (the official Python releases are compiled with MSVC).

I made some changes on src/CMakeLists.txt to add the linker flags into boolector and managed to export both .def and converted it into .dll but still had some issues when linking.

Can you give the error? This seems like a sensible approach, but you might also need to link the libs for the solvers too (e.g., for Lingeling).

aytey commented 3 years ago

@rafaelsamenezes any luck with this? Let us know if you need any assistance (or if you got it working!).

rafaelsamenezes commented 3 years ago

Sorry for the delay... I couldn't work on this in the last month so I don't have any updates.

I may try this again at the end of November.

aniemetz commented 2 years ago

Closed due to inactivity.