search

msoos / cryptominisat

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

Python binding not installed? #429

Closed RexYuan closed 6 years ago

RexYuan commented 6 years ago

I downloaded the 5.0.1 and followed the instruction from README to compile it on my Mac. The command-line tool is working. But I couldn't import pycryptosat in both python2 and python3. I read from the README of /python that I should also install python-dev, but that should be installed when I installed python with Homebrew.

This is the output of cmake .

cmake .               
-- You can choose the type of build, options are:Debug;Release;RelWithDebInfo;MinSizeRel
-- Doing a RelWithDebInfo build
-- The C compiler identification is AppleClang 9.0.0.9000038
-- The CXX compiler identification is AppleClang 9.0.0.9000038
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- build type is RelWithDebInfo
-- No pthread will be used
-- Performing Test HAVE_FLAG_-Wall
-- Performing Test HAVE_FLAG_-Wall - Success
-- flag -Wall supported
-- Performing Test HAVE_FLAG_-Wextra
-- Performing Test HAVE_FLAG_-Wextra - Success
-- flag -Wextra supported
-- Performing Test HAVE_FLAG_-Wunused
-- Performing Test HAVE_FLAG_-Wunused - Success
-- flag -Wunused supported
-- Performing Test HAVE_FLAG_-pedantic
-- Performing Test HAVE_FLAG_-pedantic - Success
-- flag -pedantic supported
-- Performing Test HAVE_FLAG_-Wsign-compare
-- Performing Test HAVE_FLAG_-Wsign-compare - Success
-- flag -Wsign-compare supported
-- Performing Test HAVE_FLAG_-fno-omit-frame-pointer
-- Performing Test HAVE_FLAG_-fno-omit-frame-pointer - Success
-- flag -fno-omit-frame-pointer supported
-- Performing Test HAVE_FLAG_-Wtype-limits
-- Performing Test HAVE_FLAG_-Wtype-limits - Success
-- flag -Wtype-limits supported
-- Performing Test HAVE_FLAG_-Wuninitialized
-- Performing Test HAVE_FLAG_-Wuninitialized - Success
-- flag -Wuninitialized supported
-- Performing Test HAVE_FLAG_-Wno-deprecated
-- Performing Test HAVE_FLAG_-Wno-deprecated - Success
-- flag -Wno-deprecated supported
-- Performing Test HAVE_FLAG_-Wstrict-aliasing
-- Performing Test HAVE_FLAG_-Wstrict-aliasing - Success
-- flag -Wstrict-aliasing supported
-- Performing Test HAVE_FLAG_-Wpointer-arith
-- Performing Test HAVE_FLAG_-Wpointer-arith - Success
-- flag -Wpointer-arith supported
-- Performing Test HAVE_FLAG_-Wheader-guard
-- Performing Test HAVE_FLAG_-Wheader-guard - Success
-- flag -Wheader-guard supported
-- flag -Wpointer-arith supported
-- Performing Test HAVE_FLAG_-Wformat-nonliteral
-- Performing Test HAVE_FLAG_-Wformat-nonliteral - Success
-- flag -Wformat-nonliteral supported
-- Performing Test HAVE_FLAG_-Winit-self
-- Performing Test HAVE_FLAG_-Winit-self - Success
-- flag -Winit-self supported
-- Performing Test HAVE_FLAG_-Wparentheses
-- Performing Test HAVE_FLAG_-Wparentheses - Success
-- flag -Wparentheses supported
-- Performing Test HAVE_FLAG_-Wunreachable-code
-- Performing Test HAVE_FLAG_-Wunreachable-code - Success
-- flag -Wunreachable-code supported
-- Performing Test HAVE_FLAG_-ggdb3
-- Performing Test HAVE_FLAG_-ggdb3 - Success
-- flag -ggdb3 supported
-- GIT hash found: GIT-notfound
-- PROJECT_VERSION: 5.0.1
-- PROJECT_VERSION_MAJOR: 5
-- PROJECT_VERSION_MINOR: 0
-- PROJECT_VERSION_PATCH: 1
CMake Warning at /Applications/CMake.app/Contents/share/cmake-3.6/Modules/FindBoost.cmake:743 (message):
  Imported targets not available for Boost version 106501
Call Stack (most recent call first):
  /Applications/CMake.app/Contents/share/cmake-3.6/Modules/FindBoost.cmake:842 (_Boost_COMPONENT_DEPENDENCIES)
  /Applications/CMake.app/Contents/share/cmake-3.6/Modules/FindBoost.cmake:1395 (_Boost_MISSING_DEPENDENCIES)
  CMakeLists.txt:291 (find_package)

-- Boost version: 1.65.1
-- Found the following Boost libraries:
--   program_options
-- Looking for pthread.h
-- Looking for pthread.h - found
-- Looking for pthread_create
-- Looking for pthread_create - found
-- Found Threads: TRUE  
-- Not compiling detailed statistics. Leads to faster system
-- Found ZLIB: /usr/lib/libz.dylib (found version "1.2.8") 
-- OK, Found ZLIB!
-- Valgrind Prefix: 
-- Found VALGRIND: /usr/local/include/valgrind  
-- Cannot find valgrind or it's disabled, we will not be able to mark memory pool objects as undefined
-- Found PkgConfig: /usr/local/bin/pkg-config (found version "0.29.2") 
-- Could NOT find m4ri (missing:  M4RI_LIBRARIES M4RI_INCLUDE_DIRS) 
CMake Warning at CMakeLists.txt:365 (MESSAGE):
  Did not find M4RI, XOR detection&manipulation disabled

-- All defines at startup:  -DUSE_PTHREADS -DUSE_ZLIB
-- Found PythonInterp: /usr/local/bin/python2.7 (found suitable version "2.7.14", minimum required is "2.7") 
-- Found PythonLibs: /usr/lib/libpython2.7.dylib (found suitable version "2.7.10", minimum required is "2.7") 
-- PYTHON_EXECUTABLE:FILEPATH=/usr/local/bin/python2.7
-- PYTHON_LIBRARY:FILEPATH=/usr/lib/libpython2.7.dylib
-- PYTHON_INCLUDE_DIR:FILEPATH=/usr/include/python2.7
-- PYTHONLIBS_VERSION_STRING=2.7.10
-- OK, found python interpreter, libs and header files
-- Building python interface
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY - Success
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY - Success
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR - Success
CMake Warning at CMakeLists.txt:481 (message):
  Testing is disabled

-- Configuring done
CMake Warning (dev):
  Policy CMP0042 is not set: MACOSX_RPATH is enabled by default.  Run "cmake
  --help-policy CMP0042" for policy details.  Use the cmake_policy command to
  set the policy and suppress this warning.

  MACOSX_RPATH is not specified for the following targets:

   libcryptominisat5

This warning is for project developers.  Use -Wno-dev to suppress it.

-- Generating done
-- Build files have been written to: /Users/Rex/cr/cryptominisat-5.0.1

For make

