search

meelgroup / approxmc

Approximate Model Counter
Other
70 stars 26 forks source link

Some issue about Arjun #39

Closed ydotlai closed 11 months ago

ydotlai commented 11 months ago

Dear Developers:

I am trying to install unigen. When I tried to install approxmc, I encountered some issue. Roughly speaking, I encountered the following two errors when I tried to make.

/home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp: In function ‘int main(int, char**)’:
/home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:574:88: error: cannot convert ‘bool’ to ‘const std::vector<unsigned int>&’
  574 | = arjun->get_fully_simplified_renumbered_cnf(sampling_vars, false, true);
      |                                                             ^~~~~
      |                                                             |
      |                                                             bool
/usr/local/include/cryptominisat5/dimacsparser.h:438:17: error: ‘class ArjunNS::Arjun’ has no member named ‘add_red_clause’; did you mean ‘add_xor_clause’?
  438 |         solver->add_red_clause(lits);
      |         ~~~~~~~~^~~~~~~~~~~~~~
      |         add_xor_clause

The detailed information about building is as follows:

~/Projects/Sampling/unigen/approxmc/build$ cmake -DSTATICCOMPILE=ON ..
-- The CXX compiler identification is GNU 11.4.0
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- LIB directory is ''
-- BIN directory is ''
-- You can choose the type of build, options are:Debug;Release;RelWithDebInfo;MinSizeRel
-- Doing a RelWithDebInfo build
-- The C compiler identification is GNU 11.4.0
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Looking for pthread.h
-- Looking for pthread.h - found
-- Performing Test CMAKE_HAVE_LIBC_PTHREAD
-- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Success
-- Found Threads: TRUE  
-- build type is RelWithDebInfo
-- Performing Test HAVE_FLAG_-Wall
-- Performing Test HAVE_FLAG_-Wall - Success
-- Performing Test HAVE_FLAG_-Wextra
-- Performing Test HAVE_FLAG_-Wextra - Success
-- Performing Test HAVE_FLAG_-Wunused
-- Performing Test HAVE_FLAG_-Wunused - Success
-- Performing Test HAVE_FLAG_-Wsign-compare
-- Performing Test HAVE_FLAG_-Wsign-compare - Success
-- Performing Test HAVE_FLAG_-fno-omit-frame-pointer
-- Performing Test HAVE_FLAG_-fno-omit-frame-pointer - Success
-- Performing Test HAVE_FLAG_-Wtype-limits
-- Performing Test HAVE_FLAG_-Wtype-limits - Success
-- Performing Test HAVE_FLAG_-Wuninitialized
-- Performing Test HAVE_FLAG_-Wuninitialized - Success
-- Performing Test HAVE_FLAG_-Wno-deprecated
-- Performing Test HAVE_FLAG_-Wno-deprecated - Success
-- Performing Test HAVE_FLAG_-Wstrict-aliasing
-- Performing Test HAVE_FLAG_-Wstrict-aliasing - Success
-- Performing Test HAVE_FLAG_-Wpointer-arith
-- Performing Test HAVE_FLAG_-Wpointer-arith - Success
-- Performing Test HAVE_FLAG_-Wheader-guard
-- Performing Test HAVE_FLAG_-Wheader-guard - Failed
-- Performing Test HAVE_FLAG_-fvisibility=hidden
-- Performing Test HAVE_FLAG_-fvisibility=hidden - Success
-- Performing Test HAVE_FLAG_-Wformat-nonliteral
-- Performing Test HAVE_FLAG_-Wformat-nonliteral - Success
-- Performing Test HAVE_FLAG_-Winit-self
-- Performing Test HAVE_FLAG_-Winit-self - Success
-- Performing Test HAVE_FLAG_-Wparentheses
-- Performing Test HAVE_FLAG_-Wparentheses - Success
-- Performing Test HAVE_FLAG_-Wunreachable-code
-- Performing Test HAVE_FLAG_-Wunreachable-code - Success
-- Performing Test HAVE_FLAG_-g
-- Performing Test HAVE_FLAG_-g - Success
-- Compiling for static library use
-- GIT hash found: 8ab5426e690aeb64469904c6a425a179a8da78c9
-- PROJECT_VERSION: 4.1.15
-- PROJECT_VERSION_MAJOR: 4
-- PROJECT_VERSION_MINOR: 1
-- PROJECT_VERSION_PATCH: 15
-- Cannot find help2man, not creating manpage
-- All defines at startup:
-- Found Boost: /usr/lib/x86_64-linux-gnu/cmake/Boost-1.74.0/BoostConfig.cmake (found suitable version "1.74.0", minimum required is "1.46") found components: program_options serialization
-- Found ZLIB: /usr/lib/x86_64-linux-gnu/libz.a (found version "1.2.11")
-- OK, Found ZLIB!
-- Found GMP: /usr/include/x86_64-linux-gnu  
-- GMP dynamic lib: /usr/lib/x86_64-linux-gnu/libgmp.a
-- GMP include header location: /usr/include/x86_64-linux-gnu
-- Found CryptoMiniSat 5.x
-- CryptoMiniSat5 dynamic lib: cryptominisat5
-- CryptoMiniSat5 static lib:  cryptominisat5
-- CryptoMiniSat5 static lib deps:
-- CryptoMiniSat5 include dirs: /usr/local/include
-- Found Arjun
-- Arjun dynamic lib : arjun
-- Arjun include dirs: /usr/local/include
-- Found Louvain Communities library
-- Louvain Communities dynamic lib: louvain_communities
-- Louvain Communities include dirs: /home/leven/Projects/meelgroup/projects/louvain-community/build/include
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion - Failed
-- Performing Test HAVE_FLAG_-Wlogical-op
-- Performing Test HAVE_FLAG_-Wlogical-op - Success
-- Performing Test HAVE_FLAG_-Wrestrict
-- Performing Test HAVE_FLAG_-Wrestrict - Success
-- Performing Test HAVE_FLAG_-Wnull-dereference
-- Performing Test HAVE_FLAG_-Wnull-dereference - Success
-- Performing Test HAVE_FLAG_-Wdouble-promotion
-- Performing Test HAVE_FLAG_-Wdouble-promotion - Success
-- Performing Test HAVE_FLAG_-Wshadow
-- Performing Test HAVE_FLAG_-Wshadow - Success
-- Performing Test HAVE_FLAG_-Wformat=2
-- Performing Test HAVE_FLAG_-Wformat=2 - Success
-- Performing Test HAVE_FLAG_-Wextra-semi
-- Performing Test HAVE_FLAG_-Wextra-semi - Success
-- Performing Test HAVE_FLAG_-pedantic
-- Performing Test HAVE_FLAG_-pedantic - Success
CMake Warning at CMakeLists.txt:510 (message):
  Testing is disabled

