Using pycryptosat with Python 3.6.7 on Ubuntu terminal on Windows

[jediahkatz]

Hi, thanks so much for all the great work on this library!

I'm trying to set up the python interface for CMS. I have a Windows PC, but I'm using an Ubuntu terminal, with python 3.6.7 in a Pipenv virtual environment.

I followed all the steps in the Python Usage section, and here is the result:

• I can run cryptominisat5 from the command line anywhere, and it seems to work (at least, running on the sample file.cnf produces the correct output).
• I can import pycryptosat when running python from within the build directory only.
• I can't import Solver from pycryptosat; it gives me an ImportError and says Solver doesn't exist.

If it helps, here is my output from running cryptominisat5 from the command line. I would really appreciate any possible help on this issue! CMS compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -pedantic | COMPILE_DEFINES = -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DUSE_M4RI | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = 1 | STATS = OFF | SQLITE3_FOUND = | ZLIB_FOUND = TRUE | VALGRIND_FOUND = FALSE | ENABLE_TESTING = OFF | M4RI_FOUND = TRUE | NOM4RI = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE = /home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/bin/python3 | PYTHON_LIBRARY = /usr/lib/x86_64-linux-gnu/libpython3.6m.so | PYTHON_INCLUDE_DIRS = /usr/include/python3.6m | MY_TARGETS = | LARGEMEM = OFF | LIMITMEM = OFF | compilation date time = May 1 2019 00:58:17

[msoos]

Hey,

This is awesome feedback, thanks! Can you please tell me what kind of error you get? Could you please copy-paste the python interaction? For example, for me it looks likes this:

soos@vvv-dejavu:~$ ipython
Python 3.7.3 (default, Mar 26 2019, 21:43:19) 
Type 'copyright', 'credits' or 'license' for more information
IPython 7.3.0 -- An enhanced Interactive Python. Type '?' for help.

In [1]: import pycryptosat                                                                                                   

In [2]: a = pycryptosat.Solver()                                                                                             

In [3]: a.add_clause([1,2,3])                                                                                                

In [4]: a.solve()                                                                                                            
Out[4]: (True, (None, False, True, False))

