lsils / bill

C++ header-only reasoning library
MIT License
11 stars 6 forks source link

Incompatibility with Alpine Linux #40

Closed marcelwa closed 3 years ago

marcelwa commented 3 years ago

Hi,

I started deploying my software, which uses the EPFL Logic Synthesis Libraries, via Docker. I want to use Alpine Linux for image size reasons. As its standard C library, Alpine Linux uses musl libc instead of glibc and, therefore, does not include certain headers that glibc provides. One of which is fpu_control.h that is used in the ghack SAT solver here.

Its include is guarded by an #if defined(__linux__), but should probably be #if defined(__GLIBC__) from features.h. I don't know whether that would break anything though.

I'm not using bill directly but since it's included in mockturtle, it is affecting me.

Thank you for your help! -- Marcel

hriener commented 3 years ago

I cannot see that any of the FPU macros are used in the code. At first sight, it looks almost safe to remove the include.

hriener commented 3 years ago

Second look: This line seems to come from the original MiniSAT code [1] and is included in all the SAT solvers derived from MiniSAT. [1] https://github.com/niklasso/minisat/blob/master/minisat/utils/System.h#L25

The FPU macros are used in MiniSAT solver in the function "setX86FPUPrecision":

..//minisat/minisat/core/Main.cc:        setX86FPUPrecision();
..//minisat/minisat/utils/System.h:extern void   setX86FPUPrecision(); // Make sure double's are represented with the same precision
..//minisat/minisat/utils/System.cc:void Minisat::setX86FPUPrecision()
..//minisat/minisat/utils/System.cc:#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
..//minisat/minisat/utils/System.cc:    // Only correct FPU precision on Linux architectures that needs and supports it:
..//minisat/minisat/utils/System.cc:    _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
..//minisat/minisat/utils/System.cc:    printf("WARNING: for repeatability, setting FPU to use double precision\n");
..//minisat/minisat/simp/Main.cc:        setX86FPUPrecision();

It seems that we don't have this part in bill.

marcelwa commented 3 years ago

Thanks for your investigation. Does that mean that you will remove the include from bill to ensure compatibility with Alpine Linux?

hriener commented 3 years ago

The request is reasonable and I don't see that it would hurt us to remove these lines. If you are in a hurry I would accept your PR or otherwise fix it eventually by myself.

hriener commented 3 years ago

Fixed in #42