-- Configuring done
-- Generating done
-- Build files have been written to: /home/leven/Projects/Sampling/unigen/approxmc/build
~/Projects/Sampling/unigen/approxmc/build$ make
[  9%] Building CXX object apx-src/CMakeFiles/approxmc.dir/approxmc.cpp.o
[ 18%] Building CXX object apx-src/CMakeFiles/approxmc.dir/counter.cpp.o
[ 27%] Building CXX object apx-src/CMakeFiles/approxmc.dir/constants.cpp.o
[ 36%] Building CXX object apx-src/CMakeFiles/approxmc.dir/GitSHA1.cpp.o
[ 45%] Linking CXX static library ../lib/libapproxmc.a
[ 45%] Built target approxmc
Copying approxmc.h to /home/leven/Projects/Sampling/unigen/approxmc/build/include/approxmc
[ 45%] Built target CopyPublicHeaders
[ 54%] Building CXX object apx-src/CMakeFiles/approxmc-bin.dir/main.cpp.o
/home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp: In function ‘int main(int, char**)’:
/home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:574:88: error: cannot convert ‘bool’ to ‘const std::vector<unsigned int>&’
  574 | = arjun->get_fully_simplified_renumbered_cnf(sampling_vars, false, true);
      |                                                             ^~~~~
      |                                                             |
      |                                                             bool