make        
Scanning dependencies of target tablestruct
[  2%] Generating sql_tablestructure.cpp
[  2%] Built target tablestruct
Scanning dependencies of target libcryptominisat5
[  4%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cnf.cpp.o
[  6%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/propengine.cpp.o
/Users/Rex/cr/cryptominisat-5.0.1/src/propengine.cpp:531:16: warning: unknown
      attribute 'optimize' ignored [-Wunknown-attributes]
__attribute__((optimize("no-unroll-loops")))
               ^
1 warning generated.
[  8%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/varreplacer.cpp.o
[ 10%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausecleaner.cpp.o
[ 12%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseusagestats.cpp.o
[ 14%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/prober.cpp.o
[ 16%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/occsimplifier.cpp.o
[ 18%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumestrengthen.cpp.o
[ 20%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseallocator.cpp.o
[ 22%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sccfinder.cpp.o
/Users/Rex/cr/cryptominisat-5.0.1/src/sccfinder.cpp:96:15: warning: comparison
      of integers of different signs: 'uint32_t' (aka 'unsigned int') and 'int'
      [-Wsign-compare]
    if (depth >= solver->conf.max_scc_depth) {
        ~~~~~ ^  ~~~~~~~~~~~~~~~~~~~~~~~~~~
1 warning generated.
[ 24%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solverconf.cpp.o
[ 26%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerallwithall.cpp.o
[ 28%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerlongwithimpl.cpp.o
[ 30%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/str_impl_w_impl_stamp.cpp.o
[ 32%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solutionextender.cpp.o
[ 34%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/completedetachreattacher.cpp.o
[ 36%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searcher.cpp.o
[ 38%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solver.cpp.o
[ 40%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/gatefinder.cpp.o
[ 42%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sqlstats.cpp.o
[ 44%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/implcache.cpp.o
[ 46%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/stamp.cpp.o
[ 48%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/compfinder.cpp.o
[ 51%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/comphandler.cpp.o
[ 53%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/hyperengine.cpp.o
[ 55%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumeimplicit.cpp.o
[ 57%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cleaningstats.cpp.o
[ 59%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/datasync.cpp.o
[ 61%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/reducedb.cpp.o
[ 63%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausedumper.cpp.o
[ 65%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/bva.cpp.o
[ 67%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/intree.cpp.o
[ 69%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_calc.cpp.o
[ 71%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_to_reconf.cpp.o
[ 73%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solvefeatures.cpp.o
[ 75%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searchstats.cpp.o
[ 77%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/xorfinder.cpp.o
[ 79%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat_c.cpp.o
In file included from /Users/Rex/cr/cryptominisat-5.0.1/src/cryptominisat_c.cpp:25:
/Users/Rex/cr/cryptominisat-5.0.1/cmsat5-src/cryptominisat5/cryptominisat.h:41:5: warning: 
      'SATSolver' defined as a class here but previously declared as a struct
      [-Wmismatched-tags]
    class SATSolver
    ^
/Users/Rex/cr/cryptominisat-5.0.1/cmsat5-src/cryptominisat5/cryptominisat_c.h:35:22: note: 
      did you mean class here?
    namespace CMSat{ struct SATSolver; }
                     ^~~~~~
                     class
1 warning generated.
[ 81%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/GitSHA1.cpp.o
[ 83%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o
[ 85%] Linking CXX shared library ../lib/libcryptominisat5.dylib
clang: warning: argument unused during compilation: '-pthread' [-Wunused-command-line-argument]
[ 85%] Built target libcryptominisat5
Scanning dependencies of target python_interface
[ 87%] Generating build/timestamp
running build_ext
building 'pycryptosat' extension
creating build
creating build/temp.macosx-10.12-x86_64-2.7
creating build/temp.macosx-10.12-x86_64-2.7/Users
creating build/temp.macosx-10.12-x86_64-2.7/Users/Rex
creating build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr
creating build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr/cryptominisat-5.0.1
creating build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr/cryptominisat-5.0.1/python
clang -g -W -Wall -Wno-deprecated -std=c++11 -I/usr/local/include -I/usr/local/opt/openssl/include -I/usr/local/opt/sqlite/include -I/usr/local/Cellar/python/2.7.14/Frameworks/Python.framework/Versions/2.7/include/python2.7 -c /Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp -o build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.o -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -fno-strict-aliasing -fno-common -dynamic -arch x86_64 -arch i386 -g -Os -pipe -fno-common -fno-strict-aliasing -fwrapv -DENABLE_DTRACE -DMACOSX -DNDEBUG -Wall -Wstrict-prototypes -Wshorten-64-to-32 -DNDEBUG -g -fwrapv -Os -Wall -Wstrict-prototypes -DENABLE_DTRACE -I/Users/Rex/cr/cryptominisat-5.0.1 -I/Users/Rex/cr/cryptominisat-5.0.1/cmsat5-src
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:30: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:41: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                                        ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:56: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                                                       ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:139:28: warning: 
      implicit conversion loses integer precision: 'long' to 'uint32_t'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        lits.push_back(Lit(var, sign));
                       ~~~ ^~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:182:24: warning: 
      implicit conversion loses integer precision: 'long' to 'value_type'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        vars.push_back(var);
             ~~~~~~~~~ ^~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:194:30: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"clause", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:212:30: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"xor_clause", "rhs", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:212:44: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"xor_clause", "rhs", NULL};
                                           ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:301:39: warning: 
      implicit conversion loses integer precision: 'long' to 'uint32_t'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        assumption_lits.push_back(Lit(var, sign));
                                  ~~~ ^~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:314:30: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"assumptions", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:365:23: warning: 
      missing field 'ml_flags' initializer [-Wmissing-field-initializers]
    {NULL,        NULL}  /* sentinel */
                      ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:372:23: warning: 
      missing field 'ml_flags' initializer [-Wmissing-field-initializers]
    {NULL,        NULL}  /* sentinel */
                      ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:416:10: warning: 
      missing field 'type' initializer [-Wmissing-field-initializers]
    {NULL}  /* Sentinel */
         ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:466:1: warning: 
      missing field 'tp_free' initializer [-Wmissing-field-initializers]
};
^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:487:47: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    outofconflerr = PyErr_NewExceptionWithDoc("Solver.OutOfConflicts", "...
                                              ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:487:72: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    outofconflerr = PyErr_NewExceptionWithDoc("Solver.OutOfConflicts", "Ran ...
                                                                       ^
16 warnings generated.
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:30: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:41: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                                        ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:56: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                                                       ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:133:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= self->cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:176:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= self->cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:194:30: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"clause", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:212:30: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"xor_clause", "rhs", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:212:44: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"xor_clause", "rhs", NULL};
                                           ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:295:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:314:30: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    static char* kwlist[] = {"assumptions", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:365:23: warning: 
      missing field 'ml_flags' initializer [-Wmissing-field-initializers]
    {NULL,        NULL}  /* sentinel */
                      ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:372:23: warning: 
      missing field 'ml_flags' initializer [-Wmissing-field-initializers]
    {NULL,        NULL}  /* sentinel */
                      ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:416:10: warning: 
      missing field 'type' initializer [-Wmissing-field-initializers]
    {NULL}  /* Sentinel */
         ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:466:1: warning: 
      missing field 'tp_free' initializer [-Wmissing-field-initializers]
};
^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:487:47: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    outofconflerr = PyErr_NewExceptionWithDoc("Solver.OutOfConflicts", "...
                                              ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:487:72: warning: ISO
      C++11 does not allow conversion from string literal to 'char *'
      [-Wwritable-strings]
    outofconflerr = PyErr_NewExceptionWithDoc("Solver.OutOfConflicts", "Ran ...
                                                                       ^
16 warnings generated.
clang++ -shared -g -W -Wall -Wno-deprecated build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.o -L. -L/Users/Rex/cr/cryptominisat-5.0.1/lib -L/usr/local/lib -L/usr/local/opt/openssl/lib -L/usr/local/opt/sqlite/lib -L../lib -lcryptominisat5 -o /Users/Rex/cr/cryptominisat-5.0.1/pycryptosat/pycryptosat.so -L/System/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/config -lpython2.7 -ldl -framework CoreFoundation
[ 87%] Built target python_interface
Scanning dependencies of target cryptominisat5
[ 89%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main.cpp.o
[ 91%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main_exe.cpp.o
[ 93%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/signalcode.cpp.o
[ 95%] Linking CXX executable ../cryptominisat5
clang: warning: argument unused during compilation: '-pthread' [-Wunused-command-line-argument]
[ 95%] Built target cryptominisat5
Scanning dependencies of target CopyPublicHeaders
Copying cryptominisat_c.h to /Users/Rex/cr/cryptominisat-5.0.1/include/cryptominisat5
Copying cryptominisat.h to /Users/Rex/cr/cryptominisat-5.0.1/include/cryptominisat5
Copying solvertypesmini.h to /Users/Rex/cr/cryptominisat-5.0.1/include/cryptominisat5
[ 95%] Built target CopyPublicHeaders
Scanning dependencies of target cryptominisat5_simple
[ 97%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5_simple.dir/main_simple.cpp.o
[100%] Linking CXX executable ../cryptominisat5_simple
clang: warning: argument unused during compilation: '-pthread' [-Wunused-command-line-argument]
[100%] Built target cryptominisat5_simple

For make install

sudo make install
Password:
[  2%] Built target tablestruct
[ 85%] Built target libcryptominisat5
[ 87%] Generating build/timestamp
running build_ext
[ 87%] Built target python_interface
[ 95%] Built target cryptominisat5
Copying cryptominisat_c.h to /Users/Rex/cr/cryptominisat-5.0.1/include/cryptominisat5
Copying cryptominisat.h to /Users/Rex/cr/cryptominisat-5.0.1/include/cryptominisat5
Copying solvertypesmini.h to /Users/Rex/cr/cryptominisat-5.0.1/include/cryptominisat5
[ 95%] Built target CopyPublicHeaders
[100%] Built target cryptominisat5_simple
Install the project...
-- Install configuration: "RelWithDebInfo"
-- Installing: /usr/local/lib/cmake/cryptominisat5/cryptominisat5Config.cmake
-- Installing: /usr/local/lib/cmake/cryptominisat5/cryptominisat5Targets.cmake
-- Installing: /usr/local/lib/cmake/cryptominisat5/cryptominisat5Targets-relwithdebinfo.cmake
running install
running build
running build_py
file pycryptosat.py (for module pycryptosat) not found
running build_ext
file pycryptosat.py (for module pycryptosat) not found
building 'pycryptosat' extension
creating build
creating build/temp.macosx-10.12-x86_64-2.7
creating build/temp.macosx-10.12-x86_64-2.7/Users
creating build/temp.macosx-10.12-x86_64-2.7/Users/Rex
creating build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr
creating build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr/cryptominisat-5.0.1
creating build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr/cryptominisat-5.0.1/python
clang -g -W -Wall -Wno-deprecated -std=c++11 -I/usr/local/include -I/usr/local/opt/openssl/include -I/usr/local/opt/sqlite/include -I/usr/local/Cellar/python/2.7.14/Frameworks/Python.framework/Versions/2.7/include/python2.7 -c /Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp -o build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.o -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -fno-strict-aliasing -fno-common -dynamic -arch x86_64 -arch i386 -g -Os -pipe -fno-common -fno-strict-aliasing -fwrapv -DENABLE_DTRACE -DMACOSX -DNDEBUG -Wall -Wstrict-prototypes -Wshorten-64-to-32 -DNDEBUG -g -fwrapv -Os -Wall -Wstrict-prototypes -DENABLE_DTRACE -I/Users/Rex/cr/cryptominisat-5.0.1 -I/Users/Rex/cr/cryptominisat-5.0.1/cmsat5-src
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:30: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:41: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                                        ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:56: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                                                       ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:139:28: warning: implicit conversion loses integer precision: 'long' to 'uint32_t' (aka 'unsigned int') [-Wshorten-64-to-32]
        lits.push_back(Lit(var, sign));
                       ~~~ ^~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:182:24: warning: implicit conversion loses integer precision: 'long' to 'value_type' (aka 'unsigned int') [-Wshorten-64-to-32]
        vars.push_back(var);
             ~~~~~~~~~ ^~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:194:30: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"clause", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:212:30: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"xor_clause", "rhs", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:212:44: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"xor_clause", "rhs", NULL};
                                           ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:301:39: warning: implicit conversion loses integer precision: 'long' to 'uint32_t' (aka 'unsigned int') [-Wshorten-64-to-32]
        assumption_lits.push_back(Lit(var, sign));
                                  ~~~ ^~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:314:30: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"assumptions", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:365:23: warning: missing field 'ml_flags' initializer [-Wmissing-field-initializers]
    {NULL,        NULL}  /* sentinel */
                      ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:372:23: warning: missing field 'ml_flags' initializer [-Wmissing-field-initializers]
    {NULL,        NULL}  /* sentinel */
                      ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:416:10: warning: missing field 'type' initializer [-Wmissing-field-initializers]
    {NULL}  /* Sentinel */
         ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:466:1: warning: missing field 'tp_free' initializer [-Wmissing-field-initializers]
};
^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:487:47: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    outofconflerr = PyErr_NewExceptionWithDoc("Solver.OutOfConflicts", "Ran out of the number of conflicts", NULL, NULL);
                                              ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:487:72: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    outofconflerr = PyErr_NewExceptionWithDoc("Solver.OutOfConflicts", "Ran out of the number of conflicts", NULL, NULL);
                                                                       ^
16 warnings generated.
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:30: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:41: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                                        ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:52:56: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"verbose", "confl_limit", "threads", NULL};
                                                       ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:133:17: warning: comparison of integers of different signs: 'long' and 'unsigned int' [-Wsign-compare]
        if (var >= self->cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:176:17: warning: comparison of integers of different signs: 'long' and 'unsigned int' [-Wsign-compare]
        if (var >= self->cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:194:30: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"clause", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:212:30: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"xor_clause", "rhs", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:212:44: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"xor_clause", "rhs", NULL};
                                           ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:295:17: warning: comparison of integers of different signs: 'long' and 'unsigned int' [-Wsign-compare]
        if (var >= cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:314:30: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    static char* kwlist[] = {"assumptions", NULL};
                             ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:365:23: warning: missing field 'ml_flags' initializer [-Wmissing-field-initializers]
    {NULL,        NULL}  /* sentinel */
                      ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:372:23: warning: missing field 'ml_flags' initializer [-Wmissing-field-initializers]
    {NULL,        NULL}  /* sentinel */
                      ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:416:10: warning: missing field 'type' initializer [-Wmissing-field-initializers]
    {NULL}  /* Sentinel */
         ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:466:1: warning: missing field 'tp_free' initializer [-Wmissing-field-initializers]
};
^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:487:47: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    outofconflerr = PyErr_NewExceptionWithDoc("Solver.OutOfConflicts", "Ran out of the number of conflicts", NULL, NULL);
                                              ^
/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.cpp:487:72: warning: ISO C++11 does not allow conversion from string literal to 'char *' [-Wwritable-strings]
    outofconflerr = PyErr_NewExceptionWithDoc("Solver.OutOfConflicts", "Ran out of the number of conflicts", NULL, NULL);
                                                                       ^
16 warnings generated.
creating build/lib.macosx-10.12-x86_64-2.7
clang++ -shared -g -W -Wall -Wno-deprecated build/temp.macosx-10.12-x86_64-2.7/Users/Rex/cr/cryptominisat-5.0.1/python/pycryptosat.o -L. -L/Users/Rex/cr/cryptominisat-5.0.1/lib -L/usr/local/lib -L/usr/local/opt/openssl/lib -L/usr/local/opt/sqlite/lib -lcryptominisat5 -o build/lib.macosx-10.12-x86_64-2.7/pycryptosat.so -L/System/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/config -lpython2.7 -ldl -framework CoreFoundation
running install_lib
copying build/lib.macosx-10.12-x86_64-2.7/pycryptosat.so -> /usr/local/lib/python2.7/site-packages
running install_egg_info
Removing /usr/local/lib/python2.7/site-packages/pycryptosat-5.0.1-py2.7.egg-info
Writing /usr/local/lib/python2.7/site-packages/pycryptosat-5.0.1-py2.7.egg-info
file pycryptosat.py (for module pycryptosat) not found
writing list of installed files to 'files.txt'
-- Installing: /usr/local/lib/libcryptominisat5.5.0.dylib
-- Up-to-date: /usr/local/lib/libcryptominisat5.dylib
-- Installing: /usr/local/include/cryptominisat5/cryptominisat_c.h
-- Installing: /usr/local/include/cryptominisat5/cryptominisat.h
-- Installing: /usr/local/include/cryptominisat5/solvertypesmini.h
-- Installing: /usr/local/bin/cryptominisat5
-- Installing: /usr/local/bin/cryptominisat5_simple

I did notice the line

file pycryptosat.py (for module pycryptosat) not found

but I could not figure out what should I do to fix it. Is there something I missed or messed up?

msoos commented 6 years ago

Thanks, good catch! I think I have just fixed this. I pushed a new commit, fingers crossed :) Can you try now?

RexYuan commented 6 years ago

Thanks for the fast response. I just cloned the repo and tried to build it. Didn't work though. Something else went wrong?

cmake .

cmake .         
-- LIB directory is 'lib'
-- BIN directory is 'bin'
-- You can choose the type of build, options are:Debug;Release;RelWithDebInfo;MinSizeRel
-- Doing a RelWithDebInfo build
-- The C compiler identification is AppleClang 9.0.0.9000038
-- The CXX compiler identification is AppleClang 9.0.0.9000038
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Looking for pthread.h
-- Looking for pthread.h - found
-- Looking for pthread_create
-- Looking for pthread_create - found
-- 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 - 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_-ggdb3
-- Performing Test HAVE_FLAG_-ggdb3 - Success
-- Compiling for dynamic library use
-- GIT hash found: 1ec16dcc6395181a6a6def7aa949b23f26c58ac9
-- PROJECT_VERSION: 5.0.1
-- PROJECT_VERSION_MAJOR: 5
-- PROJECT_VERSION_MINOR: 0
-- PROJECT_VERSION_PATCH: 1
-- Boost version: 1.65.1
-- Found the following Boost libraries:
--   program_options
-- Not compiling detailed statistics. Leads to faster system
-- Found ZLIB: /usr/lib/libz.dylib (found version "1.2.11") 
-- OK, Found ZLIB!
-- Valgrind Prefix: 
-- Found VALGRIND: /usr/local/include/valgrind  
-- Cannot find valgrind or it's disabled, we will not be able to mark memory pool objects as undefined
-- Found PkgConfig: /usr/local/bin/pkg-config (found version "0.29.2") 
-- Could NOT find m4ri (missing: M4RI_LIBRARIES M4RI_INCLUDE_DIRS) 
CMake Warning at CMakeLists.txt:440 (MESSAGE):
  Did not find M4RI, XOR detection&manipulation disabled

-- All defines at startup:  -DBOOST_TEST_DYN_LINK -DUSE_ZLIB
-- Found PythonInterp: /usr/local/bin/python2.7 (found suitable version "2.7.14", minimum required is "2.7") 
-- PYTHON_EXECUTABLE=/usr/local/bin/python2.7
-- Found PythonLibs: /usr/lib/libpython2.7.dylib (found suitable version "2.7.10", minimum required is "2.7") 
-- PYTHON_LIBRARIES=/usr/lib/libpython2.7.dylib
-- PYTHON_INCLUDE_DIRS=/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.13.sdk/usr/include/python2.7
-- PYTHONLIBS_VERSION_STRING=2.7.10
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion - Success
-- Performing Test HAVE_FLAG_-Wlogical-op
-- Performing Test HAVE_FLAG_-Wlogical-op - Failed
-- Performing Test HAVE_FLAG_-Wrestrict
-- Performing Test HAVE_FLAG_-Wrestrict - Failed
-- Performing Test HAVE_FLAG_-Wnull-dereference
-- Performing Test HAVE_FLAG_-Wnull-dereference - Success
-- Performing Test HAVE_FLAG_-Wjump-misses-init
-- Performing Test HAVE_FLAG_-Wjump-misses-init - Failed
-- 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
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY - Success
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY - Success
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR - Success
CMake Warning at CMakeLists.txt:542 (message):
  Testing is disabled

-- Found python interpreter, libs and header files
-- Building python interface
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/Rex/cr/cryptominisat

make

make        
Scanning dependencies of target libcryptominisat5
[  2%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cnf.cpp.o
[  4%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/propengine.cpp.o
[  6%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/varreplacer.cpp.o
/Users/Rex/cr/cryptominisat/src/varreplacer.cpp:1054:52: warning: declaration
      shadows a field of 'CMSat::VarReplacer' [-Wshadow]
void VarReplacer::Stats::print_short(const Solver* solver) const
                                                   ^
/Users/Rex/cr/cryptominisat/src/varreplacer.h:111:17: note: previous declaration
      is here
        Solver* solver;
                ^
1 warning generated.
[  8%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausecleaner.cpp.o
/Users/Rex/cr/cryptominisat/src/clausecleaner.cpp:243:63: warning: declaration
      shadows a field of 'CMSat::ClauseCleaner' [-Wshadow]
void ClauseCleaner::ImplicitData::update_solver_stats(Solver* solver)
                                                              ^
/Users/Rex/cr/cryptominisat/src/clausecleaner.h:88:17: note: previous
      declaration is here
        Solver* solver;
                ^
1 warning generated.
[ 10%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseusagestats.cpp.o
[ 12%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/prober.cpp.o
/Users/Rex/cr/cryptominisat/src/prober.cpp:887:47: warning: declaration shadows
      a field of 'CMSat::Prober' [-Wshadow]
void Prober::Stats::print_short(const Solver* solver, const bool time_ou...
                                              ^
/Users/Rex/cr/cryptominisat/src/prober.h:217:17: note: previous declaration is
      here
        Solver* solver; ///<The solver we are updating&working with
                ^
1 warning generated.
[ 14%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/occsimplifier.cpp.o
[ 16%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumestrengthen.cpp.o
/Users/Rex/cr/cryptominisat/src/subsumestrengthen.cpp:763:58: warning: 
      declaration shadows a field of 'CMSat::SubsumeStrengthen' [-Wshadow]
void SubsumeStrengthen::Stats::print_short(const Solver* solver) const
                                                         ^
/Users/Rex/cr/cryptominisat/src/subsumestrengthen.h:112:13: note: previous
      declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 18%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseallocator.cpp.o
[ 20%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sccfinder.cpp.o
/Users/Rex/cr/cryptominisat/src/sccfinder.cpp:198:44: warning: declaration
      shadows a field of 'CMSat::SCCFinder' [-Wshadow]
void SCCFinder::Stats::print_short(Solver* solver) const
                                           ^
/Users/Rex/cr/cryptominisat/src/sccfinder.h:117:17: note: previous declaration
      is here
        Solver* solver;
                ^
1 warning generated.
[ 22%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solverconf.cpp.o
[ 25%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerallwithall.cpp.o
/Users/Rex/cr/cryptominisat/src/distillerallwithall.cpp:351:60: warning: 
      declaration shadows a field of 'CMSat::DistillerAllWithAll' [-Wshadow]
void DistillerAllWithAll::Stats::print_short(const Solver* solver) const
                                                           ^
/Users/Rex/cr/cryptominisat/src/distillerallwithall.h:81:17: note: previous
      declaration is here
        Solver* solver;
                ^
1 warning generated.
[ 27%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerlongwithimpl.cpp.o
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.cpp:558:62: warning: 
      declaration shadows a field of 'CMSat::DistillerLongWithImpl' [-Wshadow]
void DistillerLongWithImpl::Stats::print_short(const Solver* solver) const
                                                             ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.h:173:17: note: previous
      declaration is here
        Solver* solver;
                ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.cpp:576:93: warning: 
      declaration shadows a field of 'CMSat::DistillerLongWithImpl' [-Wshadow]
  ...string type, const Solver* solver) const
                                ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.h:173:17: note: previous
      declaration is here
        Solver* solver;
                ^
2 warnings generated.
[ 29%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/str_impl_w_impl_stamp.cpp.o
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.cpp:195:21: warning: 
      declaration shadows a field of 'CMSat::StrImplWImplStamp' [-Wshadow]
    , const int64_t timeAvailable
                    ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.h:87:13: note: previous
      declaration is here
    int64_t timeAvailable;
            ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.cpp:197:15: warning: 
      declaration shadows a field of 'CMSat::StrImplWImplStamp' [-Wshadow]
    , Solver* solver
              ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.h:49:13: note: previous
      declaration is here
    Solver* solver;
            ^
2 warnings generated.
[ 31%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solutionextender.cpp.o
[ 33%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/completedetachreattacher.cpp.o
[ 35%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searcher.cpp.o
/Users/Rex/cr/cryptominisat/src/searcher.cpp:2317:26: warning: declaration
      shadows a local variable [-Wshadow]
                uint32_t v = order_heap[0];
                         ^
/Users/Rex/cr/cryptominisat/src/searcher.cpp:2309:18: note: previous declaration
      is here
        uint32_t v = var_Undef;
                 ^
/Users/Rex/cr/cryptominisat/src/searcher.cpp:3128:24: warning: unused parameter
      'cl_stats' [-Wunused-parameter]
    const ClauseStats& cl_stats
                       ^
2 warnings generated.
[ 37%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solver.cpp.o
[ 39%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sqlstats.cpp.o
[ 41%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/implcache.cpp.o
[ 43%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/stamp.cpp.o
[ 45%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/compfinder.cpp.o
[ 47%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/comphandler.cpp.o
[ 50%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/hyperengine.cpp.o
[ 52%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumeimplicit.cpp.o
/Users/Rex/cr/cryptominisat/src/subsumeimplicit.cpp:176:56: warning: 
      declaration shadows a field of 'CMSat::SubsumeImplicit' [-Wshadow]
void SubsumeImplicit::Stats::print_short(const Solver* solver) const
                                                       ^
/Users/Rex/cr/cryptominisat/src/subsumeimplicit.h:68:13: note: previous
      declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 54%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/datasync.cpp.o
[ 56%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/reducedb.cpp.o
[ 58%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausedumper.cpp.o
[ 60%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/bva.cpp.o
/Users/Rex/cr/cryptominisat/src/bva.cpp:545:54: warning: declaration shadows a
      field of 'CMSat::BVA' [-Wshadow]
string BVA::PotentialClause::to_string(const Solver* solver) const
                                                     ^
/Users/Rex/cr/cryptominisat/src/bva.h:46:13: note: previous declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 62%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/intree.cpp.o
[ 64%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_calc.cpp.o
[ 66%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_to_reconf.cpp.o
[ 68%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solvefeatures.cpp.o
[ 70%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searchstats.cpp.o
[ 72%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/xorfinder.cpp.o
/Users/Rex/cr/cryptominisat/src/xorfinder.cpp:396:22: warning: declaration
      shadows a local variable [-Wshadow]
        for(uint32_t v: x_new) {
                     ^
/Users/Rex/cr/cryptominisat/src/xorfinder.cpp:360:24: note: previous declaration
      is here
        const uint32_t v = interesting.back();
                       ^
/Users/Rex/cr/cryptominisat/src/xorfinder.cpp:621:50: warning: declaration
      shadows a field of 'CMSat::XorFinder' [-Wshadow]
void XorFinder::Stats::print_short(const Solver* solver) const
                                                 ^
/Users/Rex/cr/cryptominisat/src/xorfinder.h:187:13: note: previous declaration
      is here
    Solver *solver;
            ^
2 warnings generated.
[ 75%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat_c.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/cryptominisat_c.cpp:25:
/Users/Rex/cr/cryptominisat/cmsat5-src/cryptominisat5/cryptominisat.h:43:5: warning: 
      'SATSolver' defined as a class here but previously declared as a struct
      [-Wmismatched-tags]
    class SATSolver
    ^
/Users/Rex/cr/cryptominisat/cmsat5-src/cryptominisat5/cryptominisat_c.h:35:22: note: 
      did you mean class here?
    namespace CMSat{ struct SATSolver; }
                     ^~~~~~
                     class
1 warning generated.
[ 77%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/GitSHA1.cpp.o
[ 79%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:25:
In file included from /Users/Rex/cr/cryptominisat/src/solver.h:36:
In file included from /Users/Rex/cr/cryptominisat/src/propengine.h:43:
In file included from /Users/Rex/cr/cryptominisat/src/cnf.h:36:
/Users/Rex/cr/cryptominisat/src/drat.h:95:10: warning: 'get_conf_id' overrides a
      member function but is not marked 'override'
      [-Winconsistent-missing-override]
    bool get_conf_id() {
         ^
/Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:758:20: note: in instantiation
      of template class 'CMSat::DratFile<true>' requested here
        drat = new DratFile<true>;
                   ^
/Users/Rex/cr/cryptominisat/src/drat.h:52:18: note: overridden virtual function
      is here
    virtual bool get_conf_id() {
                 ^
/Users/Rex/cr/cryptominisat/src/drat.h:95:10: warning: 'get_conf_id' overrides a
      member function but is not marked 'override'
      [-Winconsistent-missing-override]
    bool get_conf_id() {
         ^
/Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:760:20: note: in instantiation
      of template class 'CMSat::DratFile<false>' requested here
        drat = new DratFile<false>;
                   ^
/Users/Rex/cr/cryptominisat/src/drat.h:52:18: note: overridden virtual function
      is here
    virtual bool get_conf_id() {
                 ^
2 warnings generated.
[ 81%] Linking CXX shared library ../lib/libcryptominisat5.dylib
[ 81%] Built target libcryptominisat5
Scanning dependencies of target cryptominisat5
[ 83%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/main.cpp:48:
In file included from /Users/Rex/cr/cryptominisat/src/main.h:37:
In file included from /usr/local/include/boost/program_options.hpp:15:
In file included from /usr/local/include/boost/program_options/options_description.hpp:13:
In file included from /usr/local/include/boost/program_options/value_semantic.hpp:14:
In file included from /usr/local/include/boost/lexical_cast.hpp:32:
In file included from /usr/local/include/boost/lexical_cast/try_lexical_convert.hpp:42:
In file included from /usr/local/include/boost/lexical_cast/detail/converter_lexical.hpp:54:
/usr/local/include/boost/lexical_cast/detail/converter_lexical_streams.hpp:280:46: warning: 
      implicit conversion increases floating-point precision: 'float' to
      'const double' [-Wdouble-promotion]
                const double val_as_double = val;
                             ~~~~~~~~~~~~~   ^~~
/usr/local/include/boost/lexical_cast/detail/converter_lexical_streams.hpp:321:46: warning: 
      implicit conversion increases floating-point precision: 'float' to
      'const double' [-Wdouble-promotion]
                const double val_as_double = val;
                             ~~~~~~~~~~~~~   ^~~
In file included from /Users/Rex/cr/cryptominisat/src/main.cpp:48:
/Users/Rex/cr/cryptominisat/src/main.h:83:43: warning: extra ';' after member
      function definition [-Wextra-semi]
        virtual void call_after_parse() {};
                                          ^
3 warnings generated.
[ 85%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main_exe.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/main_exe.cpp:24:
In file included from /Users/Rex/cr/cryptominisat/src/main.h:37:
In file included from /usr/local/include/boost/program_options.hpp:15:
In file included from /usr/local/include/boost/program_options/options_description.hpp:13:
In file included from /usr/local/include/boost/program_options/value_semantic.hpp:14:
In file included from /usr/local/include/boost/lexical_cast.hpp:32:
In file included from /usr/local/include/boost/lexical_cast/try_lexical_convert.hpp:42:
In file included from /usr/local/include/boost/lexical_cast/detail/converter_lexical.hpp:54:
/usr/local/include/boost/lexical_cast/detail/converter_lexical_streams.hpp:280:46: warning: 
      implicit conversion increases floating-point precision: 'float' to
      'const double' [-Wdouble-promotion]
                const double val_as_double = val;
                             ~~~~~~~~~~~~~   ^~~
/usr/local/include/boost/lexical_cast/detail/converter_lexical_streams.hpp:321:46: warning: 
      implicit conversion increases floating-point precision: 'float' to
      'const double' [-Wdouble-promotion]
                const double val_as_double = val;
                             ~~~~~~~~~~~~~   ^~~
In file included from /Users/Rex/cr/cryptominisat/src/main_exe.cpp:24:
/Users/Rex/cr/cryptominisat/src/main.h:83:43: warning: extra ';' after member
      function definition [-Wextra-semi]
        virtual void call_after_parse() {};
                                          ^
3 warnings generated.
[ 87%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/signalcode.cpp.o
[ 89%] Linking CXX executable ../cryptominisat5
[ 89%] Built target cryptominisat5
Scanning dependencies of target ipasircryptominisat5
[ 91%] Building CXX object cmsat5-src/CMakeFiles/ipasircryptominisat5.dir/ipasir.cpp.o
[ 93%] Linking CXX shared library ../lib/libipasircryptominisat5.dylib
[ 93%] Built target ipasircryptominisat5
Scanning dependencies of target cryptominisat5_simple
[ 95%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5_simple.dir/main_simple.cpp.o
[ 97%] Linking CXX executable ../cryptominisat5_simple
[ 97%] Built target cryptominisat5_simple
Scanning dependencies of target CopyPublicHeaders
Copying cryptominisat_c.h to /Users/Rex/cr/cryptominisat/include/cryptominisat5
Copying cryptominisat.h to /Users/Rex/cr/cryptominisat/include/cryptominisat5
Copying solvertypesmini.h to /Users/Rex/cr/cryptominisat/include/cryptominisat5
[ 97%] Built target CopyPublicHeaders
Scanning dependencies of target python_interface
[100%] Generating build/timestamp
running build_ext
building 'pycryptosat' extension
creating build
creating build/temp.macosx-10.13-x86_64-2.7
creating build/temp.macosx-10.13-x86_64-2.7/Users
creating build/temp.macosx-10.13-x86_64-2.7/Users/Rex
creating build/temp.macosx-10.13-x86_64-2.7/Users/Rex/cr
creating build/temp.macosx-10.13-x86_64-2.7/Users/Rex/cr/cryptominisat
creating build/temp.macosx-10.13-x86_64-2.7/Users/Rex/cr/cryptominisat/python
creating build/temp.macosx-10.13-x86_64-2.7/Users/Rex/cr/cryptominisat/python/src
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -DLIBRARY_VERSION="5.0.1" -I/usr/local/include -I/usr/local/opt/openssl/include -I/usr/local/opt/sqlite/include -I/usr/local/Cellar/python/2.7.14/Frameworks/Python.framework/Versions/2.7/include/python2.7 -c /Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp -o build/temp.macosx-10.13-x86_64-2.7/Users/Rex/cr/cryptominisat/python/src/pycryptosat.o -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -fno-strict-aliasing -fno-common -dynamic -arch x86_64 -arch i386 -g -Os -pipe -fno-common -fno-strict-aliasing -fwrapv -DENABLE_DTRACE -DMACOSX -DNDEBUG -Wall -Wstrict-prototypes -Wshorten-64-to-32 -DNDEBUG -g -fwrapv -Os -Wall -Wstrict-prototypes -DENABLE_DTRACE -I/Users/Rex/cr/cryptominisat -I/Users/Rex/cr/cryptominisat/cmsat5-src
In file included from /Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:27:
In file included from /usr/local/Cellar/python/2.7.14/Frameworks/Python.framework/Versions/2.7/include/python2.7/Python.h:33:
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++/v1/stdio.h:108:15: fatal error: 
      'stdio.h' file not found
#include_next <stdio.h>
              ^~~~~~~~~
1 error generated.
error: command '/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc' failed with exit status 1
make[2]: *** [pycryptosat/build/timestamp] Error 1
make[1]: *** [pycryptosat/CMakeFiles/python_interface.dir/all] Error 2
make: *** [all] Error 2

make install:

make install
[ 81%] Built target libcryptominisat5
[ 89%] Built target cryptominisat5
[ 93%] Built target ipasircryptominisat5
[ 97%] Built target cryptominisat5_simple
Copying cryptominisat_c.h to /Users/Rex/cr/cryptominisat/include/cryptominisat5
Copying cryptominisat.h to /Users/Rex/cr/cryptominisat/include/cryptominisat5
Copying solvertypesmini.h to /Users/Rex/cr/cryptominisat/include/cryptominisat5
[ 97%] Built target CopyPublicHeaders
[100%] Generating build/timestamp
running build_ext
building 'pycryptosat' extension
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -DLIBRARY_VERSION="5.0.1" -I/usr/local/include -I/usr/local/opt/openssl/include -I/usr/local/opt/sqlite/include -I/usr/local/Cellar/python/2.7.14/Frameworks/Python.framework/Versions/2.7/include/python2.7 -c /Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp -o build/temp.macosx-10.13-x86_64-2.7/Users/Rex/cr/cryptominisat/python/src/pycryptosat.o -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -fno-strict-aliasing -fno-common -dynamic -arch x86_64 -arch i386 -g -Os -pipe -fno-common -fno-strict-aliasing -fwrapv -DENABLE_DTRACE -DMACOSX -DNDEBUG -Wall -Wstrict-prototypes -Wshorten-64-to-32 -DNDEBUG -g -fwrapv -Os -Wall -Wstrict-prototypes -DENABLE_DTRACE -I/Users/Rex/cr/cryptominisat -I/Users/Rex/cr/cryptominisat/cmsat5-src
In file included from /Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:27:
In file included from /usr/local/Cellar/python/2.7.14/Frameworks/Python.framework/Versions/2.7/include/python2.7/Python.h:33:
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++/v1/stdio.h:108:15: fatal error: 
      'stdio.h' file not found
#include_next <stdio.h>
              ^~~~~~~~~
1 error generated.
error: command '/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc' failed with exit status 1
make[2]: *** [pycryptosat/build/timestamp] Error 1
make[1]: *** [pycryptosat/CMakeFiles/python_interface.dir/all] Error 2
make: *** [all] Error 2

edit: I'm using High Sierra (10.13.1) if that makes any difference.

msoos commented 6 years ago

**Please follow the instructions that are on the main page and first make a 'build' directory, do NOT issue "cmake ." but as described in the main page, first make a build directory then change into that directory and "cmake .." **

So I suggest you delete the repository completely, the re-clone it, then follow instructions!

In case the above doesn't help. I am a bit confused because stdio.h error seems to indicate an issue with your installation. On TravisCI this actually works on MacOSX so I'm surprised. I would think this is an issue with your tool(s) installation, maybe brew, Xcode, etc. I am not familiar with Mac OS and have no access to one easily.

Can you take a peek at this?

https://stackoverflow.com/questions/23294226/compiling-gmp-for-ios-7-armv7s

Thanks,

Mate

RexYuan commented 6 years ago

The problem is probably with my mac then. I'll investigate further when I got the time and get back to you. Thanks, M8!

msoos commented 6 years ago

Not necessarily.... but I am confused. Can you please look at this:

https://travis-ci.org/msoos/cryptominisat/jobs/304303266

It's python2 here. Note that I have changed this a LOT since you opened this bugreport because I wanted to fix and improve what we had here... so please try again :) Please delete what you have, re-clone the repository, and then do the "mkdir build", "cd build" "cmake ..", "make" and "sudo make install". See where that goes :)

RexYuan commented 6 years ago

I recloned and tried to build again after reinstalling my Xcode and the command-line tools. It didn't work :(

make
Scanning dependencies of target libcryptominisat5
[  2%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cnf.cpp.o
[  4%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/propengine.cpp.o
[  6%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/varreplacer.cpp.o
/Users/Rex/cr/cryptominisat/src/varreplacer.cpp:1054:52: warning: declaration
      shadows a field of 'CMSat::VarReplacer' [-Wshadow]
void VarReplacer::Stats::print_short(const Solver* solver) const
                                                   ^
/Users/Rex/cr/cryptominisat/src/varreplacer.h:111:17: note: previous declaration
      is here
        Solver* solver;
                ^
1 warning generated.
[  8%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausecleaner.cpp.o
/Users/Rex/cr/cryptominisat/src/clausecleaner.cpp:243:63: warning: declaration
      shadows a field of 'CMSat::ClauseCleaner' [-Wshadow]
void ClauseCleaner::ImplicitData::update_solver_stats(Solver* solver)
                                                              ^
/Users/Rex/cr/cryptominisat/src/clausecleaner.h:88:17: note: previous
      declaration is here
        Solver* solver;
                ^
1 warning generated.
[ 10%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseusagestats.cpp.o
[ 12%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/prober.cpp.o
/Users/Rex/cr/cryptominisat/src/prober.cpp:887:47: warning: declaration shadows
      a field of 'CMSat::Prober' [-Wshadow]
void Prober::Stats::print_short(const Solver* solver, const bool time_ou...
                                              ^
/Users/Rex/cr/cryptominisat/src/prober.h:217:17: note: previous declaration is
      here
        Solver* solver; ///<The solver we are updating&working with
                ^
1 warning generated.
[ 14%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/occsimplifier.cpp.o
[ 16%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumestrengthen.cpp.o
/Users/Rex/cr/cryptominisat/src/subsumestrengthen.cpp:763:58: warning: 
      declaration shadows a field of 'CMSat::SubsumeStrengthen' [-Wshadow]
void SubsumeStrengthen::Stats::print_short(const Solver* solver) const
                                                         ^
/Users/Rex/cr/cryptominisat/src/subsumestrengthen.h:112:13: note: previous
      declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 18%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseallocator.cpp.o
[ 20%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sccfinder.cpp.o
/Users/Rex/cr/cryptominisat/src/sccfinder.cpp:198:44: warning: declaration
      shadows a field of 'CMSat::SCCFinder' [-Wshadow]
void SCCFinder::Stats::print_short(Solver* solver) const
                                           ^
/Users/Rex/cr/cryptominisat/src/sccfinder.h:117:17: note: previous declaration
      is here
        Solver* solver;
                ^
1 warning generated.
[ 22%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solverconf.cpp.o
[ 25%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerallwithall.cpp.o
/Users/Rex/cr/cryptominisat/src/distillerallwithall.cpp:351:60: warning: 
      declaration shadows a field of 'CMSat::DistillerAllWithAll' [-Wshadow]
void DistillerAllWithAll::Stats::print_short(const Solver* solver) const
                                                           ^
/Users/Rex/cr/cryptominisat/src/distillerallwithall.h:81:17: note: previous
      declaration is here
        Solver* solver;
                ^
1 warning generated.
[ 27%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerlongwithimpl.cpp.o
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.cpp:558:62: warning: 
      declaration shadows a field of 'CMSat::DistillerLongWithImpl' [-Wshadow]
void DistillerLongWithImpl::Stats::print_short(const Solver* solver) const
                                                             ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.h:173:17: note: previous
      declaration is here
        Solver* solver;
                ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.cpp:576:93: warning: 
      declaration shadows a field of 'CMSat::DistillerLongWithImpl' [-Wshadow]
  ...string type, const Solver* solver) const
                                ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.h:173:17: note: previous
      declaration is here
        Solver* solver;
                ^
2 warnings generated.
[ 29%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/str_impl_w_impl_stamp.cpp.o
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.cpp:195:21: warning: 
      declaration shadows a field of 'CMSat::StrImplWImplStamp' [-Wshadow]
    , const int64_t timeAvailable
                    ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.h:87:13: note: previous
      declaration is here
    int64_t timeAvailable;
            ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.cpp:197:15: warning: 
      declaration shadows a field of 'CMSat::StrImplWImplStamp' [-Wshadow]
    , Solver* solver
              ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.h:49:13: note: previous
      declaration is here
    Solver* solver;
            ^
2 warnings generated.
[ 31%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solutionextender.cpp.o
[ 33%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/completedetachreattacher.cpp.o
[ 35%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searcher.cpp.o
/Users/Rex/cr/cryptominisat/src/searcher.cpp:2317:26: warning: declaration
      shadows a local variable [-Wshadow]
                uint32_t v = order_heap[0];
                         ^
/Users/Rex/cr/cryptominisat/src/searcher.cpp:2309:18: note: previous declaration
      is here
        uint32_t v = var_Undef;
                 ^
/Users/Rex/cr/cryptominisat/src/searcher.cpp:3128:24: warning: unused parameter
      'cl_stats' [-Wunused-parameter]
    const ClauseStats& cl_stats
                       ^
2 warnings generated.
[ 37%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solver.cpp.o
[ 39%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sqlstats.cpp.o
[ 41%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/implcache.cpp.o
[ 43%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/stamp.cpp.o
[ 45%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/compfinder.cpp.o
[ 47%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/comphandler.cpp.o
[ 50%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/hyperengine.cpp.o
[ 52%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumeimplicit.cpp.o
/Users/Rex/cr/cryptominisat/src/subsumeimplicit.cpp:176:56: warning: 
      declaration shadows a field of 'CMSat::SubsumeImplicit' [-Wshadow]
void SubsumeImplicit::Stats::print_short(const Solver* solver) const
                                                       ^
/Users/Rex/cr/cryptominisat/src/subsumeimplicit.h:68:13: note: previous
      declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 54%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/datasync.cpp.o
[ 56%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/reducedb.cpp.o
[ 58%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausedumper.cpp.o
[ 60%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/bva.cpp.o
/Users/Rex/cr/cryptominisat/src/bva.cpp:545:54: warning: declaration shadows a
      field of 'CMSat::BVA' [-Wshadow]
string BVA::PotentialClause::to_string(const Solver* solver) const
                                                     ^
/Users/Rex/cr/cryptominisat/src/bva.h:46:13: note: previous declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 62%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/intree.cpp.o
[ 64%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_calc.cpp.o
[ 66%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_to_reconf.cpp.o
[ 68%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solvefeatures.cpp.o
[ 70%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searchstats.cpp.o
[ 72%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/xorfinder.cpp.o
/Users/Rex/cr/cryptominisat/src/xorfinder.cpp:396:22: warning: declaration
      shadows a local variable [-Wshadow]
        for(uint32_t v: x_new) {
                     ^
/Users/Rex/cr/cryptominisat/src/xorfinder.cpp:360:24: note: previous declaration
      is here
        const uint32_t v = interesting.back();
                       ^
/Users/Rex/cr/cryptominisat/src/xorfinder.cpp:621:50: warning: declaration
      shadows a field of 'CMSat::XorFinder' [-Wshadow]
void XorFinder::Stats::print_short(const Solver* solver) const
                                                 ^
/Users/Rex/cr/cryptominisat/src/xorfinder.h:187:13: note: previous declaration
      is here
    Solver *solver;
            ^
2 warnings generated.
[ 75%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat_c.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/cryptominisat_c.cpp:25:
/Users/Rex/cr/cryptominisat/build/cmsat5-src/cryptominisat5/cryptominisat.h:43:5: warning: 
      'SATSolver' defined as a class here but previously declared as a struct
      [-Wmismatched-tags]
    class SATSolver
    ^
/Users/Rex/cr/cryptominisat/build/cmsat5-src/cryptominisat5/cryptominisat_c.h:35:22: note: 
      did you mean class here?
    namespace CMSat{ struct SATSolver; }
                     ^~~~~~
                     class
1 warning generated.
[ 77%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/GitSHA1.cpp.o
[ 79%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:25:
In file included from /Users/Rex/cr/cryptominisat/src/solver.h:36:
In file included from /Users/Rex/cr/cryptominisat/src/propengine.h:43:
In file included from /Users/Rex/cr/cryptominisat/src/cnf.h:36:
/Users/Rex/cr/cryptominisat/src/drat.h:95:10: warning: 'get_conf_id' overrides a
      member function but is not marked 'override'
      [-Winconsistent-missing-override]
    bool get_conf_id() {
         ^
/Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:758:20: note: in instantiation
      of template class 'CMSat::DratFile<true>' requested here
        drat = new DratFile<true>;
                   ^
/Users/Rex/cr/cryptominisat/src/drat.h:52:18: note: overridden virtual function
      is here
    virtual bool get_conf_id() {
                 ^
/Users/Rex/cr/cryptominisat/src/drat.h:95:10: warning: 'get_conf_id' overrides a
      member function but is not marked 'override'
      [-Winconsistent-missing-override]
    bool get_conf_id() {
         ^
/Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:760:20: note: in instantiation
      of template class 'CMSat::DratFile<false>' requested here
        drat = new DratFile<false>;
                   ^
/Users/Rex/cr/cryptominisat/src/drat.h:52:18: note: overridden virtual function
      is here
    virtual bool get_conf_id() {
                 ^
2 warnings generated.
[ 81%] Linking CXX shared library ../lib/libcryptominisat5.dylib
[ 81%] Built target libcryptominisat5
Scanning dependencies of target cryptominisat5
[ 83%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/main.cpp:48:
/Users/Rex/cr/cryptominisat/src/main.h:83:43: warning: extra ';' after member
      function definition [-Wextra-semi]
        virtual void call_after_parse() {};
                                          ^
1 warning generated.
[ 85%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main_exe.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/main_exe.cpp:24:
/Users/Rex/cr/cryptominisat/src/main.h:83:43: warning: extra ';' after member
      function definition [-Wextra-semi]
        virtual void call_after_parse() {};
                                          ^
1 warning generated.
[ 87%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/signalcode.cpp.o
[ 89%] Linking CXX executable ../cryptominisat5
[ 89%] Built target cryptominisat5
Scanning dependencies of target ipasircryptominisat5
[ 91%] Building CXX object cmsat5-src/CMakeFiles/ipasircryptominisat5.dir/ipasir.cpp.o
[ 93%] Linking CXX shared library ../lib/libipasircryptominisat5.dylib
[ 93%] Built target ipasircryptominisat5
Scanning dependencies of target cryptominisat5_simple
[ 95%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5_simple.dir/main_simple.cpp.o
[ 97%] Linking CXX executable ../cryptominisat5_simple
[ 97%] Built target cryptominisat5_simple
Scanning dependencies of target CopyPublicHeaders
Copying cryptominisat_c.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
Copying cryptominisat.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
Copying solvertypesmini.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
[ 97%] Built target CopyPublicHeaders
Scanning dependencies of target python_interface
[100%] Generating build/timestamp
running build_ext
building 'pycryptosat' extension
creating build
creating build/temp.macosx-10.12-x86_64-3.6
creating build/temp.macosx-10.12-x86_64-3.6/Users
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python/src
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -DLIBRARY_VERSION="5.0.1" -I/usr/local/include -I/usr/local/opt/openssl/include -I/usr/local/opt/sqlite/include -I/usr/local/Cellar/python3/3.6.3/Frameworks/Python.framework/Versions/3.6/include/python3.6m -c /Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp -o build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python/src/pycryptosat.o -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -fno-strict-aliasing -fno-common -dynamic -arch x86_64 -arch i386 -g -Os -pipe -fno-common -fno-strict-aliasing -fwrapv -DENABLE_DTRACE -DMACOSX -DNDEBUG -Wall -Wstrict-prototypes -Wshorten-64-to-32 -DNDEBUG -g -fwrapv -Os -Wall -Wstrict-prototypes -DENABLE_DTRACE -I/Users/Rex/cr/cryptominisat -I/Users/Rex/cr/cryptominisat/build/cmsat5-src
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:179:28: warning: 
      implicit conversion loses integer precision: 'long' to 'uint32_t'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        lits.push_back(Lit(var, sign));
                       ~~~ ^~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:222:24: warning: 
      implicit conversion loses integer precision: 'long' to 'value_type'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        vars.push_back(var);
             ~~~~~~~~~ ^~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:344:57: error: ordered
      comparison between pointer and zero ('PyObject *' (aka '_object *') and
      'int')
    if (PyTuple_SET_ITEM(tuple, (Py_ssize_t)0, Py_None) < 0) {
        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ^ ~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:368:64: error: ordered
      comparison between pointer and zero ('PyObject *' (aka '_object *') and
      'int')
        if (PyTuple_SET_ITEM(tuple, (Py_ssize_t)i+1, py_value) < 0) {
            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ^ ~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:403:68: error: ordered
      comparison between pointer and zero ('PyObject *' (aka '_object *') and
      'int')
            if (PyTuple_SET_ITEM(tuple, (Py_ssize_t)var, py_value) < 0) {
                ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ^ ~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:462:39: warning: 
      implicit conversion loses integer precision: 'long' to 'uint32_t'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        assumption_lits.push_back(Lit(var, sign));
                                  ~~~ ^~~
3 warnings and 3 errors generated.
error: command '/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc' failed with exit status 1
make[2]: *** [pycryptosat/build/timestamp] Error 1
make[1]: *** [pycryptosat/CMakeFiles/python_interface.dir/all] Error 2
make: *** [all] Error 2

I'm trying to figure out what went wrong exactly with my Xcode. I've probably somehow messed up too much my system. Sorry ;(

I'm not sure what to look at on TravisCI. Anyway, this probably doesn't make a difference, but my clang is:

clang --version
Apple LLVM version 9.0.0 (clang-900.0.38)
Target: x86_64-apple-darwin17.2.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin
capiman commented 6 years ago

@Mate: There is following page: https://docs.travis-ci.com/user/reference/osx/#OS-X-Version There is mentioned: Xcode 9.1 is available by adding osx_image: xcode9.1 to your .travis.yml. Seems to be newest/latest version. Perhaps it helps to reproduce the problem on Travis CI?

msoos commented 6 years ago

Waaaait... your new error seems a LOT better :) That can actually be fixed! You fixed the major error around the standard library, yay! I think I can fix this now, thanks! :)

msoos commented 6 years ago

OK, gave it a shot :) Can you please check it again? I think it should work (or there may be another issue, but the ones above have been fixed AFAIK). Thanks!

RexYuan commented 6 years ago

Those old errors are gone! 🎆 But there are some new ones...

make                   
Scanning dependencies of target libcryptominisat5
[  2%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cnf.cpp.o
[  4%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/propengine.cpp.o
[  6%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/varreplacer.cpp.o
/Users/Rex/cr/cryptominisat/src/varreplacer.cpp:1054:52: warning: declaration
      shadows a field of 'CMSat::VarReplacer' [-Wshadow]
void VarReplacer::Stats::print_short(const Solver* solver) const
                                                   ^
/Users/Rex/cr/cryptominisat/src/varreplacer.h:111:17: note: previous declaration
      is here
        Solver* solver;
                ^
1 warning generated.
[  8%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausecleaner.cpp.o
/Users/Rex/cr/cryptominisat/src/clausecleaner.cpp:243:63: warning: declaration
      shadows a field of 'CMSat::ClauseCleaner' [-Wshadow]
void ClauseCleaner::ImplicitData::update_solver_stats(Solver* solver)
                                                              ^
/Users/Rex/cr/cryptominisat/src/clausecleaner.h:88:17: note: previous
      declaration is here
        Solver* solver;
                ^
1 warning generated.
[ 10%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseusagestats.cpp.o
[ 12%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/prober.cpp.o
/Users/Rex/cr/cryptominisat/src/prober.cpp:887:47: warning: declaration shadows
      a field of 'CMSat::Prober' [-Wshadow]
void Prober::Stats::print_short(const Solver* solver, const bool time_ou...
                                              ^
/Users/Rex/cr/cryptominisat/src/prober.h:217:17: note: previous declaration is
      here
        Solver* solver; ///<The solver we are updating&working with
                ^
1 warning generated.
[ 14%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/occsimplifier.cpp.o
[ 16%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumestrengthen.cpp.o
/Users/Rex/cr/cryptominisat/src/subsumestrengthen.cpp:763:58: warning: 
      declaration shadows a field of 'CMSat::SubsumeStrengthen' [-Wshadow]
void SubsumeStrengthen::Stats::print_short(const Solver* solver) const
                                                         ^
/Users/Rex/cr/cryptominisat/src/subsumestrengthen.h:112:13: note: previous
      declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 18%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseallocator.cpp.o
[ 20%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sccfinder.cpp.o
/Users/Rex/cr/cryptominisat/src/sccfinder.cpp:198:44: warning: declaration
      shadows a field of 'CMSat::SCCFinder' [-Wshadow]
void SCCFinder::Stats::print_short(Solver* solver) const
                                           ^
/Users/Rex/cr/cryptominisat/src/sccfinder.h:117:17: note: previous declaration
      is here
        Solver* solver;
                ^
1 warning generated.
[ 22%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solverconf.cpp.o
[ 25%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerallwithall.cpp.o
/Users/Rex/cr/cryptominisat/src/distillerallwithall.cpp:351:60: warning: 
      declaration shadows a field of 'CMSat::DistillerAllWithAll' [-Wshadow]
void DistillerAllWithAll::Stats::print_short(const Solver* solver) const
                                                           ^
/Users/Rex/cr/cryptominisat/src/distillerallwithall.h:81:17: note: previous
      declaration is here
        Solver* solver;
                ^
1 warning generated.
[ 27%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerlongwithimpl.cpp.o
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.cpp:558:62: warning: 
      declaration shadows a field of 'CMSat::DistillerLongWithImpl' [-Wshadow]
void DistillerLongWithImpl::Stats::print_short(const Solver* solver) const
                                                             ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.h:173:17: note: previous
      declaration is here
        Solver* solver;
                ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.cpp:576:93: warning: 
      declaration shadows a field of 'CMSat::DistillerLongWithImpl' [-Wshadow]
  ...string type, const Solver* solver) const
                                ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.h:173:17: note: previous
      declaration is here
        Solver* solver;
                ^
2 warnings generated.
[ 29%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/str_impl_w_impl_stamp.cpp.o
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.cpp:195:21: warning: 
      declaration shadows a field of 'CMSat::StrImplWImplStamp' [-Wshadow]
    , const int64_t timeAvailable
                    ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.h:87:13: note: previous
      declaration is here
    int64_t timeAvailable;
            ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.cpp:197:15: warning: 
      declaration shadows a field of 'CMSat::StrImplWImplStamp' [-Wshadow]
    , Solver* solver
              ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.h:49:13: note: previous
      declaration is here
    Solver* solver;
            ^
2 warnings generated.
[ 31%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solutionextender.cpp.o
[ 33%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/completedetachreattacher.cpp.o
[ 35%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searcher.cpp.o
/Users/Rex/cr/cryptominisat/src/searcher.cpp:3128:24: warning: unused parameter
      'cl_stats' [-Wunused-parameter]
    const ClauseStats& cl_stats
                       ^
1 warning generated.
[ 37%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solver.cpp.o
[ 39%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sqlstats.cpp.o
[ 41%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/implcache.cpp.o
[ 43%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/stamp.cpp.o
[ 45%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/compfinder.cpp.o
[ 47%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/comphandler.cpp.o
[ 50%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/hyperengine.cpp.o
[ 52%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumeimplicit.cpp.o
/Users/Rex/cr/cryptominisat/src/subsumeimplicit.cpp:176:56: warning: 
      declaration shadows a field of 'CMSat::SubsumeImplicit' [-Wshadow]
void SubsumeImplicit::Stats::print_short(const Solver* solver) const
                                                       ^
/Users/Rex/cr/cryptominisat/src/subsumeimplicit.h:68:13: note: previous
      declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 54%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/datasync.cpp.o
[ 56%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/reducedb.cpp.o
[ 58%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausedumper.cpp.o
[ 60%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/bva.cpp.o
/Users/Rex/cr/cryptominisat/src/bva.cpp:545:54: warning: declaration shadows a
      field of 'CMSat::BVA' [-Wshadow]
string BVA::PotentialClause::to_string(const Solver* solver) const
                                                     ^
/Users/Rex/cr/cryptominisat/src/bva.h:46:13: note: previous declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 62%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/intree.cpp.o
[ 64%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_calc.cpp.o
[ 66%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_to_reconf.cpp.o
[ 68%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solvefeatures.cpp.o
[ 70%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searchstats.cpp.o
[ 72%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/xorfinder.cpp.o
/Users/Rex/cr/cryptominisat/src/xorfinder.cpp:621:50: warning: declaration
      shadows a field of 'CMSat::XorFinder' [-Wshadow]
void XorFinder::Stats::print_short(const Solver* solver) const
                                                 ^
/Users/Rex/cr/cryptominisat/src/xorfinder.h:187:13: note: previous declaration
      is here
    Solver *solver;
            ^
1 warning generated.
[ 75%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat_c.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/cryptominisat_c.cpp:25:
/Users/Rex/cr/cryptominisat/build/cmsat5-src/cryptominisat5/cryptominisat.h:43:5: warning: 
      'SATSolver' defined as a class here but previously declared as a struct
      [-Wmismatched-tags]
    class SATSolver
    ^
/Users/Rex/cr/cryptominisat/build/cmsat5-src/cryptominisat5/cryptominisat_c.h:35:22: note: 
      did you mean class here?
    namespace CMSat{ struct SATSolver; }
                     ^~~~~~
                     class
1 warning generated.
[ 77%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/GitSHA1.cpp.o
[ 79%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:25:
In file included from /Users/Rex/cr/cryptominisat/src/solver.h:36:
In file included from /Users/Rex/cr/cryptominisat/src/propengine.h:43:
In file included from /Users/Rex/cr/cryptominisat/src/cnf.h:36:
/Users/Rex/cr/cryptominisat/src/drat.h:95:10: warning: 'get_conf_id' overrides a
      member function but is not marked 'override'
      [-Winconsistent-missing-override]
    bool get_conf_id() {
         ^
/Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:758:20: note: in instantiation
      of template class 'CMSat::DratFile<true>' requested here
        drat = new DratFile<true>;
                   ^
/Users/Rex/cr/cryptominisat/src/drat.h:52:18: note: overridden virtual function
      is here
    virtual bool get_conf_id() {
                 ^
/Users/Rex/cr/cryptominisat/src/drat.h:95:10: warning: 'get_conf_id' overrides a
      member function but is not marked 'override'
      [-Winconsistent-missing-override]
    bool get_conf_id() {
         ^
/Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:760:20: note: in instantiation
      of template class 'CMSat::DratFile<false>' requested here
        drat = new DratFile<false>;
                   ^
/Users/Rex/cr/cryptominisat/src/drat.h:52:18: note: overridden virtual function
      is here
    virtual bool get_conf_id() {
                 ^
2 warnings generated.
[ 81%] Linking CXX shared library ../lib/libcryptominisat5.dylib
[ 81%] Built target libcryptominisat5
Scanning dependencies of target cryptominisat5
[ 83%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/main.cpp:48:
/Users/Rex/cr/cryptominisat/src/main.h:83:43: warning: extra ';' after member
      function definition [-Wextra-semi]
        virtual void call_after_parse() {};
                                          ^
1 warning generated.
[ 85%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main_exe.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/main_exe.cpp:24:
/Users/Rex/cr/cryptominisat/src/main.h:83:43: warning: extra ';' after member
      function definition [-Wextra-semi]
        virtual void call_after_parse() {};
                                          ^
1 warning generated.
[ 87%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/signalcode.cpp.o
[ 89%] Linking CXX executable ../cryptominisat5
[ 89%] Built target cryptominisat5
Scanning dependencies of target ipasircryptominisat5
[ 91%] Building CXX object cmsat5-src/CMakeFiles/ipasircryptominisat5.dir/ipasir.cpp.o
[ 93%] Linking CXX shared library ../lib/libipasircryptominisat5.dylib
[ 93%] Built target ipasircryptominisat5
Scanning dependencies of target cryptominisat5_simple
[ 95%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5_simple.dir/main_simple.cpp.o
[ 97%] Linking CXX executable ../cryptominisat5_simple
[ 97%] Built target cryptominisat5_simple
Scanning dependencies of target CopyPublicHeaders
Copying cryptominisat_c.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
Copying cryptominisat.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
Copying solvertypesmini.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
[ 97%] Built target CopyPublicHeaders
Scanning dependencies of target python_interface
[100%] Generating build/timestamp
running build_ext
building 'pycryptosat' extension
creating build
creating build/temp.macosx-10.12-x86_64-3.6
creating build/temp.macosx-10.12-x86_64-3.6/Users
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python/src
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -DLIBRARY_VERSION="5.0.1" -I/usr/local/include -I/usr/local/opt/openssl/include -I/usr/local/opt/sqlite/include -I/usr/local/Cellar/python3/3.6.3/Frameworks/Python.framework/Versions/3.6/include/python3.6m -c /Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp -o build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python/src/pycryptosat.o -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -fno-strict-aliasing -fno-common -dynamic -arch x86_64 -arch i386 -g -Os -pipe -fno-common -fno-strict-aliasing -fwrapv -DENABLE_DTRACE -DMACOSX -DNDEBUG -Wall -Wstrict-prototypes -Wshorten-64-to-32 -DNDEBUG -g -fwrapv -Os -Wall -Wstrict-prototypes -DENABLE_DTRACE -I/Users/Rex/cr/cryptominisat -I/Users/Rex/cr/cryptominisat/build/cmsat5-src
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:179:28: warning: 
      implicit conversion loses integer precision: 'long' to 'uint32_t'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        lits.push_back(Lit(var, sign));
                       ~~~ ^~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:222:24: warning: 
      implicit conversion loses integer precision: 'long' to 'value_type'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        vars.push_back(var);
             ~~~~~~~~~ ^~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:446:39: warning: 
      implicit conversion loses integer precision: 'long' to 'uint32_t'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        assumption_lits.push_back(Lit(var, sign));
                                  ~~~ ^~~
3 warnings generated.
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:173:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= self->cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:216:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= self->cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:440:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~
3 warnings generated.
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ -shared -g -W -Wall -Wno-deprecated build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python/src/pycryptosat.o -L. -L/Users/Rex/cr/cryptominisat/build/lib -L/usr/local/lib -L/usr/local/opt/openssl/lib -L/usr/local/opt/sqlite/lib -L/usr/local/lib -L../lib -lcryptominisat5 -o /Users/Rex/cr/cryptominisat/build/pycryptosat/pycryptosat.cpython-36m-darwin.so -L/System/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/config -lpython2.7 -ldl -framework CoreFoundation
Undefined symbols for architecture x86_64:
  "_PyModule_Create2", referenced from:
      _PyInit_pycryptosat in pycryptosat.o
  "_PyUnicode_FromString", referenced from:
      _PyInit_pycryptosat in pycryptosat.o
  "__Py_FalseStruct", referenced from:
      solve(Solver*, _object*, _object*) in pycryptosat.o
      is_satisfiable(Solver*) in pycryptosat.o
      get_solution(CMSat::SATSolver*) in pycryptosat.o
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: command '/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++' failed with exit status 1
make[2]: *** [pycryptosat/build/timestamp] Error 1
make[1]: *** [pycryptosat/CMakeFiles/python_interface.dir/all] Error 2
make: *** [all] Error 2

From Googling it looks maybe like I didn't completely clean up the old unsuccessful compiles? Or something to do with linker flags but I'm not sure.

msoos commented 6 years ago

Yes. Please re-compile from scratch. I hope you created a "build" directory. So please delete the "build" directory and then recreate, move into it, and "cmake .." and make then. If you do not have a "build" directory then you are not following the instructions and therefore I cannot help, as you must first help yourself before I can help you :)

So, delete "build", create again, compile again (inside build!!) and see what happens :)

RexYuan commented 6 years ago

Sorry I wasn't clear. That I did. I remove the entire cryptominisat, reclone, make a build folder, cmake and make there every time. I was wondering if the old make install runs installed something in other places.

edit:

~/cr/cryptominisat/build master*
❯ cd ..

~/cr/cryptominisat master*
❯ cd ..

~/cr
❯ trash cryptominisat

~/cr
❯ ls

~/cr
❯ git clone https://github.com/msoos/cryptominisat.git
Cloning into 'cryptominisat'...
warning: templates not found /Users/Rex/.git_template
remote: Counting objects: 55496, done.
remote: Compressing objects: 100% (218/218), done.
remote: Total 55496 (delta 245), reused 241 (delta 144), pack-reused 55133
Receiving objects: 100% (55496/55496), 50.70 MiB | 1.90 MiB/s, done.
Resolving deltas: 100% (42840/42840), done.

~/cr 31s
❯ cd cryptominisat 

~/cr/cryptominisat master
❯ mkdir build && cd build

~/cr/cryptominisat/build master
❯ cmake ..        
-- LIB directory is 'lib'
-- BIN directory is 'bin'
-- You can choose the type of build, options are:Debug;Release;RelWithDebInfo;MinSizeRel
-- Doing a RelWithDebInfo build
-- The C compiler identification is AppleClang 9.0.0.9000038
-- The CXX compiler identification is AppleClang 9.0.0.9000038
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Looking for pthread.h
-- Looking for pthread.h - found
-- Looking for pthread_create
-- Looking for pthread_create - found
-- 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 - 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_-ggdb3
-- Performing Test HAVE_FLAG_-ggdb3 - Success
-- Compiling for dynamic library use
-- GIT hash found: e4ca77bff8612ffb06947584157340a9c3b71a8c
-- PROJECT_VERSION: 5.0.1
-- PROJECT_VERSION_MAJOR: 5
-- PROJECT_VERSION_MINOR: 0
-- PROJECT_VERSION_PATCH: 1
-- Boost version: 1.65.1
-- Found the following Boost libraries:
--   program_options
-- Not compiling detailed statistics. Leads to faster system
-- Found ZLIB: /usr/lib/libz.dylib (found version "1.2.11") 
-- OK, Found ZLIB!
-- Valgrind Prefix: 
-- Found VALGRIND: /usr/local/include/valgrind  
-- Cannot find valgrind or it's disabled, we will not be able to mark memory pool objects as undefined
-- Found PkgConfig: /usr/local/bin/pkg-config (found version "0.29.2") 
-- Could NOT find m4ri (missing: M4RI_LIBRARIES M4RI_INCLUDE_DIRS) 
CMake Warning at CMakeLists.txt:431 (MESSAGE):
  Did not find M4RI, XOR detection&manipulation disabled

-- All defines at startup:  -DBOOST_TEST_DYN_LINK -DUSE_ZLIB
-- Found PythonInterp: /usr/local/bin/python3 (found suitable version "3.6.3", minimum required is "3") 
-- Found PythonLibs: /usr/local/Frameworks/Python.framework/Versions/3.6/lib/libpython3.6m.dylib (found suitable version "3.6.3", minimum required is "3") 
-- PYTHON_EXECUTABLE=/usr/local/bin/python3
-- PYTHON_LIBRARIES=/usr/local/Frameworks/Python.framework/Versions/3.6/lib/libpython3.6m.dylib
-- PYTHON_INCLUDE_DIRS=/usr/local/Frameworks/Python.framework/Versions/3.6/include/python3.6m
-- PYTHONLIBS_VERSION_STRING=3.6.3
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion - Success
-- Performing Test HAVE_FLAG_-Wlogical-op
-- Performing Test HAVE_FLAG_-Wlogical-op - Failed
-- Performing Test HAVE_FLAG_-Wrestrict
-- Performing Test HAVE_FLAG_-Wrestrict - Failed
-- Performing Test HAVE_FLAG_-Wnull-dereference
-- Performing Test HAVE_FLAG_-Wnull-dereference - Success
-- Performing Test HAVE_FLAG_-Wjump-misses-init
-- Performing Test HAVE_FLAG_-Wjump-misses-init - Failed
-- 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
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY - Success
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY - Success
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR - Success
CMake Warning at CMakeLists.txt:538 (message):
  Testing is disabled

-- Found python interpreter, libs and header files
-- Building python interface
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/Rex/cr/cryptominisat/build

~/cr/cryptominisat/build master* 17s
❯ make                   
Scanning dependencies of target libcryptominisat5
[  2%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cnf.cpp.o
[  4%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/propengine.cpp.o
[  6%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/varreplacer.cpp.o
/Users/Rex/cr/cryptominisat/src/varreplacer.cpp:1054:52: warning: declaration
      shadows a field of 'CMSat::VarReplacer' [-Wshadow]
void VarReplacer::Stats::print_short(const Solver* solver) const
                                                   ^
/Users/Rex/cr/cryptominisat/src/varreplacer.h:111:17: note: previous declaration
      is here
        Solver* solver;
                ^
1 warning generated.
[  8%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausecleaner.cpp.o
/Users/Rex/cr/cryptominisat/src/clausecleaner.cpp:243:63: warning: declaration
      shadows a field of 'CMSat::ClauseCleaner' [-Wshadow]
void ClauseCleaner::ImplicitData::update_solver_stats(Solver* solver)
                                                              ^
/Users/Rex/cr/cryptominisat/src/clausecleaner.h:88:17: note: previous
      declaration is here
        Solver* solver;
                ^
1 warning generated.
[ 10%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseusagestats.cpp.o
[ 12%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/prober.cpp.o
/Users/Rex/cr/cryptominisat/src/prober.cpp:887:47: warning: declaration shadows
      a field of 'CMSat::Prober' [-Wshadow]
void Prober::Stats::print_short(const Solver* solver, const bool time_ou...
                                              ^
/Users/Rex/cr/cryptominisat/src/prober.h:217:17: note: previous declaration is
      here
        Solver* solver; ///<The solver we are updating&working with
                ^
1 warning generated.
[ 14%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/occsimplifier.cpp.o
[ 16%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumestrengthen.cpp.o
/Users/Rex/cr/cryptominisat/src/subsumestrengthen.cpp:763:58: warning: 
      declaration shadows a field of 'CMSat::SubsumeStrengthen' [-Wshadow]
void SubsumeStrengthen::Stats::print_short(const Solver* solver) const
                                                         ^
/Users/Rex/cr/cryptominisat/src/subsumestrengthen.h:112:13: note: previous
      declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 18%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clauseallocator.cpp.o
[ 20%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sccfinder.cpp.o
/Users/Rex/cr/cryptominisat/src/sccfinder.cpp:198:44: warning: declaration
      shadows a field of 'CMSat::SCCFinder' [-Wshadow]
void SCCFinder::Stats::print_short(Solver* solver) const
                                           ^
/Users/Rex/cr/cryptominisat/src/sccfinder.h:117:17: note: previous declaration
      is here
        Solver* solver;
                ^
1 warning generated.
[ 22%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solverconf.cpp.o
[ 25%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerallwithall.cpp.o
/Users/Rex/cr/cryptominisat/src/distillerallwithall.cpp:351:60: warning: 
      declaration shadows a field of 'CMSat::DistillerAllWithAll' [-Wshadow]
void DistillerAllWithAll::Stats::print_short(const Solver* solver) const
                                                           ^
/Users/Rex/cr/cryptominisat/src/distillerallwithall.h:81:17: note: previous
      declaration is here
        Solver* solver;
                ^
1 warning generated.
[ 27%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/distillerlongwithimpl.cpp.o
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.cpp:558:62: warning: 
      declaration shadows a field of 'CMSat::DistillerLongWithImpl' [-Wshadow]
void DistillerLongWithImpl::Stats::print_short(const Solver* solver) const
                                                             ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.h:173:17: note: previous
      declaration is here
        Solver* solver;
                ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.cpp:576:93: warning: 
      declaration shadows a field of 'CMSat::DistillerLongWithImpl' [-Wshadow]
  ...string type, const Solver* solver) const
                                ^
/Users/Rex/cr/cryptominisat/src/distillerlongwithimpl.h:173:17: note: previous
      declaration is here
        Solver* solver;
                ^
2 warnings generated.
[ 29%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/str_impl_w_impl_stamp.cpp.o
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.cpp:195:21: warning: 
      declaration shadows a field of 'CMSat::StrImplWImplStamp' [-Wshadow]
    , const int64_t timeAvailable
                    ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.h:87:13: note: previous
      declaration is here
    int64_t timeAvailable;
            ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.cpp:197:15: warning: 
      declaration shadows a field of 'CMSat::StrImplWImplStamp' [-Wshadow]
    , Solver* solver
              ^
/Users/Rex/cr/cryptominisat/src/str_impl_w_impl_stamp.h:49:13: note: previous
      declaration is here
    Solver* solver;
            ^
2 warnings generated.
[ 31%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solutionextender.cpp.o
[ 33%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/completedetachreattacher.cpp.o
[ 35%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searcher.cpp.o
/Users/Rex/cr/cryptominisat/src/searcher.cpp:3128:24: warning: unused parameter
      'cl_stats' [-Wunused-parameter]
    const ClauseStats& cl_stats
                       ^
1 warning generated.
[ 37%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solver.cpp.o
[ 39%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/sqlstats.cpp.o
[ 41%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/implcache.cpp.o
[ 43%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/stamp.cpp.o
[ 45%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/compfinder.cpp.o
[ 47%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/comphandler.cpp.o
[ 50%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/hyperengine.cpp.o
[ 52%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/subsumeimplicit.cpp.o
/Users/Rex/cr/cryptominisat/src/subsumeimplicit.cpp:176:56: warning: 
      declaration shadows a field of 'CMSat::SubsumeImplicit' [-Wshadow]
void SubsumeImplicit::Stats::print_short(const Solver* solver) const
                                                       ^
/Users/Rex/cr/cryptominisat/src/subsumeimplicit.h:68:13: note: previous
      declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 54%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/datasync.cpp.o
[ 56%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/reducedb.cpp.o
[ 58%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/clausedumper.cpp.o
[ 60%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/bva.cpp.o
/Users/Rex/cr/cryptominisat/src/bva.cpp:545:54: warning: declaration shadows a
      field of 'CMSat::BVA' [-Wshadow]
string BVA::PotentialClause::to_string(const Solver* solver) const
                                                     ^
/Users/Rex/cr/cryptominisat/src/bva.h:46:13: note: previous declaration is here
    Solver* solver;
            ^
1 warning generated.
[ 62%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/intree.cpp.o
[ 64%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_calc.cpp.o
[ 66%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/features_to_reconf.cpp.o
[ 68%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/solvefeatures.cpp.o
[ 70%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/searchstats.cpp.o
[ 72%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/xorfinder.cpp.o
/Users/Rex/cr/cryptominisat/src/xorfinder.cpp:621:50: warning: declaration
      shadows a field of 'CMSat::XorFinder' [-Wshadow]
void XorFinder::Stats::print_short(const Solver* solver) const
                                                 ^
/Users/Rex/cr/cryptominisat/src/xorfinder.h:187:13: note: previous declaration
      is here
    Solver *solver;
            ^
1 warning generated.
[ 75%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat_c.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/cryptominisat_c.cpp:25:
/Users/Rex/cr/cryptominisat/build/cmsat5-src/cryptominisat5/cryptominisat.h:43:5: warning: 
      'SATSolver' defined as a class here but previously declared as a struct
      [-Wmismatched-tags]
    class SATSolver
    ^
/Users/Rex/cr/cryptominisat/build/cmsat5-src/cryptominisat5/cryptominisat_c.h:35:22: note: 
      did you mean class here?
    namespace CMSat{ struct SATSolver; }
                     ^~~~~~
                     class
1 warning generated.
[ 77%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/GitSHA1.cpp.o
[ 79%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:25:
In file included from /Users/Rex/cr/cryptominisat/src/solver.h:36:
In file included from /Users/Rex/cr/cryptominisat/src/propengine.h:43:
In file included from /Users/Rex/cr/cryptominisat/src/cnf.h:36:
/Users/Rex/cr/cryptominisat/src/drat.h:95:10: warning: 'get_conf_id' overrides a
      member function but is not marked 'override'
      [-Winconsistent-missing-override]
    bool get_conf_id() {
         ^
/Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:758:20: note: in instantiation
      of template class 'CMSat::DratFile<true>' requested here
        drat = new DratFile<true>;
                   ^
/Users/Rex/cr/cryptominisat/src/drat.h:52:18: note: overridden virtual function
      is here
    virtual bool get_conf_id() {
                 ^
/Users/Rex/cr/cryptominisat/src/drat.h:95:10: warning: 'get_conf_id' overrides a
      member function but is not marked 'override'
      [-Winconsistent-missing-override]
    bool get_conf_id() {
         ^
/Users/Rex/cr/cryptominisat/src/cryptominisat.cpp:760:20: note: in instantiation
      of template class 'CMSat::DratFile<false>' requested here
        drat = new DratFile<false>;
                   ^
/Users/Rex/cr/cryptominisat/src/drat.h:52:18: note: overridden virtual function
      is here
    virtual bool get_conf_id() {
                 ^
2 warnings generated.
[ 81%] Linking CXX shared library ../lib/libcryptominisat5.dylib
[ 81%] Built target libcryptominisat5
Scanning dependencies of target cryptominisat5
[ 83%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/main.cpp:48:
/Users/Rex/cr/cryptominisat/src/main.h:83:43: warning: extra ';' after member
      function definition [-Wextra-semi]
        virtual void call_after_parse() {};
                                          ^
1 warning generated.
[ 85%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/main_exe.cpp.o
In file included from /Users/Rex/cr/cryptominisat/src/main_exe.cpp:24:
/Users/Rex/cr/cryptominisat/src/main.h:83:43: warning: extra ';' after member
      function definition [-Wextra-semi]
        virtual void call_after_parse() {};
                                          ^
1 warning generated.
[ 87%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/signalcode.cpp.o
[ 89%] Linking CXX executable ../cryptominisat5
[ 89%] Built target cryptominisat5
Scanning dependencies of target ipasircryptominisat5
[ 91%] Building CXX object cmsat5-src/CMakeFiles/ipasircryptominisat5.dir/ipasir.cpp.o
[ 93%] Linking CXX shared library ../lib/libipasircryptominisat5.dylib
[ 93%] Built target ipasircryptominisat5
Scanning dependencies of target cryptominisat5_simple
[ 95%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5_simple.dir/main_simple.cpp.o
[ 97%] Linking CXX executable ../cryptominisat5_simple
[ 97%] Built target cryptominisat5_simple
Scanning dependencies of target CopyPublicHeaders
Copying cryptominisat_c.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
Copying cryptominisat.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
Copying solvertypesmini.h to /Users/Rex/cr/cryptominisat/build/include/cryptominisat5
[ 97%] Built target CopyPublicHeaders
Scanning dependencies of target python_interface
[100%] Generating build/timestamp
running build_ext
building 'pycryptosat' extension
creating build
creating build/temp.macosx-10.12-x86_64-3.6
creating build/temp.macosx-10.12-x86_64-3.6/Users
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python
creating build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python/src
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -DLIBRARY_VERSION="5.0.1" -I/usr/local/include -I/usr/local/opt/openssl/include -I/usr/local/opt/sqlite/include -I/usr/local/Cellar/python3/3.6.3/Frameworks/Python.framework/Versions/3.6/include/python3.6m -c /Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp -o build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python/src/pycryptosat.o -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -I/System/Library/Frameworks/Python.framework/Versions/2.7/include/python2.7 -fno-strict-aliasing -fno-common -dynamic -arch x86_64 -arch i386 -g -Os -pipe -fno-common -fno-strict-aliasing -fwrapv -DENABLE_DTRACE -DMACOSX -DNDEBUG -Wall -Wstrict-prototypes -Wshorten-64-to-32 -DNDEBUG -g -fwrapv -Os -Wall -Wstrict-prototypes -DENABLE_DTRACE -I/Users/Rex/cr/cryptominisat -I/Users/Rex/cr/cryptominisat/build/cmsat5-src
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:179:28: warning: 
      implicit conversion loses integer precision: 'long' to 'uint32_t'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        lits.push_back(Lit(var, sign));
                       ~~~ ^~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:222:24: warning: 
      implicit conversion loses integer precision: 'long' to 'value_type'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        vars.push_back(var);
             ~~~~~~~~~ ^~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:446:39: warning: 
      implicit conversion loses integer precision: 'long' to 'uint32_t'
      (aka 'unsigned int') [-Wshorten-64-to-32]
        assumption_lits.push_back(Lit(var, sign));
                                  ~~~ ^~~
3 warnings generated.
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:173:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= self->cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:216:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= self->cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~~~~~~~
/Users/Rex/cr/cryptominisat/python/src/pycryptosat.cpp:440:17: warning: 
      comparison of integers of different signs: 'long' and 'unsigned int'
      [-Wsign-compare]
        if (var >= cmsat->nVars()) {
            ~~~ ^  ~~~~~~~~~~~~~~
3 warnings generated.
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ -shared -g -W -Wall -Wno-deprecated build/temp.macosx-10.12-x86_64-3.6/Users/Rex/cr/cryptominisat/python/src/pycryptosat.o -L. -L/Users/Rex/cr/cryptominisat/build/lib -L/usr/local/lib -L/usr/local/opt/openssl/lib -L/usr/local/opt/sqlite/lib -L/usr/local/lib -L../lib -lcryptominisat5 -o /Users/Rex/cr/cryptominisat/build/pycryptosat/pycryptosat.cpython-36m-darwin.so -L/System/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/config -lpython2.7 -ldl -framework CoreFoundation
Undefined symbols for architecture x86_64:
  "_PyModule_Create2", referenced from:
      _PyInit_pycryptosat in pycryptosat.o
  "_PyUnicode_FromString", referenced from:
      _PyInit_pycryptosat in pycryptosat.o
  "__Py_FalseStruct", referenced from:
      solve(Solver*, _object*, _object*) in pycryptosat.o
      is_satisfiable(Solver*) in pycryptosat.o
      get_solution(CMSat::SATSolver*) in pycryptosat.o
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: command '/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++' failed with exit status 1
make[2]: *** [pycryptosat/build/timestamp] Error 1
make[1]: *** [pycryptosat/CMakeFiles/python_interface.dir/all] Error 2
make: *** [all] Error 2
msoos commented 6 years ago

Ahh crap. Now I can see this issue!!

https://travis-ci.org/msoos/cryptominisat/jobs/325854782

It's perfectly reproducible. So it will get fixed sooooon! :)

msoos commented 6 years ago

Yaaaay! I think I got this fixed! Can you please check? Thanks! And thanks again for your patience!

msoos commented 6 years ago

I think this is fixed now, at least TravisCI says so :) I am closing. Please re-open in case you are experiencing errors!