Could you please copy-paste this? Also, if you could delete the "build" directory and re-build cryptominisat and re-install it and then try to do the above that would be nice -- I would really need the output of your full cmake, compile and install (all 3 please -- it's important to debug!) Thanks in advance!

Mate

[jediahkatz]

Yep, absolutely! From cmake ..:

-- 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 GNU 7.3.0
-- The CXX compiler identification is GNU 7.3.0
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /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: /usr/bin/c++
-- Check for working CXX compiler: /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 - not found
-- Check if compiler accepts -pthread
-- Check if compiler accepts -pthread - yes
-- Found Threads: TRUE
-- build type is RelWithDebInfo
-- Performing Test HAVE_FLAG_-mtune=native
-- Performing Test HAVE_FLAG_-mtune=native - Success
-- Performing Test HAVE_FLAG_-Wall
-- Performing Test HAVE_FLAG_-Wall - Success
-- Performing Test HAVE_FLAG_-Wextra
-- Performing Test HAVE_FLAG_-Wextra - Success
-- Performing Test HAVE_FLAG_-Wunused
-- Performing Test HAVE_FLAG_-Wunused - Success
-- Performing Test HAVE_FLAG_-Wsign-compare
-- Performing Test HAVE_FLAG_-Wsign-compare - Success
-- Performing Test HAVE_FLAG_-fno-omit-frame-pointer
-- Performing Test HAVE_FLAG_-fno-omit-frame-pointer - Success
-- Performing Test HAVE_FLAG_-Wtype-limits
-- Performing Test HAVE_FLAG_-Wtype-limits - Success
-- Performing Test HAVE_FLAG_-Wuninitialized
-- Performing Test HAVE_FLAG_-Wuninitialized - Success
-- Performing Test HAVE_FLAG_-Wno-deprecated
-- Performing Test HAVE_FLAG_-Wno-deprecated - Success
-- Performing Test HAVE_FLAG_-Wstrict-aliasing
-- Performing Test HAVE_FLAG_-Wstrict-aliasing - Success
-- Performing Test HAVE_FLAG_-Wpointer-arith
-- Performing Test HAVE_FLAG_-Wpointer-arith - Success
-- Performing Test HAVE_FLAG_-Wheader-guard
-- Performing Test HAVE_FLAG_-Wheader-guard - Failed
-- Performing Test HAVE_FLAG_-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: GIT-notfound
-- PROJECT_VERSION: 5.6.8
-- PROJECT_VERSION_MAJOR: 5
-- PROJECT_VERSION_MINOR: 6
-- PROJECT_VERSION_PATCH: 8
-- Boost version: 1.65.1
-- Found the following Boost libraries:
--   program_options
-- Not compiling detailed statistics. The system is faster without them
-- Manpage will be created and installed
-- Found ZLIB: /usr/lib/x86_64-linux-gnu/libz.so (found version "1.2.11")
-- OK, Found ZLIB!
-- Valgrind Prefix:
-- Could NOT find VALGRIND (missing: VALGRIND_INCLUDE_DIR VALGRIND_PROGRAM)
-- Cannot find valgrind or it's disabled, we will not be able to mark memory pool objects as undefined
-- Could NOT find PkgConfig (missing: PKG_CONFIG_EXECUTABLE)
-- Found m4ri: /usr/lib/x86_64-linux-gnu/libm4ri.so
-- OK, Found M4RI lib at /usr/lib/x86_64-linux-gnu/libm4ri.so and includes at /usr/include
-- All defines at startup:  -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DUSE_M4RI
-- In case your Python interpreter is not found, or a wrong one is found, please set it with '-DPYTHON_EXECUTABLE:FILEPATH=your path here'
-- Found PythonInterp: /home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/bin/python3 (found suitable version "3.6.7", minimum required is "3")
-- Found PythonLibs: /usr/lib/x86_64-linux-gnu/libpython3.6m.so (found suitable version "3.6.7", minimum required is "3")
-- Python 3 -- PYTHON_EXECUTABLE=/home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/bin/python3
-- Python 3 -- PYTHON_LIBRARIES=/usr/lib/x86_64-linux-gnu/libpython3.6m.so
-- Python 3 -- PYTHON_INCLUDE_DIRS=/usr/include/python3.6m
-- Python 3 -- PYTHONLIBS_VERSION_STRING=3.6.7
-- Boost -- found at library: /usr/lib/x86_64-linux-gnu/libboost_program_options.so
-- Boost -- adding '/usr/lib/x86_64-linux-gnu' to link directories
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion - Failed
-- Performing Test HAVE_FLAG_-Wlogical-op
-- Performing Test HAVE_FLAG_-Wlogical-op - Success
-- Performing Test HAVE_FLAG_-Wrestrict
-- Performing Test HAVE_FLAG_-Wrestrict - Success
-- Performing Test HAVE_FLAG_-Wnull-dereference
-- Performing Test HAVE_FLAG_-Wnull-dereference - Success
-- Performing Test HAVE_FLAG_-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 - Failed
-- Performing Test HAVE_FLAG_-pedantic
-- Performing Test HAVE_FLAG_-pedantic - Success
-- Performing Test HAVE_FLAG_-Wno-class-memaccess
-- Performing Test HAVE_FLAG_-Wno-class-memaccess - Failed
-- 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:696 (message):
  Testing is disabled

-- Found python interpreter, libs and header files
-- Building python interface
-- Python CFLAGS:  '-Wno-unused-result -Wsign-compare -DNDEBUG -g -fwrapv -O2 -Wall -g   -fstack-protector-strong -Wformat -Werror=format-security  -g -flto -fuse-linker-plugin -ffat-lto-objects'
-- Python LDFLAGS: '-lpthread -ldl  -lutil'
-- Python LINKFORSHARED flags: '-Xlinker -export-dynamic -Wl,-O1 -Wl,-Bsymbolic-functions'
-- Python module will be installed to : '/usr/local'
-- Configuring done
-- Generating done
-- Build files have been written to: /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build

From make:

Scanning dependencies of target cryptominisat5
[  2%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/cnf.cpp.o
[  4%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/propengine.cpp.o
[  6%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/varreplacer.cpp.o
[  8%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/clausecleaner.cpp.o
[ 10%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/clauseusagestats.cpp.o
[ 12%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/prober.cpp.o
[ 14%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/occsimplifier.cpp.o
[ 16%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/subsumestrengthen.cpp.o
[ 18%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/clauseallocator.cpp.o
[ 20%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/sccfinder.cpp.o
[ 22%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/solverconf.cpp.o
[ 25%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/distillerlong.cpp.o
[ 27%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/distillerlongwithimpl.cpp.o
[ 29%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/str_impl_w_impl_stamp.cpp.o
[ 31%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/solutionextender.cpp.o
[ 33%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/completedetachreattacher.cpp.o
[ 35%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/searcher.cpp.o
[ 37%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/solver.cpp.o
[ 39%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/sqlstats.cpp.o
[ 41%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/implcache.cpp.o
[ 43%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/stamp.cpp.o
[ 45%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/compfinder.cpp.o
[ 47%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/comphandler.cpp.o
[ 50%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/hyperengine.cpp.o
[ 52%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/subsumeimplicit.cpp.o
[ 54%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/datasync.cpp.o
[ 56%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/reducedb.cpp.o
[ 58%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/clausedumper.cpp.o
[ 60%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/bva.cpp.o
[ 62%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/intree.cpp.o
[ 64%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/features_calc.cpp.o
[ 66%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/features_to_reconf.cpp.o
[ 68%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/solvefeatures.cpp.o
[ 70%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/searchstats.cpp.o
[ 72%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/xorfinder.cpp.o
[ 75%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/cryptominisat_c.cpp.o
[ 77%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/walksat.cpp.o
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp: In member function ‘uint32_t CMSat::WalkSAT::RANDMOD(uint32_t)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp:41:37: warning: declaration of ‘x’ shadows a member of ‘CMSat::WalkSAT’ [-Wshadow]
 uint32_t WalkSAT::RANDMOD(uint32_t x)
                                     ^
In file included from /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp:29:0:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.h:148:13: note: shadowed declaration is here
     int64_t x;
             ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp: In member function ‘void CMSat::WalkSAT::initprob()’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp:222:63: warning: format ‘%i’ expects argument of type ‘int*’, but argument 3 has type ‘uint32_t* {aka unsigned int*}’ [-Wformat=]
     if (fscanf(cnfStream, "p cnf %i %i", &numvars, &numclauses) != 2) {
                                          ~~~~~~~~             ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp:222:63: warning: format ‘%i’ expects argument of type ‘int*’, but argument 4 has type ‘uint32_t* {aka unsigned int*}’ [-Wformat=]
[ 79%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/GitSHA1.cpp.o
[ 81%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/toplevelgauss.cpp.o
[ 83%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/cryptominisat.cpp.o
[ 85%] Linking CXX shared library ../lib/libcryptominisat5.so
[ 85%] Built target cryptominisat5
Scanning dependencies of target cryptominisat5_simple-bin
[ 87%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5_simple-bin.dir/main_simple.cpp.o
[ 89%] Linking CXX executable ../cryptominisat5_simple
[ 89%] Built target cryptominisat5_simple-bin
Scanning dependencies of target man_cms5_simple
[ 89%] Built target man_cms5_simple
Scanning dependencies of target cryptominisat5-bin
[ 91%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/main.cpp.o
[ 93%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/main_exe.cpp.o
[ 95%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/signalcode.cpp.o
[ 97%] Linking CXX executable ../cryptominisat5
[ 97%] Built target cryptominisat5-bin
Scanning dependencies of target man_cms5
[ 97%] Built target man_cms5
Scanning dependencies of target CopyPublicHeaders
Copying cryptominisat_c.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying cryptominisat.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying solvertypesmini.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying dimacsparser.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying streambuffer.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/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.linux-x86_64-3.6
creating build/temp.linux-x86_64-3.6/mnt
creating build/temp.linux-x86_64-3.6/mnt/c
creating build/temp.linux-x86_64-3.6/mnt/c/Users
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src
/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -g -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -fPIC -DLIBRARY_VERSION="5.6.8" -I/usr/include/python3.6m -I/home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/include/python3.6m -c /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp -o build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.o -Wno-unused-result -Wsign-compare -DNDEBUG -g -fwrapv -O2 -Wall -g -fstack-protector-strong -Wformat -Werror=format-security -g -fuse-linker-plugin -ffat-lto-objects -I/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8 -I/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/cmsat5-src
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘CMSat::SATSolver* setup_solver(PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"verbose", "time_limit", "confl_limit", "threads", NULL};
                                                                                     ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* start_getting_small_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:242:57: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"max_len", "max_glue", NULL};
                                                         ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:242:57: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* get_next_small_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:263:15: warning: unused variable ‘max_len’ [-Wunused-variable]
     PyObject *max_len;
               ^~~~~~~
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* end_getting_small_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:297:15: warning: unused variable ‘max_len’ [-Wunused-variable]
     PyObject *max_len;
               ^~~~~~~
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:330:44: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"clause", NULL};
                                            ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:498:56: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"clauses", "max_var", NULL};
                                                        ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:498:56: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_xor_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:546:55: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"xor_clause", "rhs", NULL};
                                                       ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:546:55: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* solve(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:734:49: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"assumptions", NULL};
                                                 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* msolve_selected(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"max_nr_of_solutions", "var_selected", "raw", NULL};
                                                                                ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: At global scope:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:978:1: warning: missing initializer for member ‘PyMethodDef::ml_flags’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:978:1: warning: missing initializer for member ‘PyMethodDef::ml_doc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::type’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::offset’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::flags’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::doc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_free’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_is_gc’ [-Wmissing-field-initializer
]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_bases’ [-Wmissing-field-initializer
]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_mro’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_cache’ [-Wmissing-field-initializer
]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_subclasses’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_weaklist’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_del’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_version_tag’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_finalize’ [-Wmissing-field-initializers]
/usr/bin/c++ -pthread -shared -Wl,-O1 -Wl,-Bsymbolic-functions -Wl,-Bsymbolic-functions -Wl,-z,relro -Wl,-Bsymbolic-functions -Wl,-z,relro -g -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.o -L. -L/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/lib -L/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/lib/RelWithDebInfo -Wl,--enable-new-dtags,-R/usr/local/lib -Wl,--enable-new-dtags,-R../lib -lcryptominisat5 -o /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/pycryptosat.cpython-36m-x86_64-linux-gnu.so
[100%] Built target python_interface

And from sudo make install:

[ 85%] Built target cryptominisat5
[ 89%] Built target cryptominisat5_simple-bin
[ 89%] Built target man_cms5_simple
[ 97%] Built target cryptominisat5-bin
[ 97%] Built target man_cms5
Copying cryptominisat_c.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying cryptominisat.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying solvertypesmini.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying dimacsparser.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying streambuffer.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
[ 97%] Built target CopyPublicHeaders
[100%] Generating build/timestamp
running build_ext
[100%] Built target python_interface
Install the project...
-- Install configuration: "RelWithDebInfo"
-- Installing: /usr/local/share/man/man1/cryptominisat5.1
-- Installing: /usr/local/share/man/man1/cryptominisat5_simple.1
-- 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
-- Installing: /usr/local/lib/libcryptominisat5.so.5.6
-- Up-to-date: /usr/local/lib/libcryptominisat5.so
-- Installing: /usr/local/include/cryptominisat5/cryptominisat_c.h
-- Installing: /usr/local/include/cryptominisat5/cryptominisat.h
-- Installing: /usr/local/include/cryptominisat5/solvertypesmini.h
-- Up-to-date: /usr/local/include/cryptominisat5/dimacsparser.h
-- Up-to-date: /usr/local/include/cryptominisat5/streambuffer.h
-- Installing: /usr/local/bin/cryptominisat5_simple
-- Set runtime path of "/usr/local/bin/cryptominisat5_simple" to ""
-- Installing: /usr/local/bin/cryptominisat5
-- Set runtime path of "/usr/local/bin/cryptominisat5" to ""
running install
running build
running build_ext
building 'pycryptosat' extension
/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -g -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -fPIC -DLIBRARY_VERSION="5.6.8" -I/usr/include/python3.6m -I/home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/include/python3.6m -c /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp -o build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.o -Wno-unused-result -Wsign-compare -DNDEBUG -g -fwrapv -O2 -Wall -g -fstack-protector-strong -Wformat -Werror=format-security -g -fuse-linker-plugin -ffat-lto-objects -I/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8 -I/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/cmsat5-src
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘CMSat::SATSolver* setup_solver(PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"verbose", "time_limit", "confl_limit", "threads", NULL};
                                                                                     ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* start_getting_small_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:242:57: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"max_len", "max_glue", NULL};
                                                         ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:242:57: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* get_next_small_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:263:15: warning: unused variable ‘max_len’ [-Wunused-variable]
     PyObject *max_len;
               ^~~~~~~
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* end_getting_small_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:297:15: warning: unused variable ‘max_len’ [-Wunused-variable]
     PyObject *max_len;
               ^~~~~~~
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:330:44: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"clause", NULL};
                                            ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:498:56: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"clauses", "max_var", NULL};
                                                        ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:498:56: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_xor_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:546:55: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"xor_clause", "rhs", NULL};
                                                       ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:546:55: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* solve(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:734:49: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"assumptions", NULL};
                                                 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* msolve_selected(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"max_nr_of_solutions", "var_selected", "raw", NULL};
                                                                                ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: At global scope:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:978:1: warning: missing initializer for member ‘PyMethodDef::ml_flags’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:978:1: warning: missing initializer for member ‘PyMethodDef::ml_doc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::type’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::offset’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::flags’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::doc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_free’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_is_gc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_bases’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_mro’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_cache’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_subclasses’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_weaklist’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_del’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_version_tag’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_finalize’ [-Wmissing-field-initializers]
creating build/lib.linux-x86_64-3.6
/usr/bin/c++ -pthread -shared -Wl,-O1 -Wl,-Bsymbolic-functions -Wl,-Bsymbolic-functions -Wl,-z,relro -Wl,-Bsymbolic-functions -Wl,-z,relro -g -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.o -L. -L/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/lib -L/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/lib/RelWithDebInfo -Wl,--enable-new-dtags,-R/usr/local/lib -lcryptominisat5 -o build/lib.linux-x86_64-3.6/pycryptosat.cpython-36m-x86_64-linux-gnu.so
running install_lib
copying build/lib.linux-x86_64-3.6/pycryptosat.cpython-36m-x86_64-linux-gnu.so -> /usr/local/lib/python3.6/site-packages
running install_egg_info
Removing /usr/local/lib/python3.6/site-packages/pycryptosat-0.2.0-py3.6.egg-info
Writing /usr/local/lib/python3.6/site-packages/pycryptosat-0.2.0-py3.6.egg-info
writing list of installed files to 'files.txt'

I had just been using standalone python, but here's trying with IPython (same result):

Python 3.6.7 (default, Oct 22 2018, 11:32:17)
Type 'copyright', 'credits' or 'license' for more information
IPython 7.5.0 -- An enhanced Interactive Python. Type '?' for help.

In [1]: import pycryptosat

In [2]: a = pycryptosat.Solver()
---------------------------------------------------------------------------
AttributeError                            Traceback (most recent call last)
<ipython-input-2-790955635813> in <module>
----> 1 a = pycryptosat.Solver()

AttributeError: module 'pycryptosat' has no attribute 'Solver'

[msoos]

Hi,

Wow, thanks for the full log, that's super-useful! I think the problem is that you are installing to /usr/local/lib and not to /usr/lib can you please do:

sudo make uninstall
cd ..
rm -rf build
mkdir build
cd build
cmake -DCMAKE_INSTALL_PREFIX=/usr ..
make -j4
sudo make install

This hopefully will work :) Please don't skip any of those lines or it will build wrongly :( The build directory is best to be deleted and re-created because cmake is pretty bad unfortunately. Could you please try to do the above and let me know if it worked?

Thanks in advance,

Mate

[jediahkatz]

Unfortunately still getting the same issue. Here is the full log once again with that set of commands:

(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build$ sudo make uninstall
[sudo] password for jediah:
Scanning dependencies of target uninstall_pycyrptosat
Built target uninstall_pycyrptosat
Scanning dependencies of target uninstall
-- Uninstalling "/usr/local/bin/cryptominisat5"
-- Uninstalling "/usr/local/bin/cryptominisat5_simple"
-- Uninstalling "/usr/local/include/cryptominisat5/streambuffer.h"
-- Uninstalling "/usr/local/include/cryptominisat5/dimacsparser.h"
-- Uninstalling "/usr/local/include/cryptominisat5/solvertypesmini.h"
-- Uninstalling "/usr/local/include/cryptominisat5/cryptominisat.h"
-- Uninstalling "/usr/local/include/cryptominisat5/cryptominisat_c.h"
-- Uninstalling "/usr/local/lib/libcryptominisat5.so"
-- Uninstalling "/usr/local/lib/libcryptominisat5.so.5.6"
-- Uninstalling "/usr/local/lib/cmake/cryptominisat5/cryptominisat5Targets-relwithdebinfo.cmake"
-- Uninstalling "/usr/local/lib/cmake/cryptominisat5/cryptominisat5Targets.cmake"
-- Uninstalling "/usr/local/lib/cmake/cryptominisat5/cryptominisat5Config.cmake"
-- Uninstalling "/usr/local/share/man/man1/cryptominisat5_simple.1"
-- Uninstalling "/usr/local/share/man/man1/cryptominisat5.1"
Built target uninstall
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build$ cd ..
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8$ rm -rf build
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8$ mkdir build
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8$ cd build
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build$ cmake -DCMAKE_INSTALL_PREFIX=/usr ..
-- 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 GNU 7.3.0
-- The CXX compiler identification is GNU 7.3.0
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /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: /usr/bin/c++
-- Check for working CXX compiler: /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 - not found
-- Check if compiler accepts -pthread
-- Check if compiler accepts -pthread - yes
-- Found Threads: TRUE
-- build type is RelWithDebInfo
-- Performing Test HAVE_FLAG_-mtune=native
-- Performing Test HAVE_FLAG_-mtune=native - Success
-- Performing Test HAVE_FLAG_-Wall
-- Performing Test HAVE_FLAG_-Wall - Success
-- Performing Test HAVE_FLAG_-Wextra
-- Performing Test HAVE_FLAG_-Wextra - Success
-- Performing Test HAVE_FLAG_-Wunused
-- Performing Test HAVE_FLAG_-Wunused - Success
-- Performing Test HAVE_FLAG_-Wsign-compare
-- Performing Test HAVE_FLAG_-Wsign-compare - Success
-- Performing Test HAVE_FLAG_-fno-omit-frame-pointer
-- Performing Test HAVE_FLAG_-fno-omit-frame-pointer - Success
-- Performing Test HAVE_FLAG_-Wtype-limits
-- Performing Test HAVE_FLAG_-Wtype-limits - Success
-- Performing Test HAVE_FLAG_-Wuninitialized
-- Performing Test HAVE_FLAG_-Wuninitialized - Success
-- Performing Test HAVE_FLAG_-Wno-deprecated
-- Performing Test HAVE_FLAG_-Wno-deprecated - Success
-- Performing Test HAVE_FLAG_-Wstrict-aliasing
-- Performing Test HAVE_FLAG_-Wstrict-aliasing - Success
-- Performing Test HAVE_FLAG_-Wpointer-arith
-- Performing Test HAVE_FLAG_-Wpointer-arith - Success
-- Performing Test HAVE_FLAG_-Wheader-guard
-- Performing Test HAVE_FLAG_-Wheader-guard - Failed
-- Performing Test HAVE_FLAG_-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: GIT-notfound
-- PROJECT_VERSION: 5.6.8
-- PROJECT_VERSION_MAJOR: 5
-- PROJECT_VERSION_MINOR: 6
-- PROJECT_VERSION_PATCH: 8
-- Boost version: 1.65.1
-- Found the following Boost libraries:
--   program_options
-- Not compiling detailed statistics. The system is faster without them
-- Manpage will be created and installed
-- Found ZLIB: /usr/lib/x86_64-linux-gnu/libz.so (found version "1.2.11")
-- OK, Found ZLIB!
-- Valgrind Prefix:
-- Could NOT find VALGRIND (missing: VALGRIND_INCLUDE_DIR VALGRIND_PROGRAM)
-- Cannot find valgrind or it's disabled, we will not be able to mark memory pool objects as undefined
-- Could NOT find PkgConfig (missing: PKG_CONFIG_EXECUTABLE)
-- Found m4ri: /usr/lib/x86_64-linux-gnu/libm4ri.so
-- OK, Found M4RI lib at /usr/lib/x86_64-linux-gnu/libm4ri.so and includes at /usr/include
-- All defines at startup:  -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DUSE_M4RI
-- In case your Python interpreter is not found, or a wrong one is found, please set it with '-DPYTHON_EXECUTABLE:FILEPATH=your path here'
-- Found PythonInterp: /home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/bin/python3 (found suitable version "3.6.7", minimum required is "3")
-- Found PythonLibs: /usr/lib/x86_64-linux-gnu/libpython3.6m.so (found suitable version "3.6.7", minimum required is "3")
-- Python 3 -- PYTHON_EXECUTABLE=/home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/bin/python3
-- Python 3 -- PYTHON_LIBRARIES=/usr/lib/x86_64-linux-gnu/libpython3.6m.so
-- Python 3 -- PYTHON_INCLUDE_DIRS=/usr/include/python3.6m
-- Python 3 -- PYTHONLIBS_VERSION_STRING=3.6.7
-- Boost -- found at library: /usr/lib/x86_64-linux-gnu/libboost_program_options.so
-- Boost -- adding '/usr/lib/x86_64-linux-gnu' to link directories
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion
-- Performing Test HAVE_FLAG_-Wno-bitfield-constant-conversion - Failed
-- Performing Test HAVE_FLAG_-Wlogical-op
-- Performing Test HAVE_FLAG_-Wlogical-op - Success
-- Performing Test HAVE_FLAG_-Wrestrict
-- Performing Test HAVE_FLAG_-Wrestrict - Success
-- Performing Test HAVE_FLAG_-Wnull-dereference
-- Performing Test HAVE_FLAG_-Wnull-dereference - Success
-- Performing Test HAVE_FLAG_-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 - Failed
-- Performing Test HAVE_FLAG_-pedantic
-- Performing Test HAVE_FLAG_-pedantic - Success
-- Performing Test HAVE_FLAG_-Wno-class-memaccess
-- Performing Test HAVE_FLAG_-Wno-class-memaccess - Failed
-- 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:696 (message):
  Testing is disabled

-- Found python interpreter, libs and header files
-- Building python interface
-- Python CFLAGS:  '-Wno-unused-result -Wsign-compare -DNDEBUG -g -fwrapv -O2 -Wall -g   -fstack-protector-strong -Wformat -Werror=format-security  -g -flto -fuse-linker-plugin -ffat-lto-objects'
-- Python LDFLAGS: '-lpthread -ldl  -lutil'
-- Python LINKFORSHARED flags: '-Xlinker -export-dynamic -Wl,-O1 -Wl,-Bsymbolic-functions'
-- Python module will be installed to : '/usr'
-- Configuring done
-- Generating done
-- Build files have been written to: /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build$ make -j4
Scanning dependencies of target CopyPublicHeaders
Scanning dependencies of target cryptominisat5
Copying cryptominisat_c.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying cryptominisat.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying solvertypesmini.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying dimacsparser.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying streambuffer.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
[  0%] Built target CopyPublicHeaders
[  4%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/cnf.cpp.o
[  6%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/propengine.cpp.o
[  6%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/varreplacer.cpp.o
[  8%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/clausecleaner.cpp.o
[ 10%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/clauseusagestats.cpp.o
[ 12%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/prober.cpp.o
[ 14%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/occsimplifier.cpp.o
[ 16%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/subsumestrengthen.cpp.o
[ 18%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/clauseallocator.cpp.o
[ 20%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/sccfinder.cpp.o
[ 22%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/solverconf.cpp.o
[ 25%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/distillerlong.cpp.o
[ 27%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/distillerlongwithimpl.cpp.o
[ 29%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/str_impl_w_impl_stamp.cpp.o
[ 31%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/solutionextender.cpp.o
[ 33%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/completedetachreattacher.cpp.o
[ 35%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/searcher.cpp.o
[ 37%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/solver.cpp.o
[ 39%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/sqlstats.cpp.o
[ 41%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/implcache.cpp.o
[ 43%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/stamp.cpp.o
[ 45%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/compfinder.cpp.o
[ 47%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/comphandler.cpp.o
[ 50%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/hyperengine.cpp.o
[ 52%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/subsumeimplicit.cpp.o
[ 54%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/datasync.cpp.o
[ 56%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/reducedb.cpp.o
[ 58%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/clausedumper.cpp.o
[ 60%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/bva.cpp.o
[ 62%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/intree.cpp.o
[ 64%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/features_calc.cpp.o
[ 66%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/features_to_reconf.cpp.o
[ 68%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/solvefeatures.cpp.o
[ 70%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/searchstats.cpp.o
[ 72%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/xorfinder.cpp.o
[ 75%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/cryptominisat_c.cpp.o
[ 77%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/walksat.cpp.o
[ 79%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/GitSHA1.cpp.o
[ 81%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/toplevelgauss.cpp.o
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp: In member function ‘uint32_t CMSat::WalkSAT::RANDMOD(uint32_t)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp:41:37: warning: declaration of ‘x’ shadows a member of ‘CMSat::WalkSAT’ [-Wshadow]
 uint32_t WalkSAT::RANDMOD(uint32_t x)
                                     ^
In file included from /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp:29:0:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.h:148:13: note: shadowed declaration is here
     int64_t x;
             ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp: In member function ‘void CMSat::WalkSAT::initprob()’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp:222:63: warning: format ‘%i’ expects argument of type ‘int*’, but argument 3 has type ‘uint32_t* {aka unsigned int*}’ [-Wformat=]
     if (fscanf(cnfStream, "p cnf %i %i", &numvars, &numclauses) != 2) {
                                          ~~~~~~~~             ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/src/walksat.cpp:222:63: warning: format ‘%i’ expects argument of type ‘int*’, but argument 4 has type ‘uint32_t* {aka unsigned int*}’ [-Wformat=]
[ 83%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5.dir/cryptominisat.cpp.o
[ 85%] Linking CXX shared library ../lib/libcryptominisat5.so
[ 85%] Built target cryptominisat5
Scanning dependencies of target cryptominisat5_simple-bin
Scanning dependencies of target cryptominisat5-bin
Scanning dependencies of target python_interface
[ 87%] Generating build/timestamp
[ 89%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5_simple-bin.dir/main_simple.cpp.o
[ 93%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/main.cpp.o
[ 93%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/main_exe.cpp.o
running build_ext
building 'pycryptosat' extension
creating build
creating build/temp.linux-x86_64-3.6
creating build/temp.linux-x86_64-3.6/mnt
creating build/temp.linux-x86_64-3.6/mnt/c
creating build/temp.linux-x86_64-3.6/mnt/c/Users
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat
creating build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src
/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -g -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -fPIC -DLIBRARY_VERSION="5.6.8" -I/usr/include/python3.6m -I/home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/include/python3.6m -c /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp -o build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.o -Wno-unused-result -Wsign-compare -DNDEBUG -g -fwrapv -O2 -Wall -g -fstack-protector-strong -Wformat -Werror=format-security -g -fuse-linker-plugin -ffat-lto-objects -I/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8 -I/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/cmsat5-src
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘CMSat::SATSolver* setup_solver(PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"verbose", "time_limit", "confl_limit", "threads", NULL};
                                                                                     ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* start_getting_small_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:242:57: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"max_len", "max_glue", NULL};
                                                         ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:242:57: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* get_next_small_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:263:15: warning: unused variable ‘max_len’ [-Wunused-variable]
     PyObject *max_len;
               ^~~~~~~
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* end_getting_small_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:297:15: warning: unused variable ‘max_len’ [-Wunused-variable]
     PyObject *max_len;
               ^~~~~~~
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:330:44: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"clause", NULL};
                                            ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:498:56: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"clauses", "max_var", NULL};
                                                        ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:498:56: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_xor_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:546:55: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"xor_clause", "rhs", NULL};
                                                       ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:546:55: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* solve(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:734:49: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"assumptions", NULL};
                                                 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* msolve_selected(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"max_nr_of_solutions", "var_selected", "raw", NULL};
                                                                                ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: At global scope:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:978:1: warning: missing initializer for member ‘PyMethodDef::ml_flags’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:978:1: warning: missing initializer for member ‘PyMethodDef::ml_doc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::type’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::offset’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::flags’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::doc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_free’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_is_gc’ [-Wmissing-field-initializer
]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_bases’ [-Wmissing-field-initializer
]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_mro’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_cache’ [-Wmissing-field-initializer
]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_subclasses’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_weaklist’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_del’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_version_tag’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_finalize’ [-Wmissing-field-initializers]
[ 95%] Linking CXX executable ../cryptominisat5_simple
/usr/bin/c++ -pthread -shared -Wl,-O1 -Wl,-Bsymbolic-functions -Wl,-Bsymbolic-functions -Wl,-z,relro -Wl,-Bsymbolic-functions -Wl,-z,relro -g -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.o -L. -L/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/lib -L/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/lib/RelWithDebInfo -Wl,--enable-new-dtags,-R../lib -lcryptominisat5 -o /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/pycryptosat.cpython-36m-x86_64-linux-gnu.so
[ 95%] Built target python_interface
[ 95%] Built target cryptominisat5_simple-bin
[ 97%] Building CXX object cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/signalcode.cpp.o
Scanning dependencies of target man_cms5_simple
[ 97%] Built target man_cms5_simple
[100%] Linking CXX executable ../cryptominisat5
[100%] Built target cryptominisat5-bin
Scanning dependencies of target man_cms5
[100%] Built target man_cms5
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build$ sudo make install
[ 85%] Built target cryptominisat5
[ 89%] Built target cryptominisat5_simple-bin
[ 89%] Built target man_cms5_simple
[ 97%] Built target cryptominisat5-bin
[ 97%] Built target man_cms5
Copying cryptominisat_c.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying cryptominisat.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying solvertypesmini.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying dimacsparser.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
Copying streambuffer.h to /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/include/cryptominisat5
[ 97%] Built target CopyPublicHeaders
[100%] Generating build/timestamp
running build_ext
[100%] Built target python_interface
Install the project...
-- Install configuration: "RelWithDebInfo"
-- Installing: /usr/share/man/man1/cryptominisat5.1
-- Installing: /usr/share/man/man1/cryptominisat5_simple.1
-- Installing: /usr/lib/cmake/cryptominisat5/cryptominisat5Config.cmake
-- Installing: /usr/lib/cmake/cryptominisat5/cryptominisat5Targets.cmake
-- Installing: /usr/lib/cmake/cryptominisat5/cryptominisat5Targets-relwithdebinfo.cmake
-- Installing: /usr/lib/libcryptominisat5.so.5.6
-- Installing: /usr/lib/libcryptominisat5.so
-- Installing: /usr/include/cryptominisat5/cryptominisat_c.h
-- Installing: /usr/include/cryptominisat5/cryptominisat.h
-- Installing: /usr/include/cryptominisat5/solvertypesmini.h
-- Installing: /usr/include/cryptominisat5/dimacsparser.h
-- Installing: /usr/include/cryptominisat5/streambuffer.h
-- Installing: /usr/bin/cryptominisat5_simple
-- Set runtime path of "/usr/bin/cryptominisat5_simple" to ""
-- Installing: /usr/bin/cryptominisat5
-- Set runtime path of "/usr/bin/cryptominisat5" to ""
running install
running build
running build_ext
building 'pycryptosat' extension
/usr/bin/cc -g -W -Wall -Wno-deprecated -std=c++11 -g -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -fPIC -DLIBRARY_VERSION="5.6.8" -I/usr/include/python3.6m -I/home/jediah/.local/share/virtualenvs/PythonSAT-wzBoO1qg/include/python3.6m -c /mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp -o build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.o -Wno-unused-result -Wsign-compare -DNDEBUG -g -fwrapv -O2 -Wall -g -fstack-protector-strong -Wformat -Werror=format-security -g -fuse-linker-plugin -ffat-lto-objects -I/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8 -I/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/cmsat5-src
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘CMSat::SATSolver* setup_solver(PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"verbose", "time_limit", "confl_limit", "threads", NULL};
                                                                                     ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:94:85: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* start_getting_small_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:242:57: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"max_len", "max_glue", NULL};
                                                         ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:242:57: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* get_next_small_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:263:15: warning: unused variable ‘max_len’ [-Wunused-variable]
     PyObject *max_len;
               ^~~~~~~
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* end_getting_small_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:297:15: warning: unused variable ‘max_len’ [-Wunused-variable]
     PyObject *max_len;
               ^~~~~~~
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:330:44: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"clause", NULL};
                                            ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_clauses(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:498:56: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"clauses", "max_var", NULL};
                                                        ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:498:56: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* add_xor_clause(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:546:55: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"xor_clause", "rhs", NULL};
                                                       ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:546:55: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* solve(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:734:49: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"assumptions", NULL};
                                                 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: In function ‘PyObject* msolve_selected(Solver*, PyObject*, PyObject*)’:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
     static char* kwlist[] = {"max_nr_of_solutions", "var_selected", "raw", NULL};
                                                                                ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:858:80: warning: ISO C++ forbids converting a string constant to ‘char*’ [-Wwrite-strings]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp: At global scope:
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:978:1: warning: missing initializer for member ‘PyMethodDef::ml_flags’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:978:1: warning: missing initializer for member ‘PyMethodDef::ml_doc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::type’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::offset’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::flags’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1021:1: warning: missing initializer for member ‘PyMemberDef::doc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_free’ [-Wmissing-field-initializers]
 };
 ^
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_is_gc’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_bases’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_mro’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_cache’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_subclasses’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_weaklist’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_del’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_version_tag’ [-Wmissing-field-initializers]
/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.cpp:1062:1: warning: missing initializer for member ‘_typeobject::tp_finalize’ [-Wmissing-field-initializers]
creating build/lib.linux-x86_64-3.6
/usr/bin/c++ -pthread -shared -Wl,-O1 -Wl,-Bsymbolic-functions -Wl,-Bsymbolic-functions -Wl,-z,relro -Wl,-Bsymbolic-functions -Wl,-z,relro -g -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 build/temp.linux-x86_64-3.6/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/pycryptosat/src/pycryptosat.o -L. -L/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/lib -L/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build/lib/RelWithDebInfo -lcryptominisat5 -o build/lib.linux-x86_64-3.6/pycryptosat.cpython-36m-x86_64-linux-gnu.so
running install_lib
creating /usr/lib/python3.6/site-packages
copying build/lib.linux-x86_64-3.6/pycryptosat.cpython-36m-x86_64-linux-gnu.so -> /usr/lib/python3.6/site-packages
running install_egg_info
Writing /usr/lib/python3.6/site-packages/pycryptosat-0.2.0-py3.6.egg-info
writing list of installed files to 'files.txt'
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build$ sudo ldconfig
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build$ python
Python 3.6.7 (default, Oct 22 2018, 11:32:17)
[GCC 8.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from pycryptosat import Solver
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ImportError: cannot import name 'Solver'
>>> quit()
(PythonSAT-wzBoO1qg) jediah@DESKTOP-GB34NU9:/mnt/c/Users/jedia/Documents/PythonSAT/cryptominisat-5.6.8/build$ ipython
Python 3.6.7 (default, Oct 22 2018, 11:32:17)
Type 'copyright', 'credits' or 'license' for more information
IPython 7.5.0 -- An enhanced Interactive Python. Type '?' for help.

In [1]: import pycryptosat

In [2]: a = pycryptosat.Solver()
---------------------------------------------------------------------------
AttributeError                            Traceback (most recent call last)
<ipython-input-2-790955635813> in <module>
----> 1 a = pycryptosat.Solver()

AttributeError: module 'pycryptosat' has no attribute 'Solver'

[cipherboy]

@jediahkatz I just installed a fresh Ubuntu 18.04 VM. Could I bother you to run the following?

> import pycryptosat
> help(pycryptosat)

At the very very end, I see a section called "FILE":

VERSION
    5.6.8

FILE
    /usr/local/lib/python3.6/dist-packages/pycryptosat.cpython-36m-x86_64-linux-gnu.so

When I built CryptoMiniSat outside of a virtual environment (prior to setting it up), I got the above. However, inside a fresh virtual environment, pycryptosat is not found and thus cannot be imported. I'm wondering if you have a rogue CryptoMiniSat install somewhere.

When I install pycryptosat via pip3, we get the package on PyPI which isn't owned by @msoos, and is really out of date:

VERSION
    5.0.1

FILE
    /home/user/venv/lib/python3.6/site-packages/pycryptosat.cpython-36m-x86_64-linux-gnu.so

When I created a second virtualenv and built CMS while inside it (and ran sudo make install) I got:

Help on package pycryptosat:

NAME
    pycryptosat

PACKAGE CONTENTS
    pycryptosat
    setup
    tests (package)

FILE
    (built-in)

(END)

And looking at the instance indeed shows there's no Solver:

>>> s = pycryptosat.Solver
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
AttributeError: module 'pycryptosat' has no attribute 'Solver'

So it looks like the installation process isn't cognizant of the python3 virtual environment. You can solve this by:

cd cryptominisat/build/pycryptosat
pip3 install pycryptosat

Which will then work as follows:

VERSION
    5.6.8

FILE
    /home/user/venv2/cryptominisat/build/pycryptosat/pycryptosat.cpython-36m-x86_64-linux-gnu.so

[msoos]

Ah nice catch @cipherboy ! @jediahkatz please let me know if this worked :)

Mate

[jediahkatz]

Brilliant, that seems to work; thank you @cipherboy ! If you don't mind me asking, how is it that installing the wrong package from pip fixes the problem?

Also, @msoos , I think there may be a small bug in the python example on the readme. It has the line s.add_xor_clause([3]), but add_xor_clause takes two arguments!

[cipherboy]

The wrong package from pip3 was just a test to see if it was older than the Solver interface, but it isn't. Like I said, I wouldn't use it, but it is there for reference: putting pycryptosat in a requires.txt will almost always get you that version if you're not careful, I'd avoid it. (Since, @msoos doesn't own it).

@msoos I'll test a few more things and open a PR if it works, but I think perhaps you should use pip install in make install instead of manually installing pycryptosat. Then users won't be as surprised. :-) My 2c.

[msoos]

Thanks for that info about the add_xor_clause, fixed it thanking you :)

[msoos]

@cipherboy Yeah, I am trying to get ownership of it kind of... wrote to the guy who owns it but no reply... I just sent Pierre, the owner, another email, let's home he sees it this time :)

[cipherboy]

@msoos Ah, never mind I see what's happening. We're running:

    COMMAND ${PYTHON_EXECUTABLE} ${SETUP_PY} install --root=\$ENV{DESTDIR}/ --prefix=${CMAKE_INSTALL_PREFIX} --record files.txt

${CMAKE_INSTALL_PREFIX} is required for packaging, see e.g. #499 and isn't aware of the virtualenv. I'm not sure we can make both parties happy at the same time. Perhaps check if we're in a virtualenv and update the Python destination accordingly? Yuck!

Something like:

if(DEFINED ENV{PYCRYPTOSAT_INSTALL_PATH})
    set(INSTALL_PREFIX "--prefix=$ENV{PYCRYPTOSAT_INSTALL_PATH}")
elseif(DEFINED ENV{VIRTUAL_ENV})
    set(INSTALL_PREFIX "")
else()
    set(INSTALL_PREFIX "--prefix=${CMAKE_INSTALL_PREFIX}")
endif()

install(CODE "execute_process(
    COMMAND ${PYTHON_EXECUTABLE} ${SETUP_PY} install --root=\$ENV{DESTDIR}/ ${INSTALL_PREFIX} --record files.txt
    WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})"
)

Good luck getting ownership... :)

[msoos]

Thanks! I have given some feedback -- could you please adjust? Thanks so much! I'd love to pull this in, it would fix a lot of things I think!

[cipherboy]

@msoos Updated. I'll take an additional AI to investigate installing only pycryptosat into the virtualenv in the future and if we just want to put the cryptominisat5 binary in the virtualenv's bin/ directory.

Probably this weekend.

[jediahkatz]

Hi again @msoos - this is not entirely related but I was wondering how I could go about contributing? I am a college student currently procrastinating for my final exams, so I can't promise anything right now, but two things I would love to see (and would be happy to work on if it's within my ability):

• Adding the Solver.nb_clauses functionality back to python
• Adding some sort of Solver.add_clauses_from_file, because right now it seems (?) that you can only use CNF files from the command line, and otherwise you need to parse the file by hand

[msoos]

Hi,

I'd rather not add DIMACS parsing to the python wrapper. But you can contribute a few ways -- looking around some SAT papers could be interesting perhaps? Try looking at some research papers from the SAT conference and try implementing an idea from one of the papers. An interesting one could be cube-and-conquer: https://link.springer.com/chapter/10.1007/978-3-642-34188-5_8 (you can find the PDF very easily without paying, from Armin Biere's website for example). This would need only minimal integration of CryptoMiniSat with the lookahead solver and assoicated cubes, here:

https://github.com/marijnheule/CnC

Take a look, it's kinda interesting! I hope I helped :)

[jediahkatz]

Thanks, will check it out!

[cipherboy]

@jediahkatz I have two open PRs against CryptoMiniSat that might be of help:

• https://github.com/msoos/cryptominisat/pull/544
• https://github.com/msoos/cryptominisat/pull/543

@msoos can of course provide more information but here's what I know...

The core of CryptoMiniSat is written in C++, including these Python bindings. Some useful locations are:

• src/cryptominisat.h.in - the core declarations of the external (public) interface to the CMS SAT Solver. This is what is wrapped by pycryptosat.
• src/cryptominisat.cpp - the implementations of the above SATSolver methods.
• src/solver.h - the core declarations of the internal (private) interface to the CMS solver.
• src/solver.cpp the implementations of the above Solver methods.
• python/src/pycryptosat.cpp.in -- the Python bindings. This uses the Python/C API.
  • Each exposed method on the pycryptosat.Solver is a pair of a PyDoc_STRVAR describing the function and a static method which implements the functionality and parses arguments.
  • The table of all exposed pycryptosat.Solver methods is called Solver_methods.

Regarding your suggestions:

• Looking at the comment in the nb_clauses function, it looks like CMSat::SATSolver will need to expose a nClauses() or similar public function. It doesn't currently. It should be fairly easy to do and shouldn't take that much of a performance hit. Of course, up to Mate to ultimately approve it.
  • I've looked at this in cmsh and I prefer to keep a cache of all added clauses myself. Note: cmsh is by no means currently finished.
• add_clauses_from_file is an interesting idea. Currently there isn't any method on CMSat::SATSolver that reads a CNF file; perhaps I'm missing something obvious though, so you'd have to add that (and probably update the main CryptoMiniSat to use that instead).
  • I'm not sure how this interacts with incremental solving. Do I clear state each time? Do take the two CNFs as if they were concatenated? Do I renumber the latter CNF to start at num_vars+1 instead of 1? Etc. This'd definitely be something to iron out with Mate.

I'd love to take and take pycryptosat and turn it into an internal-only implementation and expose a public pycryptosat (with Solver class) written in Python which provides better doc text and type information. I'm not sure if the latter is possible or something Mate is interested in, so it'd probably have to come with several performance improvements too... :-) This'd give Python developers a little better auto completion and prevent mypy errors when usingpycryptosat. But I doubt Mate will spring for it right now.

[cipherboy]

Wow, Mate sniped me. :(

[jediahkatz]

@cipherboy Thanks for the thorough treatment! And you bring up some interesting points about the add_clauses_from_file idea.

I was actually wondering if you have any suggestions/resources for introducing myself to the implementation of SAT solvers at an extremely basic level? I've been reading up on DPLL and CDCL and I found this really great guide as well.

But there are a few questions I haven't had answered yet; in particular I've been wondering: how are unit clause propagation, elimination of clauses, and elimination of pure literals implemented efficiently (at a more basic level maybe, without crazy data structures)? I'm sure there are better ways than iterating through the entire formula over and over, but I was wondering how it's done.