.github/workflows/build.yml → .github/workflows/binary-build.yml

@@ -1,6 +1,9 @@
-name: build
+name: binary build
 
-on: [push, pull_request]
+on:
+  push:
+    branches:
+      - master
 
 
 jobs:

.github/workflows/python-package-build.yml → .github/workflows/python-src-pkg-build.yml

@@ -1,8 +1,9 @@
-name: Python package build
+name: Python source package build
 
-on: [push, pull_request]
-#  release:
-#    types: [created]
+on:
+  push:
+    branches:
+      - master
 
 jobs:
   deploy:

.github/workflows/newpython.yml → .github/workflows/python-wheel-build.yml

@@ -1,6 +1,9 @@
-name: better-python-build
+name: python wheel package build
 
-on: [push, pull_request]
+on:
+  push:
+    branches:
+      - master
 
 jobs:
   build_wheels:

.gitmodules

@@ -16,9 +16,6 @@
 [submodule "scripts/build_scripts"]
 	path = scripts/build_scripts
 	url = https://github.com/msoos/cryptominisat_build.git
-[submodule "utils/drat-trim"]
-	path = utils/drat-trim
-	url = https://github.com/msoos/drat-trim
 [submodule "utils/minisat_only_elim_and_subsume"]
 	path = utils/minisat_only_elim_and_subsume
 	url = https://github.com/msoos/minisat

CMakeLists.txt

@@ -148,7 +148,6 @@ if (EMSCRIPTEN)
     set(ONLY_SIMPLE ON)
     set(BUILD_SHARED_LIBS ON)
     set(NOZLIB ON)
-    set(NOM4RI ON)
 else()
     set(THREADS_PREFER_PTHREAD_FLAG ON)
     find_package (Threads REQUIRED)
@@ -261,7 +260,6 @@ else()
     # /ZI = include debug info
     # /Wall = all warnings
 
-    add_definitions(-DNGETRUSAGE)
     add_compile_options("$<$<CONFIG:RELWITHDEBINFO>:/O2>")
     add_compile_options("$<$<CONFIG:RELWITHDEBINFO>:/ZI>")
 
@@ -452,7 +450,7 @@ else()
   set(GIT_SHA "GIT-hash-notfound")
 endif()
 
-set(CMS_FULL_VERSION "5.11.14")
+set(CMS_FULL_VERSION "5.11.15")
 
 string(REPLACE "." ";" CMS_FULL_VERSION_LIST ${CMS_FULL_VERSION})
 SetVersionNumber("PROJECT" ${CMS_FULL_VERSION_LIST})
@@ -491,6 +489,7 @@ endif()
 
 if (STATS)
     find_package (SQLITE3 REQUIRED)
+    find_package(louvain_communities CONFIG REQUIRED)
     MESSAGE(STATUS "OK, Found SQLITE3!")
     include_directories(${SQLITE3_INCLUDE_DIR})
     add_definitions( -DUSE_SQLITE3 )
@@ -594,38 +593,16 @@ endif()
 # -----------------------------------------------------------------------------
 # MIT option
 # -----------------------------------------------------------------------------
-option(REQUIRE_M4RI "Must use m4ri" OFF)
-option(NOM4RI "Don't use m4ri" ON)
 option(NOBOSPHORUS "Don't use Bosphorus" ON)
 option(REQUIRE_BOSPHORUS "Must use Bosphorus" OFF)
 option(MIT "Build with only MIT licensed components" OFF)
 if (MIT)
-    set(NOM4RI ON)
     set(NOBOSPHORUS ON)
-    if(REQUIRE_M4RI)
-        message(FATAL_ERROR "Cannot have both MIT and REQUIRE_M4RI at the same time")
-    endif()
     if(REQUIRE_BOSPHORUS)
         message(FATAL_ERROR "Cannot have both MIT and REQUIRE_BOSPHORUS at the same time")
     endif()
 endif()
 
