C++ compilation failure of src/HolSat/sat_solvers/zc2hs on macOS

[binghe]

I think this issue is new on macOS 14 (Sonoma) with latest Xcode (I'm using version 15.3). Apple's c++ (clang++) cannot compile src/HolSat/sat_solvers/zc2hs/zc2hs.cpp:

src/HolSat/sat_solvers/zc2hs$ make
ln -fs ../minisat/Proof.o
ln -fs ../minisat/File.o
ln -fs ../minisat/File.h
ln -fs ../minisat/Proof.h
ln -fs ../minisat/Global.h
ln -fs ../minisat/Sort.h
ln -fs ../minisat/SolverTypes.h
In file included from zc2hs.cpp:2:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/iostream:43:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/ios:222:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__locale:15:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/shared_ptr.h:30:
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/uninitialized_algorithms.h:613:19: error: use of overloaded operator '!=' is ambiguous (with operand types 'std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>' and 'std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>')
  while (__first1 != __last1) {
         ~~~~~~~~ ^  ~~~~~~~
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1035:27: note: in instantiation of function template specialization 'std::__uninitialized_allocator_move_if_noexcept<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >' requested here
    __v.__begin_   = std::__uninitialized_allocator_move_if_noexcept(
                          ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1620:5: note: in instantiation of member function 'std::vector<std::pair<enum_ty, std::vector<int> > >::__swap_out_circular_buffer' requested here
    __swap_out_circular_buffer(__v);
    ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1648:9: note: in instantiation of function template specialization 'std::vector<std::pair<enum_ty, std::vector<int> > >::__push_back_slow_path<std::pair<enum_ty, std::vector<int> > >' requested here
        __push_back_slow_path(std::move(__x));
        ^
zc2hs.cpp:53:15: note: in instantiation of member function 'std::vector<std::pair<enum_ty, std::vector<int> > >::push_back' requested here
    pclauses->push_back(make_pair(ROOT,lits));
              ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__iterator/reverse_iterator.h:235:1: note: candidate function [with _Iter1 = std::pair<enum_ty, std::vector<int> > *, _Iter2 = std::pair<enum_ty, std::vector<int> > *]
operator!=(const reverse_iterator<_Iter1>& __x, const reverse_iterator<_Iter2>& __y)
^
./Global.h:266:39: note: candidate function [with T = std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>]
template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
                                      ^
In file included from zc2hs.cpp:2:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/iostream:43:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/ios:222:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__locale:15:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/shared_ptr.h:30:
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/uninitialized_algorithms.h:523:18: error: use of overloaded operator '!=' is ambiguous (with operand types 'std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >' and 'std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >')
  for (; __first != __last; ++__first)
         ~~~~~~~ ^  ~~~~~~
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/uninitialized_algorithms.h:535:10: note: in instantiation of function template specialization 'std::__allocator_destroy<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >, std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> > >' requested here
    std::__allocator_destroy(__alloc_, std::reverse_iterator<_Iter>(__last_), std::reverse_iterator<_Iter>(__first_));
         ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__utility/exception_guard.h:86:7: note: in instantiation of member function 'std::_AllocatorDestroyRangeReverse<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >::operator()' requested here
      __rollback_();
      ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/uninitialized_algorithms.h:612:7: note: in instantiation of member function 'std::__exception_guard_exceptions<std::_AllocatorDestroyRangeReverse<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> > >::~__exception_guard_exceptions' requested here
      std::__make_exception_guard(_AllocatorDestroyRangeReverse<_Alloc, _Iter2>(__alloc, __destruct_first, __first2));
      ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1035:27: note: in instantiation of function template specialization 'std::__uninitialized_allocator_move_if_noexcept<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >' requested here
    __v.__begin_   = std::__uninitialized_allocator_move_if_noexcept(
                          ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1620:5: note: in instantiation of member function 'std::vector<std::pair<enum_ty, std::vector<int> > >::__swap_out_circular_buffer' requested here
    __swap_out_circular_buffer(__v);
    ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1648:9: note: in instantiation of function template specialization 'std::vector<std::pair<enum_ty, std::vector<int> > >::__push_back_slow_path<std::pair<enum_ty, std::vector<int> > >' requested here
        __push_back_slow_path(std::move(__x));
        ^
zc2hs.cpp:53:15: note: in instantiation of member function 'std::vector<std::pair<enum_ty, std::vector<int> > >::push_back' requested here
    pclauses->push_back(make_pair(ROOT,lits));
              ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__iterator/reverse_iterator.h:235:1: note: candidate function [with _Iter1 = std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, _Iter2 = std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>]
operator!=(const reverse_iterator<_Iter1>& __x, const reverse_iterator<_Iter2>& __y)
^
./Global.h:266:39: note: candidate function [with T = std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >]
template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
                                      ^
2 errors generated.
make: *** [zc2hs] Error 1

The failure of building this zc2hs (what is it?) doesn't break the entire HOL builds (it seems not used when building core theories), but if you rebuild HOL (even without modifying any code), the building process will restart from generating numheap (a huge waste of time).

Using MacPorts's gcc13 (/opt/local/bin/g++-mp-13), this code can still be compiled without any modification.

I'm no expert to solve this C++ standard compatibility issue.

[binghe]

I suggest at least changing the Holmakefile inside zc2hs folder to the following:

# this assumes minisat's already been built in ../minisat

all: zc2hs

CXX = $(or $(MINISAT_CXX),c++)

zc2hs: 
	ln -fs ../minisat/Proof.o
	ln -fs ../minisat/File.o
	ln -fs ../minisat/File.h
	ln -fs ../minisat/Proof.h
	ln -fs ../minisat/Global.h
	ln -fs ../minisat/Sort.h
	ln -fs ../minisat/SolverTypes.h
	@$(CXX) -O3 Proof.o File.o zc2hs.cpp -o zc2hs

clean:
	@rm -f zc2hs *.h *.o

So that manually calling make MINISAT_CXX=g++-mp-13 could work.

[oskarabrahamsson]

The error comes from these: https://github.com/HOL-Theorem-Prover/HOL/blob/develop/src/HolSat/sat_solvers/minisat/Global.h#L264.

I don't know what this nonsense is and I suspect you could safely delete the definitions within the #ifdef, but you could try to pass -D__SGI_STL_INTERNAL_RELOPS and see if it actually improves the situation first.

[binghe]

The error comes from these: https://github.com/HOL-Theorem-Prover/HOL/blob/develop/src/HolSat/sat_solvers/minisat/Global.h#L264.

I don't know what this nonsense is and I suspect you could safely delete the definitions within the #ifdef, but you could try to pass -D__SGI_STL_INTERNAL_RELOPS and see if it actually improves the situation first.

Thanks for your investigations. Completely commenting all the 4 definitions doesn't work (even Minisat itself cannot be compiled then). But now I found that it's actually the first one - overloaded != causing problems. Just commenting out that one, and manually change two expressions from a != b to ~(a == b), will fix the building issue with Apple's latest clang++.

I will submit a PR soon.

[binghe]

See #1254