reduce nesting for jani expressions

src/storm/storage/jani/JSONExporter.cpp

@@ -31,6 +31,7 @@
 #include "storm/storage/jani/ParallelComposition.h"
 #include "storm/storage/jani/Property.h"
 #include "storm/storage/jani/traverser/AssignmentsFinder.h"
+#include "storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h"
 
 namespace storm {
     namespace jani {
@@ -619,8 +620,7 @@ namespace storm {
         modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables) {
             
             // Simplify the expression first and reduce the nesting
-            auto simplifiedExpr = expr.simplify().reduceNesting();
-            
+            auto simplifiedExpr = storm::jani::reduceNestingInJaniExpression(expr.simplify());
             
             ExpressionToJson visitor(constants, globalVariables, localVariables, auxiliaryVariables);
             return boost::any_cast<modernjson::json>(simplifiedExpr.accept(visitor, boost::none));

src/storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.cpp

@@ -0,0 +1,62 @@
+#include "storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    
+    namespace jani {
+        storm::expressions::Expression reduceNestingInJaniExpression(storm::expressions::Expression const& expression) {
+            return storm::expressions::JaniReduceNestingExpressionVisitor().reduceNesting(expression);
+        }
+    }
+    
+    namespace expressions {
+        
+        JaniReduceNestingExpressionVisitor::JaniReduceNestingExpressionVisitor() : ReduceNestingVisitor() {
+            // Intentionally left empty.
+        }
+        
+        boost::any JaniReduceNestingExpressionVisitor::visit(ValueArrayExpression const& expression, boost::any const& data) {
+            uint64_t size = expression.size()->evaluateAsInt();
+            std::vector<std::shared_ptr<BaseExpression const>> newElements;
+            newElements.reserve(size);
+            for (uint64_t i = 0; i < size; ++i) {
+                newElements.push_back(boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.at(i)->accept(*this, data)));
+            }
+            return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new ValueArrayExpression(expression.getManager(), expression.getType(), newElements)));
+        }
+    
+        boost::any JaniReduceNestingExpressionVisitor::visit(ConstructorArrayExpression const& expression, boost::any const& data) {
+            std::shared_ptr<BaseExpression const> newSize = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.size()->accept(*this, data));
+            std::shared_ptr<BaseExpression const> elementExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getElementExpression()->accept(*this, data));
+            
+            // If the arguments did not change, we simply push the expression itself.
+            if (newSize.get() == expression.size().get() && elementExpression.get() == expression.getElementExpression().get()) {
+                return expression.getSharedPointer();
+            } else {
+				return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new ConstructorArrayExpression(expression.getManager(), expression.getType(), newSize, expression.getIndexVar(), elementExpression)));
+            }
+        }
+
+        boost::any JaniReduceNestingExpressionVisitor::visit(ArrayAccessExpression const& expression, boost::any const& data) {
+            std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this, data));
+            std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getSecondOperand()->accept(*this, data));
+            
+            // If the arguments did not change, we simply push the expression itself.
+            if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
+                return expression.getSharedPointer();
+            } else {
+				return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new ArrayAccessExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression)));
+            }
+        }
+
+        boost::any JaniReduceNestingExpressionVisitor::visit(FunctionCallExpression const& expression, boost::any const& data) {
+            std::vector<std::shared_ptr<BaseExpression const>> newArguments;
+            newArguments.reserve(expression.getNumberOfArguments());
+            for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) {
+                newArguments.push_back(boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getArgument(i)->accept(*this, data)));
+            }
+            return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new FunctionCallExpression(expression.getManager(), expression.getType(), expression.getFunctionIdentifier(), newArguments)));
+        }
+    }
+}

src/storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include "storm/storage/expressions/ReduceNestingVisitor.h"
+#include "storm/storage/jani/expressions/JaniExpressions.h"
+#include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
+
+namespace storm {
+    namespace jani {
+        storm::expressions::Expression reduceNestingInJaniExpression(storm::expressions::Expression const& expression);
+    }
+    
+    namespace expressions {
+        
+        
+        class JaniReduceNestingExpressionVisitor : public ReduceNestingVisitor, public JaniExpressionVisitor {
+        public:
+            JaniReduceNestingExpressionVisitor();
+            
+            virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(ConstructorArrayExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(FunctionCallExpression const& expression, boost::any const& data) override;
+        };
+    }
+}