-# -----------------------------------------------------------------------------
-# Look for M4RI (for Gauss)
-# -----------------------------------------------------------------------------
-if (NOT NOM4RI)
-    find_package(M4RI)
-    IF (M4RI_FOUND)
-        MESSAGE(STATUS "OK, Found M4RI lib at ${M4RI_LIBRARIES} and includes at ${M4RI_INCLUDE_DIRS}")
-        add_definitions( -DUSE_M4RI )
-    ELSE (M4RI_FOUND)
-        MESSAGE(WARNING "Did not find M4RI, XOR detection&manipulation disabled")
-        if (REQUIRE_M4RI)
-            MESSAGE(FATAL_ERROR "REQUIRE_M4RI was set but M4RI was not found!")
-        endif()
-    ENDIF (M4RI_FOUND)
-endif()
-
 # -----------------------------------------------------------------------------
 # Look for Boshphorus
 # -----------------------------------------------------------------------------
@@ -746,11 +723,6 @@ endforeach()
 message(STATUS "All defines at startup: ${COMPILE_DEFINES}")
 
 add_subdirectory(src cmsat5-src)
-if(EXISTS "${PROJECT_SOURCE_DIR}/utils/drat-trim/drat-trim.cpp")
-    add_subdirectory(${PROJECT_SOURCE_DIR}/utils/drat-trim utils/drat-trim)
-else()
-    message(STATUS "GIT Subprojects not initialized, not building drat-trim")
-endif()
 
 # -----------------------------------------------------------------------------
 # Add uninstall target for makefiles
@@ -806,11 +778,6 @@ set(CRYPTOMINISAT5_VERSION_FILENAME "cryptominisat5ConfigVersion.cmake")
 set(CRYPTOMINISAT5_STATIC_DEPS
     ${SQLITE3_LIBRARIES}
 )
-IF (M4RI_FOUND)
-    set(CRYPTOMINISAT5_STATIC_DEPS
-        ${CRYPTOMINISAT5_STATIC_DEPS} ${M4RI_LIBRARIES}
-        )
-endif()
 
 # Export targets
 set(MY_TARGETS cryptominisat5)

Dockerfile