In file included from /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:45:
/usr/local/include/arjun/arjun.h:76:42: note:   initializing argument 2 of ‘std::tuple<std::pair<std::vector<std::vector<CMSat::Lit, std::allocator<CMSat::Lit> >, std::allocator<std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > > >, unsigned int>, std::vector<unsigned int, std::allocator<unsigned int> >, unsigned int> ArjunNS::Arjun::get_fully_simplified_renumbered_cnf(const std::vector<unsigned int>&, const std::vector<unsigned int>&, uint32_t)’
   76 |             const std::vector<uint32_t>& empty_vars,
      |             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~
In file included from /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:43:
/usr/local/include/cryptominisat5/dimacsparser.h: In instantiation of ‘bool CMSat::DimacsParser<C, S>::parseComments(C&, const string&) [with C = CMSat::StreamBuffer<gzFile_s*, CMSat::GZ>; S = ArjunNS::Arjun; std::string = std::__cxx11::basic_string<char>]’:
/usr/local/include/cryptominisat5/dimacsparser.h:642:18:   required from ‘bool CMSat::DimacsParser<C, S>::parse_DIMACS_main(C&) [with C = CMSat::StreamBuffer<gzFile_s*, CMSat::GZ>; S = ArjunNS::Arjun]’
/usr/local/include/cryptominisat5/dimacsparser.h:698:11:   required from ‘bool CMSat::DimacsParser<C, S>::parse_DIMACS(T, bool, uint32_t) [with T = gzFile_s*; C = CMSat::StreamBuffer<gzFile_s*, CMSat::GZ>; S = ArjunNS::Arjun; uint32_t = unsigned int]’
/home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:296:29:   required from ‘void read_in_file(const string&, T*) [with T = ArjunNS::Arjun; std::string = std::__cxx11::basic_string<char>]’
/home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:449:21:   required from ‘void read_input_cnf(T*) [with T = ArjunNS::Arjun]’
/home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:564:23:   required from here
/usr/local/include/cryptominisat5/dimacsparser.h:438:17: error: ‘class ArjunNS::Arjun’ has no member named ‘add_red_clause’; did you mean ‘add_xor_clause’?
  438 |         solver->add_red_clause(lits);
      |         ~~~~~~~~^~~~~~~~~~~~~~
      |         add_xor_clause
msoos commented 11 months ago

Please be absolutely sure you are on the LATEST "MASTER" banch for ALL of CMS, appmc, unigen, Arjun, etc. Delete ALL previous installs.

Let me know if it still fails to build.

Mate

On Thu, 21 Sept 2023, 05:40 Yong Lai, @.***> wrote:

Dear Developers:

I am trying to install unigen. When I tried to install approxmc, I encountered some issue. Roughly speaking, I encountered the following two errors when I tried to make.

/home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp: In function ‘int main(int, char**)’: /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:574:88: error: cannot convert ‘bool’ to ‘const std::vector&’ 574 = arjun->get_fully_simplified_renumbered_cnf(sampling_vars, false, true); ^~~~~
bool

/usr/local/include/cryptominisat5/dimacsparser.h:438:17: error: ‘class ArjunNS::Arjun’ has no member named ‘add_red_clause’; did you mean ‘add_xor_clause’? 438 | solver->add_red_clause(lits); | ~~^~~~ | add_xor_clause

The detailed information about building is as follows:

~/Projects/Sampling/unigen/approxmc/build$ cmake -DSTATICCOMPILE=ON .. -- The CXX compiler identification is GNU 11.4.0 -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/bin/c++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- LIB directory is '' -- BIN directory is '' -- You can choose the type of build, options are:Debug;Release;RelWithDebInfo;MinSizeRel -- Doing a RelWithDebInfo build -- The C compiler identification is GNU 11.4.0 -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/bin/cc - skipped -- Detecting C compile features -- Detecting C compile features - done -- Looking for pthread.h -- Looking for pthread.h - found -- Performing Test CMAKE_HAVE_LIBC_PTHREAD -- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Success -- Found Threads: TRUE -- build type is RelWithDebInfo -- Performing Test HAVEFLAG-Wall -- Performing Test HAVEFLAG-Wall - Success -- Performing Test HAVEFLAG-Wextra -- Performing Test HAVEFLAG-Wextra - Success -- Performing Test HAVEFLAG-Wunused -- Performing Test HAVEFLAG-Wunused - Success -- Performing Test HAVEFLAG-Wsign-compare -- Performing Test HAVEFLAG-Wsign-compare - Success -- Performing Test HAVEFLAG-fno-omit-frame-pointer -- Performing Test HAVEFLAG-fno-omit-frame-pointer - Success -- Performing Test HAVEFLAG-Wtype-limits -- Performing Test HAVEFLAG-Wtype-limits - Success -- Performing Test HAVEFLAG-Wuninitialized -- Performing Test HAVEFLAG-Wuninitialized - Success -- Performing Test HAVEFLAG-Wno-deprecated -- Performing Test HAVEFLAG-Wno-deprecated - Success -- Performing Test HAVEFLAG-Wstrict-aliasing -- Performing Test HAVEFLAG-Wstrict-aliasing - Success -- Performing Test HAVEFLAG-Wpointer-arith -- Performing Test HAVEFLAG-Wpointer-arith - Success -- Performing Test HAVEFLAG-Wheader-guard -- Performing Test HAVEFLAG-Wheader-guard - Failed -- Performing Test HAVEFLAG-fvisibility=hidden -- Performing Test HAVEFLAG-fvisibility=hidden - Success -- Performing Test HAVEFLAG-Wformat-nonliteral -- Performing Test HAVEFLAG-Wformat-nonliteral - Success -- Performing Test HAVEFLAG-Winit-self -- Performing Test HAVEFLAG-Winit-self - Success -- Performing Test HAVEFLAG-Wparentheses -- Performing Test HAVEFLAG-Wparentheses - Success -- Performing Test HAVEFLAG-Wunreachable-code -- Performing Test HAVEFLAG-Wunreachable-code - Success -- Performing Test HAVEFLAG-g -- Performing Test HAVEFLAG-g - Success -- Compiling for static library use -- GIT hash found: 8ab5426e690aeb64469904c6a425a179a8da78c9 -- PROJECT_VERSION: 4.1.15 -- PROJECT_VERSION_MAJOR: 4 -- PROJECT_VERSION_MINOR: 1 -- PROJECT_VERSION_PATCH: 15 -- Cannot find help2man, not creating manpage -- All defines at startup: -- Found Boost: /usr/lib/x86_64-linux-gnu/cmake/Boost-1.74.0/BoostConfig.cmake (found suitable version "1.74.0", minimum required is "1.46") found components: program_options serialization -- Found ZLIB: /usr/lib/x86_64-linux-gnu/libz.a (found version "1.2.11") -- OK, Found ZLIB! -- Found GMP: /usr/include/x86_64-linux-gnu -- GMP dynamic lib: /usr/lib/x86_64-linux-gnu/libgmp.a -- GMP include header location: /usr/include/x86_64-linux-gnu -- Found CryptoMiniSat 5.x -- CryptoMiniSat5 dynamic lib: cryptominisat5 -- CryptoMiniSat5 static lib: cryptominisat5 -- CryptoMiniSat5 static lib deps: -- CryptoMiniSat5 include dirs: /usr/local/include -- Found Arjun -- Arjun dynamic lib : arjun -- Arjun include dirs: /usr/local/include -- Found Louvain Communities library -- Louvain Communities dynamic lib: louvain_communities -- Louvain Communities include dirs: /home/leven/Projects/meelgroup/projects/louvain-community/build/include -- Performing Test HAVEFLAG-Wno-bitfield-constant-conversion -- Performing Test HAVEFLAG-Wno-bitfield-constant-conversion - Failed -- Performing Test HAVEFLAG-Wlogical-op -- Performing Test HAVEFLAG-Wlogical-op - Success -- Performing Test HAVEFLAG-Wrestrict -- Performing Test HAVEFLAG-Wrestrict - Success -- Performing Test HAVEFLAG-Wnull-dereference -- Performing Test HAVEFLAG-Wnull-dereference - Success -- Performing Test HAVEFLAG-Wdouble-promotion -- Performing Test HAVEFLAG-Wdouble-promotion - Success -- Performing Test HAVEFLAG-Wshadow -- Performing Test HAVEFLAG-Wshadow - Success -- Performing Test HAVEFLAG-Wformat=2 -- Performing Test HAVEFLAG-Wformat=2 - Success -- Performing Test HAVEFLAG-Wextra-semi -- Performing Test HAVEFLAG-Wextra-semi - Success -- Performing Test HAVEFLAG-pedantic -- Performing Test HAVEFLAG-pedantic - Success CMake Warning at CMakeLists.txt:510 (message): Testing is disabled

