HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
607 stars 132 forks source link

Fixed C++ compilation failure of zc2hs on macOS #1254

Closed binghe closed 2 weeks ago

binghe commented 2 weeks ago

Hi,

Once again, with help of @oskarabrahamsson (#1233, also see #985 for the last time), the failure of C++ compilation of zc2hs on macOS with Apple's clang++ is now fixed. I can only guess that, the following template function is too general to create a conflict with some other (internal) definitions:

template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }

There are only two places where this overloaded operator != is actually used. By rewriting them to !(x == y), I'm sure the semantics doesn't change, and the compilation error is gone.

Let's see when these C++ code will be broken again:)

--Chun

P.S. In src/HolSat/sat_solvers/zc2hs/Makefile, I followed the idea of Minisat's Makefile to use $(MINISAT_CXX) (with a default value c++) instead of the explicit g++. On potential *unix systems without GCC but with other C/C++ compilers, the command g++ may not be available while c++ should exist. (I have been using the command Makefile MINISAT_CXX=g++-mp-13 to compile zc2hs manually for quite several months.)

mn200 commented 2 weeks ago

Thanks for this!