Update to latest pyminisolvers.

liffiton · May 9, 2022 · e2e5303 · e2e5303
1 parent 79b784f
commit e2e5303
Show file tree

Hide file tree

Showing 12 changed files with 77 additions and 36 deletions.
diff --git a/src/pyminisolvers/README.md b/src/pyminisolvers/README.md
@@ -45,6 +45,7 @@ Setup
 Requirements:
  - Python 2.7 or 3.x
  - A standard build environment (make, gcc, etc.)
+ - zlib development libraries (e.g., `zlib1g-dev` or `zlib-devel` packages)
 
 Tested Platforms:
  - Linux

diff --git a/src/pyminisolvers/makefile b/src/pyminisolvers/makefile
@@ -3,8 +3,8 @@ CXX ?= g++
 r: libminisat.so libminicard.so
 d: libminisat.so libminicard.so
 
-r: CFLAGS=-fpic -D NDEBUG -O3 -Wall -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -Wno-parentheses -Wextra
-d: CFLAGS=-fpic -D DEBUG -O0 -ggdb -Wall -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -Wno-parentheses -Wextra
+r: CFLAGS+=-fpic -D NDEBUG -O3 -Wall -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -Wno-parentheses -Wextra
+d: CFLAGS+=-fpic -D DEBUG -O0 -ggdb -Wall -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -Wno-parentheses -Wextra
 
 OS=$(shell uname -s)
 ifeq ($(OS), Darwin)

diff --git a/src/pyminisolvers/minicard.cpp b/src/pyminisolvers/minicard.cpp
@@ -144,4 +144,12 @@ extern "C" {
         }
         return len;
     }
+
+    // getter methods for accessing solver statistics
+    uint64_t get_solves(Solver* s) { return s->solves; }
+    uint64_t get_starts(Solver* s) { return s->starts; }
+    uint64_t get_decisions(Solver* s) { return s->decisions; }
+    uint64_t get_rnd_decisions(Solver* s) { return s->rnd_decisions; }
+    uint64_t get_propagations(Solver* s) { return s->propagations; }
+    uint64_t get_conflicts(Solver* s) { return s->conflicts; }
 }
