Added singleton utility class for CUDD-based things. Added some first methods to expression classes to generate ADDs, but this should be moved to a separate class implementing the expression visitor pattern.

src/adapters/SymbolicModelAdapter.h

@@ -0,0 +1,115 @@
+/*
+ * SymbolicModelAdapter.h
+ *
+ *  Created on: 25.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_
+#define STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_
+
+#include "src/exceptions/WrongFileFormatException.h"
+
+#include "src/utility/CuddUtility.h"
+#include "src/ir/expressions/ExpressionVisitor.h"
+
+#include "cuddObj.hh"
+#include <iostream>
+
+namespace storm {
+
+namespace adapters {
+
+class SymbolicModelAdapter {
+public:
+
+	SymbolicModelAdapter() : cuddUtility(storm::utility::cuddUtilityInstance()) {
+
+	}
+
+	void toMTBDD(storm::ir::Program const& program) {
+		LOG4CPLUS_INFO(logger, "Creating MTBDD representation for probabilistic program.");
+		createDecisionDiagramVariables(program);
+
+		for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+			storm::ir::Module const& module = program.getModule(i);
+
+			for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
+				storm::ir::Command const& command = module.getCommand(j);
+
+
+			}
+		}
+
+		LOG4CPLUS_INFO(logger, "Done creating MTBDD representation for probabilistic program.");
+	}
+
+private:
+	storm::utility::CuddUtility* cuddUtility;
+
+	std::vector<ADD*> allDecisionDiagramVariables;
+	std::vector<ADD*> allRowDecisionDiagramVariables;
+	std::vector<ADD*> allColumnDecisionDiagramVariables;
+	std::vector<ADD*> booleanRowDecisionDiagramVariables;
+	std::vector<ADD*> integerRowDecisionDiagramVariables;
+	std::vector<ADD*> booleanColumnDecisionDiagramVariables;
+	std::vector<ADD*> integerColumnDecisionDiagramVariables;
+	std::unordered_map<std::string, std::vector<ADD*>> variableToRowDecisionDiagramVariableMap;
+	std::unordered_map<std::string, std::vector<ADD*>> variableToColumnDecisionDiagramVariableMap;
+
+	void createDecisionDiagramVariables(storm::ir::Program const& program) {
+		for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+			storm::ir::Module const& module = program.getModule(i);
+
+			for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
+				storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j);
+
+				ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable();
+				variableToRowDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newRowDecisionDiagramVariable);
+				booleanRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
+				allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
+				allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
+
+				ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable();
+				variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newColumnDecisionDiagramVariable);
+				booleanColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
+				allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
+				allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
+			}
+
+			for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
+				storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j);
+				uint_fast64_t integerRange = integerVariable.getUpperBound()->getValueAsInt(nullptr) - integerVariable.getLowerBound()->getValueAsInt(nullptr);
+				if (integerRange <= 0) {
+					throw storm::exceptions::WrongFileFormatException() << "Range of variable "
+							<< integerVariable.getName() << " is empty or negativ.";
+				}
+				uint_fast64_t numberOfDecisionDiagramVariables = static_cast<uint_fast64_t>(std::ceil(std::log2(integerRange)));
+
+				std::vector<ADD*> allRowDecisionDiagramVariablesForVariable;
+				std::vector<ADD*> allColumnDecisionDiagramVariablesForVariable;
+				for (uint_fast64_t k = 0; k < numberOfDecisionDiagramVariables; ++k) {
+					ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable();
+					allRowDecisionDiagramVariablesForVariable.push_back(newRowDecisionDiagramVariable);
+					integerRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
+					allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
+					allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
+
+					ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable();
+					allColumnDecisionDiagramVariablesForVariable.push_back(newColumnDecisionDiagramVariable);
+					integerColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
+					allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
+					allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
+				}
+				variableToRowDecisionDiagramVariableMap[integerVariable.getName()] = allRowDecisionDiagramVariablesForVariable;
+				variableToColumnDecisionDiagramVariableMap[integerVariable.getName()] = allColumnDecisionDiagramVariablesForVariable;
+			}
+		}
+	}
+};
+
+} // namespace adapters
+
+} // namespace storm
+
+#endif /* STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ */

src/ir/expressions/BaseExpression.h

@@ -11,6 +11,8 @@
 #include "src/exceptions/ExpressionEvaluationException.h"
 #include "src/exceptions/NotImplementedException.h"
 
+#include "src/utility/CuddUtility.h"
+
 #include <string>
 #include <vector>
 
@@ -64,6 +66,8 @@ public:
 					<< this->getTypeName() << " because evaluation implementation is missing.";
 	}
 