-- Configuring done -- Generating done -- Build files have been written to: /home/leven/Projects/Sampling/unigen/approxmc/build ~/Projects/Sampling/unigen/approxmc/build$ make [ 9%] Building CXX object apx-src/CMakeFiles/approxmc.dir/approxmc.cpp.o [ 18%] Building CXX object apx-src/CMakeFiles/approxmc.dir/counter.cpp.o [ 27%] Building CXX object apx-src/CMakeFiles/approxmc.dir/constants.cpp.o [ 36%] Building CXX object apx-src/CMakeFiles/approxmc.dir/GitSHA1.cpp.o [ 45%] Linking CXX static library ../lib/libapproxmc.a [ 45%] Built target approxmc Copying approxmc.h to /home/leven/Projects/Sampling/unigen/approxmc/build/include/approxmc [ 45%] Built target CopyPublicHeaders [ 54%] Building CXX object apx-src/CMakeFiles/approxmc-bin.dir/main.cpp.o /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp: In function ‘int main(int, char**)’: /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:574:88: error: cannot convert ‘bool’ to ‘const std::vector&’ 574 = arjun->get_fully_simplified_renumbered_cnf(sampling_vars, false, true); ^~~~~
bool

In file included from /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:45: /usr/local/include/arjun/arjun.h:76:42: note: initializing argument 2 of ‘std::tuple<std::pair<std::vector<std::vector<CMSat::Lit, std::allocator >, std::allocator<std::vector<CMSat::Lit, std::allocator > > >, unsigned int>, std::vector<unsigned int, std::allocator >, unsigned int> ArjunNS::Arjun::get_fully_simplified_renumbered_cnf(const std::vector&, const std::vector&, uint32_t)’ 76 | const std::vector& empty_vars, | ~~~~~~~^~~~ In file included from /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:43: /usr/local/include/cryptominisat5/dimacsparser.h: In instantiation of ‘bool CMSat::DimacsParser<C, S>::parseComments(C&, const string&) [with C = CMSat::StreamBuffer<gzFile_s, CMSat::GZ>; S = ArjunNS::Arjun; std::string = std::__cxx11::basic_string]’: /usr/local/include/cryptominisat5/dimacsparser.h:642:18: required from ‘bool CMSat::DimacsParser<C, S>::parse_DIMACS_main(C&) [with C = CMSat::StreamBuffer<gzFile_s, CMSat::GZ>; S = ArjunNS::Arjun]’ /usr/local/include/cryptominisat5/dimacsparser.h:698:11: required from ‘bool CMSat::DimacsParser<C, S>::parse_DIMACS(T, bool, uint32_t) [with T = gzFile_s; C = CMSat::StreamBuffer<gzFile_s, CMSat::GZ>; S = ArjunNS::Arjun; uint32_t = unsigned int]’ /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:296:29: required from ‘void read_in_file(const string&, T) [with T = ArjunNS::Arjun; std::string = std::__cxx11::basic_string]’ /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:449:21: required from ‘void read_input_cnf(T) [with T = ArjunNS::Arjun]’ /home/leven/Projects/Sampling/unigen/approxmc/src/main.cpp:564:23: required from here /usr/local/include/cryptominisat5/dimacsparser.h:438:17: error: ‘class ArjunNS::Arjun’ has no member named ‘add_red_clause’; did you mean ‘add_xor_clause’? 438 | solver->add_red_clause(lits); | ~~^~~~ | add_xor_clause

