Another intermediate commit.

Former-commit-id: 37585dbfa0

src/adapters/MathsatExpressionAdapter.cpp

@@ -0,0 +1,5 @@
+#include "src/adapters/MathsatExpressionAdapter.h"
+
+bool operator==(msat_decl decl1, msat_decl decl2) {
+    return decl1.repr == decl2.repr;
+}

src/adapters/MathsatExpressionAdapter.h

@@ -18,6 +18,7 @@
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/NotImplementedException.h"
 
+#ifdef STORM_HAVE_MSAT
 namespace std {
     // Define hashing operator for MathSAT's declarations.
     template <>
@@ -29,9 +30,8 @@ namespace std {
 }
 
 // Define equality operator to make hashing work.
-bool operator==(msat_decl decl1, msat_decl decl2) {
-    return decl1.repr == decl2.repr;
-}
+bool operator==(msat_decl decl1, msat_decl decl2);
+#endif
 
 namespace storm {
 	namespace adapters {
@@ -72,7 +72,7 @@ namespace storm {
                 STORM_LOG_ASSERT(variable.getManager() == this->manager, "Invalid expression for solver.");
 
                 auto const& variableExpressionPair = variableToDeclarationMapping.find(variable);
-                if (variableExpressionPair != variableToDeclarationMapping.end()) {
+                if (variableExpressionPair == variableToDeclarationMapping.end()) {
                     return msat_make_constant(env, createVariable(variable));
                 }
                 return msat_make_constant(env, variableExpressionPair->second);
@@ -194,7 +194,6 @@ namespace storm {
 			virtual boost::any visit(expressions::UnaryNumericalFunctionExpression const& expression) override {
 				msat_term childResult = boost::any_cast<msat_term>(expression.getOperand()->accept(*this));
 
-
 				switch (expression.getOperatorType()) {
 					case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus:
 						return msat_make_times(env, msat_make_number(env, "-1"), childResult);

src/adapters/Z3ExpressionAdapter.h

@@ -62,7 +62,7 @@ namespace storm {
                 STORM_LOG_ASSERT(variable.getManager() == this->manager, "Invalid expression for solver.");
                 
                 auto const& variableExpressionPair = variableToExpressionMapping.find(variable);
-                if (variableExpressionPair != variableToExpressionMapping.end()) {
+                if (variableExpressionPair == variableToExpressionMapping.end()) {
                     return createVariable(variable);
                 }
                 return variableExpressionPair->second;

src/storage/dd/CuddDdManager.cpp

@@ -235,13 +235,13 @@ namespace storm {
                 } else {
                     // For integer-valued meta variables, we, however, have to add the suffix.
                     for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
-                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair);
+                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair.first);
                     }
                 }
             }
             
             // Then, we sort this list according to the indices of the ADDs.
-            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<ADD, std::string> const& a, std::pair<ADD, std::string> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
+            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<ADD, storm::expressions::Variable> const& a, std::pair<ADD, storm::expressions::Variable> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
             
             // Now, we project the sorted vector to its second component.
             std::vector<storm::expressions::Variable> result;

src/storage/expressions/BaseExpression.h

@@ -231,7 +231,7 @@ namespace storm {
             ExpressionManager const& manager;
             
             // The return type of this expression.
-            Type const& type;
+            Type type;
         };
     }
 }

src/storage/expressions/Expression.cpp

@@ -123,7 +123,7 @@ namespace storm {
         }
         
         ExpressionManager const& Expression::getManager() const {
-            return *this->manager;
+            return this->getBaseExpression().getManager();
         }
         
         Type const& Expression::getType() const {
@@ -151,7 +151,7 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, Expression const& expression) {
-            stream << expression.getBaseExpression();
+            stream << expression.getBaseExpression() << "[" << &expression.getManager() << "]";
             return stream;
         }
         

src/storage/expressions/Expression.h

@@ -44,7 +44,6 @@ namespace storm {
             friend Expression minimum(Expression const& first, Expression const& second);
             friend Expression maximum(Expression const& first, Expression const& second);
 
-            
             Expression() = default;
             
             /*!
@@ -289,9 +288,6 @@ namespace storm {
                         
             // A pointer to the underlying base expression.
             std::shared_ptr<BaseExpression const> expressionPtr;
-            
-            // A pointer to the responsible manager.
-            std::shared_ptr<ExpressionManager> manager;
         };
         
         // Provide operator overloads to conveniently construct new expressions from other expressions.

src/storage/expressions/ExpressionManager.cpp

@@ -51,7 +51,7 @@ namespace storm {
             }
         }
         
-        ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), variableTypeToCountMapping(), numberOfVariables(0), auxiliaryVariableTypeToCountMapping(), numberOfAuxiliaryVariables(0), freshVariableCounter(0) {
+        ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), variableTypeToCountMapping(), numberOfVariables(0), auxiliaryVariableTypeToCountMapping(), numberOfAuxiliaryVariables(0), freshVariableCounter(0), booleanType(nullptr), integerType(nullptr), rationalType(nullptr) {
             // Intentionally left empty.
         }
         
@@ -71,20 +71,36 @@ namespace storm {
             return this == &other;
         }
         
-        Type ExpressionManager::getBooleanType() const {
-            return Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BooleanType()));
+        Type const& ExpressionManager::getBooleanType() const {
+            if (booleanType == nullptr) {
+                booleanType = std::unique_ptr<Type>(new Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BooleanType())));
+            }
+            return *booleanType;
         }
         
-        Type ExpressionManager::getIntegerType() const {
-            return Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new IntegerType()));
+        Type const& ExpressionManager::getIntegerType() const {
+            if (integerType == nullptr) {
+                integerType = std::unique_ptr<Type>(new Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new IntegerType())));
+            }
+            return *integerType;
         }
         
-        Type ExpressionManager::getBoundedIntegerType(std::size_t width) const {
-            return Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BoundedIntegerType(width)));
+        Type const& ExpressionManager::getBoundedIntegerType(std::size_t width) const {
+            auto boundedIntegerType = boundedIntegerTypes.find(width);
+            if (boundedIntegerType == boundedIntegerTypes.end()) {
+                Type newType = Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BoundedIntegerType(width)));
+                boundedIntegerTypes[width] = newType;
+                return boundedIntegerTypes[width];
+            } else {
+                return boundedIntegerType->second;
+            }
         }
         
-        Type ExpressionManager::getRationalType() const {
-            return Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new RationalType()));
+        Type const& ExpressionManager::getRationalType() const {
+            if (rationalType == nullptr) {
+                rationalType = std::unique_ptr<Type>(new Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new RationalType())));
+            }
+            return *rationalType;
         }
         
         bool ExpressionManager::isValidVariableName(std::string const& name) {

src/storage/expressions/ExpressionManager.h

@@ -114,14 +114,14 @@ namespace storm {
              *
              * @return The boolean type.
              */
-            Type getBooleanType() const;
+            Type const& getBooleanType() const;
             
             /*!
              * Retrieves the integer type.
              *
              * @return The integer type.
              */
-            Type getIntegerType() const;
+            Type const& getIntegerType() const;
             
             /*!
              * Retrieves the bounded integer type.
@@ -129,14 +129,14 @@ namespace storm {
              * @param width The bit width of the bounded type.
              * @return The bounded integer type.
              */
-            Type getBoundedIntegerType(std::size_t width) const;
+            Type const& getBoundedIntegerType(std::size_t width) const;
             
             /*!
              * Retrieves the rational type.
              *
              * @return The rational type.
              */
-            Type getRationalType() const;
+            Type const& getRationalType() const;
             
             /*!
              * Declares a variable with a name that must not yet exist and its corresponding type. Note that the name
@@ -404,6 +404,12 @@ namespace storm {
             // A counter used to create fresh variables.
             uint_fast64_t freshVariableCounter;
             
+            // The types managed by this manager.
+            mutable std::unique_ptr<Type> booleanType;
+            mutable std::unique_ptr<Type> integerType;
+            mutable std::unique_ptr<Type> rationalType;
+            mutable std::map<std::size_t, Type> boundedIntegerTypes;
+            
             // A mask that can be used to query whether a variable is an auxiliary variable.
             static const uint64_t auxiliaryMask = (1 << 60);
             

src/storage/expressions/Type.cpp

@@ -1,15 +1,53 @@
 #include "src/storage/expressions/Type.h"
 
+#include <sstream>
+
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/utility/macros.h"
 
 namespace storm {
     namespace expressions {
         
+        BaseType::BaseType() {
+            // Intentionally left empty.
+        }
+        
         bool BaseType::operator==(BaseType const& other) const {
             return this->getMask() == other.getMask();
         }
         
+        bool BaseType::isBooleanType() const {
+            return false;
+        }
+        
+        bool BooleanType::isBooleanType() const {
+            return true;
+        }
+        
+        bool BaseType::isIntegerType() const {
+            return false;
+        }
+        
+        bool IntegerType::isIntegerType() const {
+            return true;
+        }
+        
+        bool BaseType::isBoundedIntegerType() const {
+            return false;
+        }
+        
+        bool BoundedIntegerType::isBoundedIntegerType() const {
+            return true;
+        }
+        
+        bool BaseType::isRationalType() const {
+            return false;
+        }
+        
+        bool RationalType::isRationalType() const {
+            return true;
+        }
+        
         uint64_t BooleanType::getMask() const {
             return BooleanType::mask;
         }
@@ -30,7 +68,6 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        
         uint64_t BoundedIntegerType::getMask() const {
             return BoundedIntegerType::mask;
         }
@@ -55,7 +92,11 @@ namespace storm {
             return "rational";
         }
         
-        Type::Type(std::shared_ptr<ExpressionManager const> const& manager, std::shared_ptr<BaseType> innerType) : manager(manager), innerType(innerType) {
+        Type::Type() : manager(nullptr), innerType(nullptr) {
+            // Intentionally left empty.
+        }
+        
+        Type::Type(std::shared_ptr<ExpressionManager const> const& manager, std::shared_ptr<BaseType> const& innerType) : manager(manager), innerType(innerType) {
             // Intentionally left empty.
         }
         
@@ -80,15 +121,15 @@ namespace storm {
         }
         
         bool Type::isBooleanType() const {
-            return typeid(*this->innerType) == typeid(BooleanType);
+            return this->innerType->isBooleanType();
         }
         
         bool Type::isUnboundedIntegralType() const {
-            return typeid(*this->innerType) == typeid(IntegerType);
+            return this->innerType->isIntegerType();
         }
         
         bool Type::isBoundedIntegralType() const {
-            return typeid(*this->innerType) == typeid(BoundedIntegerType);
+            return this->innerType->isBoundedIntegerType();
         }
         
         std::size_t Type::getWidth() const {
@@ -96,7 +137,7 @@ namespace storm {
         }
 
         bool Type::isRationalType() const {
-            return typeid(*this->innerType) == typeid(RationalType);
+            return this->innerType->isRationalType();
         }
         
         storm::expressions::ExpressionManager const& Type::getManager() const {

src/storage/expressions/Type.h

@@ -14,6 +14,8 @@ namespace storm {
         
         class BaseType {
         public:
+            BaseType();
+            
             /*!
              * Retrieves the mask that is associated with this type.
              *
@@ -35,12 +37,18 @@ namespace storm {
              * @return A string representation of the type.
              */
             virtual std::string getStringRepresentation() const = 0;
+            
+            virtual bool isBooleanType() const;
+            virtual bool isIntegerType() const;
+            virtual bool isBoundedIntegerType() const;
+            virtual bool isRationalType() const;
         };
 
         class BooleanType : public BaseType {
         public:
             virtual uint64_t getMask() const override;
             virtual std::string getStringRepresentation() const override;
+            virtual bool isBooleanType() const override;
 
         private:
             static const uint64_t mask = (1 << 61);
@@ -50,6 +58,7 @@ namespace storm {
         public:
             virtual uint64_t getMask() const override;
             virtual std::string getStringRepresentation() const override;
+            virtual bool isIntegerType() const override;
 
         private:
             static const uint64_t mask = (1 << 62);
@@ -77,6 +86,8 @@ namespace storm {
 
             virtual std::string getStringRepresentation() const override;
 
+            virtual bool isBoundedIntegerType() const override;
+
         private:
             static const uint64_t mask = (1 << 61) | (1 << 62);
             
@@ -87,8 +98,8 @@ namespace storm {
         class RationalType : public BaseType {
         public:
             virtual uint64_t getMask() const override;
-            
             virtual std::string getStringRepresentation() const override;
+            virtual bool isRationalType() const override;
 
         private:
             static const uint64_t mask = (1 << 63);
@@ -106,7 +117,7 @@ namespace storm {
         
         class Type {
         public:
-            Type() = default;
+            Type();
             
             /*!
              * Constructs a new type of the given manager with the given encapsulated type.
@@ -114,7 +125,7 @@ namespace storm {
              * @param manager The manager responsible for this type.
              * @param innerType The encapsulated type.
              */
-            Type(std::shared_ptr<ExpressionManager const> const& manager, std::shared_ptr<BaseType> innerType);
+            Type(std::shared_ptr<ExpressionManager const> const& manager, std::shared_ptr<BaseType> const& innerType);
 
             /*!
              * Checks whether two types are the same.