From b14fbfb7afce62b06ea416a04adf892a983899a4 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Thu, 23 Apr 2020 11:35:55 -0700
Subject: [PATCH] flatten composition in jani, (+smtsolverfactory)

---
 lib/stormpy/storage/__init__.py | 3 ++-
 src/storage/jani.cpp            | 1 +
 src/utility/smtsolver.cpp       | 4 ++++
 3 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py
index d235dea..60c473c 100644
--- a/lib/stormpy/storage/__init__.py
+++ b/lib/stormpy/storage/__init__.py
@@ -1,3 +1,4 @@
+
+import stormpy.utility
 from . import storage
 from .storage import *
-
diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp
index ee57359..a18a542 100644
--- a/src/storage/jani.cpp
+++ b/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(); })
     ;
diff --git a/src/utility/smtsolver.cpp b/src/utility/smtsolver.cpp
index 4e8e258..2ff258d 100644
--- a/src/utility/smtsolver.cpp
+++ b/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");
 }
\ No newline at end of file