search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
103 stars 40 forks source link

Compilation with CVC5 fails on GCC >= 11 #305

Closed CyanoKobalamyne closed 1 year ago

CyanoKobalamyne commented 1 year ago

Compilation fails with the following error:

/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp: In member function ‘cvc5::Op smt::Cvc5Solver::make_cvc5_op(smt::Op) const’:
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:986:24: error: ‘numeric_limits’ is not a member of ‘std’
  986 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                        ^~~~~~~~~~~~~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:986:47: error: expected primary-expression before ‘>’ token
  986 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                                               ^
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:986:50: error: ‘::max’ has not been declared; did you mean ‘std::max’?
  986 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                                                  ^~~
      |                                                  std::max
In file included from /usr/include/c++/12.2.0/functional:64,
                 from /mnt/data/git/smt-switch/../cvc5/src/api/cpp/cvc5.h:21,
                 from /mnt/data/git/smt-switch/cvc5/include/cvc5_solver.h:26,
                 from /mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:17:
/usr/include/c++/12.2.0/bits/stl_algo.h:5756:5: note: ‘std::max’ declared here
 5756 |     max(initializer_list<_Tp> __l, _Compare __comp)
      |     ^~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:996:24: error: ‘numeric_limits’ is not a member of ‘std’
  996 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                        ^~~~~~~~~~~~~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:996:47: error: expected primary-expression before ‘>’ token
  996 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                                               ^
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:996:50: error: ‘::max’ has not been declared; did you mean ‘std::max’?
  996 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                                                  ^~~
      |                                                  std::max
/usr/include/c++/12.2.0/bits/stl_algo.h:5756:5: note: ‘std::max’ declared here
 5756 |     max(initializer_list<_Tp> __l, _Compare __comp)
      |     ^~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:1001:24: error: ‘numeric_limits’ is not a member of ‘std’
 1001 |     if (op.idx1 > std::numeric_limits<uint32_t>::max())
      |                        ^~~~~~~~~~~~~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:1001:47: error: expected primary-expression before ‘>’ token
 1001 |     if (op.idx1 > std::numeric_limits<uint32_t>::max())
      |                                               ^
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:1001:50: error: ‘::max’ has not been declared; did you mean ‘std::max’?
 1001 |     if (op.idx1 > std::numeric_limits<uint32_t>::max())
      |                                                  ^~~
      |                                                  std::max
/usr/include/c++/12.2.0/bits/stl_algo.h:5756:5: note: ‘std::max’ declared here
 5756 |     max(initializer_list<_Tp> __l, _Compare __comp)
      |     ^~~

This is due to https://www.gnu.org/software/gcc/gcc-11/porting_to.html#header-dep-changes. The limits library needs to be included everywhere it is used.