Made expression module part of storage module

CMakeLists.txt

@@ -44,7 +44,6 @@ endfunction(stormpy_module)
 
 stormpy_module(core "${STORMPY_LIB_DIR}")
 stormpy_module(info)
-stormpy_module(expressions)
 stormpy_module(logic)
 stormpy_module(storage)
 stormpy_module(utility)

lib/stormpy/expressions/__init__.py

@@ -1,2 +0,0 @@
-from . import expressions
-from .expressions import *

setup.py

@@ -181,13 +181,12 @@ setup(
     maintainer_email="sebastian.junges@cs.rwth-aachen.de",
     url="http://moves.rwth-aachen.de",
     description="stormpy - Python Bindings for Storm",
-    packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility',
+    packages=['stormpy', 'stormpy.info', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility',
               'stormpy.pars', 'stormpy.dft'],
     package_dir={'': 'lib'},
     ext_package='stormpy',
     ext_modules=[CMakeExtension('core', subdir=''),
                  CMakeExtension('info', subdir='info'),
-                 CMakeExtension('expressions', subdir='expressions'),
                  CMakeExtension('logic', subdir='logic'),
                  CMakeExtension('storage', subdir='storage'),
                  CMakeExtension('utility', subdir='utility'),

src/logic/formulae.cpp

@@ -11,11 +11,6 @@ void define_formulae(py::module& m) {
         .value("GEQ", storm::logic::ComparisonType::GreaterEqual)
     ;
 
-    /*py::class_<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
-        .def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
-    ;*/
-
-
     py::class_<storm::logic::Formula, std::shared_ptr<storm::logic::Formula>> formula(m, "Formula", "Generic Storm Formula");
     formula.def("__str__", &storm::logic::Formula::toString)
     ;
@@ -57,6 +52,9 @@ void define_formulae(py::module& m) {
                 return f.getThresholdAs<storm::RationalNumber>();
             }
         }, "Threshold of bound (currently only applicable to rational expressions)")
+        .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")

src/mod_expressions.cpp

@@ -1,21 +0,0 @@
-#include "common.h"
-#include "storm/storage/expressions/ExpressionManager.h"
-
-PYBIND11_MODULE(expressions, m) {
-    m.doc() = "Storm expressions";
-
-#ifdef STORMPY_DISABLE_SIGNATURE_DOC
-    py::options options;
-    options.disable_function_signatures();
-#endif
-
-    py::class_<std::shared_ptr<storm::expressions::ExpressionManager>>(m, "ExpressionManager", "Manages variables for expressions");
-
-    py::class_<storm::expressions::Expression>(m, "Expression", "Holds an expression")
-        .def("__str__", &storm::expressions::Expression::toString)
-        .def_property_readonly("contains_variables", &storm::expressions::Expression::containsVariables)
-        .def_property_readonly("has_boolean_type", &storm::expressions::Expression::hasBooleanType)
-        .def_property_readonly("has_integer_type", &storm::expressions::Expression::hasIntegerType)
-        .def_property_readonly("has_rational_type", &storm::expressions::Expression::hasRationalType)
-    ;
-}

src/mod_storage.cpp

@@ -5,6 +5,7 @@
 #include "storage/matrix.h"
 #include "storage/state.h"
 #include "storage/labeling.h"
+#include "storage/expressions.h"
 
 PYBIND11_MODULE(storage, m) {
     m.doc() = "Data structures in Storm";
@@ -19,4 +20,5 @@ PYBIND11_MODULE(storage, m) {
     define_sparse_matrix(m);
     define_state(m);
     define_labeling(m);
+    define_expressions(m);
 }

src/storage/expressions.cpp

@@ -0,0 +1,30 @@
+#include "expressions.h"
+#include "src/helpers.h"
+
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/storage/expressions/Expression.h"
+
+//Define python bindings
+void define_expressions(py::module& m) {
+
+    // ExpressionManager
+    py::class_<storm::expressions::ExpressionManager, std::shared_ptr<storm::expressions::ExpressionManager>>(m, "ExpressionManager", "Manages variables for expressions")
+        .def(py::init(), "Constructor")
+        .def("create_boolean", &storm::expressions::ExpressionManager::boolean, py::arg("boolean"), "Create expression from boolean")
+        .def("create_integer", &storm::expressions::ExpressionManager::integer, py::arg("integer"), "Create expression from integer number")
+        .def("create_rational", [](storm::expressions::ExpressionManager const& manager, storm::RationalNumber number) {
+                return manager.rational(number);
+            }, py::arg("rational"), "Create expression from rational number")
+    ;
+
+    // Expression
+    py::class_<storm::expressions::Expression, std::shared_ptr<storm::expressions::Expression>>(m, "Expression", "Holds an expression")
+        .def("contains_variables", &storm::expressions::Expression::containsVariables, "Check if the expression contains variables.")
+        .def("is_literal", &storm::expressions::Expression::isLiteral, "Check if the expression is a literal")
+        .def("has_boolean_type", &storm::expressions::Expression::hasBooleanType, "Check if the expression is a boolean")
+        .def("has_integer_type", &storm::expressions::Expression::hasIntegerType, "Check if the expression is an integer")
+        .def("has_rational_type", &storm::expressions::Expression::hasRationalType, "Check if the expression is a rational")
+        .def("__str__", &streamToString<storm::expressions::Expression>)
+    ;
+
+}

src/storage/expressions.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_STORAGE_EXPRESSIONS_H_
+#define PYTHON_STORAGE_EXPRESSIONS_H_
+
+#include "common.h"
+
+void define_expressions(py::module& m);
+
+#endif /* PYTHON_STORAGE_EXPRESSIONS_H_ */

tests/expressions/test_expressions.py

@@ -1,10 +0,0 @@
-import stormpy
-from stormpy.expressions import expressions
-
-
-class TestExpressions:
-    def test_expression_manager(self):
-        manager = expressions.ExpressionManager
-
-    def test_expression(self):
-        expression = expressions.Expression

tests/logic/test_formulas.py

@@ -42,14 +42,18 @@ class TestFormulas:
         assert formula.comparison_type == stormpy.logic.ComparisonType.LESS
 
     # setter not currently implemented (non-trivial due to Expression container)
-   #def test_set_bounds(self):
-   #    prop = "P<0.4 [F \"one\"]"
-   #    formula = stormpy.parse_properties(prop)[0].raw_formula
-   #    formula.threshold = pycarl.Rational("0.2")
-   #    formula.comparison_type = stormpy.logic.ComparisonType.GEQ
-   #    assert formula.threshold == pycarl.Rational("0.2")
-   #    assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ
-   #    assert str(formula) == "P>=1/5 [F \"one\"]"
+    def test_set_bounds(self):
+        import pycarl
+        import pycarl.gmp
+        prop = "P<0.4 [F \"one\"]"
+        formula = stormpy.parse_properties(prop)[0].raw_formula
+        expression_manager = stormpy.ExpressionManager()
+        rational = pycarl.gmp.Rational("0.2")
+        expression = expression_manager.create_rational(rational)
+        formula.set_bound(stormpy.logic.ComparisonType.GEQ, expression)
+        assert formula.threshold == pycarl.gmp.Rational("0.2")
+        assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ
+        assert str(formula) == "P>=1/5 [F \"one\"]"
 
     def test_subformula(self):
         prop = "P=? [F \"one\"]"

tests/storage/test_expressions.py

@@ -0,0 +1,34 @@
+import stormpy
+
+
+class TestExpressions:
+    def test_expression_manager(self):
+        manager = stormpy.ExpressionManager()
+
+    def test_boolean_expression(self):
+        manager = stormpy.ExpressionManager()
+        expression = manager.create_boolean(True)
+        assert expression.is_literal()
+        assert not expression.contains_variables()
+        assert expression.has_boolean_type()
+        assert not expression.has_integer_type()
+        assert not expression.has_rational_type()
+
+    def test_integer_expression(self):
+        manager = stormpy.ExpressionManager()
+        expression = manager.create_integer(2)
+        assert expression.is_literal()
+        assert not expression.contains_variables()
+        assert not expression.has_boolean_type()
+        assert expression.has_integer_type()
+        assert not expression.has_rational_type()
+
+    def test_rational_expression(self):
+        import pycarl.gmp
+        manager = stormpy.ExpressionManager()
+        expression = manager.create_rational(pycarl.gmp.Rational(0.2))
+        assert expression.is_literal()
+        assert not expression.contains_variables()
+        assert not expression.has_boolean_type()
+        assert not expression.has_integer_type()
+        assert expression.has_rational_type()