Function SolveTask

python/symsan-py.cpp:532–580

}

static PyObject* SolveTask(PyObject *self, PyObject *args) {
  if (__z3_parser == nullptr) {
    PyErr_SetString(PyExc_RuntimeError, "parser not initialized");
    return NULL;
  }

  uint64_t id = 0;
  unsigned timeout = 5000;
  if (!PyArg_ParseTuple(args, "K|I", &id, &timeout)) {
    return NULL;
  }

  symsan::Z3ParserSolver::solution_t solutions;
  int status = __z3_parser->solve_task(id, timeout, solutions);

  PyObject *sols = PyList_New(solutions.size());
  for (size_t i = 0; i < solutions.size(); i++) {
    auto &val = solutions[i];
    PyObject *sol = PyDict_New();

    // Common fields for all operations
    PyDict_SetItemString(sol, "op", PyLong_FromLong((int)val.op));
    PyDict_SetItemString(sol, "id", PyLong_FromUnsignedLong(val.id));
    PyDict_SetItemString(sol, "offset", PyLong_FromLong(val.offset));

    // Operation-specific fields
    using op_t = symsan::Z3ParserSolver::solution_op_t;
    switch (val.op) {
      case op_t::SET:
        PyDict_SetItemString(sol, "val", PyLong_FromUnsignedLong(val.val));
        break;
      case op_t::INSERT:
        PyDict_SetItemString(sol, "data",
            PyBytes_FromStringAndSize((char*)val.data.data(), val.data.size()));
        break;
      case op_t::DELETE:
        PyDict_SetItemString(sol, "len", PyLong_FromUnsignedLong(val.len));
        break;
    }

    PyList_SetItem(sols, i, sol);
  }

  PyObject *ret = PyTuple_New(2);
  PyTuple_SetItem(ret, 0, PyLong_FromLong(status));
  PyTuple_SetItem(ret, 1, sols);

  return ret;
}

static PyObject* ExportTaskSMT2(PyObject *self, PyObject *args) {
  if (__z3_parser == nullptr) {