Merge branch 'master' of github.com:meelgroup/unigen into master

.github/workflows/build.yml

@@ -0,0 +1,69 @@
+name: build
+
+on: [push]
+
+env:
+  # Customize the CMake build type here (Release, Debug, RelWithDebInfo, etc.)
+  BUILD_TYPE: Release
+
+jobs:
+  build:
+    # The CMake configure and build commands are platform agnostic and should work equally
+    # well on Windows or Mac.  You can convert this to a matrix build if you need
+    # cross-platform coverage.
+    # See: https://docs.github.com/en/actions/configuring-and-managing-workflows/configuring-a-workflow#configuring-a-build-matrix
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+
+    - name: Create Build Environment
+      # Some projects don't allow in-source building, so create a separate build directory
+      # We'll use this as our working directory for all subsequent commands
+      run: cmake -E make_directory ${{runner.workspace}}/build
+
+    - name: Get Dependencies
+      run: sudo apt-get update && sudo apt-get install -yq libboost1.65-dev libboost-program-options-dev help2man
+
+    - name: Build CMS
+      run: |
+       mkdir cms_git && cd cms_git
+       git clone --depth 1 https://github.com/msoos/cryptominisat
+       cd cryptominisat
+       mkdir build && cd build
+       cmake ..
+       make
+       cd ../../..
+
+    - name: Build AppMC
+      run: |
+       mkdir appmc_git && cd appmc_git
+       git clone --depth 1 https://github.com/meelgroup/approxmc
+       cd approxmc
+       mkdir build && cd build
+       cmake ..
+       make
+       cd ../../..
+
+    - name: Configure CMake
+      # Use a bash shell so we can use the same syntax for environment variable
+      # access regardless of the host operating system
+      shell: bash
+      working-directory: ${{runner.workspace}}/build
+      # Note the current convention is to use the -S and -B options here to specify source 
+      # and build directories, but this is only available with CMake 3.13 and higher.  
+      # The CMake binaries on the Github Actions machines are (as of this writing) 3.12
+      run: cmake $GITHUB_WORKSPACE -DCMAKE_BUILD_TYPE=$BUILD_TYPE
+
+    - name: Build
+      working-directory: ${{runner.workspace}}/build
+      shell: bash
+      # Execute the build.  You can specify a specific target with "--target <NAME>"
+      run: cmake --build . --config $BUILD_TYPE
+
+    - name: Test
+      working-directory: ${{runner.workspace}}/build
+      shell: bash
+      # Execute tests defined by the CMake configuration.  
+      # See https://cmake.org/cmake/help/latest/manual/ctest.1.html for more detail
+      run: ctest -C $BUILD_TYPE

README.md

@@ -1,4 +1,6 @@
 [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
+![build](https://github.com/meelgroup/unigen/workflows/build/badge.svg)
+[![Docker Hub](https://img.shields.io/badge/docker-latest-blue.svg)](https://hub.docker.com/r/msoos/unigen/)
 
 # UniGen3: Almost-Uniform Sampler
 UniGen3 is the state of the art almost-uniform sampler  utilizing an improved version of CryptoMiniSat to handle problems of size and complexity that were not possible before. The current version is based on work Mate Soos, Stephan Gocht, and Kuldeep S. Meel, as [published in CAV-20](http://comp.nus.edu.sg/~meel/Papers/cav20-sgm.pdf). Please see below for credits.  A large part of the work is in CryptoMiniSat [here](https://github.com/msoos/cryptominisat).
@@ -21,14 +23,11 @@ cat formula.cnf | docker run --rm -i -a stdin -a stdout msoos/unigen
 ```
 
 ## How to Build
-To build on Linux, you will need the following:
+To build on Linux:
+
 ```
 sudo apt-get install build-essential cmake
 sudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev
-```
-
-Then, build CryptoMiniSat, ApproxMC, and UniGen:
-```
 git clone https://github.com/msoos/cryptominisat
 cd cryptominisat
 mkdir build && cd build
@@ -51,9 +50,6 @@ make
 sudo make install
 ```
 
-## How to Use
-First, you must translate your problem to CNF and just pass your file as input to UniGen. Voila -- and it will print the set of samples. 
-
 ### Sampling Set
 
 For some applications, one is not interested in solutions over all the variables and instead interested in sampling over the solutions projected to a subset of variables, called sampling set. UniGen allows you to specify the sampling set using the following modified version of DIMACS format:
@@ -78,11 +74,53 @@ c ind 3 4 7 8 10 11 14 17 18 26 30 35 36 39 42 47 60 62 67 0
 
 You must copy the line starting with `c ind ...` to the top of your CNF before running ApproxMC.
 
-### Running UniGen
+### Library Use
+Below is an example library use:
 
+```
+#include <unigen/unigen.h>
+using namespace CMSat;
+using namespace UniGen;
+using std::cout;
+using std::endl;
+
+void mycallback(const std::vector<int>& solution, void*)
+{
+    for(uint32_t i = 0; i < solution.size(); i++) {
+        cout << solution[i] <<  " ";
+    }
+     cout << "0" << endl;
+}
+
+int main () {
+    auto appmc = new ApproxMC::AppMC;
+    auto unigen = new UniG(appmc);
+    appmc->set_verbosity(verbosity);
+    unigen->set_callback(mycallback, NULL);
+    vector<Lit> lits;
+
+    appmc->add_variables(3);
+    lits.clear();
+    lits.push_back(Lit(0, true));
+    lits.push_back(Lit(1, true));
+    appmc->addClause(lits);
+
+    auto sol_count = appmc->count();
+    unigen->sample(&sol_count, num_samples);
+
+    lits.clear();
+    lits.push_back(Lit(0, true));
+    lits.push_back(Lit(2, true));
+    appmc->addClause(lits);
+
+    sol_count = appmc->count();
+    unigen->sample(&sol_count, num_samples);
+    return 0;
+}
+```
 
-### Guarantees
 
+### Guarantees
 UniGen ensures that the generated distribution is within (1+\epsilon)-multiplicative factor of the ideal uniform distribution.