From 723999f8854fc17f6c79835700fb4e822c33a81a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 4 Aug 2016 16:04:32 +0200
Subject: [PATCH] intermediate work-place switch commit

Former-commit-id: 818179d2864862dc0710919707275bcee96a954c
---
 src/abstraction/AbstractionInformation.cpp |  77 ++++++++++++
 src/abstraction/AbstractionInformation.h   | 129 +++++++++++++++++++++
 2 files changed, 206 insertions(+)
 create mode 100644 src/abstraction/AbstractionInformation.cpp
 create mode 100644 src/abstraction/AbstractionInformation.h

diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp
new file mode 100644
index 000000000..071f9150e
--- /dev/null
+++ b/src/abstraction/AbstractionInformation.cpp
@@ -0,0 +1,77 @@
+#include "src/abstraction/AbstractionInformation.h"
+
+namespace storm {
+    namespace abstraction {
+
+        template<storm::dd::DdType DdType, typename ValueType>
+        AbstractionInformation<DdType, ValueType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager) : expressionManager(expressionManager) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        void AbstractionInformation<DdType, ValueType>::addVariable(storm::expressions::Variable const& variable) {
+            variables.insert(variable);
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        void AbstractionInformation<DdType, ValueType>::addVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint) {
+            addVariable(variable);
+            addConstraint(constraint);
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        void AbstractionInformation<DdType, ValueType>::addConstraint(storm::expressions::Expression const& constraint) {
+            constraints.push_back(constraint);
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        void AbstractionInformation<DdType, ValueType>::addPredicate(storm::expressions::Expression const& predicate) {
+            predicates.push_back(predicate);
+        }
+
+        template<storm::dd::DdType DdType, typename ValueType>
+        void AbstractionInformation<DdType, ValueType>::addPredicates(std::vector<storm::expressions::Expression> const& predicates) {
+            for (auto const& predicate : predicates) {
+                this->addPredicate(predicate);
+            }
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::expressions::ExpressionManager& AbstractionInformation<DdType, ValueType>::getExpressionManager() {
+            return expressionManager;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::expressions::ExpressionManager const& AbstractionInformation<DdType, ValueType>::getExpressionManager() const {
+            return expressionManager;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType, ValueType>::getPredicates() const {
+            return predicates;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::expressions::Expression const& AbstractionInformation<DdType, ValueType>::getPredicateByIndex(uint_fast64_t index) const {
+            return predicates[index];
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        std::size_t AbstractionInformation<DdType, ValueType>::getNumberOfPredicates() const {
+            return predicates.size();
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        std::set<storm::expressions::Variable> const& AbstractionInformation<DdType, ValueType>::getVariables() const {
+            return variables;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType, ValueType>::getConstraints() const {
+            return constraints;
+        }
+        
+        template class AbstractionInformation<storm::dd::DdType::CUDD, double>;
+        template class AbstractionInformation<storm::dd::DdType::Sylvan, double>;
+    }
+}
\ No newline at end of file
diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h
new file mode 100644
index 000000000..6af6e7e17
--- /dev/null
+++ b/src/abstraction/AbstractionInformation.h
@@ -0,0 +1,129 @@
+#pragma once
+
+#include <vector>
+#include <set>
+
+#include "src/storage/dd/DdType.h"
+
+namespace storm {
+    namespace expressions {
+        class ExpressionManager;
+        class Expression;
+        class Variable;
+    }
+    
+    namespace abstraction {
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        class AbstractionInformation {
+        public:
+            /*!
+             * Creates a new abstraction information object.
+             *
+             * @param expressionManager The manager responsible for all variables and expressions during the abstraction process.
+             */
+            AbstractionInformation(storm::expressions::ExpressionManager& expressionManager);
+
+            /*!
+             * Adds the given variable.
+             *
+             * @param variable The variable to add.
+             */
+            void addVariable(storm::expressions::Variable const& variable);
+
+            /*!
+             * Adds the given variable whose range is restricted.
+             *
+             * @param variable The variable to add.
+             * @param constraint An expression characterizing the legal values of the variable.
+             */
+            void addVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint);
+
+            /*!
+             * Adds an expression that constrains the legal variable values.
+             *
+             * @param constraint The constraint.
+             */
+            void addConstraint(storm::expressions::Expression const& constraint);
+            
+            /*!
+             * Adds the given predicate.
+             *
+             * @param predicate The predicate to add.
+             */
+            void addPredicate(storm::expressions::Expression const& predicate);
+            
+            /*!
+             * Adds the given predicates.
+             *
+             * @param predicates The predicates to add.
+             */
+            void addPredicates(std::vector<storm::expressions::Expression> const& predicates);
+            
+            /*!
+             * Retrieves the expression manager.
+             *
+             * @return The manager.
+             */
+            storm::expressions::ExpressionManager& getExpressionManager();
+            
+            /*!
+             * Retrieves the expression manager.
+             *
+             * @return The manager.
+             */
+            storm::expressions::ExpressionManager const& getExpressionManager() const;
+            
+            /*!
+             * Retrieves all currently known predicates.
+             *
+             * @return The list of known predicates.
+             */
+            std::vector<storm::expressions::Expression> const& getPredicates() const;
+
+            /*!
+             * Retrieves the predicate with the given index.
+             *
+             * @param index The index of the predicate.
+             */
+            storm::expressions::Expression const& getPredicateByIndex(uint_fast64_t index) const;
+            
+            /*!
+             * Retrieves the number of predicates.
+             *
+             * @return The number of predicates.
+             */
+            std::size_t getNumberOfPredicates() const;
+            
+            /*!
+             * Retrieves all currently known variables.
+             *
+             * @return The set of known variables.
+             */
+            std::set<storm::expressions::Variable> const& getVariables() const;
+            
+            /*!
+             * Retrieves a list of expressions that constrain the valid variable values.
+             *
+             * @return The constraint expressions.
+             */
+            std::vector<storm::expressions::Expression> const& getConstraints() const;
+            
+        private:
+            // The expression related data.
+            
+            /// The manager responsible for the expressions of the program and the SMT solvers.
+            storm::expressions::ExpressionManager& expressionManager;
+            
+            /// The current set of predicates used in the abstraction.
+            std::vector<storm::expressions::Expression> predicates;
+            
+            /// The set of all variables.
+            std::set<storm::expressions::Variable> variables;
+            
+            /// The expressions characterizing legal variable values.
+            std::vector<storm::expressions::Expression> constraints;
+        };
+        
+    }
+}
\ No newline at end of file