[MSVC][std:c++latest] Z3 build failed due to error C2666: 'lp::stacked_vector<lp::numeric_pair<lp::mpq>>::ref::operator ==': overloaded functions have similar conversions

[fangzhouxia]

Description:
After the MSVC team implented P2468R2 The Equality Operator You Are Looking For, we got a compiler error with /std:c++latest like below, the error is due to the operator== https://github.com/Z3Prover/z3/blob/master/src/math/lp/stacked_vector.h#L55. In order to fix this the 'ref' log_entry::ref class needs a corresponding 'operator!=' like so, could you please look this issue? Thanks.

     bool operator!=(B const& other) const {
            return m_vec.m_vector[m_i] != other;
        }

Note: this issue will be reproduced on next release version of VS(17.6 or later).

Reproduction steps:

1. open VS2019 x64 tools command
2. git clone https://github.com/Z3Prover/z3 F:\gitP\Z3Prover\z3
3. cd F:\gitP\Z3Prover\z3 &mkdir build_amd64 &cd F:\gitP\Z3Prover\z3\build_amd64
4. cmake -G "Visual Studio 16 2019" -A x64 -DCMAKE_SYSTEM_VERSION=10.0.18362.0 ..
5. set CL=/D_SILENCE_STDEXT_HASH_DEPRECATION_WARNINGS /D_HAS_AUTO_PTR_ETC=1 /std:c++latest
6. msbuild /m /p:Platform=x64 /p:Configuration=Release Z3.sln /t:Rebuild /p:BuildInParallel=true
7. msbuild /m /p:Platform=x64 /p:Configuration=Release .\examples\c_example.vcxproj /t:Rebuild /p:BuildInParallel=true
8. msbuild /m /p:Platform=x64 /p:Configuration=Release .\examples\cpp_example.vcxproj /t:Rebuild /p:BuildInParallel=true

Expected behavio:r
Build successfully.

Actual behavior:
build.log
F:\gitP\Z3Prover\z3\src\math\lp\lar_solver.cpp(2161): error C2666: 'lp::stacked_vector<lp::numeric_pairlp::mpq>::ref::operator ==': overloaded functions have similar conversions
F:\gitP\Z3Prover\z3\src\math/lp/stacked_vector.h(55): note: could be 'bool lp::stacked_vector<lp::numeric_pairlp::mpq>::ref::operator ==(const B &) const'
with
[
B=lp::numeric_pairlp::mpq
]
F:\gitP\Z3Prover\z3\src\util/mpbq.h(331): note: or 'bool operator ==(const scoped_mpbq &,const mpz &)'
F:\gitP\Z3Prover\z3\src\util/mpbq.h(331): note: or 'bool operator ==(const scoped_mpbq &,const int &)'
F:\gitP\Z3Prover\z3\src\util/rational.h(550): note: or 'bool operator ==(const rational &,int)'
F:\gitP\Z3Prover\z3\src\math/lp/stacked_vector.h(55): note: or 'bool lp::stacked_vector<lp::numeric_pairlp::mpq>::ref::operator ==(const B &) const' [synthesized expression 'y == x']
with
[
B=lp::numeric_pairlp::mpq
]
F:\gitP\Z3Prover\z3\src\util/rational.h(550): note: or 'bool operator ==(const rational &,int)' [synthesized expression 'y == x']
F:\gitP\Z3Prover\z3\src\util/mpbq.h(331): note: or 'bool operator ==(const scoped_mpbq &,const int &)' [synthesized expression 'y == x']
F:\gitP\Z3Prover\z3\src\util/mpbq.h(331): note: or 'bool operator ==(const scoped_mpbq &,const mpz &)' [synthesized expression 'y == x']
F:\gitP\Z3Prover\z3\src\util/obj_ref.h(128): note: or 'bool operator ==(const obj_ref<T1,TManager> &,const obj_ref<T2,TManager> &)'
src\math\lp\lar_solver.cpp(2161): note: 'bool operator ==(const obj_ref<T1,TManager> &,const obj_ref<T2,TManager> &)': could not deduce template argument for 'const obj_ref<T1,TManager> &' from 'lp::stacked_vector<lp::numeric_pairlp::mpq>::ref'
F:\gitP\Z3Prover\z3\src\util/obj_ref.h(123): note: or 'bool operator ==(const obj_ref<T,TManager> &,const obj_ref<T,TManager> &)'
src\math\lp\lar_solver.cpp(2161): note: 'bool operator ==(const obj_ref<T,TManager> &,const obj_ref<T,TManager> &)': could not deduce template argument for 'const obj_ref<T,TManager> &' from 'lp::stacked_vector<lp::numeric_pairlp::mpq>::ref'
F:\gitP\Z3Prover\z3\src\util/obj_ref.h(123): note: or 'bool operator ==(const obj_ref<T,TManager> &,const obj_ref<T,TManager> &)' [synthesized expression 'y == x']
src\math\lp\lar_solver.cpp(2161): note: 'bool operator ==(const obj_ref<T,TManager> &,const obj_ref<T,TManager> &)': could not deduce template argument for 'const obj_ref<T,TManager> &' from 'lp::stacked_vector<lp::numeric_pairlp::mpq>::ref'
F:\gitP\Z3Prover\z3\src\util/obj_ref.h(128): note: or 'bool operator ==(const obj_ref<T1,TManager> &,const obj_ref<T2,TManager> &)' [synthesized expression 'y == x']
src\math\lp\lar_solver.cpp(2161): note: 'bool operator ==(const obj_ref<T1,TManager> &,const obj_ref<T2,TManager> &)': could not deduce template argument for 'const obj_ref<T1,TManager> &' from 'lp::stacked_vector<lp::numeric_pairlp::mpq>::ref'
src\math\lp\lar_solver.cpp(2161): note: while trying to match the argument list '(lp::stacked_vector<lp::numeric_pairlp::mpq>::ref, lp::stacked_vector<lp::numeric_pairlp::mpq>::ref)'

[nunoplopes]

Is godbolt's MSVC up-to-date? Can you help me repro the issue?
The code feels similar to this: https://gcc.godbolt.org/z/4jxv486f1
But it compiles just fine.

[fangzhouxia]

We are using internal the latest version of the compiler for testing. Therefore, neither the latest release VS and Godbolt cannot reproduce it.

Use our internal version compile the code in https://gcc.godbolt.org/z/4jxv486f1 with /std:c++latest, which also reports the error C2666. I try to add bool operator!=(const A&a) const; the error can indeed be solved.

[nunoplopes]

I'm sorry, but I don't understand the problem. It seems MSVC/the ISO committee wants to break all code out there..
Is the issue that there's an automatic cast operator declared?

[fangzhouxia]

@NikolajBjorner, thanks, I use 8981d32 test, this issue has indeed been fixed.