diff --git a/src/pyminisolvers/minicard/core/Main.cc b/src/pyminisolvers/minicard/core/Main.cc
@@ -38,11 +38,11 @@ void printStats(Solver& solver)
 {
     double cpu_time = cpuTime();
     double mem_used = memUsedPeak();
-    printf("restarts              : %"PRIu64"\n", solver.starts);
-    printf("conflicts             : %-12"PRIu64"   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
-    printf("decisions             : %-12"PRIu64"   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
-    printf("propagations          : %-12"PRIu64"   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
-    printf("conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
+    printf("restarts              : %" PRIu64 "\n", solver.starts);
+    printf("conflicts             : %-12" PRIu64 "   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
+    printf("decisions             : %-12" PRIu64 "   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
+    printf("propagations          : %-12" PRIu64 "   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+    printf("conflict literals     : %-12" PRIu64 "   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
     if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
     printf("CPU time              : %g s\n", cpu_time);
 }

diff --git a/src/pyminisolvers/minicard/minicard/Main.cc b/src/pyminisolvers/minicard/minicard/Main.cc
@@ -46,11 +46,11 @@ void printStats(Solver& solver)
 {
     double cpu_time = cpuTime();
     double mem_used = memUsedPeak();
-    printf("c restarts              : %"PRIu64"\n", solver.starts);
-    printf("c conflicts             : %-12"PRIu64"   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
-    printf("c decisions             : %-12"PRIu64"   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
-    printf("c propagations          : %-12"PRIu64"   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
-    printf("c conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
+    printf("c restarts              : %" PRIu64 "\n", solver.starts);
+    printf("c conflicts             : %-12" PRIu64 "   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
+    printf("c decisions             : %-12" PRIu64 "   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
+    printf("c propagations          : %-12" PRIu64 "   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+    printf("c conflict literals     : %-12" PRIu64 "   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
     if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
     printf("c CPU time              : %g s\n", cpu_time);
 }

diff --git a/src/pyminisolvers/minicard/minicard_encodings/Main.cc b/src/pyminisolvers/minicard/minicard_encodings/Main.cc
@@ -45,11 +45,11 @@ void printStats(Solver& solver)
 {
     double cpu_time = cpuTime();
     double mem_used = memUsedPeak();
-    printf("c restarts              : %"PRIu64"\n", solver.starts);
-    printf("c conflicts             : %-12"PRIu64"   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
-    printf("c decisions             : %-12"PRIu64"   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
-    printf("c propagations          : %-12"PRIu64"   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
-    printf("c conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
+    printf("c restarts              : %" PRIu64 "\n", solver.starts);
+    printf("c conflicts             : %-12" PRIu64 "   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
+    printf("c decisions             : %-12" PRIu64 "   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
+    printf("c propagations          : %-12" PRIu64 "   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+    printf("c conflict literals     : %-12" PRIu64 "   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
     if (mem_used != 0) printf("c Memory used           : %.2f MB\n", mem_used);
     printf("c CPU time              : %g s\n", cpu_time);
 }

diff --git a/src/pyminisolvers/minicard/minicard_simp_encodings/Main.cc b/src/pyminisolvers/minicard/minicard_simp_encodings/Main.cc
@@ -46,11 +46,11 @@ void printStats(Solver& solver)
 {
     double cpu_time = cpuTime();
     double mem_used = memUsedPeak();
-    printf("c restarts              : %"PRIu64"\n", solver.starts);
-    printf("c conflicts             : %-12"PRIu64"   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
-    printf("c decisions             : %-12"PRIu64"   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
-    printf("c propagations          : %-12"PRIu64"   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
-    printf("c conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
+    printf("c restarts              : %" PRIu64 "\n", solver.starts);
+    printf("c conflicts             : %-12" PRIu64 "   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
+    printf("c decisions             : %-12" PRIu64 "   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
+    printf("c propagations          : %-12" PRIu64 "   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+    printf("c conflict literals     : %-12" PRIu64 "   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
     if (mem_used != 0) printf("c Memory used           : %.2f MB\n", mem_used);
     printf("c CPU time              : %g s\n", cpu_time);
 }

diff --git a/src/pyminisolvers/minicard/utils/Options.h b/src/pyminisolvers/minicard/utils/Options.h
@@ -282,15 +282,15 @@ class Int64Option : public Option
         if (range.begin == INT64_MIN)
             fprintf(stderr, "imin");
         else
-            fprintf(stderr, "%4"PRIi64, range.begin);
+            fprintf(stderr, "%4" PRIi64, range.begin);
 
         fprintf(stderr, " .. ");
         if (range.end == INT64_MAX)
             fprintf(stderr, "imax");
         else
-            fprintf(stderr, "%4"PRIi64, range.end);
+            fprintf(stderr, "%4" PRIi64, range.end);
 
-        fprintf(stderr, "] (default: %"PRIi64")\n", value);
+        fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
         if (verbose){
             fprintf(stderr, "\n        %s\n", description);
             fprintf(stderr, "\n");

diff --git a/src/pyminisolvers/minisat.cpp b/src/pyminisolvers/minisat.cpp
@@ -137,4 +137,12 @@ extern "C" {
         }
         return len;
     }
+
+    // getter methods for accessing solver statistics
+    uint64_t get_solves(Solver* s) { return s->solves; }
+    uint64_t get_starts(Solver* s) { return s->starts; }
+    uint64_t get_decisions(Solver* s) { return s->decisions; }
+    uint64_t get_rnd_decisions(Solver* s) { return s->rnd_decisions; }
+    uint64_t get_propagations(Solver* s) { return s->propagations; }
+    uint64_t get_conflicts(Solver* s) { return s->conflicts; }
 }
diff --git a/src/pyminisolvers/minisat/minisat/core/Solver.cc b/src/pyminisolvers/minisat/minisat/core/Solver.cc
@@ -994,11 +994,11 @@ void Solver::printStats() const
 {
     double cpu_time = cpuTime();
     double mem_used = memUsedPeak();
-    printf("restarts              : %"PRIu64"\n", starts);
-    printf("conflicts             : %-12"PRIu64"   (%.0f /sec)\n", conflicts   , conflicts   /cpu_time);
-    printf("decisions             : %-12"PRIu64"   (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions   /cpu_time);
-    printf("propagations          : %-12"PRIu64"   (%.0f /sec)\n", propagations, propagations/cpu_time);
-    printf("conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
+    printf("restarts              : %" PRIu64 "\n", starts);
+    printf("conflicts             : %-12" PRIu64 "   (%.0f /sec)\n", conflicts   , conflicts   /cpu_time);
+    printf("decisions             : %-12" PRIu64 "   (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions   /cpu_time);
+    printf("propagations          : %-12" PRIu64 "   (%.0f /sec)\n", propagations, propagations/cpu_time);
+    printf("conflict literals     : %-12" PRIu64 "   (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
     if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
     printf("CPU time              : %g s\n", cpu_time);
 }

diff --git a/src/pyminisolvers/minisat/minisat/utils/Options.h b/src/pyminisolvers/minisat/minisat/utils/Options.h
@@ -282,15 +282,15 @@ class Int64Option : public Option
         if (range.begin == INT64_MIN)
             fprintf(stderr, "imin");
         else
-            fprintf(stderr, "%4"PRIi64, range.begin);
+            fprintf(stderr, "%4" PRIi64, range.begin);
 
         fprintf(stderr, " .. ");
         if (range.end == INT64_MAX)
             fprintf(stderr, "imax");
         else
-            fprintf(stderr, "%4"PRIi64, range.end);
+            fprintf(stderr, "%4" PRIi64, range.end);
 
-        fprintf(stderr, "] (default: %"PRIi64")\n", value);
+        fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
         if (verbose){
             fprintf(stderr, "\n        %s\n", description);
             fprintf(stderr, "\n");

diff --git a/src/pyminisolvers/minisolvers.py b/src/pyminisolvers/minisolvers.py
@@ -24,7 +24,7 @@
 import os
 import ctypes  # type: ignore
 from abc import ABCMeta, abstractmethod
-from ctypes import c_void_p, c_ubyte, c_bool, c_int, c_double  # type: ignore
+from ctypes import c_void_p, c_ubyte, c_bool, c_int, c_int64, c_double, pointer  # type: ignore
 
 try:
     import typing  # noqa: for mypy-lang type-checking
@@ -109,12 +109,25 @@ def _setup_lib(self, libfilename):  # type: (str) -> None
         l.getImplies_assumptions.argtypes = [c_void_p, c_void_p, c_void_p, c_int]
         l.getImplies_assumptions.restype = c_int
 
+        l.get_solves.argtypes = [c_void_p]
+        l.get_solves.restype = c_int64
+        l.get_starts.argtypes = [c_void_p]
+        l.get_starts.restype = c_int64
+        l.get_decisions.argtypes = [c_void_p]
+        l.get_decisions.restype = c_int64
+        l.get_rnd_decisions.argtypes = [c_void_p]
+        l.get_rnd_decisions.restype = c_int64
+        l.get_propagations.argtypes = [c_void_p]
+        l.get_propagations.restype = c_int64
+        l.get_conflicts.argtypes = [c_void_p]
+        l.get_conflicts.restype = c_int64
+
     def __del__(self):  # type: () -> None
         """Delete the Solver object"""
         self.lib.Solver_delete(self.s)
 
     @staticmethod
-    def _to_intptr(a):  # type: (array.array) -> Tuple[int, int]
+    def _to_intptr(a):  # type: (array.array) -> Tuple[pointer[c_int], int]
         """Helper function to get a ctypes POINTER(c_int) for an array"""
         addr, size = a.buffer_info()
         return ctypes.cast(addr, ctypes.POINTER(c_int)), size
@@ -297,7 +310,7 @@ def get_model_trues(self, start=0, end=-1, offset=0):  # type: (int, int, int) -
     def block_model(self):
         """Block the current model from the solver."""
         model = self.get_model()
-        self.add_clause([-(x+1) if model[x] > 0 else x+1 for x in range(1, len(model))])
+        self.add_clause([-(x+1) if model[x] > 0 else x+1 for x in range(len(model))])
 
     def model_value(self, i):  # type: (int) -> bool
         '''Get the value of a given variable in the current model.'''
@@ -329,6 +342,17 @@ def implies(self, assumptions=None):  # type(Sequence[int]) -> array.array
         # reduce the array down to just the valid indexes
         return res[:count]
 
+    def get_stats(self):
+        """Returns a dictionary of solver statistics."""
+        return {
+            "solves": self.lib.get_solves(self.s),
+            "starts": self.lib.get_starts(self.s),
+            "decisions": self.lib.get_decisions(self.s),
+            "rnd_decisions": self.lib.get_rnd_decisions(self.s),
+            "propagations": self.lib.get_propagations(self.s),
+            "conflicts": self.lib.get_conflicts(self.s),
+        }
+
 
 class SubsetMixin(Solver):
     """A mixin for any Solver class that lets it reason about subsets of a clause set."""