diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index a0d87b3..21da419 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -6,6 +6,7 @@ #include "src/helpers.h" template using SparseMatrix = storm::storage::SparseMatrix; +template using SparseMatrixBuilder = storm::storage::SparseMatrixBuilder; template using entry_index = typename storm::storage::SparseMatrix::index_type; template using MatrixEntry = storm::storage::MatrixEntry, ValueType>; using RationalFunction = storm::RationalFunction; @@ -30,6 +31,42 @@ void define_sparse_matrix(py::module& m) { .def_property_readonly("column", &MatrixEntry::getColumn, "Column") ; + // SparseMatrixBuilder + py::class_>(m, "SparseMatrixBuilder", "Builder of sparse matrix") + .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "forceDimensions"_a = true, "hasCustomRowGrouping"_a = false, "rowGroups"_a = 0) + + .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( + + Sets the matrix entry at the given row and column to the given value. After all entries have been added, + a call to finalize(false) is mandatory. + + Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and + column by column. As multiple entries per column are admitted, consecutive calls to this method are + admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are + treated as empty. If these constraints are not met, an exception is thrown. + + :param double row: The row in which the matrix entry is to be set + :param double column: The column in which the matrix entry is to be set + :param double const& value: The value that is to be set at the specified row and column + )dox", py::arg("row"), py::arg("column"), py::arg("value")) + + .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") + .def("build", &SparseMatrixBuilder::build, py::arg("overriddenRowCount") = 0, py::arg("overriddenColumnCount") = 0, py::arg("overriddenRowGroupCount") = 0, "Finalize the sparse matrix") + .def("get_last_row", &SparseMatrixBuilder::getLastRow, "Get the most recently used row") + .def("get_current_row_group_count", &SparseMatrixBuilder::getCurrentRowGroupCount, "Get the current row group count") + .def("get_last_column", &SparseMatrixBuilder::getLastColumn, "the most recently used column") + .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( + + Replaces all columns with id >= offset according to replacements. + Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. + + :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i + :param double offset: Offset to add to each id in vector index. + )dox", py::arg("replacements"), py::arg("offset")) + ; + + // todo py::class_>(m, "SparseMatrixBuilder", "Builder of parametric sparse matrix") + // SparseMatrix py::class_>(m, "SparseMatrix", "Sparse matrix") .def("__iter__", [](SparseMatrix& matrix) {