search

sambayless / monosat

MonoSAT - An SMT solver for Monotonic Theories
MIT License
106 stars 29 forks source link

Use of `_FPU_EXTENDED`/`_FPU_DOUBLE` is x86/x87-specific #33

Open risicle opened 2 years ago

risicle commented 2 years ago

Hi,

Main.cc tries to disable the x87 extended precision mode @ https://github.com/sambayless/monosat/blob/55af2fbf15b628eddfd74675d469689613c2a9dc/src/monosat/Main.cc#L550

But this is platform-specific and compilation fails on aarch64 linux:

/build/source/src/monosat/Main.cc:550:27: error: '_FPU_EXTENDED' was not declared in this scope
  550 |         newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
      |                           ^~~~~~~~~~~~~
/build/source/src/monosat/Main.cc:550:44: error: '_FPU_DOUBLE' was not declared in this scope
  550 |         newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
      |                                            ^~~~~~~~~~~

Full build log: https://hydra.nixos.org/log/gdvq3inxzcyinf032y7vwrdm1lncnw4z-monosat-1.8.0.drv

I've worked around it by patching it out, but it would be better to detect this somehow. Platforms like aarch64 do seem to have an fpu_control.h, possibly for backward compatibility, but they don't seem to have _FPU_EXTENDED or _FPU_DOUBLE defined. So possibly you could actually check for those being defined to enable/disable this block.

Although documentation around this suggests that the C99 standard fenv.h should be used these days in preference to use of fpu_control.h at all, so.. :shrug:

sambayless commented 2 years ago

I see that recent versions of minisat guard this setting the way you've suggested:

https://github.com/niklasso/minisat/blob/master/minisat/utils/System.cc#L100

#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)

I should be able to update to use the same checks