expression manager now caches types, expression evaluator avoid creating unnecessary expressions and traversals

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -209,7 +209,7 @@ namespace storm {
                     printAsRange = true;
                 } else {
                     if (valuesAsMap.size() == 1) {
-                        out << valuesAsMap.begin()->second;
+                        print(out, valuesAsMap.begin()->second);
                     } else {
                         out << "{";
                         bool first = true;

src/storm/storage/expressions/ExpressionEvaluator.cpp

@@ -1,6 +1,8 @@
 #include "storm/storage/expressions/ExpressionEvaluator.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
+#include "storm/utility/constants.h"
+
 namespace storm {
     namespace expressions {
         ExpressionEvaluator<double>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluator(manager) {
@@ -31,22 +33,52 @@ namespace storm {
         }
 
 #ifdef STORM_HAVE_CARL
-        ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber>(manager) {
+        ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalNumber>(manager) {
             // Intentionally left empty.
         }
 
+        void ExpressionEvaluator<RationalNumber>::setBooleanValue(storm::expressions::Variable const& variable, bool value) {
+            ExprtkExpressionEvaluatorBase<RationalNumber>::setBooleanValue(variable, value);
+            
+            // Not forwarding value of variable to rational number visitor as it cannot treat boolean variables anyway.
+        }
+        
+        void ExpressionEvaluator<RationalNumber>::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) {
+            ExprtkExpressionEvaluatorBase<RationalNumber>::setIntegerValue(variable, value);
+            rationalNumberVisitor.setMapping(variable, storm::utility::convertNumber<RationalNumber>(value));
+        }
+        
+        void ExpressionEvaluator<RationalNumber>::setRationalValue(storm::expressions::Variable const& variable, double value) {
+            ExprtkExpressionEvaluatorBase<RationalNumber>::setRationalValue(variable, value);
+            rationalNumberVisitor.setMapping(variable, storm::utility::convertNumber<RationalNumber>(value));
+        }
+
         RationalNumber ExpressionEvaluator<RationalNumber>::asRational(Expression const& expression) const {
-            Expression substitutedExpression = expression.substitute(this->variableToExpressionMap);
-            return this->rationalNumberVisitor.toRationalNumber(substitutedExpression);
+            return this->rationalNumberVisitor.toRationalNumber(expression);
         }
         
-        ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap<RationalFunction>(manager) {
+        ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager) {
             // Intentionally left empty.
         }
         
+        void ExpressionEvaluator<RationalFunction>::setBooleanValue(storm::expressions::Variable const& variable, bool value) {
+            ExprtkExpressionEvaluatorBase<RationalFunction>::setBooleanValue(variable, value);
+            
+            // Not forwarding value of variable to rational number visitor as it cannot treat boolean variables anyway.
+        }
+        
+        void ExpressionEvaluator<RationalFunction>::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) {
+            ExprtkExpressionEvaluatorBase<RationalFunction>::setIntegerValue(variable, value);
+            rationalFunctionVisitor.setMapping(variable, storm::utility::convertNumber<RationalFunction>(value));
+        }
+        
+        void ExpressionEvaluator<RationalFunction>::setRationalValue(storm::expressions::Variable const& variable, double value) {
+            ExprtkExpressionEvaluatorBase<RationalFunction>::setRationalValue(variable, value);
+            rationalFunctionVisitor.setMapping(variable, storm::utility::convertNumber<RationalFunction>(value));
+        }
+        
         RationalFunction ExpressionEvaluator<RationalFunction>::asRational(Expression const& expression) const {
-            Expression substitutedExpression = expression.substitute(this->variableToExpressionMap);
-            return this->rationalFunctionVisitor.toRationalFunction(substitutedExpression);
+            return this->rationalFunctionVisitor.toRationalFunction(expression);
         }
         
         template class ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber>;

src/storm/storage/expressions/ExpressionEvaluator.h

@@ -37,10 +37,14 @@ namespace storm {
         
 #ifdef STORM_HAVE_CARL
         template<>
-        class ExpressionEvaluator<RationalNumber> : public ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber> {
+        class ExpressionEvaluator<RationalNumber> : public ExprtkExpressionEvaluatorBase<RationalNumber> {
         public:
             ExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
             
+            void setBooleanValue(storm::expressions::Variable const& variable, bool value) override;
+            void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) override;
+            void setRationalValue(storm::expressions::Variable const& variable, double value) override;
+            
             RationalNumber asRational(Expression const& expression) const override;
             
         private:
@@ -49,10 +53,14 @@ namespace storm {
         };
         
         template<>
-        class ExpressionEvaluator<RationalFunction> : public ExpressionEvaluatorWithVariableToExpressionMap<RationalFunction> {
+        class ExpressionEvaluator<RationalFunction> : public ExprtkExpressionEvaluatorBase<RationalFunction> {
         public:
             ExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
             
+            void setBooleanValue(storm::expressions::Variable const& variable, bool value) override;
+            void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) override;
+            void setRationalValue(storm::expressions::Variable const& variable, double value) override;
+
             RationalFunction asRational(Expression const& expression) const override;
             
         private:

src/storm/storage/expressions/ExpressionManager.cpp

@@ -52,7 +52,7 @@ namespace storm {
             }
         }
         
-        ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), numberOfBooleanVariables(0), numberOfIntegerVariables(0), numberOfBitVectorVariables(0), numberOfRationalVariables(0), numberOfAuxiliaryVariables(0), numberOfAuxiliaryBooleanVariables(0), numberOfAuxiliaryIntegerVariables(0), numberOfAuxiliaryBitVectorVariables(0), numberOfAuxiliaryRationalVariables(0), freshVariableCounter(0), types() {
+        ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), numberOfBooleanVariables(0), numberOfIntegerVariables(0), numberOfBitVectorVariables(0), numberOfRationalVariables(0), numberOfAuxiliaryVariables(0), numberOfAuxiliaryBooleanVariables(0), numberOfAuxiliaryIntegerVariables(0), numberOfAuxiliaryBitVectorVariables(0), numberOfAuxiliaryRationalVariables(0), freshVariableCounter(0) {
             // Intentionally left empty.
         }
         
@@ -65,19 +65,19 @@ namespace storm {
         }
         
         Expression ExpressionManager::boolean(bool value) const {
-            return Expression(std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(*this, value)));
+            return Expression(std::make_shared<BooleanLiteralExpression>(*this, value));
         }
 
         Expression ExpressionManager::integer(int_fast64_t value) const {
-            return Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(*this, value)));
+            return Expression(std::make_shared<IntegerLiteralExpression>(*this, value));
         }
 
         Expression ExpressionManager::rational(double value) const {
-            return Expression(std::shared_ptr<BaseExpression>(new RationalLiteralExpression(*this, value)));
+            return Expression(std::make_shared<RationalLiteralExpression>(*this, value));
         }
         
         Expression ExpressionManager::rational(storm::RationalNumber const& value) const {
-            return Expression(std::shared_ptr<BaseExpression>(new RationalLiteralExpression(*this, value)));
+            return Expression(std::make_shared<RationalLiteralExpression>(*this, value));
         }
         
         bool ExpressionManager::operator==(ExpressionManager const& other) const {
@@ -85,43 +85,34 @@ namespace storm {
         }
         
         Type const& ExpressionManager::getBooleanType() const {
-            Type type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BooleanType()));
-            auto typeIterator = types.find(type);
-            if (typeIterator == types.end()) {
-                auto iteratorBoolPair = types.insert(type);
-                return *iteratorBoolPair.first;
+            if (!booleanType) {
+                booleanType = Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BooleanType()));
             }
-            return *typeIterator;
+            return booleanType.get();
         }
         
         Type const& ExpressionManager::getIntegerType() const {
-            Type type(this->getSharedPointer(), std::shared_ptr<BaseType>(new IntegerType()));
-            auto typeIterator = types.find(type);
-            if (typeIterator == types.end()) {
-                auto iteratorBoolPair = types.insert(type);
-                return *iteratorBoolPair.first;
+            if (!integerType) {
+                integerType = Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new IntegerType()));
             }
