flatten composition in jani, (+smtsolverfactory)

lib/stormpy/storage/__init__.py

@@ -1,3 +1,4 @@
+
+import stormpy.utility
 from . import storage
 from .storage import *
-

src/storage/jani.cpp

@@ -44,6 +44,7 @@ void define_jani(py::module& m) {
         .def_static("decode_automaton_and_edge_index", &Model::decodeAutomatonAndEdgeIndices, "get edge and automaton from edge/automaton index")
         .def("make_standard_compliant", &Model::makeStandardJaniCompliant, "make standard JANI compliant")
         .def("has_standard_composition", &Model::hasStandardComposition, "is the composition the standard composition")
+        .def("flatten_composition", &Model::flattenComposition, py::arg("smt_solver_factory")=std::make_shared<storm::utility::solver::SmtSolverFactory>())
         .def("finalize", &Model::finalize,"finalizes the model. After this action, be careful changing the data structure.")
         .def("to_dot", [](Model& model) {std::stringstream ss; model.writeDotToStream(ss); return ss.str(); })
     ;

src/utility/smtsolver.cpp

@@ -1,6 +1,8 @@
 #include "smtsolver.h"
 #include <storm/solver/Z3SmtSolver.h>
 #include "storm/storage/expressions/ExpressionManager.h"
+#include <storm/solver/SmtSolver.h>
+#include <storm/utility/solver.h>
 
 void define_smt(py::module& m) {
     using SmtSolver              = storm::solver::SmtSolver;
@@ -29,4 +31,6 @@ void define_smt(py::module& m) {
 
     py::class_<Z3SmtSolver> z3solver(m, "Z3SmtSolver", "z3 API for storm smtsolver wrapper", smtsolver);
     z3solver.def(pybind11::init<storm::expressions::ExpressionManager&>());
+
+    py::class_<storm::utility::solver::SmtSolverFactory, std::shared_ptr<storm::utility::solver::SmtSolverFactory>> (m, "SmtSolverFactory", "Factory for creating SMT Solvers");
 }