Skip to content

Commit

Permalink
Export concat smt2lib to bindings. Related to #230
Browse files Browse the repository at this point in the history
  • Loading branch information
JonathanSalwan committed Dec 11, 2015
1 parent c204a14 commit 48672b8
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 2 deletions.
2 changes: 1 addition & 1 deletion .build_number
Original file line number Diff line number Diff line change
@@ -1 +1 @@
760
761
24 changes: 23 additions & 1 deletion src/bindings/python/modules/smt2libCallbacks.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -572,7 +572,7 @@ static PyObject *smt2lib_compound(PyObject *self, PyObject *exprsList) {
if (exprsList == nullptr || !PyList_Check(exprsList))
return PyErr_Format(PyExc_TypeError, "compound(): expected a list of SmtAstNodes as first argument");

/* Check if the mems list contains only integer item and craft a std::list */
/* Check if the list contains only PySmtAstNode */
for (Py_ssize_t i = 0; i < PyList_Size(exprsList); i++){
PyObject *item = PyList_GetItem(exprsList, i);

Expand All @@ -586,6 +586,27 @@ static PyObject *smt2lib_compound(PyObject *self, PyObject *exprsList) {
}


static char smt2lib_concat_doc[] = "Returns a concatenated expression";
static PyObject *smt2lib_concat(PyObject *self, PyObject *exprsList) {
std::vector<smt2lib::smtAstAbstractNode *> exprs;

if (exprsList == nullptr || !PyList_Check(exprsList))
return PyErr_Format(PyExc_TypeError, "concat(): expected a list of SmtAstNodes as first argument");

/* Check if the list contains only PySmtAstNode */
for (Py_ssize_t i = 0; i < PyList_Size(exprsList); i++){
PyObject *item = PyList_GetItem(exprsList, i);

if (!PySmtAstNode_Check(item))
return PyErr_Format(PyExc_TypeError, "concat(): Each element from the list must be a SmtAstNode");

exprs.push_back(PySmtAstNode_AsSmtAstNode(item));
}

return PySmtAstNode(smt2lib::concat(exprs));
}


static char smt2lib_equal_doc[] = "Returns an 'equal' expression";
static PyObject *smt2lib_equal(PyObject *self, PyObject *args) {
PyObject *op1 = nullptr;
Expand Down Expand Up @@ -746,6 +767,7 @@ PyMethodDef smt2libCallbacks[] = {
{"bvxor", smt2lib_bvxor, METH_VARARGS, smt2lib_bvxor_doc},
{"distinct", smt2lib_distinct, METH_VARARGS, smt2lib_distinct_doc},
{"compound", smt2lib_compound, METH_O, smt2lib_compound_doc},
{"concat", smt2lib_concat, METH_O, smt2lib_concat_doc},
{"equal", smt2lib_equal, METH_VARARGS, smt2lib_equal_doc},
{"extract", smt2lib_extract, METH_VARARGS, smt2lib_extract_doc},
{"ite", smt2lib_ite, METH_VARARGS, smt2lib_ite_doc},
Expand Down

0 comments on commit 48672b8

Please sign in to comment.