You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
I think this issue is new on macOS 14 (Sonoma) with latest Xcode (I'm using version 15.3). Apple's
c++
(clang++
) cannot compilesrc/HolSat/sat_solvers/zc2hs/zc2hs.cpp
: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 generatingnumheap
(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.
The text was updated successfully, but these errors were encountered: