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
335 stars 62 forks source link

When building statically, prefer PicoSAT's archives over its shared objects #45

Closed aytey closed 5 years ago

aytey commented 5 years ago

Currently, when building Boolector with its Python modules, you can only link against PicoSAT if you build a shared (i.e., dynamically linked) Boolector.

This PR modifies Boolector's build system such that you can link PicoSAT even when building Boolector's Python module and linking statically.

It is worth noting that contrib/setup-picosat.sh already builds libpicosat.a and libpicosat.so. All this PR does is prefer linking libpicosat.a over libpicosat.so, when building statically.

mpreiner commented 5 years ago

@andrewvaughanj Sorry this took waay too long... This is now fixed on master with bfeeb67

aytey commented 5 years ago

Let me check!

mpreiner commented 5 years ago

@andrewvaughanj Is this still an issue with current master? I checked it on my machine and it correctly recognizes libpicosat.a.

aytey commented 5 years ago

Oops, I never checked this. I'll try to do this today -- sorry about that!

aytey commented 5 years ago

From https://github.com/Boolector/boolector/commit/f689fbbfe820392d35e26be368f9d87d2dbdb037 (Apr 26):

git checkout f689fbbfe820392d35e26be368f9d87d2dbdb037 && rm -rf build && mkdir build && cd build && cmake .. -DPYTHON=ON -DONLY_PICOSAT=ON

Uses .so!

From https://github.com/Boolector/boolector/commit/113d1d11b8f848b422338099143789ff952721fd (Jul 30):

git checkout 113d1d11b8f848b422338099143789ff952721fd && rm -rf build && mkdir build && cd build && cmake .. -DPYTHON=ON -DONLY_PICOSAT=ON

Uses .a!

Closing issue :)