diff --git a/src/adapters/MathsatExpressionAdapter.cpp b/src/adapters/MathsatExpressionAdapter.cpp new file mode 100644 index 000000000..32ff09e55 --- /dev/null +++ b/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; +} diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 94b1e1e9e..d62ab8310 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/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(expression.getOperand()->accept(*this)); - switch (expression.getOperatorType()) { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: return msat_make_times(env, msat_make_number(env, "-1"), childResult); diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index bee1b42da..0279df1ec 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/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; diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 2a689ab13..896e39fcc 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/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 const& a, std::pair const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); }); + std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); }); // Now, we project the sorted vector to its second component. std::vector result; diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h index df30292cb..15e88379e 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/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; }; } } diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 7c46235bc..fc8b1ebc6 100644 --- a/src/storage/expressions/Expression.cpp +++ b/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; } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 943440090..a52acdce7 100644 --- a/src/storage/expressions/Expression.h +++ b/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 expressionPtr; - - // A pointer to the responsible manager. - std::shared_ptr manager; }; // Provide operator overloads to conveniently construct new expressions from other expressions. diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index bd5459ad8..00d28875b 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/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(new BooleanType())); + Type const& ExpressionManager::getBooleanType() const { + if (booleanType == nullptr) { + booleanType = std::unique_ptr(new Type(this->getSharedPointer(), std::shared_ptr(new BooleanType()))); + } + return *booleanType; } - Type ExpressionManager::getIntegerType() const { - return Type(this->getSharedPointer(), std::shared_ptr(new IntegerType())); + Type const& ExpressionManager::getIntegerType() const { + if (integerType == nullptr) { + integerType = std::unique_ptr(new Type(this->getSharedPointer(), std::shared_ptr(new IntegerType()))); + } + return *integerType; } - Type ExpressionManager::getBoundedIntegerType(std::size_t width) const { - return Type(this->getSharedPointer(), std::shared_ptr(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(new BoundedIntegerType(width))); + boundedIntegerTypes[width] = newType; + return boundedIntegerTypes[width]; + } else { + return boundedIntegerType->second; + } } - Type ExpressionManager::getRationalType() const { - return Type(this->getSharedPointer(), std::shared_ptr(new RationalType())); + Type const& ExpressionManager::getRationalType() const { + if (rationalType == nullptr) { + rationalType = std::unique_ptr(new Type(this->getSharedPointer(), std::shared_ptr(new RationalType()))); + } + return *rationalType; } bool ExpressionManager::isValidVariableName(std::string const& name) { diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index 2c89315b2..3000b44cd 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/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 booleanType; + mutable std::unique_ptr integerType; + mutable std::unique_ptr rationalType; + mutable std::map boundedIntegerTypes; + // A mask that can be used to query whether a variable is an auxiliary variable. static const uint64_t auxiliaryMask = (1 << 60); diff --git a/src/storage/expressions/Type.cpp b/src/storage/expressions/Type.cpp index fcc683cd2..459550cfa 100644 --- a/src/storage/expressions/Type.cpp +++ b/src/storage/expressions/Type.cpp @@ -1,15 +1,53 @@ #include "src/storage/expressions/Type.h" +#include + #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; } @@ -29,7 +67,6 @@ namespace storm { BoundedIntegerType::BoundedIntegerType(std::size_t width) : width(width) { // Intentionally left empty. } - uint64_t BoundedIntegerType::getMask() const { return BoundedIntegerType::mask; @@ -55,7 +92,11 @@ namespace storm { return "rational"; } - Type::Type(std::shared_ptr const& manager, std::shared_ptr innerType) : manager(manager), innerType(innerType) { + Type::Type() : manager(nullptr), innerType(nullptr) { + // Intentionally left empty. + } + + Type::Type(std::shared_ptr const& manager, std::shared_ptr 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 { diff --git a/src/storage/expressions/Type.h b/src/storage/expressions/Type.h index a4a8c0307..3e3fa87f9 100644 --- a/src/storage/expressions/Type.h +++ b/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,7 +58,8 @@ 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 const& manager, std::shared_ptr innerType); + Type(std::shared_ptr const& manager, std::shared_ptr const& innerType); /*! * Checks whether two types are the same.