+	virtual ADD* toAdd() const = 0;
+
 	virtual std::string toString() const = 0;
 
 	std::string getTypeName() const {

src/ir/expressions/BinaryBooleanFunctionExpression.h

@@ -10,6 +10,8 @@
 
 #include "src/ir/expressions/BaseExpression.h"
 
+#include "src/utility/CuddUtility.h"
+
 #include <memory>
 #include <sstream>
 
@@ -42,6 +44,18 @@ public:
 		}
 	}
 
+	virtual ADD* toAdd() const {
+		ADD* leftAdd = left->toAdd();
+		ADD* rightAdd = right->toAdd();
+
+		switch(functionType) {
+		case AND: return new ADD(leftAdd->Times(*rightAdd)); break;
+		case OR: return new ADD(leftAdd->Plus(*rightAdd)); break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown boolean binary operator: '" << functionType << "'.";
+		}
+	}
+
 	virtual std::string toString() const {
 		std::stringstream result;
 		result << left->toString();

src/ir/expressions/BinaryNumericalFunctionExpression.h

@@ -10,6 +10,8 @@
 
 #include "src/ir/expressions/BaseExpression.h"
 
+#include "src/utility/CuddUtility.h"
+
 namespace storm {
 
 namespace ir {
@@ -62,6 +64,20 @@ public:
 		}
 	}
 
+	virtual ADD* toAdd() const {
+		ADD* leftAdd = left->toAdd();
+		ADD* rightAdd = right->toAdd();
+
+		switch(functionType) {
+		case PLUS: return new ADD(leftAdd->Plus(*rightAdd)); break;
+		case MINUS: return new ADD(leftAdd->Minus(*rightAdd)); break;
+		case TIMES: return new ADD(leftAdd->Times(*rightAdd)); break;
+		case DIVIDE: return new ADD(leftAdd->Divide(*rightAdd)); break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown boolean binary operator: '" << functionType << "'.";
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = left->toString();
 		switch (functionType) {

src/ir/expressions/BinaryRelationExpression.h

@@ -10,6 +10,8 @@
 
 #include "src/ir/expressions/BaseExpression.h"
 
+#include "src/utility/CuddUtility.h"
+
 namespace storm {
 
 namespace ir {
@@ -18,7 +20,7 @@ namespace expressions {
 
 class BinaryRelationExpression : public BaseExpression {
 public:
-	enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL};
+	enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL};
 
 	BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relationType) : BaseExpression(bool_), left(left), right(right), relationType(relationType) {
 
@@ -33,6 +35,7 @@ public:
 		int_fast64_t resultRight = right->getValueAsInt(variableValues);
 		switch(relationType) {
 		case EQUAL: return resultLeft == resultRight; break;
+		case NOT_EQUAL: return resultLeft != resultRight; break;
 		case LESS: return resultLeft < resultRight; break;
 		case LESS_OR_EQUAL: return resultLeft <= resultRight; break;
 		case GREATER: return resultLeft > resultRight; break;
@@ -42,10 +45,27 @@ public:
 		}
 	}
 
+	virtual ADD* toAdd() const {
+		ADD* leftAdd = left->toAdd();
+		ADD* rightAdd = right->toAdd();
+
+		switch(relationType) {
+		case EQUAL: return new ADD(leftAdd->Equals(*rightAdd)); break;
+		case NOT_EQUAL: return new ADD(leftAdd->NotEquals(*rightAdd)); break;
+		case LESS: return new ADD(leftAdd->LessThan(*rightAdd)); break;
+		case LESS_OR_EQUAL: return new ADD(leftAdd->LessThanOrEqual(*rightAdd)); break;
+		case GREATER: return new ADD(leftAdd->GreaterThan(*rightAdd)); break;
+		case GREATER_OR_EQUAL: return new ADD(leftAdd->GreaterThanOrEqual(*rightAdd)); break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown boolean binary operator: '" << relationType << "'.";
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = left->toString();
 		switch (relationType) {
 		case EQUAL: result += " = "; break;
+		case NOT_EQUAL: result += " != "; break;
 		case LESS: result += " < "; break;
 		case LESS_OR_EQUAL: result += " <= "; break;
 		case GREATER: result += " > "; break;

src/ir/expressions/BooleanConstantExpression.h

@@ -10,6 +10,8 @@
 
 #include "ConstantExpression.h"
 
+#include "src/utility/CuddUtility.h"
+
 #include <boost/lexical_cast.hpp>
 
 namespace storm {
@@ -38,6 +40,16 @@ public:
 		}
 	}
 
+	virtual ADD* toAdd() const {
+		if (!defined) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+					<< "Boolean constant '" << this->getConstantName() << "' is undefined.";
+		}
+
+		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
+		return new ADD(*cuddUtility->getConstant(value ? 1 : 0));
+	}
+
 	virtual std::string toString() const {
 		std::string result = this->constantName;
 		if (defined) {

src/ir/expressions/BooleanLiteral.h

@@ -32,6 +32,11 @@ public:
 		return value;
 	}
 
+	virtual ADD* toAdd() const {
+		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
+		return new ADD(*cuddUtility->getConstant(value ? 1 : 0));
+	}
+
 	virtual std::string toString() const {
 		if (value) {
 			return std::string("true");

src/ir/expressions/DoubleConstantExpression.h

@@ -35,6 +35,16 @@ public:
 		}
 	}
 
+	virtual ADD* toAdd() const {
+		if (!defined) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+					<< "Double constant '" << this->getConstantName() << "' is undefined.";
+		}
+
+		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
+		return new ADD(*cuddUtility->getConstant(value));
+	}
+
 	virtual std::string toString() const {
 		std::string result = this->constantName;
 		if (defined) {

src/ir/expressions/DoubleLiteral.h

@@ -34,6 +34,11 @@ public:
 		return value;
 	}
 
+	virtual ADD* toAdd() const {
+		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
+		return new ADD(*cuddUtility->getConstant(value));
+	}
+
 	virtual std::string toString() const {
 		return boost::lexical_cast<std::string>(value);
 	}

src/ir/expressions/ExpressionVisitor.h

@@ -0,0 +1,44 @@
+/*
+ * ExpressionVisitor.h
+ *
+ *  Created on: 26.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_
+#define STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_
+
+#include "Expressions.h"
+
+namespace storm {
+
+namespace ir {
+
+namespace expressions {
+
+class ExpressionVisitor {
+public:
+	virtual void visit(BaseExpression expression) = 0;
+	virtual void visit(BinaryBooleanFunctionExpression expression) = 0;
+	virtual void visit(BinaryNumericalFunctionExpression expression) = 0;
+	virtual void visit(BinaryRelationExpression expression) = 0;
+	virtual void visit(BooleanConstantExpression expression) = 0;
+	virtual void visit(BooleanLiteral expression) = 0;
+	virtual void visit(ConstantExpression expression) = 0;
+	virtual void visit(DoubleConstantExpression expression) = 0;
+	virtual void visit(DoubleLiteral expression) = 0;
+	virtual void visit(IntegerConstantExpression expression) = 0;
+	virtual void visit(IntegerLiteral expression) = 0;
+	virtual void visit(UnaryBooleanFunctionExpression expression) = 0;
+	virtual void visit(UnaryNumericalFunctionExpression expression) = 0;
+	virtual void visit(VariableExpression expression) = 0;
+};
+
+} // namespace expressions
+
+} // namespace ir
+
+} // namespace storm
+
+
+#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ */

src/ir/expressions/Expressions.h

@@ -2,11 +2,11 @@
  * Expressions.h
  *
  *  Created on: 03.01.2013
- *      Author: chris
+ *      Author: Christian Dehnert
  */
 
-#ifndef EXPRESSIONS_H_
-#define EXPRESSIONS_H_
+#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONS_H_
+#define STORM_IR_EXPRESSIONS_EXPRESSIONS_H_
 
 #include "BaseExpression.h"
 #include "BinaryBooleanFunctionExpression.h"
@@ -18,8 +18,9 @@
 #include "UnaryBooleanFunctionExpression.h"
 #include "UnaryNumericalFunctionExpression.h"
 #include "VariableExpression.h"
+#include "ConstantExpression.h"
 #include "BooleanConstantExpression.h"
 #include "IntegerConstantExpression.h"
 #include "DoubleConstantExpression.h"
 
-#endif /* EXPRESSIONS_H_ */
+#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ */

src/ir/expressions/IntegerConstantExpression.h

@@ -35,6 +35,16 @@ public:
 		}
 	}
 
+	virtual ADD* toAdd() const {
+		if (!defined) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+					<< "Integer constant '" << this->getConstantName() << "' is undefined.";
+		}
+
+		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
+		return new ADD(*cuddUtility->getConstant(value));
+	}
+
 	virtual std::string toString() const {
 		std::string result = this->constantName;
 		if (defined) {

src/ir/expressions/IntegerLiteral.h

@@ -32,6 +32,11 @@ public:
 		return value;
 	}
 
+	virtual ADD* toAdd() const {
+		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
+		return new ADD(*cuddUtility->getConstant(value));
+	}
+
 	virtual std::string toString() const {
 		return boost::lexical_cast<std::string>(value);
 	}

src/ir/expressions/UnaryBooleanFunctionExpression.h

@@ -37,6 +37,11 @@ public:
 		}
 	}
 
+	virtual ADD* toAdd() const {
+		ADD* childResult = child->toAdd();
+		return new ADD(~(*childResult));
+	}
+
 	virtual std::string toString() const {
 		std::string result = "";
 		switch (functionType) {

src/ir/expressions/UnaryNumericalFunctionExpression.h

@@ -54,6 +54,13 @@ public:
 		}
 	}
 
+	virtual ADD* toAdd() const {
+		ADD* childResult = child->toAdd();
+		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
+		ADD* result = cuddUtility->getConstant(0);
+		return new ADD(result->Minus(*childResult));
+	}
+
 	virtual std::string toString() const {
 		std::string result = "";
 		switch (functionType) {

src/ir/expressions/VariableExpression.h

@@ -10,6 +10,7 @@
 
 #include "src/ir/expressions/BaseExpression.h"
 
+#include <memory>
 #include <iostream>
 
 namespace storm {
@@ -20,7 +21,11 @@ namespace expressions {
 
 class VariableExpression : public BaseExpression {
 public:
-	VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName) : BaseExpression(type), index(index), variableName(variableName) {
+	VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName,
+			std::shared_ptr<BaseExpression> lowerBound = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr),
+			std::shared_ptr<BaseExpression> upperBound = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr))
+			: BaseExpression(type), index(index), variableName(variableName),
+			  lowerBound(lowerBound), upperBound(upperBound) {
 
 	}
 
@@ -67,9 +72,28 @@ public:
 				<< " variable '" << variableName << "' of type double.";
 	}
 
+	virtual ADD* toAdd() const {
+		storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance();
+
+		return nullptr;
+
+		if (this->getType() == bool_) {
+			ADD* result = cuddUtility->getConstant(0);
+			//cuddUtility->addValueForEncodingOfConstant(result, 1, )
+		} else {
+			int64_t low = lowerBound->getValueAsInt(nullptr);
+			int64_t high = upperBound->getValueAsInt(nullptr);
+		}
+
+		return new ADD();
+	}
+
 private:
 	uint_fast64_t index;
 	std::string variableName;
+
+	std::shared_ptr<BaseExpression> lowerBound;
+	std::shared_ptr<BaseExpression> upperBound;
 };
 
 }

src/parser/PrismParser.cpp

@@ -188,7 +188,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		// This block defines all entities that are neede for parsing variable definitions.
 		booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct<storm::ir::BooleanVariable>(phoenix::ref(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::ref(nextBooleanVariableIndex))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(storm::ir::expressions::BaseExpression::bool_, phoenix::ref(nextBooleanVariableIndex), qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), phoenix::ref(nextBooleanVariableIndex) = phoenix::ref(nextBooleanVariableIndex) + 1];
 		booleanVariableDefinition.name("boolean variable declaration");
-		integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct<storm::ir::IntegerVariable>(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::ref(nextIntegerVariableIndex))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(storm::ir::expressions::BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1];
+		integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct<storm::ir::IntegerVariable>(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::ref(nextIntegerVariableIndex))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(storm::ir::expressions::BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1];
 		integerVariableDefinition.name("integer variable declaration");
 		variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4));
 		variableDefinition.name("variable declaration");

