ltentrup / quabs Goto Github PK

std err
CMake Warning at CMakeLists.txt:716 (message):
Testing is disabled

make[3]: *** No rule to make target 'libcryptominisat5'. Stop.
make[2]: *** [libsolve/src/cmsat-prefix/src/cmsat-stamp/cmsat-build] Error 2
make[1]: *** [libsolve/src/CMakeFiles/cmsat.dir/all] Error 2
make: *** [all] Error 2

std out
[ 22%] Built target quabs-base
[ 24%] Built target solve
[ 27%] Built target qcir2qdimacs
[ 29%] Built target qaiger2qcir
[ 31%] Skipping update step for 'cmsat'
[ 32%] Performing configure step for 'cmsat'
-- LIB directory is 'lib'
-- BIN directory is 'bin'
-- Doing a RelWithDebInfo build
-- build type is RelWithDebInfo
-- Performing Test HAVE_FLAG_-mtune=native
-- Performing Test HAVE_FLAG_-mtune=native - Success
-- Compiling for static library use
-- GIT hash found: b6e9914ece2e9575c39e19ec90b8388118c3a0ee
-- PROJECT_VERSION: 5.6.8
-- PROJECT_VERSION_MAJOR: 5
-- PROJECT_VERSION_MINOR: 6
-- PROJECT_VERSION_PATCH: 8
-- Boost version: 1.65.1
-- Found the following Boost libraries:
-- program_options
-- Not compiling detailed statistics. The system is faster without them
-- Manpage will be created and installed
-- OK, Found ZLIB!
-- OK, Found M4RI lib at /usr/lib/x86_64-linux-gnu/libm4ri.a and includes at /usr/include
-- All defines at startup: -DUSE_ZLIB -DUSE_M4RI
-- In case your Python interpreter is not found, or a wrong one is found, please set it with '-DPYTHON_EXECUTABLE:FILEPATH=your path here'
-- Python 3 -- PYTHON_EXECUTABLE=/usr/bin/python3
-- Python 3 -- PYTHON_LIBRARIES=/usr/lib/x86_64-linux-gnu/libpython3.6m.a
-- Python 3 -- PYTHON_INCLUDE_DIRS=/usr/include/python3.6m
-- Python 3 -- PYTHONLIBS_VERSION_STRING=3.6.7
-- Boost -- found at library: /usr/lib/x86_64-linux-gnu/libboost_program_options.a
-- Boost -- adding '/usr/lib/x86_64-linux-gnu' to link directories
-- Performing Test HAVE_FLAG_-Wformat=2
-- Performing Test HAVE_FLAG_-Wformat=2 - Success
-- Configuring done
-- Generating done
-- Build files have been written to: /home/mikolas/git/quabs/build/libsolve/src/cmsat-prefix/src/cmsat-build
[ 33%] Performing build step for 'cmsat'
libsolve/src/CMakeFiles/cmsat.dir/build.make:105: recipe for target 'libsolve/src/cmsat-prefix/src/cmsat-stamp/cmsat-build' failed
CMakeFiles/Makefile2:370: recipe for target 'libsolve/src/CMakeFiles/cmsat.dir/all' failed
Makefile:83: recipe for target 'all' failed

During compilation, following the instructions in readme.md:

[ 93%] Performing configure step for 'glucose-src'
/bin/sh: 1: cd: can't cd to /usr/local/src/quabs/build/libsolve/src/glucose-src-prefix/src/glucose-src/simp

I get this linker error during building (Ubuntu 18.04 Linux 4.15.0-33 CMake 3.10.2 GNU Make 4.1 GCC 7.3.0)

[ 40%] Built target cmsat
[ 42%] Built target sat_cryptominisat
[ 44%] Linking CXX executable quabs
libsolve/src/cmsat-prefix/src/cmsat-build/lib/libcryptominisat5.a(toplevelgauss.cpp.o): In function `CMSat::TopLevelGauss::TopLevelGauss(CMSat::Solver*)':
/home/peitl/quabs/build/libsolve/src/cmsat-prefix/src/cmsat/src/toplevelgauss.cpp:41: undefined reference to `m4ri_build_all_codes'
libsolve/src/cmsat-prefix/src/cmsat-build/lib/libcryptominisat5.a(toplevelgauss.cpp.o): In function `CMSat::TopLevelGauss::extractInfoFromBlock(std::vector<unsigned int, std::allocator<unsigned int> > const&, unsigned long)':
/home/peitl/quabs/build/libsolve/src/cmsat-prefix/src/cmsat/src/toplevelgauss.cpp:199: undefined reference to `mzd_init'
/home/peitl/quabs/build/libsolve/src/cmsat-prefix/src/cmsat/src/toplevelgauss.cpp:200: undefined reference to `mzd_is_zero'
/home/peitl/quabs/build/libsolve/src/cmsat-prefix/src/cmsat/src/toplevelgauss.cpp:224: undefined reference to `mzd_echelonize_pluq'
/home/peitl/quabs/build/libsolve/src/cmsat-prefix/src/cmsat/src/toplevelgauss.cpp:278: undefined reference to `mzd_free'
/home/peitl/quabs/build/libsolve/src/cmsat-prefix/src/cmsat/src/toplevelgauss.cpp:224: undefined reference to `mzd_echelonize_pluq'
collect2: error: ld returned 1 exit status
CMakeFiles/quabs.dir/build.make:98: recipe for target 'quabs' failed
make[2]: *** [quabs] Error 1
CMakeFiles/Makefile2:146: recipe for target 'CMakeFiles/quabs.dir/all' failed
make[1]: *** [CMakeFiles/quabs.dir/all] Error 2
Makefile:83: recipe for target 'all' failed
make: *** [all] Error 2

From some limited searching, I suspect the problem might be that CryptoMiniSat is linked dynamically, but QuAbS is trying to link statically against it, although I do not know whether that's really the case or how to fix it.

Hi,

Myself and @lollospadalaser are interested in using a QBF solver that supports the QCIR format. Given the results of last year's QBFGallery we decided to try quabs, but ran into a problem. We would appreciate any insight into this you could provide us.

When following the build instructions on a Linux machine (we tried on Ubuntu 20.04 and Mint 21.2) we get the following message:

/usr/bin/ld: attempted static link of dynamic object `/usr/lib/libboost_program_options.so.1.85.0'
collect2: error: ld returned 1 exit status
make[5]: *** [cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/build.make:132: cryptominisat5] Error 1
make[4]: *** [CMakeFiles/Makefile2:202: cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/all] Error 2
make[3]: *** [Makefile:136: all] Error 2
make[2]: *** [libsolve/src/CMakeFiles/cmsat.dir/build.make:85: libsolve/src/cmsat-prefix/src/cmsat-stamp/cmsat-build] Error 2
make[1]: *** [CMakeFiles/Makefile2:405: libsolve/src/CMakeFiles/cmsat.dir/all] Error 2
make: *** [Makefile:91: all] Error 2

We thought it might be the Boost version, but even with 1.85 the problem persists. Building on a macOS 14.5 worked without problem.