diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index 6738a0502..2685c940c 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -200,11 +200,23 @@ namespace storm { return nameToIndexMapping.find(name) != nameToIndexMapping.end(); } - Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary) { - std::string newName = "__x" + std::to_string(freshVariableCounter++); + Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary, std::string const& prefix) { + std::string newName = prefix + std::to_string(freshVariableCounter++); return declareOrGetVariable(newName, variableType, auxiliary, false); } + Variable ExpressionManager::declareFreshBooleanVariable(bool auxiliary, const std::string& prefix) { + return declareFreshVariable(this->getBooleanType(), auxiliary, prefix); + } + + Variable ExpressionManager::declareFreshIntegerVariable(bool auxiliary, const std::string& prefix) { + return declareFreshVariable(this->getIntegerType(), auxiliary, prefix); + } + + Variable ExpressionManager::declareFreshRationalVariable(bool auxiliary, const std::string& prefix) { + return declareFreshVariable(this->getRationalType(), auxiliary, prefix); + } + uint_fast64_t ExpressionManager::getNumberOfVariables(storm::expressions::Type const& variableType) const { if (variableType.isBooleanType()) { return numberOfBooleanVariables; diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index c0bda2a5c..cef581dcf 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -230,9 +230,37 @@ namespace storm { * * @param variableType The type of the variable to declare. * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @param prefix The prefix which should be used. * @return The variable. */ - Variable declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary = false); + Variable declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary = false, std::string const& prefix = "x"); + + /*! + * Declares a variable with rational type whose name is guaranteed to be unique and not yet in use. + * + * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @param prefix The prefix which should be used. + * @return The variable. + */ + Variable declareFreshRationalVariable(bool auxiliary = false, std::string const& prefix = "x"); + + /*! + * Declares a variable with Boolean type whose name is guaranteed to be unique and not yet in use. + * + * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @param prefix The prefix which should be used. + * @return The variable. + */ + Variable declareFreshBooleanVariable(bool auxiliary = false, std::string const& prefix = "x"); + + /*! + * Declares a variable with integer type whose name is guaranteed to be unique and not yet in use. + * + * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @param prefix The prefix which should be used. + * @return The variable. + */ + Variable declareFreshIntegerVariable(bool auxiliary = false, std::string const& prefix = "x"); /*! * Retrieves the number of variables.