diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index e902dc8f9..861a7d76d 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -13,7 +13,7 @@ namespace storm { namespace solver { - GlpkLpSolver::GlpkLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), lp(nullptr), variableNameToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() { + GlpkLpSolver::GlpkLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() { // Create the LP problem for glpk. lp = glp_create_prob(); @@ -47,51 +47,60 @@ namespace storm { glp_free_env(); } - void GlpkLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - this->addVariable(name, GLP_CV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient); + storm::expressions::Variable GlpkLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + this->addVariable(newVariable, GLP_CV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient); + return newVariable; } - void GlpkLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - this->addVariable(name, GLP_CV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient); + storm::expressions::Variable GlpkLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + this->addVariable(newVariable, GLP_CV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient); + return newVariable; } - void GlpkLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - this->addVariable(name, GLP_CV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient); + storm::expressions::Variable GlpkLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + this->addVariable(newVariable, GLP_CV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient); + return newVariable; } - void GlpkLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) { - this->addVariable(name, GLP_CV, GLP_FR, 0, 0, objectiveFunctionCoefficient); + storm::expressions::Variable GlpkLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + this->addVariable(newVariable, GLP_CV, GLP_FR, 0, 0, objectiveFunctionCoefficient); + return newVariable; } - void GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { this->addVariable(name, GLP_IV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; + return newVariable; } - void GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { this->addVariable(name, GLP_IV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; } - void GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { this->addVariable(name, GLP_IV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; } - void GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) { + storm::expressions::Variable GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) { this->addVariable(name, GLP_IV, GLP_FR, 0, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; } - void GlpkLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) { + storm::expressions::Variable GlpkLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) { this->addVariable(name, GLP_BV, GLP_FR, 0, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; } - void GlpkLpSolver::addVariable(std::string const& name, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + void GlpkLpSolver::addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { // Check whether variable already exists. - auto nameIndexPair = this->variableNameToIndexMap.find(name); - STORM_LOG_THROW(nameIndexPair == this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Variable '" << nameIndexPair->first << "' already exists."); + auto nameIndexPair = this->variableToIndexMap.find(name); + STORM_LOG_THROW(nameIndexPair == this->variableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Variable '" << nameIndexPair->first << "' already exists."); // Check for valid variable type. STORM_LOG_ASSERT(variableType == GLP_CV || variableType == GLP_IV || variableType == GLP_BV, "Illegal type '" << variableType << "' for glpk variable."); @@ -105,7 +114,7 @@ namespace storm { glp_set_col_bnds(lp, nextVariableIndex, boundType, lowerBound, upperBound); glp_set_col_kind(this->lp, nextVariableIndex, variableType); glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient); - this->variableNameToIndexMap.emplace(name, this->nextVariableIndex); + this->variableToIndexMap.emplace(name, this->nextVariableIndex); ++this->nextVariableIndex; } @@ -121,23 +130,16 @@ namespace storm { STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression."); STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator."); - std::pair leftCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(0)); - std::pair rightCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(1)); - for (auto const& identifier : rightCoefficients.first.getDoubleIdentifiers()) { - if (leftCoefficients.first.containsDoubleIdentifier(identifier)) { - leftCoefficients.first.setDoubleValue(identifier, leftCoefficients.first.getDoubleValue(identifier) - rightCoefficients.first.getDoubleValue(identifier)); - } else { - leftCoefficients.first.addDoubleIdentifier(identifier, -rightCoefficients.first.getDoubleValue(identifier)); - } - } - rightCoefficients.second -= leftCoefficients.second; + storm::expressions::LinearCoefficientVisitor::VariableCoefficients leftCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(0)); + storm::expressions::LinearCoefficientVisitor::VariableCoefficients rightCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(1)); + leftCoefficients.separateVariablesFromConstantPart(rightCoefficients); // Now we need to transform the coefficients to the vector representation. std::vector variables; std::vector coefficients; - for (auto const& identifier : leftCoefficients.first.getDoubleIdentifiers()) { - auto identifierIndexPair = this->variableNameToIndexMap.find(identifier); - STORM_LOG_THROW(identifierIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Constraint contains illegal identifier '" << identifier << "'."); + for (auto const& variableCoefficientPair : leftCoefficients) { + auto variableIndexPair = this->variableToIndexMap.find(variableCoefficientPair.first); + STORM_LOG_THROW(identifierIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Constraint contains illegal identifier '" << identifier << "'."); variables.push_back(identifierIndexPair->second); coefficients.push_back(leftCoefficients.first.getDoubleValue(identifier)); } @@ -255,8 +257,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model."); } - auto variableIndexPair = this->variableNameToIndexMap.find(name); - STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'."); + auto variableIndexPair = this->variableToIndexMap.find(name); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'."); double value = 0; if (this->modelContainsIntegerVariables) { @@ -274,8 +276,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model."); } - auto variableIndexPair = this->variableNameToIndexMap.find(name); - STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'."); + auto variableIndexPair = this->variableToIndexMap.find(name); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'."); double value = 0; if (this->modelContainsIntegerVariables) { @@ -297,8 +299,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model."); } - auto variableIndexPair = this->variableNameToIndexMap.find(name); - STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'."); + auto variableIndexPair = this->variableToIndexMap.find(name); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'."); double value = 0; if (this->modelContainsIntegerVariables) { diff --git a/src/solver/GlpkLpSolver.h b/src/solver/GlpkLpSolver.h index 85a0847af..130d59a9b 100644 --- a/src/solver/GlpkLpSolver.h +++ b/src/solver/GlpkLpSolver.h @@ -56,19 +56,19 @@ namespace storm { virtual ~GlpkLpSolver(); // Methods to add continuous variables. - virtual void addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual void addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; - virtual void addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual void addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; // Methods to add integer variables. - virtual void addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual void addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; - virtual void addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual void addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; // Methods to add binary variables. - virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; // Methods to incorporate recent changes. virtual void update() const override; @@ -83,9 +83,9 @@ namespace storm { virtual bool isOptimal() const override; // Methods to retrieve values of variables and the objective function in the optimal solutions. - virtual double getContinuousValue(std::string const& name) const override; - virtual int_fast64_t getIntegerValue(std::string const& name) const override; - virtual bool getBinaryValue(std::string const& name) const override; + virtual double getContinuousValue(storm::expressions::Variable const& name) const override; + virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override; + virtual bool getBinaryValue(storm::expressions::Variable const& name) const override; virtual double getObjectiveValue() const override; // Methods to print the LP problem to a file. @@ -95,20 +95,20 @@ namespace storm { /*! * Adds a variable with the given name, type, lower and upper bound and objective function coefficient. * - * @param name The name of the variable. + * @param variable The variable to add. * @param variableType The type of the variable in terms of glpk's constants. * @param boundType A glpk flag indicating which bounds apply to the variable. * @param lowerBound The lower bound of the range of the variable. * @param upperBound The upper bound of the range of the variable. * @param objectiveFunctionCoefficient The coefficient of the variable in the objective function. */ - void addVariable(std::string const& name, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient); + void addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient); // The glpk LP problem. glp_prob* lp; - // A mapping from variable names to their indices. - std::map variableNameToIndexMap; + // A mapping from variables to their indices. + std::map variableToIndexMap; // A counter used for getting the next variable index. int nextVariableIndex; @@ -152,39 +152,39 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } @@ -212,15 +212,15 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual double getContinuousValue(std::string const& name) const override { + virtual double getContinuousValue(storm::expressions::Variable const& variable) const override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual int_fast64_t getIntegerValue(std::string const& name) const override { + virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual bool getBinaryValue(std::string const& name) const override { + virtual bool getBinaryValue(storm::expressions::Variable const& variable) const override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } diff --git a/src/solver/LpSolver.h b/src/solver/LpSolver.h index 8c729a323..6c97cb778 100644 --- a/src/solver/LpSolver.h +++ b/src/solver/LpSolver.h @@ -6,6 +6,7 @@ #include #include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/ExpressionManager.h" namespace storm { namespace solver { @@ -23,7 +24,7 @@ namespace storm { /*! * Creates an empty LP solver. By default the objective function is assumed to be minimized. */ - LpSolver() : currentModelHasBeenOptimized(false), modelSense(ModelSense::Minimize) { + LpSolver() : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), modelSense(ModelSense::Minimize) { // Intentionally left empty. } @@ -47,7 +48,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0; /*! * Registers a lower-bounded continuous variable, i.e. a variable that may take all real values up to its @@ -58,7 +59,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0; /*! * Registers an upper-bounded continuous variable, i.e. a variable that may take all real values up to its @@ -69,7 +70,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0; /*! * Registers a unbounded continuous variable, i.e. a variable that may take all real values. @@ -78,7 +79,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; /*! * Registers an upper- and lower-bounded integer variable, i.e. a variable that may take all integer values @@ -90,7 +91,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0; /*! * Registers a lower-bounded integer variable, i.e. a variable that may take all integer values up to its @@ -101,7 +102,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0; /*! * Registers an upper-bounded integer variable, i.e. a variable that may take all integer values up to its @@ -112,7 +113,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0; /*! * Registers an unbounded integer variable, i.e. a variable that may take all integer values. @@ -121,7 +122,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; /*! * Registers a boolean variable, i.e. a variable that may be either 0 or 1. @@ -130,7 +131,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; /*! * Updates the model to make the variables that have been declared since the last call to update @@ -182,28 +183,28 @@ namespace storm { * Retrieves the value of the integer variable with the given name. Note that this may only be called, if * the model was found to be optimal, i.e. iff isOptimal() returns true. * - * @param name The name of the variable whose integer value (in the optimal solution) to retrieve. + * @param variable The variable whose integer value (in the optimal solution) to retrieve. * @return The value of the integer variable in the optimal solution. */ - virtual int_fast64_t getIntegerValue(std::string const& name) const = 0; + virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const = 0; /*! * Retrieves the value of the binary variable with the given name. Note that this may only be called, if * the model was found to be optimal, i.e. iff isOptimal() returns true. * - * @param name The name of the variable whose binary (boolean) value (in the optimal solution) to retrieve. + * @param variable The variable whose integer value (in the optimal solution) to retrieve. * @return The value of the binary variable in the optimal solution. */ - virtual bool getBinaryValue(std::string const& name) const = 0; + virtual bool getBinaryValue(storm::expressions::Variable const& variable) const = 0; /*! * Retrieves the value of the continuous variable with the given name. Note that this may only be called, * if the model was found to be optimal, i.e. iff isOptimal() returns true. * - * @param name The name of the variable whose continuous value (in the optimal solution) to retrieve. + * @param variable The variable whose integer value (in the optimal solution) to retrieve. * @return The value of the continuous variable in the optimal solution. */ - virtual double getContinuousValue(std::string const& name) const = 0; + virtual double getContinuousValue(storm::expressions::Variable const& variable) const = 0; /*! * Retrieves the value of the objective function. Note that this may only be called, if the model was found @@ -242,6 +243,9 @@ namespace storm { } protected: + // The manager responsible for the variables. + std::shared_ptr manager; + // A flag indicating whether the current model has been optimized and not changed afterwards. mutable bool currentModelHasBeenOptimized; diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 4d85b851d..2d543884d 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -240,7 +240,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() { - storm::expressions::SimpleValuation stormModel(this->getManager()); + storm::expressions::SimpleValuation stormModel(this->getManager().getSharedPointer()); msat_model_iterator modelIterator = msat_create_model_iterator(env); STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(modelIterator), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator."); @@ -289,7 +289,7 @@ namespace storm { static int allsatValuationsCallback(msat_term* model, int size, void* user_data) { AllsatValuationCallbackUserData* user = reinterpret_cast(user_data); - storm::expressions::SimpleValuation valuation(user->manager); + storm::expressions::SimpleValuation valuation(user->manager.getSharedPointer()); for (int i = 0; i < size; ++i) { bool currentTermValue = true; msat_term currentTerm = model[i]; diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 724b20018..bbd886f9f 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -5,12 +5,14 @@ #include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/CuddDdManager.h" #include "src/utility/vector.h" +#include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/NotImplementedException.h" namespace storm { namespace dd { - Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { + Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariables(containedMetaVariables) { // Intentionally left empty. } @@ -23,9 +25,9 @@ namespace storm { } Dd Dd::ite(Dd const& thenDd, Dd const& elseDd) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(thenDd.getContainedMetaVariableNames().begin(), thenDd.getContainedMetaVariableNames().end()); - metaVariableNames.insert(elseDd.getContainedMetaVariableNames().begin(), elseDd.getContainedMetaVariableNames().end()); + std::set metaVariableNames(this->getContainedMetaVariables()); + metaVariableNames.insert(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end()); + metaVariableNames.insert(elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end()); return Dd(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames); } @@ -40,7 +42,7 @@ namespace storm { this->cuddAdd += other.getCuddAdd(); // Join the variable sets of the two participating DDs. - this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); return *this; } @@ -55,7 +57,7 @@ namespace storm { this->cuddAdd *= other.getCuddAdd(); // Join the variable sets of the two participating DDs. - this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); return *this; } @@ -74,7 +76,7 @@ namespace storm { this->cuddAdd -= other.getCuddAdd(); // Join the variable sets of the two participating DDs. - this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); return *this; } @@ -89,7 +91,7 @@ namespace storm { this->cuddAdd = this->cuddAdd.Divide(other.getCuddAdd()); // Join the variable sets of the two participating DDs. - this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); return *this; } @@ -101,17 +103,17 @@ namespace storm { } Dd Dd::operator&&(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); // Rewrite a and b to not((not a) or (not b)). - return Dd(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariableNames); + return Dd(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariables); } Dd Dd::operator||(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariables); } Dd& Dd::complement() { @@ -120,138 +122,128 @@ namespace storm { } Dd Dd::equals(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariables); } Dd Dd::notEquals(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariables); } Dd Dd::less(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariables); } Dd Dd::lessOrEqual(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariables); } Dd Dd::greater(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariables); } Dd Dd::greaterOrEqual(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariables); } Dd Dd::minimum(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariables); } Dd Dd::maximum(Dd const& other) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariableNames); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariables); } - Dd Dd::existsAbstract(std::set const& metaVariableNames) const { + Dd Dd::existsAbstract(std::set const& metaVariables) const { Dd cubeDd(this->getDdManager()->getOne()); - std::set newMetaVariables = this->getContainedMetaVariableNames(); - for (auto const& metaVariableName : metaVariableNames) { + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - if (!this->containsMetaVariable(metaVariableName)) { - throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; - } - newMetaVariables.erase(metaVariableName); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + newMetaVariables.erase(metaVariable); - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); - cubeDd *= metaVariable.getCube(); + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd *= ddMetaVariable.getCube(); } return Dd(this->getDdManager(), this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()), newMetaVariables); } - Dd Dd::universalAbstract(std::set const& metaVariableNames) const { + Dd Dd::universalAbstract(std::set const& metaVariables) const { Dd cubeDd(this->getDdManager()->getOne()); - std::set newMetaVariables = this->getContainedMetaVariableNames(); - for (auto const& metaVariableName : metaVariableNames) { + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - if (!this->containsMetaVariable(metaVariableName)) { - throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; - } - newMetaVariables.erase(metaVariableName); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + newMetaVariables.erase(metaVariable); - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); - cubeDd *= metaVariable.getCube(); + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd *= ddMetaVariable.getCube(); } return Dd(this->getDdManager(), this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()), newMetaVariables); } - Dd Dd::sumAbstract(std::set const& metaVariableNames) const { + Dd Dd::sumAbstract(std::set const& metaVariables) const { Dd cubeDd(this->getDdManager()->getOne()); - std::set newMetaVariables = this->getContainedMetaVariableNames(); - for (auto const& metaVariableName : metaVariableNames) { + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - if (!this->containsMetaVariable(metaVariableName)) { - throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; - } - newMetaVariables.erase(metaVariableName); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + newMetaVariables.erase(metaVariable); - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); - cubeDd *= metaVariable.getCube(); + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd *= ddMetaVariable.getCube(); } return Dd(this->getDdManager(), this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()), newMetaVariables); } - Dd Dd::minAbstract(std::set const& metaVariableNames) const { + Dd Dd::minAbstract(std::set const& metaVariables) const { Dd cubeDd(this->getDdManager()->getOne()); - std::set newMetaVariables = this->getContainedMetaVariableNames(); - for (auto const& metaVariableName : metaVariableNames) { + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - if (!this->containsMetaVariable(metaVariableName)) { - throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; - } - newMetaVariables.erase(metaVariableName); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + newMetaVariables.erase(metaVariable); - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); - cubeDd *= metaVariable.getCube(); + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd *= ddMetaVariable.getCube(); } return Dd(this->getDdManager(), this->cuddAdd.MinAbstract(cubeDd.getCuddAdd()), newMetaVariables); } - Dd Dd::maxAbstract(std::set const& metaVariableNames) const { + Dd Dd::maxAbstract(std::set const& metaVariables) const { Dd cubeDd(this->getDdManager()->getOne()); - std::set newMetaVariables = this->getContainedMetaVariableNames(); - for (auto const& metaVariableName : metaVariableNames) { + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - if (!this->containsMetaVariable(metaVariableName)) { - throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; - } - newMetaVariables.erase(metaVariableName); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + newMetaVariables.erase(metaVariable); - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); - cubeDd *= metaVariable.getCube(); + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd *= ddMetaVariable.getCube(); } return Dd(this->getDdManager(), this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()), newMetaVariables); @@ -265,7 +257,7 @@ namespace storm { } } - void Dd::swapVariables(std::vector> const& metaVariablePairs) { + void Dd::swapVariables(std::vector> const& metaVariablePairs) { std::vector from; std::vector to; for (auto const& metaVariablePair : metaVariablePairs) { @@ -301,58 +293,58 @@ namespace storm { this->cuddAdd = this->cuddAdd.SwapVariables(from, to); } - Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) const { + Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const { std::vector summationDdVariables; // Create the CUDD summation variables. - for (auto const& metaVariableName : summationMetaVariableNames) { - for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariableName).getDdVariables()) { + for (auto const& metaVariable : summationMetaVariables) { + for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { summationDdVariables.push_back(ddVariable.getCuddAdd()); } } std::set unionOfMetaVariableNames; - std::set_union(this->getContainedMetaVariableNames().begin(), this->getContainedMetaVariableNames().end(), otherMatrix.getContainedMetaVariableNames().begin(), otherMatrix.getContainedMetaVariableNames().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin())); + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin())); std::set containedMetaVariableNames; - std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariableNames.begin(), summationMetaVariableNames.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin())); + std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin())); - return Dd(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames); + return Dd(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables); } Dd Dd::greater(double value) const { - return Dd(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value).Add(), this->getContainedMetaVariableNames()); + return Dd(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value).Add(), this->getContainedMetaVariables()); } Dd Dd::greaterOrEqual(double value) const { - return Dd(this->getDdManager(), this->getCuddAdd().BddThreshold(value).Add(), this->getContainedMetaVariableNames()); + return Dd(this->getDdManager(), this->getCuddAdd().BddThreshold(value).Add(), this->getContainedMetaVariables()); } Dd Dd::notZero() const { - return Dd(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariableNames()); + return Dd(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariables()); } Dd Dd::constrain(Dd const& constraint) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(constraint.getContainedMetaVariableNames().begin(), constraint.getContainedMetaVariableNames().end()); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariableNames); + return Dd(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariables); } Dd Dd::restrict(Dd const& constraint) const { - std::set metaVariableNames(this->getContainedMetaVariableNames()); - metaVariableNames.insert(constraint.getContainedMetaVariableNames().begin(), constraint.getContainedMetaVariableNames().end()); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariableNames); + return Dd(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariables); } Dd Dd::getSupport() const { - return Dd(this->getDdManager(), this->getCuddAdd().Support().Add(), this->getContainedMetaVariableNames()); + return Dd(this->getDdManager(), this->getCuddAdd().Support().Add(), this->getContainedMetaVariables()); } uint_fast64_t Dd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; - for (auto const& metaVariableName : this->containedMetaVariableNames) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariableName).getNumberOfDdVariables(); + for (auto const& metaVariable : this->getContainedMetaVariables()) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); } return static_cast(this->cuddAdd.CountMinterm(static_cast(numberOfDdVariables))); } @@ -375,22 +367,22 @@ namespace storm { return static_cast(Cudd_V(constantMaxAdd.getNode())); } - void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { - std::map metaVariableNameToValueMap; - metaVariableNameToValueMap.emplace(metaVariableName, variableValue); - this->setValue(metaVariableNameToValueMap, targetValue); + void Dd::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue) { + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(metaVariable, variableValue); + this->setValue(metaVariableToValueMap, targetValue); } - void Dd::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) { - std::map metaVariableNameToValueMap; - metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1); - metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2); - this->setValue(metaVariableNameToValueMap, targetValue); + void Dd::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue) { + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(metaVariable1, variableValue1); + metaVariableToValueMap.emplace(metaVariable2, variableValue2); + this->setValue(metaVariableToValueMap, targetValue); } - void Dd::setValue(std::map const& metaVariableNameToValueMap, double targetValue) { + void Dd::setValue(std::map const& metaVariableToValueMap, double targetValue) { Dd valueEncoding(this->getDdManager()->getOne()); - for (auto const& nameValuePair : metaVariableNameToValueMap) { + for (auto const& nameValuePair : metaVariableToValueMap) { valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); // Also record that the DD now contains the meta variable. this->addContainedMetaVariable(nameValuePair.first); @@ -399,10 +391,10 @@ namespace storm { this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); } - double Dd::getValue(std::map const& metaVariableNameToValueMap) const { - std::set remainingMetaVariables(this->getContainedMetaVariableNames()); + double Dd::getValue(std::map const& metaVariableToValueMap) const { + std::set remainingMetaVariables(this->getContainedMetaVariables()); Dd valueEncoding(this->getDdManager()->getOne()); - for (auto const& nameValuePair : metaVariableNameToValueMap) { + for (auto const& nameValuePair : metaVariableToValueMap) { valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); if (this->containsMetaVariable(nameValuePair.first)) { remainingMetaVariables.erase(nameValuePair.first); @@ -414,7 +406,7 @@ namespace storm { } Dd value = *this * valueEncoding; - value = value.sumAbstract(this->getContainedMetaVariableNames()); + value = value.sumAbstract(this->getContainedMetaVariables()); return static_cast(Cudd_V(value.getCuddAdd().getNode())); } @@ -448,14 +440,14 @@ namespace storm { } storm::storage::SparseMatrix Dd::toMatrix() const { - std::set rowVariables; - std::set columnVariables; + std::set rowVariables; + std::set columnVariables; - for (auto const& variableName : this->getContainedMetaVariableNames()) { - if (variableName.size() > 0 && variableName.back() == '\'') { - columnVariables.insert(variableName); + for (auto const& variable : this->getContainedMetaVariables()) { + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnVariables.insert(variable); } else { - rowVariables.insert(variableName); + rowVariables.insert(variable); } } @@ -463,32 +455,32 @@ namespace storm { } storm::storage::SparseMatrix Dd::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::set rowMetaVariables; - std::set columnMetaVariables; + std::set rowMetaVariables; + std::set columnMetaVariables; - for (auto const& variableName : this->getContainedMetaVariableNames()) { - if (variableName.size() > 0 && variableName.back() == '\'') { - columnMetaVariables.insert(variableName); + for (auto const& variable : this->getContainedMetaVariables()) { + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnMetaVariables.insert(variable); } else { - rowMetaVariables.insert(variableName); + rowMetaVariables.insert(variable); } } return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); } - storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; - for (auto const& variableName : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddRowVariableIndices.push_back(ddVariable.getIndex()); } } - for (auto const& variableName : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& variable : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddColumnVariableIndices.push_back(ddVariable.getIndex()); } @@ -536,28 +528,28 @@ namespace storm { return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices)); } - storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; - std::set rowAndColumnMetaVariables; + std::set rowAndColumnMetaVariables; - for (auto const& variableName : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddRowVariableIndices.push_back(ddVariable.getIndex()); } - rowAndColumnMetaVariables.insert(variableName); + rowAndColumnMetaVariables.insert(variable); } - for (auto const& variableName : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& variable : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddColumnVariableIndices.push_back(ddVariable.getIndex()); } - rowAndColumnMetaVariables.insert(variableName); + rowAndColumnMetaVariables.insert(variable); } - for (auto const& variableName : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& variable : groupMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddGroupVariableIndices.push_back(ddVariable.getIndex()); } @@ -690,7 +682,7 @@ namespace storm { } } - void Dd::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const { + void Dd::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const { // For the empty DD, we do not need to create a group. if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { return; @@ -731,7 +723,7 @@ namespace storm { std::vector Dd::getSortedVariableIndices() const { std::vector ddVariableIndices; - for (auto const& metaVariableName : this->getContainedMetaVariableNames()) { + for (auto const& metaVariableName : this->getContainedMetaVariables()) { auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddVariableIndices.push_back(ddVariable.getIndex()); @@ -743,28 +735,27 @@ namespace storm { return ddVariableIndices; } - bool Dd::containsMetaVariable(std::string const& metaVariableName) const { - auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); - return metaVariable != containedMetaVariableNames.end(); + bool Dd::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { + return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); } - bool Dd::containsMetaVariables(std::set metaVariableNames) const { - for (auto const& metaVariableName : metaVariableNames) { - auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); + bool Dd::containsMetaVariables(std::set const& metaVariables) const { + for (auto const& metaVariable : metaVariables) { + auto const& ddMetaVariable = containedMetaVariables.find(metaVariable); - if (metaVariable == containedMetaVariableNames.end()) { + if (ddMetaVariable == containedMetaVariables.end()) { return false; } } return true; } - std::set const& Dd::getContainedMetaVariableNames() const { - return this->containedMetaVariableNames; + std::set const& Dd::getContainedMetaVariables() const { + return this->containedMetaVariables; } - std::set& Dd::getContainedMetaVariableNames() { - return this->containedMetaVariableNames; + std::set& Dd::getContainedMetaVariables() { + return this->containedMetaVariables; } void Dd::exportToDot(std::string const& filename) const { @@ -809,12 +800,12 @@ namespace storm { return this->cuddAdd; } - void Dd::addContainedMetaVariable(std::string const& metaVariableName) { - this->getContainedMetaVariableNames().insert(metaVariableName); + void Dd::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) { + this->getContainedMetaVariables().insert(metaVariable); } - void Dd::removeContainedMetaVariable(std::string const& metaVariableName) { - this->getContainedMetaVariableNames().erase(metaVariableName); + void Dd::removeContainedMetaVariable(storm::expressions::Variable const& metaVariable) { + this->getContainedMetaVariables().erase(metaVariable); } std::shared_ptr> Dd::getDdManager() const { @@ -825,7 +816,7 @@ namespace storm { int* cube; double value; DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); - return DdForwardIterator(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariableNames(), enumerateDontCareMetaVariables); + return DdForwardIterator(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables); } DdForwardIterator Dd::end(bool enumerateDontCareMetaVariables) const { @@ -833,47 +824,49 @@ namespace storm { } storm::expressions::Expression Dd::toExpression() const { - return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariableNames()); + return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariables()); } storm::expressions::Expression Dd::getMintermExpression() const { // Note that we first transform the ADD into a BDD to convert all non-zero terminals to ones and therefore // make the DD more compact. - Dd tmp(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariableNames()); - return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->getCuddAdd().BddPattern().getNode(), this->getDdManager()->getDdVariableNames()); + Dd tmp(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariables()); + return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->getCuddAdd().BddPattern().getNode(), this->getDdManager()->getDdVariables()); } - storm::expressions::Expression Dd::toExpressionRecur(DdNode const* dd, std::vector const& variableNames) { + storm::expressions::Expression Dd::toExpressionRecur(DdNode const* dd, std::vector const& variables) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This feature is currently unavailable."); // If the DD is a terminal node, we can simply return a constant expression. - if (Cudd_IsConstant(dd)) { - return storm::expressions::Expression::createDoubleLiteral(static_cast(Cudd_V(dd))); - } else { - return storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(toExpressionRecur(Cudd_T(dd), variableNames), toExpressionRecur(Cudd_E(dd), variableNames)); - } +// if (Cudd_IsConstant(dd)) { +// return storm::expressions::Expression::createDoubleLiteral(static_cast(Cudd_V(dd))); +// } else { +// return storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(toExpressionRecur(Cudd_T(dd), variableNames), toExpressionRecur(Cudd_E(dd), variableNames)); +// } } - storm::expressions::Expression Dd::getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variableNames) { + storm::expressions::Expression Dd::getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variables) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This feature is currently unavailable."); // If the DD is a terminal node, we can simply return a constant expression. - if (Cudd_IsConstant(dd)) { - if (Cudd_IsComplement(dd)) { - return storm::expressions::Expression::createBooleanLiteral(false); - } else { - return storm::expressions::Expression::createBooleanLiteral((dd == Cudd_ReadOne(manager)) ? true : false); - } - } else { - // Get regular versions of the pointers. - DdNode* regularDd = Cudd_Regular(dd); - DdNode* thenDd = Cudd_T(regularDd); - DdNode* elseDd = Cudd_E(regularDd); - - // Compute expression recursively. - storm::expressions::Expression result = storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(getMintermExpressionRecur(manager, thenDd, variableNames), getMintermExpressionRecur(manager, elseDd, variableNames)); - if (Cudd_IsComplement(dd)) { - result = !result; - } - - return result; - } +// if (Cudd_IsConstant(dd)) { +// if (Cudd_IsComplement(dd)) { +// return storm::expressions::Expression::createBooleanLiteral(false); +// } else { +// return storm::expressions::Expression::createBooleanLiteral((dd == Cudd_ReadOne(manager)) ? true : false); +// } +// } else { +// // Get regular versions of the pointers. +// DdNode* regularDd = Cudd_Regular(dd); +// DdNode* thenDd = Cudd_T(regularDd); +// DdNode* elseDd = Cudd_E(regularDd); +// +// // Compute expression recursively. +// storm::expressions::Expression result = storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(getMintermExpressionRecur(manager, thenDd, variableNames), getMintermExpressionRecur(manager, elseDd, variableNames)); +// if (Cudd_IsComplement(dd)) { +// result = !result; +// } +// +// return result; +// } } std::ostream & operator<<(std::ostream& out, const Dd& dd) { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index adcb2e490..2a56b96a5 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -10,6 +10,7 @@ #include "src/storage/dd/CuddDdForwardIterator.h" #include "src/storage/SparseMatrix.h" #include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/Variable.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. @@ -233,37 +234,37 @@ namespace storm { /*! * Existentially abstracts from the given meta variables. * - * @param metaVariableNames The names of all meta variables from which to abstract. + * @param metaVariables The meta variables from which to abstract. */ - Dd existsAbstract(std::set const& metaVariableNames) const; + Dd existsAbstract(std::set const& metaVariables) const; /*! * Universally abstracts from the given meta variables. * - * @param metaVariableNames The names of all meta variables from which to abstract. + * @param metaVariables The meta variables from which to abstract. */ - Dd universalAbstract(std::set const& metaVariableNames) const; + Dd universalAbstract(std::set const& metaVariables) const; /*! * Sum-abstracts from the given meta variables. * - * @param metaVariableNames The names of all meta variables from which to abstract. + * @param metaVariables The meta variables from which to abstract. */ - Dd sumAbstract(std::set const& metaVariableNames) const; + Dd sumAbstract(std::set const& metaVariables) const; /*! * Min-abstracts from the given meta variables. * - * @param metaVariableNames The names of all meta variables from which to abstract. + * @param metaVariables The meta variables from which to abstract. */ - Dd minAbstract(std::set const& metaVariableNames) const; + Dd minAbstract(std::set const& metaVariables) const; /*! * Max-abstracts from the given meta variables. * - * @param metaVariableNames The names of all meta variables from which to abstract. + * @param metaVariables The meta variables from which to abstract. */ - Dd maxAbstract(std::set const& metaVariableNames) const; + Dd maxAbstract(std::set const& metaVariables) const; /*! * Checks whether the current and the given DD represent the same function modulo some given precision. @@ -282,18 +283,18 @@ namespace storm { * * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. */ - void swapVariables(std::vector> const& metaVariablePairs); + void swapVariables(std::vector> const& metaVariablePairs); /*! * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta * variables. * * @param otherMatrix The matrix with which to multiply. - * @param summationMetaVariableNames The names of the meta variables over which to sum during the matrix- + * @param summationMetaVariables The names of the meta variables over which to sum during the matrix- * matrix multiplication. * @return A DD representing the result of the matrix-matrix multiplication. */ - Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) const; + Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const; /*! * Computes a DD that represents the function in which all assignments with a function value strictly larger @@ -387,47 +388,47 @@ namespace storm { * Sets the function values of all encodings that have the given value of the meta variable to the given * target value. * - * @param metaVariableName The name of the meta variable that has to be equal to the given value. + * @param metaVariable The meta variable that has to be equal to the given value. * @param variableValue The value that the meta variable is supposed to have. This must be within the range * of the meta variable. * @param targetValue The new function value of the modified encodings. */ - void setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue); + void setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue); /*! * Sets the function values of all encodings that have the given values of the two meta variables to the * given target value. * - * @param metaVariableName1 The name of the first meta variable that has to be equal to the first given + * @param metaVariable1 The first meta variable that has to be equal to the first given * value. * @param variableValue1 The value that the first meta variable is supposed to have. This must be within the * range of the meta variable. - * @param metaVariableName2 The name of the first meta variable that has to be equal to the second given + * @param metaVariable2 The second meta variable that has to be equal to the second given * value. * @param variableValue2 The value that the second meta variable is supposed to have. This must be within * the range of the meta variable. * @param targetValue The new function value of the modified encodings. */ - void setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue); + void setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue); /*! * Sets the function values of all encodings that have the given values of the given meta variables to the * given target value. * - * @param metaVariableNameToValueMap A mapping of meta variable names to the values they are supposed to - * have. All values must be within the range of the respective meta variable. + * @param metaVariableToValueMap A mapping of meta variables to the values they are supposed to have. All + * values must be within the range of the respective meta variable. * @param targetValue The new function value of the modified encodings. */ - void setValue(std::map const& metaVariableNameToValueMap = std::map(), double targetValue = 0); + void setValue(std::map const& metaVariableToValueMap = std::map(), double targetValue = 0); /*! * Retrieves the value of the function when all meta variables are assigned the values of the given mapping. * Note that the mapping must specify values for all meta variables contained in the DD. * - * @param metaVariableNameToValueMap A mapping of meta variable names to their values. + * @param metaVariableToValueMap A mapping of meta variables to their values. * @return The value of the function evaluated with the given input. */ - double getValue(std::map const& metaVariableNameToValueMap = std::map()) const; + double getValue(std::map const& metaVariableToValueMap = std::map()) const; /*! * Retrieves whether this DD represents the constant one function. @@ -504,7 +505,7 @@ namespace storm { * @param columnOdd The ODD used for determining the correct column. * @return The matrix that is represented by this DD. */ - storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; /*! * Converts the DD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to @@ -518,37 +519,37 @@ namespace storm { * @param columnOdd The ODD used for determining the correct column. * @return The matrix that is represented by this DD. */ - storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; /*! * Retrieves whether the given meta variable is contained in the DD. * - * @param metaVariableName The name of the meta variable for which to query membership. + * @param metaVariable The meta variable for which to query membership. * @return True iff the meta variable is contained in the DD. */ - bool containsMetaVariable(std::string const& metaVariableName) const; + bool containsMetaVariable(storm::expressions::Variable const& metaVariable) const; /*! * Retrieves whether the given meta variables are all contained in the DD. * - * @param metaVariableNames The names of the meta variable for which to query membership. + * @param metaVariables The meta variables for which to query membership. * @return True iff all meta variables are contained in the DD. */ - bool containsMetaVariables(std::set metaVariableNames) const; + bool containsMetaVariables(std::set const& metaVariables) const; /*! - * Retrieves the set of all names of meta variables contained in the DD. + * Retrieves the set of all meta variables contained in the DD. * - * @return The set of names of all meta variables contained in the DD. + * @return The set of all meta variables contained in the DD. */ - std::set const& getContainedMetaVariableNames() const; + std::set const& getContainedMetaVariables() const; /*! - * Retrieves the set of all names of meta variables contained in the DD. + * Retrieves the set of all meta variables contained in the DD. * - * @return The set of names of all meta variables contained in the DD. + * @return The set of all meta variables contained in the DD. */ - std::set& getContainedMetaVariableNames(); + std::set& getContainedMetaVariables(); /*! * Exports the DD to the given file in the dot format. @@ -619,46 +620,46 @@ namespace storm { ADD const& getCuddAdd() const; /*! - * Adds the given meta variable name to the set of meta variables that are contained in this DD. + * Adds the given meta variable to the set of meta variables that are contained in this DD. * - * @param metaVariableName The name of the meta variable to add. + * @param metaVariable The name of the meta variable to add. */ - void addContainedMetaVariable(std::string const& metaVariableName); + void addContainedMetaVariable(storm::expressions::Variable const& metaVariable); /*! - * Removes the given meta variable name to the set of meta variables that are contained in this DD. + * Removes the given meta variable to the set of meta variables that are contained in this DD. * - * @param metaVariableName The name of the meta variable to remove. + * @param metaVariable The name of the meta variable to remove. */ - void removeContainedMetaVariable(std::string const& metaVariableName); + void removeContainedMetaVariable(storm::expressions::Variable const& metaVariable); /*! * Performs the recursive step of toExpression on the given DD. * * @param dd The dd to translate into an expression. - * @param variableNames The names of the variables to use in the expression. + * @param variables The variables to use in the expression. * @return The resulting expression. */ - static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector const& variableNames); + static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector const& variables); /*! * Performs the recursive step of getMintermExpression on the given DD. * * @param manager The manager of the DD. * @param dd The dd whose minterms to translate into an expression. - * @param variableNames The names of the variables to use in the expression. + * @param variables The variables to use in the expression. * @return The resulting expression. */ - static storm::expressions::Expression getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variableNames); + static storm::expressions::Expression getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variables); /*! * Creates a DD that encapsulates the given CUDD ADD. * * @param ddManager The manager responsible for this DD. * @param cuddAdd The CUDD ADD to store. - * @param containedMetaVariableNames The names of the meta variables that appear in the DD. + * @param containedMetaVariables The meta variables that appear in the DD. */ - Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames = std::set()); + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariables = std::set()); /*! * Helper function to convert the DD into a (sparse) matrix. @@ -697,7 +698,7 @@ namespace storm { * @param maxLevel The number of levels that need to be considered. * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. */ - void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; + void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; /*! * Performs a recursive step to add the given DD-based vector to the given explicit vector. @@ -727,8 +728,8 @@ namespace storm { // The ADD created by CUDD. ADD cuddAdd; - // The names of all meta variables that appear in this DD. - std::set containedMetaVariableNames; + // The meta variables that appear in this DD. + std::set containedMetaVariables; }; } } diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp index dd1f58189..c1d0f7392 100644 --- a/src/storage/dd/CuddDdForwardIterator.cpp +++ b/src/storage/dd/CuddDdForwardIterator.cpp @@ -5,23 +5,14 @@ namespace storm { namespace dd { - DdForwardIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + DdForwardIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { // Intentionally left empty. } - DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { // If the given generator is not yet at its end, we need to create the current valuation from the cube from // scratch. if (!this->isAtEnd) { - // Start by registering all meta variables in the valuation with the appropriate type. - for (auto const& metaVariableName : *this->metaVariables) { - auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); - switch (metaVariable.getType()) { - case DdMetaVariable::MetaVariableType::Bool: currentValuation.addBooleanIdentifier(metaVariableName); break; - case DdMetaVariable::MetaVariableType::Int: currentValuation.addIntegerIdentifier(metaVariableName); break; - } - } - // And then get ready for treating the first cube. this->treatNewCube(); } @@ -89,18 +80,19 @@ namespace storm { ++this->cubeCounter; for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) { - auto const& metaVariable = this->ddManager->getMetaVariable(std::get<1>(this->relevantDontCareDdVariables[index])); - if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<1>(this->relevantDontCareDdVariables[index])); + if (ddMetaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { if ((this->cubeCounter & (1ull << index)) != 0) { - currentValuation.setBooleanValue(metaVariable.getName(), true); + currentValuation.setBooleanValue(std::get<1>(this->relevantDontCareDdVariables[index]), true); } else { - currentValuation.setBooleanValue(metaVariable.getName(), false); + currentValuation.setBooleanValue(std::get<1>(this->relevantDontCareDdVariables[index]), false); } } else { + storm::expressions::Variable const& metaVariable = std::get<1>(this->relevantDontCareDdVariables[index]); if ((this->cubeCounter & (1ull << index)) != 0) { - currentValuation.setIntegerValue(metaVariable.getName(), ((currentValuation.getIntegerValue(metaVariable.getName()) - metaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + metaVariable.getLow()); + currentValuation.setIntegerValue(metaVariable, ((currentValuation.getIntegerValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); } else { - currentValuation.setIntegerValue(metaVariable.getName(), ((currentValuation.getIntegerValue(metaVariable.getName()) - metaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + metaVariable.getLow()); + currentValuation.setIntegerValue(metaVariable, ((currentValuation.getIntegerValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); } } } @@ -112,48 +104,37 @@ namespace storm { // Now loop through the bits of all meta variables and check whether they need to be set, not set or are // don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete // valuations later. - for (auto const& metaVariableName : *this->metaVariables) { + for (auto const& metaVariable : *this->metaVariables) { bool metaVariableAppearsInCube = false; - std::vector> localRelenvantDontCareDdVariables; - auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); - if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { - if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) { + std::vector> localRelenvantDontCareDdVariables; + auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable); + if (ddMetaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + if (this->cube[ddMetaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) { metaVariableAppearsInCube = true; - if (!currentValuation.containsBooleanIdentifier(metaVariableName)) { - currentValuation.addBooleanIdentifier(metaVariableName, false); - } else { - currentValuation.setBooleanValue(metaVariableName, false); - } - } else if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) { + currentValuation.setBooleanValue(metaVariable, false); + } else if (this->cube[ddMetaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) { metaVariableAppearsInCube = true; - if (!currentValuation.containsBooleanIdentifier(metaVariableName)) { - currentValuation.addBooleanIdentifier(metaVariableName, true); - } else { - currentValuation.setBooleanValue(metaVariableName, true); - } + currentValuation.setBooleanValue(metaVariable, true); } else { - localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0)); + localRelenvantDontCareDdVariables.push_back(std::make_tuple(ddMetaVariable.getDdVariables()[0].getCuddAdd(), metaVariable, 0)); } } else { int_fast64_t intValue = 0; - for (uint_fast64_t bitIndex = 0; bitIndex < metaVariable.getNumberOfDdVariables(); ++bitIndex) { - if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) { + for (uint_fast64_t bitIndex = 0; bitIndex < ddMetaVariable.getNumberOfDdVariables(); ++bitIndex) { + if (cube[ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) { // Leave bit unset. metaVariableAppearsInCube = true; - } else if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) { - intValue |= 1ull << (metaVariable.getNumberOfDdVariables() - bitIndex - 1); + } else if (cube[ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) { + intValue |= 1ull << (ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1); metaVariableAppearsInCube = true; } else { // Temporarily leave bit unset so we can iterate trough the other option later. // Add the bit to the relevant don't care bits. - localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1)); + localRelenvantDontCareDdVariables.push_back(std::make_tuple(ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1)); } } if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { - if (!currentValuation.containsIntegerIdentifier(metaVariableName)) { - currentValuation.addIntegerIdentifier(metaVariableName); - } - currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow()); + currentValuation.setIntegerValue(metaVariable, intValue + ddMetaVariable.getLow()); } } @@ -162,12 +143,6 @@ namespace storm { if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end()); } - - // If the meta variable does not appear in the cube and we're not supposed to enumerate such meta variables - // we remove the meta variable from the valuation. - if (!this->enumerateDontCareMetaVariables && !metaVariableAppearsInCube) { - currentValuation.removeIdentifier(metaVariableName); - } } // Finally, reset the cube counter. diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h index 8b08af929..aad7db67c 100644 --- a/src/storage/dd/CuddDdForwardIterator.h +++ b/src/storage/dd/CuddDdForwardIterator.h @@ -85,7 +85,7 @@ namespace storm { * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even * if a meta variable does not at all influence the the function value. */ - DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true); + DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true); /*! * Recreates the internal information when a new cube needs to be treated. @@ -114,7 +114,7 @@ namespace storm { bool isAtEnd; // The set of meta variables appearing in the DD. - std::set const* metaVariables; + std::set const* metaVariables; // A flag that indicates whether the iterator is supposed to enumerate meta variable valuations even if // they don't influence the function value. @@ -124,8 +124,8 @@ namespace storm { // This is needed, because cubes may represent many assignments (if they have don't care variables). uint_fast64_t cubeCounter; - // A vector of tuples of the form . - std::vector> relevantDontCareDdVariables; + // A vector of tuples of the form . + std::vector> relevantDontCareDdVariables; // The current valuation of meta variables. storm::expressions::SimpleValuation currentValuation; diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 21a1d3d7f..217903852 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -9,7 +9,7 @@ namespace storm { namespace dd { - DdManager::DdManager() : metaVariableMap(), cuddManager(), reorderingTechnique(CUDD_REORDER_NONE) { + DdManager::DdManager() : metaVariableMap(), cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()) { this->cuddManager.SetMaxMemory(static_cast(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul)); this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision()); @@ -49,10 +49,10 @@ namespace storm { return Dd(this->shared_from_this(), cuddManager.constant(value)); } - Dd DdManager::getEncoding(std::string const& metaVariableName, int_fast64_t value) { - DdMetaVariable const& metaVariable = this->getMetaVariable(metaVariableName); + Dd DdManager::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) { + DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << metaVariableName << "'."); + STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'."); // Now compute the encoding relative to the low value of the meta variable. value -= metaVariable.getLow(); @@ -77,28 +77,28 @@ namespace storm { return result; } - Dd DdManager::getRange(std::string const& metaVariableName) { - storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(metaVariableName); + Dd DdManager::getRange(storm::expressions::Variable const& variable) { + storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); Dd result = this->getZero(); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result.setValue(metaVariableName, value, static_cast(1)); + result.setValue(variable, value, static_cast(1)); } return result; } - Dd DdManager::getIdentity(std::string const& metaVariableName) { - storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(metaVariableName); + Dd DdManager::getIdentity(storm::expressions::Variable const& variable) { + storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); Dd result = this->getZero(); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result.setValue(metaVariableName, value, static_cast(value)); + result.setValue(variable, value, static_cast(value)); } return result; } - void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { + std::pair DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { // Check whether the variable name is legal. STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); @@ -110,11 +110,14 @@ namespace storm { std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); + storm::expressions::Variable unprimed = manager->declareVariable(name, manager->getBoundedIntegerType(numberOfBits)); + storm::expressions::Variable primed = manager->declareVariable(name + "'", manager->getBoundedIntegerType(numberOfBits)); + std::vector> variables; std::vector> variablesPrime; for (std::size_t i = 0; i < numberOfBits; ++i) { - variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name})); - variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name + "'"})); + variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {unprimed})); + variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {primed})); } // Now group the non-primed and primed variable. @@ -122,42 +125,49 @@ namespace storm { this->getCuddManager().MakeTreeNode(variables[i].getCuddAdd().NodeReadIndex(), 2, MTR_FIXED); } - metaVariableMap.emplace(name, DdMetaVariable(name, low, high, variables, this->shared_from_this())); - metaVariableMap.emplace(name + "'", DdMetaVariable(name + "'", low, high, variablesPrime, this->shared_from_this())); + metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables, this->shared_from_this())); + metaVariableMap.emplace(primed, DdMetaVariable(name + "'", low, high, variablesPrime, this->shared_from_this())); + + return std::make_pair(unprimed, primed); } - void DdManager::addMetaVariable(std::string const& name) { + std::pair DdManager::addMetaVariable(std::string const& name) { // Check whether the variable name is legal. STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); // Check whether a meta variable already exists. STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists."); + storm::expressions::Variable unprimed = manager->declareVariable(name, manager->getBooleanType()); + storm::expressions::Variable primed = manager->declareVariable(name + "'", manager->getBooleanType()); + std::vector> variables; std::vector> variablesPrime; - variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name})); - variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name + "'"})); + variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {unprimed})); + variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {primed})); // Now group the non-primed and primed variable. this->getCuddManager().MakeTreeNode(variables.front().getCuddAdd().NodeReadIndex(), 2, MTR_FIXED); - metaVariableMap.emplace(name, DdMetaVariable(name, variables, this->shared_from_this())); - metaVariableMap.emplace(name + "'", DdMetaVariable(name + "'", variablesPrime, this->shared_from_this())); + metaVariableMap.emplace(unprimed, DdMetaVariable(name, variables, this->shared_from_this())); + metaVariableMap.emplace(primed, DdMetaVariable(name + "'", variablesPrime, this->shared_from_this())); + + return std::make_pair(unprimed, primed); } - DdMetaVariable const& DdManager::getMetaVariable(std::string const& metaVariableName) const { - auto const& nameVariablePair = metaVariableMap.find(metaVariableName); + DdMetaVariable const& DdManager::getMetaVariable(storm::expressions::Variable const& variable) const { + auto const& variablePair = metaVariableMap.find(variable); // Check whether the meta variable exists. - STORM_LOG_THROW(nameVariablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << metaVariableName << "'."); + STORM_LOG_THROW(variablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << variable.getName() << "'."); - return nameVariablePair->second; + return variablePair->second; } std::set DdManager::getAllMetaVariableNames() const { std::set result; - for (auto const& nameValuePair : metaVariableMap) { - result.insert(nameValuePair.first); + for (auto const& variablePair : metaVariableMap) { + result.insert(variablePair.first.getName()); } return result; } @@ -167,7 +177,7 @@ namespace storm { } bool DdManager::hasMetaVariable(std::string const& metaVariableName) const { - return this->metaVariableMap.find(metaVariableName) != this->metaVariableMap.end(); + return manager->hasVariable(metaVariableName); } Cudd& DdManager::getCuddManager() { @@ -178,6 +188,14 @@ namespace storm { return this->cuddManager; } + storm::expressions::ExpressionManager const& DdManager::getExpressionManager() const { + return *manager; + } + + storm::expressions::ExpressionManager& DdManager::getExpressionManager() { + return *manager; + } + std::vector DdManager::getDdVariableNames() const { // First, we initialize a list DD variables and their names. std::vector> variableNamePairs; diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 682fb4c8b..8ff263ed2 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -2,9 +2,12 @@ #define STORM_STORAGE_DD_CUDDDDMANAGER_H_ #include +#include #include "src/storage/dd/DdManager.h" #include "src/storage/dd/CuddDdMetaVariable.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/Variable.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. @@ -57,46 +60,46 @@ namespace storm { * Retrieves the DD representing the function that maps all inputs which have the given meta variable equal * to the given value one. * - * @param metaVariableName The meta variable that is supposed to have the given value. + * @param variable The expression variable associated with the meta variable. * @param value The value the meta variable is supposed to have. * @return The DD representing the function that maps all inputs which have the given meta variable equal * to the given value one. */ - Dd getEncoding(std::string const& metaVariableName, int_fast64_t value); + Dd getEncoding(storm::expressions::Variable const& variable, int_fast64_t value); /*! * Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values * of the range of the meta variable to one. * - * @param metaVariableName The name of the meta variable whose range to retrieve. + * @param variable The expression variable associated with the meta variable. * @return The range of the meta variable. */ - Dd getRange(std::string const& metaVariableName); + Dd getRange(storm::expressions::Variable const& variable); /*! * Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal * values of the range of the meta variable to themselves. * - * @param metaVariableName The name of the meta variable whose identity to retrieve. + * @param variable The expression variable associated with the meta variable. * @return The identity of the meta variable. */ - Dd getIdentity(std::string const& metaVariableName); + Dd getIdentity(storm::expressions::Variable const& variable); /*! - * Adds an integer meta variable with the given name and range. + * Adds an integer meta variable with the given range. * - * @param name The (non-empty) name of the meta variable. + * @param variableName The name of the new variable. * @param low The lowest value of the range of the variable. * @param high The highest value of the range of the variable. */ - void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high); + std::pair addMetaVariable(std::string const& variableName, int_fast64_t low, int_fast64_t high); /*! - * Adds a boolean meta variable with the given name. + * Adds a boolean meta variable. * - * @param name The (non-empty) name of the meta variable. + * @param variableName The name of the new variable. */ - void addMetaVariable(std::string const& name); + std::pair addMetaVariable(std::string const& variableName); /*! * Retrieves the names of all meta variables that have been added to the manager. @@ -115,10 +118,10 @@ namespace storm { /*! * Retrieves whether the given meta variable name is already in use. * - * @param metaVariableName The meta variable name whose membership to query. + * @param variableName The name of the variable. * @return True if the given meta variable name is managed by this manager. */ - bool hasMetaVariable(std::string const& metaVariableName) const; + bool hasMetaVariable(std::string const& variableName) const; /*! * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. @@ -142,10 +145,10 @@ namespace storm { /*! * Retrieves the meta variable with the given name if it exists. * - * @param metaVariableName The name of the meta variable to retrieve. - * @return The meta variable with the given name. + * @param variable The expression variable associated with the meta variable. + * @return The corresponding meta variable. */ - DdMetaVariable const& getMetaVariable(std::string const& metaVariableName) const; + DdMetaVariable const& getMetaVariable(storm::expressions::Variable const& variable) const; private: /*! @@ -155,6 +158,13 @@ namespace storm { */ std::vector getDdVariableNames() const; + /*! + * Retrieves a list of expression variables in the order of their index. + * + * @return A list of DD variables. + */ + std::vector getDdVariables() const; + /*! * Retrieves the underlying CUDD manager. * @@ -169,14 +179,31 @@ namespace storm { */ Cudd const& getCuddManager() const; - // A mapping from variable names to the meta variable information. - std::unordered_map> metaVariableMap; + /*! + * Retrieves the underlying expression manager. + * + * @return The underlying expression manager. + */ + storm::expressions::ExpressionManager const& getExpressionManager() const; + + /*! + * Retrieves the underlying expression manager. + * + * @return The underlying expression manager. + */ + storm::expressions::ExpressionManager& getExpressionManager(); + + // A mapping from variables to the meta variable information. + std::unordered_map> metaVariableMap; // The manager responsible for the DDs created/modified with this DdManager. Cudd cuddManager; // The technique that is used for dynamic reordering. Cudd_ReorderingType reorderingTechnique; + + // The manager responsible for the variables. + std::shared_ptr manager; }; } } diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index 3e07bcfae..32c1cf8f6 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -155,6 +155,10 @@ namespace storm { Expression ExpressionManager::getVariableExpression(std::string const& name) const { return Expression(getVariable(name)); } + + bool ExpressionManager::hasVariable(std::string const& name) const { + return nameToIndexMapping.find(name) != nameToIndexMapping.end(); + } Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType) { std::string newName = "__x" + std::to_string(freshVariableCounter++); diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index 9b4acfc8c..bb313ff9c 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -182,6 +182,14 @@ namespace storm { */ Variable getVariable(std::string const& name) const; + /*! + * Retrieves whether a variable with the given name is known to the manager. + * + * @param name The name of the variable whose membership to query. + * @return True iff a variable with the given name is known to the manager. + */ + bool hasVariable(std::string const& name) const; + /*! * Retrieves an expression that represents the variable with the given name. * @@ -314,21 +322,21 @@ namespace storm { */ const_iterator end() const; - private: /*! * Retrieves a shared pointer to the expression manager. * * @return A shared pointer to the expression manager. */ std::shared_ptr getSharedPointer(); - + /*! * Retrieves a shared pointer to the expression manager. * * @return A shared pointer to the expression manager. */ std::shared_ptr getSharedPointer() const; - + + private: /*! * Checks whether the given variable name is valid. * diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp index aa644f588..6a8f855c5 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.cpp +++ b/src/storage/expressions/LinearCoefficientVisitor.cpp @@ -63,6 +63,22 @@ namespace storm { return variableToCoefficientMapping[variable]; } + void LinearCoefficientVisitor::VariableCoefficients::separateVariablesFromConstantPart(VariableCoefficients& rhs) { + for (auto const& rhsVariableCoefficientPair : rhs.variableToCoefficientMapping) { + this->variableToCoefficientMapping[rhsVariableCoefficientPair.first] -= rhsVariableCoefficientPair.second; + } + rhs.variableToCoefficientMapping.clear(); + rhs.constantPart -= this->constantPart; + } + + std::map::const_iterator LinearCoefficientVisitor::VariableCoefficients::begin() const { + return this->variableToCoefficientMapping.begin(); + } + + std::map::const_iterator LinearCoefficientVisitor::VariableCoefficients::end() const { + return this->variableToCoefficientMapping.end(); + } + LinearCoefficientVisitor::VariableCoefficients LinearCoefficientVisitor::getLinearCoefficients(Expression const& expression) { return boost::any_cast(expression.getBaseExpression().accept(*this)); } diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index 38bcd88c7..011f14482 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -30,6 +30,20 @@ namespace storm { void setCoefficient(storm::expressions::Variable const& variable, double coefficient); double getCoefficient(storm::expressions::Variable const& variable); + /*! + * Brings all variables of the right-hand side coefficients to the left-hand side by negating them and + * moves the constant part of the current coefficients to the right-hand side by subtracting it from the + * constant part of the rhs. After performing this operation, the left-hand side has a constant part of + * 0 and all variables and the right-hand side has no variables, but possibly a non-zero constant part. + * + * @param other The variable coefficients of the right-hand side. + */ + void separateVariablesFromConstantPart(VariableCoefficients& rhs); + + // Propagate the iterators to variable-coefficient pairs. + std::map::const_iterator begin() const; + std::map::const_iterator end() const; + private: std::map variableToCoefficientMapping; double constantPart; diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index bf2154620..a79dcef6f 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -7,19 +7,19 @@ namespace storm { namespace expressions { - SimpleValuation::SimpleValuation(ExpressionManager const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) { - if (manager.getNumberOfBooleanVariables() > 0) { - booleanValues = std::unique_ptr>(new std::vector(manager.getNumberOfBooleanVariables())); + SimpleValuation::SimpleValuation(std::shared_ptr const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) { + if (this->getManager().getNumberOfBooleanVariables() > 0) { + booleanValues = std::unique_ptr>(new std::vector(this->getManager().getNumberOfBooleanVariables())); } - if (manager.getNumberOfIntegerVariables() > 0) { - integerValues = std::unique_ptr>(new std::vector(manager.getNumberOfIntegerVariables())); + if (this->getManager().getNumberOfIntegerVariables() > 0) { + integerValues = std::unique_ptr>(new std::vector(this->getManager().getNumberOfIntegerVariables())); } - if (manager.getNumberOfRationalVariables() > 0) { - rationalValues = std::unique_ptr>(new std::vector(manager.getNumberOfRationalVariables())); + if (this->getManager().getNumberOfRationalVariables() > 0) { + rationalValues = std::unique_ptr>(new std::vector(this->getManager().getNumberOfRationalVariables())); } } - SimpleValuation::SimpleValuation(SimpleValuation const& other) : Valuation(other.getManager()) { + SimpleValuation::SimpleValuation(SimpleValuation const& other) : Valuation(other.getManager().getSharedPointer()) { if (other.booleanValues != nullptr) { booleanValues = std::unique_ptr>(new std::vector(*other.booleanValues)); } @@ -30,6 +30,40 @@ namespace storm { rationalValues = std::unique_ptr>(new std::vector(*other.rationalValues)); } } + + SimpleValuation& SimpleValuation::operator=(SimpleValuation const& other) { + if (this != &other) { + this->setManager(other.getManager().getSharedPointer()); + if (other.booleanValues != nullptr) { + booleanValues = std::unique_ptr>(new std::vector(*other.booleanValues)); + } + if (other.integerValues != nullptr) { + integerValues = std::unique_ptr>(new std::vector(*other.integerValues)); + } + if (other.booleanValues != nullptr) { + rationalValues = std::unique_ptr>(new std::vector(*other.rationalValues)); + } + } + return *this; + } + + SimpleValuation::SimpleValuation(SimpleValuation&& other) : Valuation(other.getManager().getSharedPointer()) { + if (this != &other) { + booleanValues = std::move(other.booleanValues); + integerValues = std::move(other.integerValues); + rationalValues = std::move(other.rationalValues); + } + } + + SimpleValuation& SimpleValuation::operator=(SimpleValuation&& other) { + if (this != &other) { + this->setManager(other.getManager().getSharedPointer()); + booleanValues = std::move(other.booleanValues); + integerValues = std::move(other.integerValues); + rationalValues = std::move(other.rationalValues); + } + return *this; + } bool SimpleValuation::operator==(SimpleValuation const& other) const { return this->getManager() == other.getManager() && booleanValues == other.booleanValues && integerValues == other.integerValues && rationalValues == other.rationalValues; diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 53142fd31..2d8fff7a3 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -19,15 +19,16 @@ namespace storm { /*! * Creates a new valuation over the non-auxiliary variables of the given manager. - */ - SimpleValuation(storm::expressions::ExpressionManager const& manager); - - /*! - * Deep-copies the valuation. * - * @param other The valuation to copy + * @param manager The manager responsible for the variables of this valuation. */ + SimpleValuation(std::shared_ptr const& manager); + + // Define deep-copy and move operators. SimpleValuation(SimpleValuation const& other); + SimpleValuation& operator=(SimpleValuation const& other); + SimpleValuation(SimpleValuation&& other); + SimpleValuation& operator=(SimpleValuation&& other); /*! * Checks whether the two valuations are semantically equivalent. diff --git a/src/storage/expressions/Valuation.cpp b/src/storage/expressions/Valuation.cpp index 831e49066..9696e7d8d 100644 --- a/src/storage/expressions/Valuation.cpp +++ b/src/storage/expressions/Valuation.cpp @@ -3,8 +3,17 @@ namespace storm { namespace expressions { + Valuation::Valuation(std::shared_ptr const& manager) : manager(manager) { + // Intentionally left empty. + } + ExpressionManager const& Valuation::getManager() const { - return manager; + return *manager; + } + + void Valuation::setManager(std::shared_ptr const& manager) { + this->manager = manager; } + } } \ No newline at end of file diff --git a/src/storage/expressions/Valuation.h b/src/storage/expressions/Valuation.h index 00ffb4283..1dd08751a 100644 --- a/src/storage/expressions/Valuation.h +++ b/src/storage/expressions/Valuation.h @@ -21,7 +21,7 @@ namespace storm { * * @param manager The manager of the variables. */ - Valuation(ExpressionManager const& manager); + Valuation(std::shared_ptr const& manager); /*! * Retrieves the value of the given boolean variable. @@ -78,9 +78,17 @@ namespace storm { */ ExpressionManager const& getManager() const; + protected: + /*! + * Sets the manager responsible for the variables in this valuation. + * + * @param manager The manager to set. + */ + void setManager(std::shared_ptr const& manager); + private: // The manager responsible for the variables of this valuation. - ExpressionManager const& manager; + std::shared_ptr manager; }; } }