Merge branch 'master' into flippable

.github/workflows/newpython.yml

@@ -35,6 +35,8 @@ jobs:
         # to supply options, put them in 'env', like:
         env:
           CIBW_BEFORE_ALL_LINUX: yum install -y boost-devel zlib-devel
+          CIBW_TEST_REQUIRES: pytest
+          CIBW_TEST_COMMAND: "pytest --color=yes -v {project}/python/tests/test_pyapproxmc.py"
           CIBW_SKIP: "*musl*"
           CIBW_ARCHS: "auto64"
 

CMakeLists.txt

@@ -350,7 +350,7 @@ if (GIT_EXECUTABLE)
 else()
   set(GIT_SHA "GIT-hash-notfound")
 endif()
-set(APPROXMC_FULL_VERSION "4.1.22")
+set(APPROXMC_FULL_VERSION "4.1.23")
 
 string(REPLACE "." ";" APPROXMC_FULL_VERSION_LIST ${APPROXMC_FULL_VERSION})
 SetVersionNumber("PROJECT" ${APPROXMC_FULL_VERSION_LIST})

README.md

@@ -32,7 +32,7 @@ count = c.count()
 print("Approximate count is: %d*2**%d" % (count[0], count[1]))
 ```
 
-The above will print that `Approximate count is: 11*2**16`. Since the largest variable in the clauses was 20, the system contained 2**20 (i.e. 1048576) potential models. However, some of these models were prohibited by the two clauses, and so only approximately 11*2**16 (i.e. 720896) models remained.
+The above will print that `Approximate count is: 11*2**16`. Since the largest variable in the clauses was 20, the system contained 2\*\*20 (i.e. 1048576) potential models. However, some of these models were prohibited by the two clauses, and so only approximately 11*2\*\*16 (i.e. 720896) models remained.
 
 If you want to count over a projection set, you need to call `count(projection_set)`, for example:
 
@@ -179,7 +179,7 @@ If you use sparse XORs, please also cite the [LICS20](https://www.comp.nus.edu.s
 
 ApproxMC builds on a series of papers on hashing-based approach: [Related Publications](https://www.comp.nus.edu.sg/~meel/publications.html)
 
-The benchmarks used in our evaluation can be found [here](https://www.comp.nus.edu.sg/~meel/Benchmarks/).
+The benchmarks used in our evaluation can be found [here](https://zenodo.org/records/10449477).
 
 ## Old Versions
 The old version, 2.0 is available under the branch "ver2". Please check out the releases for the 2.x versions under GitHub [releases](https://github.com/meelgroup/approxmc/releases). Please read the README of the old release to know how to compile the code. Old releases should easily compile.

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "setuptools.build_meta"
 
 [project]
 name = "pyapproxmc"
-version = "4.1.22"
+version = "4.1.23"
 description = "Bindings to ApproxMC, an approximate model counter"
 keywords = ["sat", "model-counting"]
 license = { file = "LICENSE" }

python/src/pyapproxmc.cpp

@@ -160,7 +160,7 @@ static int parse_clause(Counter *self, PyObject *clause, std::vector<CMSat::Lit>
         if (allow_more_vars)
             self->arjun->new_vars(max_var-(long int)self->arjun->nVars()+1);
         else {
-            PyErr_SetString(PyExc_SystemError,
+            PyErr_SetString(PyExc_ValueError,
                     "ERROR: Sampling vars contain variables that are not in the original clauses!");
             return 0;
         }
@@ -241,10 +241,10 @@ static int _add_clauses_from_array(Counter *self, const size_t array_length, con
             lits.push_back(CMSat::Lit(var, sign));
         }
         if (!lits.empty()) {
-            if (max_var >= (long int)self->appmc->nVars()) {
-                self->appmc->new_vars(max_var-(long int)self->appmc->nVars()+1);
+            if (max_var >= (long int)self->arjun->nVars()) {
+                self->arjun->new_vars(max_var-(long int)self->arjun->nVars()+1);
             }
-            self->appmc->add_clause(lits);
+            self->arjun->add_clause(lits);
         }
     }
     return 1;
@@ -413,8 +413,7 @@ Approximately count the number of solutions to the formula. It can only be calle
 static PyObject* count(Counter *self, PyObject *args, PyObject *kwds)
 {
     if (self->count_called) {
-        PyErr_SetString(PyExc_SystemError,
-                        "ERROR: Sampling vars contain variables that are not in the original clauses!");
+        PyErr_SetString(PyExc_ValueError, "ERROR: Counter.count() may only be called once!");
         return NULL;
     } else {
         self->count_called = true;
@@ -436,7 +435,7 @@ static PyObject* count(Counter *self, PyObject *args, PyObject *kwds)
         }
         for(const auto& l: sampling_lits) {
             if (l.var() > self->arjun->nVars()) {
-                PyErr_SetString(PyExc_SystemError,
+                PyErr_SetString(PyExc_ValueError,
                         "ERROR: Sampling vars contain variables that are not in the original clauses!");
                 return NULL;
             }

python/tests/test_pyapproxmc.py

@@ -1,19 +1,33 @@
+#!/usr/bin/env python3
+import sys
+from array import array
+from pathlib import Path
+
+import pytest
+
 from pyapproxmc import Counter
 
-def minimal_test():
+
+def test_minimal():
     counter = Counter(seed=2157, epsilon=0.8, delta=0.2)
     counter.add_clause(list(range(1,100)))
-    assert counter.count() == (512, 90)
 
-def sampling_set_test():
+    significand, exponent = counter.count()
+    print(f'count: {significand} * 2**{exponent}')
+    assert significand * 2**exponent == 512 * 2**90
+
+
+def test_sampling_set():
     counter = Counter(seed=2157, epsilon=0.8, delta=0.2)
     counter.add_clause(range(1,100))
     assert counter.count(list(range(1,50))) == (64, 43)
 
-def real_example_test():
+
+def test_real_example():
     counter = Counter(seed=120, epsilon=0.8, delta=0.2)
 
-    with open("test_1.cnf") as test_cnf:
+    cnf_file = Path(__file__).parent / "test_1.cnf"
+    with open(cnf_file) as test_cnf:
         # Pop sampling set and metadata lines
         lines = test_cnf.readlines()[2:]
 
@@ -24,7 +38,37 @@ def real_example_test():
 
     assert counter.count(list(range(1,21))) == (64,14)
 
+
+def test_add_clauses_minimal():
+    counter = Counter(seed=2157, epsilon=0.8, delta=0.2)
+    clauses = array('i', list(range(1,100)) + [0])
+    counter.add_clauses(clauses)
+
+    significand, exponent = counter.count()
+    print(f'count: {significand} * 2**{exponent}')
+    assert significand * 2**exponent == 512 * 2**90
+
+
+def test_add_clauses_real_example():
+    counter = Counter(seed=120, epsilon=0.8, delta=0.2)
+    clauses = []
+
+    cnf_file = Path(__file__).parent / "test_1.cnf"
+    with open((cnf_file)) as test_cnf:
+        # Pop sampling set and metadata lines
+        lines = test_cnf.readlines()[2:]
+
+        # Add clauses to counter
+        for line in lines:
+            clause = [int(i) for i in line.split()]
+            clauses += clause
+
+    counter.add_clauses(array('i', clauses))
+    significand, exponent = counter.count(list(range(1,21)))
+    print(f'count: {significand} * 2**{exponent}')
+    assert significand * 2**exponent == 64 * 2**14
+
+
 if __name__ == '__main__':
-    minimal_test()
-    sampling_set_test()
-    real_example_test()
+    ret = pytest.main([__file__, '-v'] + sys.argv[1:])
+    raise SystemExit(ret)

src/approxmc.cpp

@@ -59,7 +59,6 @@ DLL_PUBLIC AppMC::AppMC()
     data->counter.solver = new SATSolver();
     data->counter.solver->set_up_for_scalmc();
     data->counter.solver->set_allow_otf_gauss();
-    data->counter.solver->set_xor_detach(data->conf.cms_detach_xor);
 }
 
 DLL_PUBLIC AppMC::~AppMC()
@@ -164,12 +163,6 @@ DLL_PUBLIC void AppMC::set_var_elim_ratio(double var_elim_ratio)
     data->conf.var_elim_ratio = var_elim_ratio;
 }
 
-DLL_PUBLIC void AppMC::set_detach_xors(uint32_t detach_xors)
-{
-    data->conf.cms_detach_xor = detach_xors;
-    data->counter.solver->set_xor_detach(data->conf.cms_detach_xor);
-}
-
 DLL_PUBLIC void AppMC::set_reuse_models(uint32_t reuse_models)
 {
     data->conf.reuse_models = reuse_models;
@@ -295,17 +288,11 @@ DLL_PUBLIC bool AppMC::add_bnn_clause(
     return data->counter.solver->add_bnn_clause(lits, cutoff, out);
 }
 
-DLL_PUBLIC void AppMC::set_detach_warning()
-{
-    data->counter.solver->set_verbosity_detach_warning(true);
-}
-
 DLL_PUBLIC CMSat::SATSolver* AppMC::get_solver()
 {
     return data->counter.solver;
 }
 
-
 DLL_PUBLIC const std::vector<uint32_t>& AppMC::get_sampling_set() const
 {
     return data->conf.sampling_set;

src/approxmc.h

@@ -90,7 +90,6 @@ class AppMC
     //Main options
     void set_up_log(std::string log_file_name);
     void set_verbosity(uint32_t verb);
-    void set_detach_warning();
     void set_seed(uint32_t seed);
     void set_epsilon(double epsilon);
     void set_delta(double delta);

src/config.h

@@ -48,7 +48,6 @@ struct Config {
     int reuse_models = 1;
     std::vector<uint32_t> sampling_set;
     std::string logfilename = "";
-    int cms_detach_xor = 1;
     int dump_intermediary_cnf = 0;
     int debug = 0;
     int force_sol_extension = false;

src/main.cpp

@@ -67,7 +67,6 @@ uint32_t start_iter = 0;
 uint32_t verb_cls = 0;
 uint32_t simplify;
 double var_elim_ratio;
-uint32_t detach_xors = 1;
 uint32_t reuse_models = 1;
 uint32_t force_sol_extension = 0;
 uint32_t sparse = 0;
@@ -134,8 +133,6 @@ void add_appmc_options()
     improvement_options.add_options()
     ("sparse", po::value(&sparse)->default_value(sparse)
         , "0 = (default) Do not use sparse method. 1 = Generate sparse XORs when possible.")
-    ("detachxor", po::value(&detach_xors)->default_value(detach_xors)
-        , "Detach XORs in CMS")
     ("reusemodels", po::value(&reuse_models)->default_value(reuse_models)
         , "Reuse models while counting solutions")
     ("forcesolextension", po::value(&force_sol_extension)->default_value(force_sol_extension)
@@ -472,15 +469,11 @@ void set_approxmc_options()
 {
     //Main options
     appmc->set_verbosity(verbosity);
-    if (verbosity >= 2) {
-        appmc->set_detach_warning();
-    }
     appmc->set_seed(seed);
     appmc->set_epsilon(epsilon);
     appmc->set_delta(delta);
 
     //Improvement options
-    appmc->set_detach_xors(detach_xors);
     appmc->set_reuse_models(reuse_models);
     appmc->set_sparse(sparse);