From 70efd85576c959a10c41c66b5926becc54e35518 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Mon, 2 Dec 2019 16:57:26 +0100
Subject: [PATCH] [lib] C: Refactor shift_clause & forward_code Remove calls to
python functions and replace them with much more efficient pure C functions
---
library/_cadbiom/cadbiom.c | 268 ++++++++++++++++++++++---------------
1 file changed, 159 insertions(+), 109 deletions(-)
diff --git a/library/_cadbiom/cadbiom.c b/library/_cadbiom/cadbiom.c
index ff90048..58aed70 100644
--- a/library/_cadbiom/cadbiom.c
+++ b/library/_cadbiom/cadbiom.c
@@ -116,55 +116,13 @@ int raw_get_unshift_code(int* var_num, int* shift_step)
return var_code * ((*var_num < 0) ? -1 : 1);
}
-PyDoc_STRVAR(shift_clause_doc,
-"shift_clause(numeric_clause, shift_step)\n\
-Implementation of the shift operator. Shift a numeric clause in one step.\n\
-\n\
-Basically, `shift_step` is added to positive variables and subtracted\n\
-from negative variables in `numeric_clause`.\n\
-\n\
-.. warning:: Before the call you MUST lock the unfolder with:\n\
-\"self.__locked = True\".\n\
-\n\
-:param numeric_clause: DIMACS clause (list of literals)\n\
-:param shift_step: Shift step dependant on the run\n\
-:return: DIMACS literal coding of x_0 with same value\n\
-:type numeric_clause: <list <int>>\n\
-:type shift_step: <int>\n\
-:rtype: <list>"
-);
-
-static PyObject* shift_clause(PyObject *self, PyObject *args, PyObject *kwds)
+static int _shift_clause(PyObject *self, PyObject *numeric_clause, PyObject *shifted_clause, int* shift_step)
{
- // https://docs.python.org/2/c-api/iter.html
- #ifndef NDEBUG
- /* Debugging code */
- printf("shift clause\n");
- #endif
-
- int shift_step;
- PyObject *numeric_clause;
-
- static char* kwlist[] = {"numeric_clause", "shift_step", NULL};
-
- if (!PyArg_ParseTupleAndKeywords(args, kwds, "Oi", kwlist,
- &numeric_clause,
- &shift_step)) {
- return NULL;
- }
-
PyObject *numeric_clause_iterator = PyObject_GetIter(numeric_clause);
if (numeric_clause_iterator == NULL) {
/* propagate error */
PyErr_SetString(PyExc_SystemError, "could not create iterator on clause");
- return NULL;
- }
-
- // Declare a new list with the size of the given one
- PyObject *shifted_clause = PyList_New(PySequence_Size(numeric_clause));
- if (shifted_clause == NULL) {
- PyErr_SetString(PyExc_SystemError, "failed to create a list");
- return NULL;
+ return 0;
}
PyObject *lit;
@@ -176,7 +134,9 @@ static PyObject* shift_clause(PyObject *self, PyObject *args, PyObject *kwds)
/* Debugging code */
if (!IS_INT(lit)) {
PyErr_SetString(PyExc_TypeError, "integer expected in list");
- return NULL;
+ Py_DECREF(numeric_clause_iterator);
+ Py_DECREF(lit);
+ return 0;
}
#endif
@@ -185,15 +145,15 @@ static PyObject* shift_clause(PyObject *self, PyObject *args, PyObject *kwds)
if (lit_val > 0) {
#ifdef IS_PY3K
- shifted_lit = PyLong_FromLong(lit_val + shift_step);
+ shifted_lit = PyLong_FromLong(lit_val + *shift_step);
#else
- shifted_lit = PyInt_FromLong(lit_val + shift_step);
+ shifted_lit = PyInt_FromLong(lit_val + *shift_step);
#endif
} else {
#ifdef IS_PY3K
- shifted_lit = PyLong_FromLong(lit_val - shift_step);
+ shifted_lit = PyLong_FromLong(lit_val - *shift_step);
#else
- shifted_lit = PyInt_FromLong(lit_val - shift_step);
+ shifted_lit = PyInt_FromLong(lit_val - *shift_step);
#endif
}
@@ -215,73 +175,88 @@ static PyObject* shift_clause(PyObject *self, PyObject *args, PyObject *kwds)
if (PyErr_Occurred()) {
/* propagate error */
- Py_DECREF(shifted_clause);
- return PyErr_SetFromErrno(outofconflerr);
+ return 0;
}
-
- // Return list of all shifted literals
- return shifted_clause;
+ return 1;
}
-PyDoc_STRVAR(forward_code_doc,
-"forward_code(clause, var_code_table, shift_step)\n\
-Translation from names to num codes. The translation depends on the shift direction.\n\
+PyDoc_STRVAR(shift_clause_doc,
+"shift_clause(numeric_clause, shift_step)\n\
+Implementation of the shift operator. Shift a numeric clause in one step.\n\
\n\
-Numerically code a clause with the numeric codes found in self.__var_code_table for\n\
-a base variable x and numeric_code + shift_step for x'\n\
-variable integer coding increases in future steps.\n\
+Basically, `shift_step` is added to positive variables and subtracted\n\
+from negative variables in `numeric_clause`.\n\
\n\
-..note:: Future variables x' are noted \"name`\" in Literal names.\n\
- Values of variables increases of __shift_step in future steps.\n\
+.. warning:: Before the call you MUST lock the unfolder with:\n\
+\"self.__locked = True\".\n\
\n\
-:param clause: a Clause object\n\
-:param var_code_table: Var code table from the model\n\
+:param numeric_clause: DIMACS clause (list of literals)\n\
:param shift_step: Shift step dependant on the run\n\
-:return: the DIMACS coding of the forward shifted clause\n\
-:type clause: <list <int>>\n\
-:type var_code_table: <dict>\n\
+:return: DIMACS literal coding of x_0 with same value\n\
+:type numeric_clause: <list <int>>\n\
:type shift_step: <int>\n\
:rtype: <list>"
);
-static PyObject* forward_code(PyObject *self, PyObject *args, PyObject *kwds)
+static PyObject* shift_clause(PyObject *self, PyObject *args, PyObject *kwds)
{
+ // https://docs.python.org/2/c-api/iter.html
#ifndef NDEBUG
/* Debugging code */
- printf("forward code\n");
+ printf("shift clause\n");
#endif
int shift_step;
- PyObject *clause;
- PyObject *var_code_table;
+ PyObject *numeric_clause;
- static char* kwlist[] = {"clause", "var_code_table", "shift_step", NULL};
+ static char* kwlist[] = {"numeric_clause", "shift_step", NULL};
- if (!PyArg_ParseTupleAndKeywords(args, kwds, "OOi", kwlist,
- &clause,
- &var_code_table,
+ if (!PyArg_ParseTupleAndKeywords(args, kwds, "Oi", kwlist,
+ &numeric_clause,
&shift_step)) {
return NULL;
}
+ // Declare a new list with the size of the given one
+ PyObject *shifted_clause = PyList_New(PySequence_Size(numeric_clause));
+ if (shifted_clause == NULL) {
+ PyErr_SetString(PyExc_SystemError, "failed to create a list");
+ return NULL;
+ }
+
+ // Shift clause and fill shifted_clause (new ref)
+ int ret = _shift_clause(self, numeric_clause, shifted_clause, &shift_step);
+ if (ret == 0 || PyErr_Occurred()) {
+ /* propagate error */
+ Py_XDECREF(shifted_clause);
+ return PyErr_SetFromErrno(outofconflerr);
+ }
+
+ // Return list of all shifted literals
+ return shifted_clause;
+}
+
+static int _forward_code(PyObject *self, PyObject *clause, PyObject **numeric_clause, PyObject *var_code_table, int* shift_step)
+{
+
// Get attr literals of clause object
PyObject* literals = PyObject_GetAttrString(clause, "literals");
if (literals == NULL) {
PyErr_SetString(PyExc_SystemError, "failed get attribute 'literals' on clause object");
- return NULL;
+ return 0;
}
PyObject *literals_iterator = PyObject_GetIter(literals);
if (literals_iterator == NULL) {
PyErr_SetString(PyExc_SystemError, "could not create iterator on 'literals' attribute");
- return NULL;
+ return 0;
}
// Declare a new list with the size of 'literals'
- PyObject *numeric_clause = PyList_New(PySequence_Size(literals));
- if (numeric_clause == NULL) {
+ *numeric_clause = PyList_New(PySequence_Size(literals));
+ if (*numeric_clause == NULL) {
PyErr_SetString(PyExc_SystemError, "failed to create a list");
- return NULL;
+ return 0;
}
// Append does not steal a reference, so we need Py_DECREF
// SET_ITEM steals a reference, so: no Py_DECREF on items !
@@ -295,12 +270,10 @@ static PyObject* forward_code(PyObject *self, PyObject *args, PyObject *kwds)
PyObject *multiply_result;
#ifdef IS_PY3K
PyObject *last_char = PyUnicode_FromString("`");
- PyObject *py_shift_step = PyLong_FromLong(shift_step);
- PyObject *minus_one = PyLong_FromLong(-1);
+ PyObject *py_shift_step = PyLong_FromLong(*shift_step);
#else
PyObject *last_char = PyString_FromString("`");
- PyObject *py_shift_step = PyInt_FromLong(shift_step);
- PyObject *minus_one = PyInt_FromLong(-1);
+ PyObject *py_shift_step = PyInt_FromLong(*shift_step);
#endif
Py_ssize_t i = 0;
Py_ssize_t name_size = 0;
@@ -320,8 +293,16 @@ static PyObject* forward_code(PyObject *self, PyObject *args, PyObject *kwds)
// Borrowed reference
variable_value = PyDict_GetItem(var_code_table, lit_name);
if (variable_value == NULL) {
+ Py_DECREF(lit_name);
+ Py_DECREF(lit_sign);
+ Py_DECREF(lit);
+
+ Py_DECREF(literals);
+ Py_DECREF(literals_iterator);
+ Py_DECREF(last_char);
+ Py_DECREF(py_shift_step);
PyErr_SetString(PyExc_KeyError, "lit_name not found in dict");
- return NULL;
+ return 0;
}
// Because variable_value reference IS borrowed (owned by PyDict_GetItem)
// we don't do Py_DECREF(variable_value);
@@ -334,7 +315,7 @@ static PyObject* forward_code(PyObject *self, PyObject *args, PyObject *kwds)
// t+1 variable
// Add shift_step to the value corresponding to the given name
- lit_val = PyLong_AsLong(variable_value) + shift_step;
+ lit_val = PyLong_AsLong(variable_value) + *shift_step;
// Ret of PyObject_Not is: 1 if lit is false, -1 on failure
#ifdef IS_PY3K
@@ -358,7 +339,7 @@ static PyObject* forward_code(PyObject *self, PyObject *args, PyObject *kwds)
}
// Because PyList_SET_ITEM steals the reference of multiply_result, we don't do Py_DECREF(multiply_result);
- PyList_SET_ITEM(numeric_clause, i, multiply_result);
+ PyList_SET_ITEM(*numeric_clause, i, multiply_result);
// Note:
// Add new lit_cod (use SET_ITEM instead of PyList_Append)
@@ -381,11 +362,62 @@ static PyObject* forward_code(PyObject *self, PyObject *args, PyObject *kwds)
Py_DECREF(literals_iterator);
Py_DECREF(last_char);
Py_DECREF(py_shift_step);
- Py_DECREF(minus_one);
if (PyErr_Occurred()) {
/* propagate error */
- Py_DECREF(numeric_clause);
+ return 0;
+ }
+ return 1;
+}
+
+PyDoc_STRVAR(forward_code_doc,
+"forward_code(clause, var_code_table, shift_step)\n\
+Translation from names to num codes. The translation depends on the shift direction.\n\
+\n\
+Numerically code a clause with the numeric codes found in self.__var_code_table for\n\
+a base variable x and numeric_code + shift_step for x'\n\
+variable integer coding increases in future steps.\n\
+\n\
+..note:: Future variables x' are noted \"name`\" in Literal names.\n\
+ Values of variables increases of __shift_step in future steps.\n\
+\n\
+:param clause: a Clause object\n\
+:param var_code_table: Var code table from the model\n\
+:param shift_step: Shift step dependant on the run\n\
+:return: the DIMACS coding of the forward shifted clause\n\
+:type clause: <list <int>>\n\
+:type var_code_table: <dict>\n\
+:type shift_step: <int>\n\
+:rtype: <list>"
+);
+
+static PyObject* forward_code(PyObject *self, PyObject *args, PyObject *kwds)
+{
+ #ifndef NDEBUG
+ /* Debugging code */
+ printf("forward code\n");
+ #endif
+
+ int shift_step;
+ PyObject *clause;
+ PyObject *var_code_table;
+
+ static char* kwlist[] = {"clause", "var_code_table", "shift_step", NULL};
+
+ if (!PyArg_ParseTupleAndKeywords(args, kwds, "OOi", kwlist,
+ &clause,
+ &var_code_table,
+ &shift_step)) {
+ return NULL;
+ }
+
+ PyObject *numeric_clause = NULL;
+
+ // Shift clause and fill shifted_clause (new ref)
+ int ret = _forward_code(self, clause, &numeric_clause, var_code_table, &shift_step);
+ if (ret == 0 || PyErr_Occurred()) {
+ /* propagate error */
+ Py_XDECREF(numeric_clause);
return PyErr_SetFromErrno(outofconflerr);
}
@@ -460,18 +492,25 @@ static PyObject* forward_init_dynamic(PyObject *self, PyObject *args, PyObject *
}
PyObject *clause;
- PyObject *arglist;
Py_ssize_t i = 0;
+ PyObject *numeric_clause = NULL;
while ((clause = PyIter_Next(clauses_iterator)) != NULL) {
- // Build parameters of forward_code
- // {"clause", "var_code_table", "shift_step", NULL};
- arglist = Py_BuildValue("(OOi)", clause, var_code_table, shift_step);
- PyList_SET_ITEM(numeric_clauses, i, forward_code(self, arglist, NULL));
+ // Forward code the non numeric clause to numeric_clause (new ref)
+ int ret = _forward_code(self, clause, &numeric_clause, var_code_table, &shift_step);
+ if (ret == 0 || PyErr_Occurred()) {
+ /* propagate error */
+ Py_XDECREF(numeric_clause);
+ Py_DECREF(clauses_iterator);
+ Py_DECREF(clause);
+ Py_DECREF(numeric_clauses);
+ return PyErr_SetFromErrno(outofconflerr);
+ }
+
+ PyList_SET_ITEM(numeric_clauses, i, numeric_clause);
/* release reference when done */
// no DECREF on the return of forward_code, because PyList_SET_ITEM steals reference
- Py_DECREF(arglist);
Py_DECREF(clause);
i++;
@@ -491,14 +530,21 @@ static PyObject* forward_init_dynamic(PyObject *self, PyObject *args, PyObject *
while ((clause = PyIter_Next(clauses_iterator)) != NULL) {
- // Build parameters of forward_code
- // {"clause", "var_code_table", "shift_step", NULL};
- arglist = Py_BuildValue("(OOi)", clause, var_code_table, shift_step);
- PyList_SET_ITEM(numeric_clauses, i, forward_code(self, arglist, NULL));
+ // Forward code the non numeric clause to numeric_clause (new ref)
+ int ret = _forward_code(self, clause, &numeric_clause, var_code_table, &shift_step);
+ if (ret == 0 || PyErr_Occurred()) {
+ /* propagate error */
+ Py_XDECREF(numeric_clause);
+ Py_DECREF(clauses_iterator);
+ Py_DECREF(clause);
+ Py_DECREF(numeric_clauses);
+ return PyErr_SetFromErrno(outofconflerr);
+ }
+
+ PyList_SET_ITEM(numeric_clauses, i, numeric_clause);
/* release reference when done */
// no DECREF on the return of forward_code, because PyList_SET_ITEM steals reference
- Py_DECREF(arglist);
Py_DECREF(clause);
i++;
@@ -585,21 +631,25 @@ static PyObject* shift_dynamic(PyObject *self, PyObject *args, PyObject *kwds)
PyObject *shifted_clause;
PyObject *clause;
- PyObject *arglist;
Py_ssize_t i = 0;
while ((clause = PyIter_Next(numeric_clauses_iterator)) != NULL) {
- // Build parameters of shift_clause
- // shifted_clause = shift_clause(self, clause, shift_step);
- arglist = Py_BuildValue("(Oi)", clause, shift_step);
- shifted_clause = shift_clause(self, arglist, NULL); // new ref
- Py_DECREF(arglist);
+ // Declare a new list with the size of the given one
+ shifted_clause = PyList_New(PySequence_Size(clause));
+ if (shifted_clause == NULL) {
+ PyErr_SetString(PyExc_SystemError, "failed to create a list");
+ return NULL;
+ }
- if(shifted_clause == NULL) {
- /* Pass error back */
+ // Shift clause and fill shifted_clause (new ref)
+ int ret = _shift_clause(self, clause, shifted_clause, &shift_step);
+ if (ret == 0 || PyErr_Occurred()) {
+ /* propagate error */
+ Py_XDECREF(shifted_clause);
Py_DECREF(shifted_numeric_clauses);
Py_DECREF(numeric_clauses_iterator);
- return NULL;
+ Py_DECREF(clause);
+ return PyErr_SetFromErrno(outofconflerr);
}
PyList_SET_ITEM(shifted_numeric_clauses, i, shifted_clause);
--
GitLab