-            return *typeIterator;
+            return integerType.get();
         }
         
         Type const& ExpressionManager::getBitVectorType(std::size_t width) const {
             Type type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BitVectorType(width)));
-            auto typeIterator = types.find(type);
-            if (typeIterator == types.end()) {
-                auto iteratorBoolPair = types.insert(type);
+            auto typeIterator = bitvectorTypes.find(type);
+            if (typeIterator == bitvectorTypes.end()) {
+                auto iteratorBoolPair = bitvectorTypes.insert(type);
                 return *iteratorBoolPair.first;
             }
             return *typeIterator;
         }
         
         Type const& ExpressionManager::getRationalType() const {
-            Type type(this->getSharedPointer(), std::shared_ptr<BaseType>(new RationalType()));
-            auto typeIterator = types.find(type);
-            if (typeIterator == types.end()) {
-                auto iteratorBoolPair = types.insert(type);
-                return *iteratorBoolPair.first;
+            if (!rationalType) {
+                rationalType = Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new RationalType()));
             }
-            return *typeIterator;
+            return rationalType.get();
         }
         
         bool ExpressionManager::isValidVariableName(std::string const& name) {

src/storm/storage/expressions/ExpressionManager.h

@@ -8,6 +8,8 @@
 #include <unordered_set>
 #include <iostream>
 
+#include <boost/optional.hpp>
+
 #include "storm/storage/expressions/Variable.h"
 #include "storm/storage/expressions/Expression.h"
 #include "storm/adapters/CarlAdapter.h"
@@ -455,8 +457,11 @@ namespace storm {
             uint_fast64_t freshVariableCounter;
             
             // The types managed by this manager.
-            mutable std::unordered_set<Type> types;
-            
+            mutable boost::optional<Type> booleanType;
+            mutable boost::optional<Type> integerType;
+            mutable std::unordered_set<Type> bitvectorTypes;
+            mutable boost::optional<Type> rationalType;
+
             // A mask that can be used to query whether a variable is an auxiliary variable.
             static const uint64_t auxiliaryMask = (1ull << 50);
             

src/storm/storage/expressions/ToCppVisitor.cpp

@@ -317,7 +317,7 @@ namespace storm {
             ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
             switch (options.getMode()) {
                 case ToCppTranslationMode::KeepType:
-                    stream << "(static_cast<double>(" << carl::getNum(expression.getValue()) << ")/carl::getDenom(expression.getValue()))";
+                    stream << "(static_cast<double>(" << carl::getNum(expression.getValue()) << ")/" << carl::getDenom(expression.getValue()) << ")";
                     break;
                 case ToCppTranslationMode::CastDouble:
                     stream << "static_cast<double>(" << expression.getValueAsDouble() << ")";

src/storm/storage/expressions/ToRationalFunctionVisitor.cpp

@@ -68,6 +68,11 @@ namespace storm {
         
         template<typename RationalFunctionType>
         boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(VariableExpression const& expression, boost::any const&) {
+            auto valueIt = valueMapping.find(expression.getVariable());
+            if (valueIt != valueMapping.end()) {
+                return valueIt->second;
+            }
+            
             auto variablePair = variableToVariableMap.find(expression.getVariable());
             if (variablePair != variableToVariableMap.end()) {
                 return convertVariableToPolynomial(variablePair->second);
@@ -95,13 +100,18 @@ namespace storm {
         
         template<typename RationalFunctionType>
         boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IntegerLiteralExpression const& expression, boost::any const&) {
-            return RationalFunctionType(carl::rationalize<storm::RationalNumber>(static_cast<size_t>(expression.getValue())));
+            return RationalFunctionType(storm::utility::convertNumber<storm::RationalFunction>(expression.getValue()));
         }
         
         template<typename RationalFunctionType>
         boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(RationalLiteralExpression const& expression, boost::any const&) {
             return storm::utility::convertNumber<storm::RationalFunction>(expression.getValue());
         }
+        
+        template<typename RationalFunctionType>
+        void ToRationalFunctionVisitor<RationalFunctionType>::setMapping(storm::expressions::Variable const& variable, RationalFunctionType const& value) {
+            valueMapping[variable] = value;
+        }
 
         template class ToRationalFunctionVisitor<storm::RationalFunction>;
 #endif

src/storm/storage/expressions/ToRationalFunctionVisitor.h

@@ -1,7 +1,10 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_
 #define STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_
 
+#include <unordered_map>
+
 #include "storm/adapters/CarlAdapter.h"
+
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/Expressions.h"
 #include "storm/storage/expressions/ExpressionVisitor.h"
@@ -29,6 +32,8 @@ namespace storm {
             virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
             
+            void setMapping(storm::expressions::Variable const& variable, RationalFunctionType const& value);
+            
         private:
             template<typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
             RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
@@ -45,6 +50,9 @@ namespace storm {
             
             // The cache that is used in case the underlying type needs a cache.
             std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
+            
+            // A mapping from variables to their values.
+            std::unordered_map<storm::expressions::Variable, RationalFunctionType> valueMapping;
         };
 #endif
     }

src/storm/storage/expressions/ToRationalNumberVisitor.cpp

@@ -68,8 +68,8 @@ namespace storm {
         }
         
         template<typename RationalNumberType>
-        boost::any ToRationalNumberVisitor<RationalNumberType>::visit(VariableExpression const&, boost::any const&) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot transform expressions containing variables to a rational number.");
+        boost::any ToRationalNumberVisitor<RationalNumberType>::visit(VariableExpression const& expression, boost::any const&) {
+            return valueMapping.at(expression.getVariable());
         }
         
         template<typename RationalNumberType>
@@ -112,6 +112,11 @@ namespace storm {
 #endif
         }
         
+        template<typename RationalNumberType>
+        void ToRationalNumberVisitor<RationalNumberType>::setMapping(storm::expressions::Variable const& variable, RationalNumberType const& value) {
+            valueMapping[variable] = value;
+        }
+        
 #ifdef STORM_HAVE_CARL
         template class ToRationalNumberVisitor<storm::RationalNumber>;
 #endif

src/storm/storage/expressions/ToRationalNumberVisitor.h

@@ -1,6 +1,9 @@
 #pragma once
 
+#include <unordered_map>
+
 #include "storm/adapters/CarlAdapter.h"
+
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/Expressions.h"
 #include "storm/storage/expressions/ExpressionVisitor.h"
@@ -26,6 +29,11 @@ namespace storm {
             virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
+            
+            void setMapping(storm::expressions::Variable const& variable, RationalNumberType const& value);
+            
+        private:
+            std::unordered_map<storm::expressions::Variable, RationalNumberType> valueMapping;
         };
     }
 }

src/storm/storage/jani/Model.cpp

@@ -998,7 +998,12 @@ namespace storm {
                 for (auto const& location : automaton.get().getLocations()) {
                     for (auto const& assignment : location.getAssignments().getTransientAssignments()) {
                         if (assignment.getExpressionVariable() == transientVariable.getExpressionVariable()) {
-                            auto newExpression = (locationVariable == this->getManager().integer(automaton.get().getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression());
+                            storm::expressions::Expression newExpression;
+                            if (automaton.get().getNumberOfLocations() <= 1) {
+                                newExpression = (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression());
+                            } else {
+                                newExpression = (locationVariable == this->getManager().integer(automaton.get().getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression());
+                            }
                             if (result.isInitialized()) {
                                 result = result || newExpression;
                             } else {

src/storm/storage/prism/ToJaniConverter.cpp

@@ -94,10 +94,18 @@ namespace storm {
                 }
             }
             
+            // Go through the labels and construct assignments to transient variables that are added to the loctions.
+            std::vector<storm::jani::Assignment> transientLocationAssignments;
+            for (auto const& label : program.getLabels()) {
+                auto newExpressionVariable = manager->declareBooleanVariable("label_" + label.getName());
+                storm::jani::BooleanVariable const& newTransientVariable = janiModel.addVariable(storm::jani::BooleanVariable(newExpressionVariable.getName(), newExpressionVariable, manager->boolean(false), true));
+
+                transientLocationAssignments.emplace_back(newTransientVariable, label.getStatePredicateExpression());
+            }
+            
             // Go through the reward models and construct assignments to the transient variables that are to be added to
             // edges and transient assignments that are added to the locations.
             std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientEdgeAssignments;
-            std::vector<storm::jani::Assignment> transientLocationAssignments;
             for (auto const& rewardModel : program.getRewardModels()) {
                 auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName());
                 storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true));

src/storm/utility/constants.cpp

@@ -357,11 +357,23 @@ namespace storm {
             return carl::rationalize<RationalNumber>(static_cast<carl::uint>(number));
         }
 
+        template<>
+        RationalNumber convertNumber(int_fast64_t const& number){
+            STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");
+            return carl::rationalize<RationalNumber>(static_cast<carl::sint>(number));
+        }
+
         template<>
         RationalFunction convertNumber(double const& number){
             return RationalFunction(carl::rationalize<RationalNumber>(number));
         }
 
+        template<>
+        RationalFunction convertNumber(int_fast64_t const& number){
+            STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");
+            return RationalFunction(carl::rationalize<RationalNumber>(static_cast<carl::uint>(number)));
+        }
+
         template<>
         RationalNumber convertNumber(std::string const& number) {
             return carl::rationalize<RationalNumber>(number);

src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp

@@ -76,8 +76,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
     
-    EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
 TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {