msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
797 stars 180 forks source link

searcher.cpp & occsimplifier.cpp: "no member named ‘randDblExc’" #753

Open Geremia opened 3 weeks ago

Geremia commented 3 weeks ago
/tmp/SBo/cryptominisat-5.11.21/src/searcher.cpp: In member function ‘CMSat::Clause* CMSat::Searcher::handle_last_confl(uint32_t, uint32_t, uint32_t, uint32_t, bool, uint32_t, int32_t&)’:
/tmp/SBo/cryptominisat-5.11.21/src/searcher.cpp:1673:27: error: ‘std::mt19937_64’ {aka ‘class std::mersenne_twister_engine<long unsigned int, 64, 312, 156, 31, 13043109905998158313, 29, 6148914691236517205, 17, 8202884508482404352, 37, 18444473444759240704, 43, 6364136223846793005>’} has no member named ‘randDblExc’
 1673 |     double myrnd = mtrand.randDblExc();
      |                           ^~~~~~~~~~
/tmp/SBo/cryptominisat-5.11.21/src/searcher.cpp:1730:20: error: ‘std::mt19937_64’ {aka ‘class std::mersenne_twister_engine<long unsigned int, 64, 312, 156, 31, 13043109905998158313, 29, 6148914691236517205, 17, 8202884508482404352, 37, 18444473444759240704, 43, 6364136223846793005>’} has no member named ‘randDblExc’
 1730 |             mtrand.randDblExc() < conf.lock_for_data_gen_ratio;
      |                    ^~~~~~~~~~

and

/tmp/SBo/cryptominisat-5.11.21/src/occsimplifier.cpp:2593:39: error: ‘std::mt19937_64’ {aka ‘class std::mersenne_twister_engine<long unsigned int, 64, 312, 156, 31, 13043109905998158313, 29, 6148914691236517205, 17, 8202884508482404352, 37, 18444473444759240704, 43, 6364136223846793005>’} has no member named ‘randDblExc’
 2593 |         double myrnd = solver->mtrand.randDblExc();
      |                                       ^~~~~~~~~~
/tmp/SBo/cryptominisat-5.11.21/src/occsimplifier.cpp:2608:32: error: ‘std::mt19937_64’ {aka ‘class std::mersenne_twister_engine<long unsigned int, 64, 312, 156, 31, 13043109905998158313, 29, 6148914691236517205, 17, 8202884508482404352, 37, 18444473444759240704, 43, 6364136223846793005>’} has no member named ‘randDblExc’
 2608 |                 solver->mtrand.randDblExc() < solver->conf.lock_for_data_gen_ratio;
      |                                ^~~~~~~~~~
make[2]: *** [cmsat5-src/CMakeFiles/cryptominisat5.dir/build.make:333: cmsat5-src/CMakeFiles/cryptominisat5.dir/searcher.cpp.o] Error 1
# gcc -v
Reading specs from /usr/lib64/gcc/x86_64-slackware-linux/13.2.0/specs
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=/usr/libexec/gcc/x86_64-slackware-linux/13.2.0/lto-wrapper
Target: x86_64-slackware-linux
Configured with: ../gcc-13.2.0/configure --prefix=/usr --libdir=/usr/lib64 --mandir=/usr/man --infodir=/usr/info --enable-shared --enable-bootstrap --enable-languages=ada,c,c++,d,fortran,go,lto,m2,objc,obj-c++ --enable-threads=posix --enable-checking=release --enable-objc-gc --with-system-zlib --enable-libstdcxx-dual-abi --with-default-libstdcxx-abi=new --disable-libstdcxx-pch --disable-libunwind-exceptions --enable-__cxa_atexit --disable-libssp --enable-gnu-unique-object --enable-plugin --enable-lto --disable-install-libiberty --enable-gnu-indirect-function --with-linker-hash-style=gnu --with-gnu-ld --with-isl --verbose --with-arch-directory=amd64 --disable-gtktest --disable-werror --enable-clocale=gnu --enable-multilib --target=x86_64-slackware-linux --build=x86_64-slackware-linux --host=x86_64-slackware-linux
Thread model: posix
Supported LTO compression algorithms: zlib zstd
gcc version 13.2.0 (GCC)
msoos commented 3 weeks ago

Hi,

I suggest building this from GitHub source. There, it builds without an issue:

https://github.com/msoos/cryptominisat/actions/workflows/binary-build.yml

I hope this helps,

Mate