@@ -9,15 +9,6 @@ RUN apt-get update && apt-get install --no-install-recommends -y software-proper
 RUN add-apt-repository -y ppa:ubuntu-toolchain-r/test && rm -rf /var/lib/apt/lists/*
 RUN apt-get update && apt-get install --no-install-recommends -y libboost-program-options-dev gcc g++ make cmake zlib1g-dev wget && rm -rf /var/lib/apt/lists/*
 
-# get M4RI
-RUN wget https://bitbucket.org/malb/m4ri/downloads/m4ri-20140914.tar.gz \
-    && tar -xvf m4ri-20140914.tar.gz
-WORKDIR m4ri-20140914
-RUN ./configure \
-    && make \
-    && make install \
-    && make clean
-
 # set up build env
 RUN groupadd -r solver -g 433
 RUN useradd -u 431 -r -g solver -d /home/solver -s /sbin/nologin -c "Docker image user" solver

LICENSE.txt

@@ -5,7 +5,7 @@ The general priciple of the licensing is as follows. Everything that's
 needed to run/build/install/link the system is MIT licensed. This allows
 easy distribution and running of the system everywhere. Files that
 have no copyright header are also MIT licensed. Note that in case you
-compile with M4RI, then M4RI's GPL license affects the final executable
+compile with Bliss, then Bliss's GPL license affects the final executable
 and library.
 
 Everything else that's not needed to run/build/install/link is usually GPLv2

README.markdown

@@ -19,7 +19,7 @@ When citing, always reference our [SAT 2009 conference paper](https://link.sprin
 License
 -----
 
-Everything that is needed to build by default is MIT licensed. If you specifically instruct the system it can build with M4RI and Bliss, which are both GPL. However, by default CryptoMiniSat will not build with these.
+Everything that is needed to build by default is MIT licensed. If you specifically instruct the system it can build with Bliss, which are both GPL. However, by default CryptoMiniSat will not build with these.
 
 
 Compiling in Linux
@@ -407,6 +407,15 @@ sudo apt-get install libboost-program-options-dev libboost-serialization-dev
 sudo apt-get install python3-pip
 sudo pip3 install sklearn pandas numpy lit matplotlib
 
+# build and install Louvain Communities
+git clone https://github.com/meelgroup/louvain-community
+cd louvain-community
+mkdir build && cd build
+cmake ..
+make -j10
+sudo make install
+cd ../..
+
 # build and install XGBoost
 git clone https://github.com/dmlc/xgboost
 cd xgboost
@@ -456,24 +465,12 @@ sqlite> select count() from sum_cl_use;
 94507
 ```
 
-The CNFs go through the following set of transformations to become the generated code:
-
-1. `./cryptominisat` dumps the data. Options: `--cldatadumpratio 0.08`, `--gluecut0 100`
-2. `./drat-trim`
-3. `./add_lemma_ind.py`
-4. `./clean_update_data.py`
-5. `./rem_data.py` Options: `--fair`, etc.
-6. `./vardata_gen_pandas.py`. Options: `--limit`
-7. `./gen_pandas.py` Options: `--limit`, `--confs`
-8. `./concat_pandas.py`
-9. `./predict.py` Options: `--forest/--tree/etc`, `--depth/--split/etc`
-
 Configuring a build for a minimal binary&library
 -----
 The following configures the system to build a bare minimal binary&library. It needs a compiler, but nothing much else:
 
 ```
-cmake -DONLY_SIMPLE=ON -DNOZLIB=ON -DSTATS=OFF -DNOVALGRIND=ON -DENABLE_TESTING=OFF .
+cmake -DONLY_SIMPLE=ON -DNOZLIB=ON -DSTATS=OFF -DENABLE_TESTING=OFF .
 ```
 
 CMake Arguments
@@ -482,15 +479,12 @@ The following arguments to cmake configure the generated build artifacts. To use
 
 - `-DSTATICCOMPILE=<ON/OFF>` -- statically linked library and binary. You must build&link `BreakID` with the same `DSTATICCOMPILE=<ON/OFF>` setting as well. You can get the BreakID library from [our GitHub repository](https://github.com/meelgroup/breakid)
 - `-DUSE_GAUSS=<ON/OFF>` -- Gauss-Jordan Elimination support. On by default.
-- `-DSTATS=<ON/OFF>` -- advanced statistics (slower)
+- `-DSTATS=<ON/OFF>` -- advanced statistics (slower). Needs [louvain communities](https://github.com/meelgroup/louvain-community) installed.
 - `-DENABLE_TESTING=<ON/OFF>` -- test suite support
 - `-DMIT=<ON/OFF>` -- MIT licensed components only
-- `-DNOM4RI=<ON/OFF>` -- without M4RI-based toplevel Gauss-Jordan Elimination support. Otherweise, we use the built-in one.
 - `-DNOMPI=<ON/OFF>` -- without MPI support
-- `-DREQUIRE_M4RI=<ON/OFF>` -- abort if M4RI is not present
 - `-DNOZLIB=<ON/OFF>` -- no gzip DIMACS input support
 - `-DONLY_SIMPLE=<ON/OFF>` -- only the simple binary is built
-- `-DNOVALGRIND=<ON/OFF>` -- no extended valgrind memory checking support
 - `-DLARGEMEM=<ON/OFF>` -- more memory available for clauses (but slower on most problems)
 - `-DIPASIR=<ON/OFF>` -- Build `libipasircryptominisat.so` for [IPASIR](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/IPASIR____IPASIR) interface support
 

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "setuptools.build_meta"
 
 [project]
 name = "pycryptosat"
-version = "5.11.14"
+version = "5.11.15"
 description = "Bindings to CryptoMiniSat, an advanced SAT solver"
 keywords = ["sat", "cryptography"]
 license = { file = "LICENSE.txt" }