1 /*
2 Copyright (c) 2013-2017, Ilan Schnell, Continuum Analytics, Inc.
3 Python bindings to picosat (http://fmv.jku.at/picosat/)
4 This file is published under the same license as picosat itself, which
5 uses an MIT style license.
6 */
7 #define PYCOSAT_URL "https://pypi.python.org/pypi/pycosat"
8 #define PYCOSAT_VERSION "0.6.3"
9
10 #include <Python.h>
11
12 #ifdef _MSC_VER
13 #define NGETRUSAGE
14 #define inline __inline
15 #endif
16
17 #include "picosat.h"
18 #ifndef DONT_INCLUDE_PICOSAT
19 #include "picosat.c"
20 #endif
21
22 /* When defined, picosat uses the Python memory manager
23 We cannot do this while we:
24 "release GIL during main picosat computation"
25 https://github.com/ContinuumIO/pycosat/commit/f50c89a10db2e87c3e6b896c43ce0549f92039d0
26 I am assuming here that we would rather release the GIL than use the Python mem allocation
27 though there is no comments to explain the trade-offs between the Python vs libc allocators
28 */
29 /* #define WITH_PYMEM */
30
31
32 #if PY_MAJOR_VERSION >= 3
33 #define IS_PY3K
34 #endif
35
36 #ifdef IS_PY3K
37 #define PyInt_FromLong PyLong_FromLong
38 #define IS_INT(x) (PyLong_Check(x))
39 #else
40 #define IS_INT(x) (PyInt_Check(x) || PyLong_Check(x))
41 #endif
42
43 #if PY_MAJOR_VERSION == 2 && PY_MINOR_VERSION <= 5
44 #define PyUnicode_FromString PyString_FromString
45 #endif
46
47 #if defined(WITH_PYMEM)
48 /* the following three adapter functions are used as arguments to
49 picosat_minit, such that picosat used the Python memory manager */
py_malloc(void * mmgr,size_t bytes)50 inline static void *py_malloc(void *mmgr, size_t bytes)
51 {
52 return PyMem_Malloc(bytes);
53 }
54
py_realloc(void * mmgr,void * ptr,size_t old,size_t new)55 inline static void *py_realloc(void *mmgr, void *ptr, size_t old, size_t new)
56 {
57 return PyMem_Realloc(ptr, new);
58 }
59
py_free(void * mmgr,void * ptr,size_t bytes)60 inline static void py_free(void *mmgr, void *ptr, size_t bytes)
61 {
62 PyMem_Free(ptr);
63 }
64 #endif
65
66 /* Add the inverse of the (current) solution to the clauses.
67 This function is essentially the same as the function blocksol in app.c
68 in the picosat source. */
blocksol(PicoSAT * picosat,signed char * mem)69 static int blocksol(PicoSAT *picosat, signed char *mem)
70 {
71 int max_idx, i;
72
73 max_idx = picosat_variables(picosat);
74 if (mem == NULL) {
75 mem = PyMem_Malloc(max_idx + 1);
76 if (mem == NULL) {
77 PyErr_NoMemory();
78 return -1;
79 }
80 }
81 for (i = 1; i <= max_idx; i++)
82 mem[i] = (picosat_deref(picosat, i) > 0) ? 1 : -1;
83
84 for (i = 1; i <= max_idx; i++)
85 picosat_add(picosat, (mem[i] < 0) ? i : -i);
86
87 picosat_add(picosat, 0);
88 return 0;
89 }
90
add_clause(PicoSAT * picosat,PyObject * clause)91 static int add_clause(PicoSAT *picosat, PyObject *clause)
92 {
93 PyObject *iterator; /* each clause is an iterable of literals */
94 PyObject *lit; /* the literals are integers */
95 int v;
96
97 iterator = PyObject_GetIter(clause);
98 if (iterator == NULL)
99 return -1;
100
101 while ((lit = PyIter_Next(iterator)) != NULL) {
102 if (!IS_INT(lit)) {
103 Py_DECREF(lit);
104 Py_DECREF(iterator);
105 PyErr_SetString(PyExc_TypeError, "integer expected");
106 return -1;
107 }
108 v = PyLong_AsLong(lit);
109 Py_DECREF(lit);
110 if (v == 0) {
111 Py_DECREF(iterator);
112 PyErr_SetString(PyExc_ValueError, "non-zero integer expected");
113 return -1;
114 }
115 picosat_add(picosat, v);
116 }
117 Py_DECREF(iterator);
118 if (PyErr_Occurred())
119 return -1;
120 picosat_add(picosat, 0);
121 return 0;
122 }
123
add_clauses(PicoSAT * picosat,PyObject * clauses)124 static int add_clauses(PicoSAT *picosat, PyObject *clauses)
125 {
126 PyObject *iterator; /* clauses can be any iterable */
127 PyObject *item; /* each clause is an iterable of integers */
128
129 iterator = PyObject_GetIter(clauses);
130 if (iterator == NULL)
131 return -1;
132
133 while ((item = PyIter_Next(iterator)) != NULL) {
134 if (add_clause(picosat, item) < 0) {
135 Py_DECREF(item);
136 Py_DECREF(iterator);
137 return -1;
138 }
139 Py_DECREF(item);
140 }
141 Py_DECREF(iterator);
142 if (PyErr_Occurred())
143 return -1;
144 return 0;
145 }
146
setup_picosat(PyObject * args,PyObject * kwds)147 static PicoSAT* setup_picosat(PyObject *args, PyObject *kwds)
148 {
149 PicoSAT *picosat;
150 PyObject *clauses; /* iterable of clauses */
151 int vars = -1, verbose = 0;
152 unsigned long long prop_limit = 0;
153 static char* kwlist[] = {"clauses",
154 "vars", "verbose", "prop_limit", NULL};
155
156 if (!PyArg_ParseTupleAndKeywords(args, kwds, "O|iiK:(iter)solve", kwlist,
157 &clauses,
158 &vars, &verbose, &prop_limit))
159 return NULL;
160
161 #if defined(WITH_PYMEM)
162 picosat = picosat_minit(NULL, py_malloc, py_realloc, py_free);
163 #else
164 picosat = picosat_init();
165 #endif
166 picosat_set_verbosity(picosat, verbose);
167 if (vars != -1)
168 picosat_adjust(picosat, vars);
169
170 if (prop_limit)
171 picosat_set_propagation_limit(picosat, prop_limit);
172
173 if (add_clauses(picosat, clauses) < 0) {
174 picosat_reset(picosat);
175 return NULL;
176 }
177
178 if (verbose >= 2)
179 picosat_print(picosat, stdout);
180
181 return picosat;
182 }
183
184 /* read the solution from the picosat object and return a Python list */
get_solution(PicoSAT * picosat)185 static PyObject* get_solution(PicoSAT *picosat)
186 {
187 PyObject *list;
188 int max_idx, i, v;
189
190 max_idx = picosat_variables(picosat);
191 list = PyList_New((Py_ssize_t) max_idx);
192 if (list == NULL) {
193 picosat_reset(picosat);
194 return NULL;
195 }
196 for (i = 1; i <= max_idx; i++) {
197 v = picosat_deref(picosat, i);
198 assert(v == -1 || v == 1);
199 if (PyList_SetItem(list, (Py_ssize_t) (i - 1),
200 PyInt_FromLong((long) (v * i))) < 0) {
201 Py_DECREF(list);
202 picosat_reset(picosat);
203 return NULL;
204 }
205 }
206 return list;
207 }
208
solve(PyObject * self,PyObject * args,PyObject * kwds)209 static PyObject* solve(PyObject *self, PyObject *args, PyObject *kwds)
210 {
211 PicoSAT *picosat;
212 PyObject *result = NULL; /* return value */
213 int res;
214
215 picosat = setup_picosat(args, kwds);
216 if (picosat == NULL)
217 return NULL;
218
219 Py_BEGIN_ALLOW_THREADS /* release GIL */
220 res = picosat_sat(picosat, -1);
221 Py_END_ALLOW_THREADS
222
223 switch (res) {
224 case PICOSAT_SATISFIABLE:
225 result = get_solution(picosat);
226 break;
227
228 case PICOSAT_UNSATISFIABLE:
229 result = PyUnicode_FromString("UNSAT");
230 break;
231
232 case PICOSAT_UNKNOWN:
233 result = PyUnicode_FromString("UNKNOWN");
234 break;
235
236 default:
237 PyErr_Format(PyExc_SystemError, "picosat return value: %d", res);
238 }
239
240 picosat_reset(picosat);
241 return result;
242 }
243
244 PyDoc_STRVAR(solve_doc,
245 "solve(clauses [, kwargs]) -> list\n\
246 \n\
247 Solve the SAT problem for the clauses, and return a solution as a\n\
248 list of integers, or one of the strings \"UNSAT\", \"UNKNOWN\".\n\
249 Please see " PYCOSAT_URL " for more details.");
250
251 /*********************** Solution Iterator *********************/
252
253 typedef struct {
254 PyObject_HEAD
255 PicoSAT *picosat;
256 signed char *mem; /* temporary storage */
257 } soliterobject;
258
259 static PyTypeObject SolIter_Type;
260
261 #define SolIter_Check(op) PyObject_TypeCheck(op, &SolIter_Type)
262
itersolve(PyObject * self,PyObject * args,PyObject * kwds)263 static PyObject* itersolve(PyObject *self, PyObject *args, PyObject *kwds)
264 {
265 soliterobject *it; /* iterator to be returned */
266
267 it = PyObject_GC_New(soliterobject, &SolIter_Type);
268 if (it == NULL)
269 return NULL;
270
271 it->picosat = setup_picosat(args, kwds);
272 if (it->picosat == NULL)
273 return NULL;
274
275 it->mem = NULL;
276 PyObject_GC_Track(it);
277 return (PyObject *) it;
278 }
279
280 PyDoc_STRVAR(itersolve_doc,
281 "itersolve(clauses [, kwargs]) -> iterator\n\
282 \n\
283 Solve the SAT problem for the clauses, and return an iterator over\n\
284 the solutions (which are lists of integers).\n\
285 Please see " PYCOSAT_URL " for more details.");
286
soliter_next(soliterobject * it)287 static PyObject* soliter_next(soliterobject *it)
288 {
289 PyObject *result = NULL; /* return value */
290 int res;
291
292 assert(SolIter_Check(it));
293
294 Py_BEGIN_ALLOW_THREADS /* release GIL */
295 res = picosat_sat(it->picosat, -1);
296 Py_END_ALLOW_THREADS
297
298 switch (res) {
299 case PICOSAT_SATISFIABLE:
300 result = get_solution(it->picosat);
301 if (result == NULL) {
302 PyErr_SetString(PyExc_SystemError, "failed to create list");
303 return NULL;
304 }
305 /* add inverse solution to the clauses, for next iteration */
306 if (blocksol(it->picosat, it->mem) < 0)
307 return NULL;
308 break;
309
310 case PICOSAT_UNSATISFIABLE:
311 case PICOSAT_UNKNOWN:
312 /* no more solutions -- stop iteration */
313 break;
314
315 default:
316 PyErr_Format(PyExc_SystemError, "picosat return value: %d", res);
317 }
318 return result;
319 }
320
soliter_dealloc(soliterobject * it)321 static void soliter_dealloc(soliterobject *it)
322 {
323 PyObject_GC_UnTrack(it);
324 if (it->mem)
325 PyMem_Free(it->mem);
326 picosat_reset(it->picosat);
327 PyObject_GC_Del(it);
328 }
329
soliter_traverse(soliterobject * it,visitproc visit,void * arg)330 static int soliter_traverse(soliterobject *it, visitproc visit, void *arg)
331 {
332 return 0;
333 }
334
335 static PyTypeObject SolIter_Type = {
336 #ifdef IS_PY3K
337 PyVarObject_HEAD_INIT(NULL, 0)
338 #else
339 PyObject_HEAD_INIT(NULL)
340 0, /* ob_size */
341 #endif
342 "soliterator", /* tp_name */
343 sizeof(soliterobject), /* tp_basicsize */
344 0, /* tp_itemsize */
345 /* methods */
346 (destructor) soliter_dealloc, /* tp_dealloc */
347 0, /* tp_print */
348 0, /* tp_getattr */
349 0, /* tp_setattr */
350 0, /* tp_compare */
351 0, /* tp_repr */
352 0, /* tp_as_number */
353 0, /* tp_as_sequence */
354 0, /* tp_as_mapping */
355 0, /* tp_hash */
356 0, /* tp_call */
357 0, /* tp_str */
358 PyObject_GenericGetAttr, /* tp_getattro */
359 0, /* tp_setattro */
360 0, /* tp_as_buffer */
361 Py_TPFLAGS_DEFAULT | Py_TPFLAGS_HAVE_GC, /* tp_flags */
362 0, /* tp_doc */
363 (traverseproc) soliter_traverse, /* tp_traverse */
364 0, /* tp_clear */
365 0, /* tp_richcompare */
366 0, /* tp_weaklistoffset */
367 PyObject_SelfIter, /* tp_iter */
368 (iternextfunc) soliter_next, /* tp_iternext */
369 0, /* tp_methods */
370 };
371
372 /*************************** Method definitions *************************/
373
374 /* declaration of methods supported by this module */
375 static PyMethodDef module_functions[] = {
376 {"solve", (PyCFunction) solve, METH_VARARGS | METH_KEYWORDS,
377 solve_doc},
378 {"itersolve", (PyCFunction) itersolve, METH_VARARGS | METH_KEYWORDS,
379 itersolve_doc},
380 {NULL, NULL} /* sentinel */
381 };
382
383 PyDoc_STRVAR(module_doc, "\
384 pycosat: bindings to PicoSAT\n\
385 ============================\n\n\
386 There are two functions in this module, solve and itersolve.\n\
387 Please see " PYCOSAT_URL " for more details.");
388
389 /* initialization routine for the shared library */
390 #ifdef IS_PY3K
391 static PyModuleDef moduledef = {
392 PyModuleDef_HEAD_INIT, "pycosat", module_doc, -1, module_functions,
393 };
PyInit_pycosat(void)394 PyMODINIT_FUNC PyInit_pycosat(void)
395 #else
396 PyMODINIT_FUNC initpycosat(void)
397 #endif
398 {
399 PyObject *m;
400
401 #ifdef IS_PY3K
402 if (PyType_Ready(&SolIter_Type) < 0)
403 return NULL;
404 m = PyModule_Create(&moduledef);
405 if (m == NULL)
406 return NULL;
407 #else
408 if (PyType_Ready(&SolIter_Type) < 0)
409 return;
410 m = Py_InitModule3("pycosat", module_functions, module_doc);
411 if (m == NULL)
412 return;
413 #endif
414
415 PyModule_AddObject(m, "__version__",
416 PyUnicode_FromString(PYCOSAT_VERSION));
417
418 #ifdef IS_PY3K
419 return m;
420 #endif
421 }
422