src/storm.cpp

@@ -140,6 +140,7 @@ void cleanUp() {
 	if (storm::settings::instance() != nullptr) {
 		delete storm::settings::instance();
 	}
+	delete storm::utility::cuddUtilityInstance();
 }
 
 void testCheckingDie(storm::models::Dtmc<double>& dtmc) {

src/utility/CuddUtility.cpp

@@ -0,0 +1,125 @@
+/*
+ * CuddUtility.cpp
+ *
+ *  Created on: 26.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#include "CuddUtility.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+extern log4cplus::Logger logger;
+
+#include <stdio.h>
+#include <iostream>
+
+namespace storm {
+
+namespace utility {
+
+storm::utility::CuddUtility* storm::utility::CuddUtility::instance = nullptr;
+
+ADD* CuddUtility::getNewAddVariable() {
+	ADD* result = new ADD(manager.addVar());
+	allDecisionDiagramVariables.push_back(result);
+	return result;
+}
+
+ADD* CuddUtility::getAddVariable(int index) const {
+	return new ADD(manager.addVar(index));
+}
+
+ADD* CuddUtility::getConstantEncoding(uint_fast64_t constant, std::vector<ADD*>& variables) const {
+	if ((constant >> variables.size()) != 0) {
+		LOG4CPLUS_ERROR(logger, "Cannot create encoding for constant " << constant << " with "
+				<< variables.size()	<< " variables.");
+		throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding"
+				<< " for constant " << constant << " with " << variables.size()
+				<< " variables.";
+	}
+
+	// Determine whether the new ADD will be rooted by the first variable or its complement.
+	ADD initialNode;
+	if ((constant & (1 << (variables.size() - 1))) != 0) {
+		initialNode = *variables[0];
+	} else {
+		initialNode = ~(*variables[0]);
+	}
+	ADD* result = new ADD(initialNode);
+
+	// Add (i.e. multiply) the other variables as well according to whether their bit is set or not.
+	for (uint_fast64_t i = 1; i < variables.size(); ++i) {
+		if ((constant & (1 << (variables.size() - i - 1))) != 0) {
+			*result *= *variables[i];
+		} else {
+			*result *= ~(*variables[i]);
+		}
+	}
+
+	return result;
+}
+
+ADD* CuddUtility::addValueForEncodingOfConstant(ADD* add, uint_fast64_t constant, std::vector<ADD*>& variables, double value) const {
+	if ((constant >> variables.size()) != 0) {
+		LOG4CPLUS_ERROR(logger, "Cannot create encoding for constant " << constant << " with "
+				<< variables.size()	<< " variables.");
+		throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding"
+				<< " for constant " << constant << " with " << variables.size()
+				<< " variables.";
+	}
+
+	// Determine whether the new ADD will be rooted by the first variable or its complement.
+	ADD initialNode;
+	if ((constant & (1 << (variables.size() - 1))) != 0) {
+		initialNode = *variables[0];
+	} else {
+		initialNode = ~(*variables[0]);
+	}
+	ADD* encoding = new ADD(initialNode);
+
+	// Add (i.e. multiply) the other variables as well according to whether their bit is set or not.
+	for (uint_fast64_t i = 1; i < variables.size(); ++i) {
+		if ((constant & (1 << (variables.size() - i - 1))) != 0) {
+			*encoding *= *variables[i];
+		} else {
+			*encoding *= ~(*variables[i]);
+		}
+	}
+
+	ADD* result = new ADD(add->Ite(manager.constant(value), *add));
+	return result;
+}
+
+ADD* CuddUtility::getConstant(double value) const {
+	return new ADD(manager.constant(value));
+}
+
+void CuddUtility::dumpDotToFile(ADD* add, std::string filename) const {
+	std::vector<ADD> nodes;
+	nodes.push_back(*add);
+
+	FILE* filePtr;
+	filePtr = fopen(filename.c_str(), "w");
+	manager.DumpDot(nodes, 0, 0, filePtr);
+	fclose(filePtr);
+}
+
+Cudd const& CuddUtility::getManager() const {
+	return manager;
+}
+
+CuddUtility* cuddUtilityInstance() {
+	if (CuddUtility::instance != nullptr) {
+		CuddUtility::instance = new CuddUtility();
+	}
+	return CuddUtility::instance;
+}
+
+} // namespace utility
+
+} // namespace storm
+
+

src/utility/CuddUtility.h

@@ -0,0 +1,57 @@
+/*
+ * CuddUtility.h
+ *
+ *  Created on: 26.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_UTILITY_CUDDUTILITY_H_
+#define STORM_UTILITY_CUDDUTILITY_H_
+
+#include "cuddObj.hh"
+
+namespace storm {
+
+namespace utility {
+
+class CuddUtility {
+public:
+	~CuddUtility() {
+		for (auto element : allDecisionDiagramVariables) {
+			delete element;
+		}
+	}
+
+	ADD* getNewAddVariable();
+	ADD* getAddVariable(int index) const;
+
+	ADD* getConstantEncoding(uint_fast64_t constant, std::vector<ADD*>& variables) const;
+
+	ADD* addValueForEncodingOfConstant(ADD* add, uint_fast64_t constant, std::vector<ADD*>& variables, double value) const;
+
+	ADD* getConstant(double value) const;
+
+	void dumpDotToFile(ADD* add, std::string filename) const;
+
+	Cudd const& getManager() const;
+
+	friend CuddUtility* cuddUtilityInstance();
+
+private:
+	CuddUtility() : manager(0, 0), allDecisionDiagramVariables() {
+
+	}
+
+	Cudd manager;
+	std::vector<ADD*> allDecisionDiagramVariables;
+
+	static CuddUtility* instance;
+};
+
+CuddUtility* cuddUtilityInstance();
+
+} // namespace utility
+
+} // namespace storm
+
+#endif /* STORM_UTILITY_CUDDUTILITY_H_ */