arminbiere / cadical

CaDiCaL SAT Solver
MIT License
379 stars 133 forks source link

Issue with `isinf` under `-std=c++0x` #11

Closed aytey closed 5 years ago

aytey commented 5 years ago

Hi,

I just tried to compile CaDiCaL for 64-bit Linux using GCC 4.9.4, but I received the following error:

../src/analyze.cpp: In member function ‘void CaDiCaL::Internal::bump_score(int)’:
../src/analyze.cpp:86:23: error: call of overloaded ‘isinf(double&)’ is ambiguous
   if (isinf (new_score)) {

it seems it is related to this:

My solution was to insert the following at the top of src/analyze.cpp:

#ifndef isinf
#if __cplusplus <= 199711L  // c++98 or older
#  define isinf(x) ::isinf(x)
#else
#  define isinf(x) std::isinf(x)
#endif
#endif

It would be awesome if this is a change that could be made in master (I haven't raised a PR, as I'm aware of what's in CONTRIBUTING).

Cheers,

Andrew

arminbiere commented 5 years ago

Worse, this (re)appeared when trying to port to MacOS (there are 'std::isinf', '::isinf' and on some systems 'isinf' is a macro). I was travelling and had a fast fix for MacOS compilation. I plan to simply remove the 'isinf' test. It is the most elegant solution for that part of the code, but since robust porting is more important, I will just add a hard limit for the bumping overflow (as in older solvers and MiniSAT does). I will keep this open until I have time to fix it.

aytey commented 5 years ago

No worries! Great to know that an official fix is coming "in time"!

Cheers,

Andrew

arminbiere commented 5 years ago

Now, fixed as in the old EVSIDS code of MiniSAT (hard limit of 1e150 which is half the maximum represetable 64-bit double).