optimality type for formulae

src/core/core.cpp

@@ -2,6 +2,7 @@
 #include "storm/utility/initialize.h"
 #include "storm/utility/DirectEncodingExporter.h"
 #include "storm/storage/ModelFormulasPair.h"
+#include "storm/solver/OptimizationDirection.h"
 
 void define_core(py::module& m) {
     // Init
@@ -68,6 +69,13 @@ void define_build(py::module& m) {
 
 }
 
+void define_optimality_type(py::module& m) {
+    py::enum_<storm::solver::OptimizationDirection>(m, "OptimizationDirection")
+            .value("Minimize", storm::solver::OptimizationDirection::Minimize)
+            .value("Maximize", storm::solver::OptimizationDirection::Maximize)
+            ;
+}
+
 // Thin wrapper for exporting model
 template<typename ValueType>
 void exportDRN(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::string const& file) {

src/core/core.h

@@ -7,5 +7,6 @@ void define_core(py::module& m);
 void define_parse(py::module& m);
 void define_build(py::module& m);
 void define_export(py::module& m);
+void define_optimality_type(py::module& m);
 
 #endif /* PYTHON_CORE_CORE_H_ */

src/logic/formulae.cpp

@@ -58,10 +58,8 @@ void define_formulae(py::module& m) {
         .def("set_bound", [](storm::logic::OperatorFormula& f, storm::logic::ComparisonType comparisonType, storm::expressions::Expression const& bound) {
             f.setBound(storm::logic::Bound(comparisonType, bound));
         }, "Set bound", py::arg("comparison_type"), py::arg("bound"))
-        // the above method should be sufficient for now; reinstate the following if needed
-        //.def_property("_threshold_expression", &storm::logic::OperatorFormula::getThreshold, &storm::logic::OperatorFormula::setThreshold, "Threshold expression")
-        //.def_property_readonly("_threshold_as_rational", &storm::logic::OperatorFormula::getThresholdAs<storm::RationalNumber>, "Rational threshold of bound, if applicable")
-        //.def_property_readonly("_threshold_expression_has_rational_type", [](storm::logic::OperatorFormula const& f) { return f.getThreshold().hasRationalType(); } , "Check expression type [without needing a Python expression object]")
+        .def_property_readonly("has_optimality_type",  &storm::logic::OperatorFormula::hasOptimalityType, "Flag if an optimality type is present")
+        .def_property_readonly("optimality_type", &storm::logic::OperatorFormula::getOptimalityType, "Flag for the optimality type")
     ;
     py::class_<storm::logic::TimeOperatorFormula, std::shared_ptr<storm::logic::TimeOperatorFormula>>(m, "TimeOperator", "The time operator", operatorFormula);
     py::class_<storm::logic::LongRunAverageOperatorFormula, std::shared_ptr<storm::logic::LongRunAverageOperatorFormula>>(m, "LongRunAvarageOperator", "Long run average operator", operatorFormula);

src/mod_core.cpp

@@ -20,6 +20,7 @@ PYBIND11_MODULE(core, m) {
     define_property(m);
     define_parse(m);
     define_build(m);
+    define_optimality_type(m);
     define_export(m);
     define_result(m);
     define_modelchecking(m);