ltentrup / quabs Goto Github PK
View Code? Open in Web Editor NEWQuAbS is a circuit-based QBF solver
QuAbS is a circuit-based QBF solver
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.