— Reply to this email directly, view it on GitHub https://github.com/meelgroup/approxmc/issues/39, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKF4OPJWN5HFI4IHI7GHQ3X3OZJ5ANCNFSM6AAAAAA5A3SVUA . You are receiving this because you are subscribed to this thread.Message ID: @.***>

ydotlai commented 11 months ago

All branches are under master. I had uninstalled all previous installs, but it still failed to build. I installed with -DSTATICCOMPILE=ON

ydotlai commented 11 months ago

I noticed that for building approxmc, the following commands are required: cd ../.. git clone https://github.com/meelgroup/arjun cd arjun mkdir build && cd build cmake .. make sudo make install sudo ldconfig But the readme document of unigen does not mention them.

msoos commented 11 months ago

Hi,

The issue is likely that you have dangling header files lying around from the private Arjun repository. Please don't use the private Arjun repository, that has a different get_fully_simplified_renumbered_cnf. You must use the public Arjun repository.

Building of Arjun should be documented here: https://github.com/meelgroup/approxmc#how-to-build-a-binary That should explain the set of commands you have written I think? Let me know if something is wrong there.

I have just re-built CMS, Arjun, and ApproxMC from the PUBLIC repository, MASTER branch, in static compile mode. All PUBLIC repositories are all pushed to master. The output says:

c ApproxMC SHA revision 8ab5426e690aeb64469904c6a425a179a8da78c9
c ApproxMC version 4.1.15
c ApproxMC compilation env CMAKE_CXX_COMPILER = /usr/lib/ccache/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -fvisibility=hidden -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -g -fvisibility=hidden -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  | STATICCOMPILE = ON | Boost_FOUND = TRUE | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | GMP_FOUND = TRUE | ENABLE_ASSERTIONS = ON | MY_TARGETS =  | compilation date time = Sep 21 2023 18:43:06
c ApproxMC compiled with gcc version 13.2.1 20230801
c CryptoMiniSat version 5.11.12
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision e566b36a274435f9f25634071a4a2d25b628bc9e
c CMS is MIT licensed
c Using VMTF code by Armin Biere from CaDiCaL
c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14
c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96,
c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'
c       by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos
c Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]'
c       by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015
c CMS compilation env CMAKE_CXX_COMPILER = /usr/lib/ccache/bin/c++ | CMAKE_CXX_FLAGS =  -fvisibility=hidden -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -g -Wno-class-memaccess -mpopcnt -msse4.2 -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DRDB0_ONLY_FEATURES -DUSE_ZLIB -DYALSAT_FPU | STATICCOMPILE = ON | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING = OFF | M4RI_FOUND =  | NOM4RI = ON | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . | compilation date time = Sep 21 2023 18:42:41
c CMS compiled with gcc version 13.2.1 20230801
c executed with command line: ./approxmc
c Arjun SHA revision b4ecb91af31e5d66d05519d47a9f64c15e3f1ad9
c Reading from standard input... Use '-h' or '--help' for help.

Please make sure you have the following git rev-parse HEAD outputs on all:

The static binary is attached: approxmc.gz

Please let me know if this helped,

Mate

ydotlai commented 11 months ago

I re-installed arjun, and then successfully built approxmc and unigen. In the readme file of unigen, it does not say arjun is required.

msoos commented 11 months ago

Aaah, sorry, you are right! The UniGen documentation was lacking the explanation about Arjun! Good point. I now fixed that: https://github.com/meelgroup/unigen/commit/a5309d208816477d888b05683740cb8fd3069778

Thanks again, and I'm glad it works for you now,

Mate