Somewhat cleaner setup

CMakeLists.txt

@@ -327,7 +327,7 @@ if (GIT_EXECUTABLE)
 else()
   set(GIT_SHA "GIT-hash-notfound")
 endif()
-set(CMSGEN_FULL_VERSION "6.0.6")
+set(CMSGEN_FULL_VERSION "6.1.0")
 
 string(REPLACE "." ";" CMSGEN_FULL_VERSION_LIST ${CMSGEN_FULL_VERSION})
 SetVersionNumber("PROJECT" ${CMSGEN_FULL_VERSION_LIST})

README.markdown

@@ -1,13 +1,19 @@
 [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
 [![build](https://github.com/meelgroup/cmsgen/actions/workflows/build.yml/badge.svg)](https://github.com/meelgroup/cmsgen/actions/workflows/build.yml)
 
-CMSGen a fast weighted-like sampler
-===========================================
-
-This system provides CMSGen, a fast weighted-like sampler. While we give no guarntees that the sampling follows the desired distribution, it is currently the best non-guaranteed (uniform) sampler as per our testing with [Barbarik](https://github.com/meelgroup/barbarik). In case you need guaranteed uniform sampling, please check out [UniGen](https://github.com/meelgroup/unigen). When citing CMSGen, always reference our [FMCAD'21 paper](https://meelgroup.github.io/files/publications/fmcad21_shakuni.pdf) (bibtex [here](https://meelgroup.github.io/publication/fmcad21/cite.bib)).
-
-Command-line usage
------
+# CMSGen a fast weighted, uniform-like sampler
+
+This system provides CMSGen, a fast weighted uniform-like sampler. While we give no
+guarantees that the sampling follows the desired distribution, it is currently
+the best non-guaranteed (uniform) sampler as per our testing with
+[Barbarik](https://github.com/meelgroup/barbarik). In case you need guaranteed
+uniform sampling, please check out
+[UniGen](https://github.com/meelgroup/unigen). When citing CMSGen, always
+reference our [FMCAD'21
+paper](https://meelgroup.github.io/files/publications/fmcad21_shakuni.pdf)
+(bibtex [here](https://meelgroup.github.io/publication/fmcad21/cite.bib)).
+
+## Command-line usage
 Let's take a DIMACS CNF file `input.cnf`. To get 50 uniform-like samples, run:
 
 ```
@@ -22,9 +28,10 @@ w 1 0.1
 2 0
 ```
 
-This will give solutions where variable 2 is TRUE and where variable 1 is TRUE with a probability of 0.1. This is indeed the case:
+The above gives solutions where variable 2 is TRUE always, and where variable 1 is TRUE
+with a probability of 0.1. This is indeed the case:
 
-```
+```bash
 $ echo "p cnf 2 1
 w 1 0.1
 2 0" | ./cmsgen
@@ -38,8 +45,7 @@ $ sort -n samples.out | uniq -c
 
 In other words, we got 8% samples where we had variable 1 as TRUE.
 
-Python usage
------
+## Python usage
 
 Install via pip:
 ```bash
@@ -57,15 +63,14 @@ sat, sol = solver.solve()
 
 Where the return value `sat` will be `True`, indicating there is a solution found (i.e. it's not unsatisfiable), and `sol[1]`, `sol[2]`, etc. will indicate the solution to variables 1, 2, etc.
 
-Compiling in Linux
------
+## Compiling in Linux
 
 To build and install, issue:
 
-```
+```bash
 sudo apt-get install build-essential cmake
 # not required but very useful
-sudo apt-get install zlib1g-dev libboost-program-options-dev help2man
+sudo apt-get install zlib1g-dev help2man
 git clone https://github.com/meelgroup/cmsgen
 cd cmsgen
 mkdir build && cd build
@@ -75,13 +80,12 @@ sudo make install
 sudo ldconfig
 ```
 
-Compiling in Mac OSX
------
+## Compiling in Mac OSX
 
 First, you must get Homebew from https://brew.sh/ then:
 
-```
-brew install cmake boost zlib
+```bash
+brew install cmake zlib
 tar xzvf cmsgen-[version].tar.gz
 cd cmsgen-[version]
 mkdir build && cd build

src/CMakeLists.txt

@@ -19,7 +19,6 @@
 # THE SOFTWARE.
 
 include_directories( ${PROJECT_SOURCE_DIR} )
-include_directories( ${BOSPHORUS_INCLUDE_DIRS} )
 
 if (NOT WIN32)
     add_cxx_flag_if_supported("-Wno-bitfield-constant-conversion")

src/GitSHA1.cpp.in

@@ -41,26 +41,14 @@ const char* CMSGen::get_compilation_env()
     "CMAKE_CXX_FLAGS = @CMAKE_CXX_FLAGS@ | "
     "COMPILE_DEFINES = @COMPILE_DEFINES@ | "
     "STATICCOMPILE = @STATICCOMPILE@ | "
-    "ONLY_SIMPLE = @ONLY_SIMPLE@ | "
-    "Boost_FOUND = @Boost_FOUND@ | "
-    "STATS = @STATS@ | "
-    "SQLITE3_FOUND = @SQLITE3_FOUND@ | "
     "ZLIB_FOUND = @ZLIB_FOUND@ | "
     "VALGRIND_FOUND = @VALGRIND_FOUND@ | "
     "ENABLE_TESTING = @ENABLE_TESTING@ | "
-    "M4RI_FOUND = @M4RI_FOUND@ | "
-    "NOM4RI = @NOM4RI@ | "
     "SLOW_DEBUG = @SLOW_DEBUG@ | "
     "ENABLE_ASSERTIONS = @ENABLE_ASSERTIONS@ | "
-    "PYTHON_EXECUTABLE = @PYTHON_EXECUTABLE@ | "
-    "PYTHON_LIBRARY = @PYTHON_LIBRARY@ | "
-    "PYTHON_INCLUDE_DIRS = @PYTHON_INCLUDE_DIRS@ | "
     "MY_TARGETS = @MY_TARGETS@ | "
     "LARGEMEM = @LARGEMEM@ | "
     "LIMITMEM = @LIMITMEM@ | "
-    "BOSPHORUS_LIBRARIES = @BOSPHORUS_LIBRARIES@ | "
-    "BOSPH-VER = @BOSPHORUS_VERSION_MAJOR@.@BOSPHORUS_VERSION_MINOR@ | "
-    "compilation date time = " __DATE__ " " __TIME__
     ""
     ;
     return compilation_env;

src/main.h

@@ -86,7 +86,6 @@ class Main: public MainCommon
         string command_line;
         uint32_t max_nr_of_solutions = 100;
         int sql = 0;
-        string sqlite_filename;
         string decisions_for_model_fname;
 
         //Sampling vars

src/solver.cpp

@@ -63,10 +63,6 @@ using namespace CMSGen;
 using std::cout;
 using std::endl;
 
-#ifdef USE_SQLITE3
-#include "sqlitestats.h"
-#endif
-
 //#define DRAT_DEBUG
 
 //#define DEBUG_RENUMBER

src/solverconf.cpp

@@ -256,9 +256,6 @@ DLL_PUBLIC SolverConf::SolverConf() :
         , shorten_with_gates_time_limitM(200)
         , remove_cl_with_gates_time_limitM(100)
 
-        //Gauss
-        , doM4RI(true)
-
         //Sampling
         , sampling_vars(NULL)
 

src/solverconf.h

@@ -323,7 +323,6 @@ class DLL_PUBLIC SolverConf
 
         //Gauss
         GaussConf gaussconf;
-        bool doM4RI;
 
         //Sampling
         std::vector<uint32_t>* sampling_vars;