diff options
Diffstat (limited to 'impl/EquationSystem.hpp')
-rw-r--r-- | impl/EquationSystem.hpp | 44 |
1 files changed, 21 insertions, 23 deletions
diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp index ac0b3b2..5aaadfb 100644 --- a/impl/EquationSystem.hpp +++ b/impl/EquationSystem.hpp @@ -3,7 +3,13 @@ #include <map> +template<typename T> +struct EquationSystem; + +#include "IdSet.hpp" #include "Expression.hpp" +#include "FixpointAlgorithm.hpp" + template<typename T> struct MaxStrategy; @@ -31,6 +37,9 @@ struct EquationSystem { const std::vector<Variable<T>*> vars() const { return _vars; } + const Variable<T>* getVar(unsigned int i) const { + return _vars[i]; + } unsigned int varCount() const { return _vars.size(); } @@ -58,7 +67,7 @@ struct EquationSystem { MaxStrategy<T> strategy() const { return MaxStrategy<T>(_max_expressions.size()); } - + VariableAssignment<T> assignment() const { return VariableAssignment<T>(_vars.size()); } @@ -69,7 +78,7 @@ struct EquationSystem { } return _right_expressions[v.id()]; } - const Expression<T>*& operator[] (const Variable<T>& v) const { + const Expression<T>* operator[] (const Variable<T>& v) const { if (_right_expressions.size() <= v.id()) { throw "Out of range"; } @@ -95,38 +104,27 @@ struct EquationSystem { VariableAssignment<T> maxFixpoint() const { unsigned int size = _vars.size(); - VariableAssignment<T> result(size, infinity<T>()); - for (unsigned int i = 0; i < size; ++i) { - result = (*this)(result); - } - result = result.expand((*this)(result), -infinity<T>()); - for (unsigned int i = 0; i < size-1; ++i) { - result = (*this)(result); - } + VariableAssignment<T> newResult(size, infinity<T>()); + VariableAssignment<T> result(0); + do { + result = newResult; + newResult = (*this)(result); + } while (newResult != result); return result; } - VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat) const { - unsigned int size = _vars.size(); - VariableAssignment<T> result(size, infinity<T>()); - for (unsigned int i = 0; i < size; ++i) { - result = strat(*this, result); - } - result = result.expand(strat(*this, result), -infinity<T>()); - for (unsigned int i = 0; i < size-1; ++i) { - result = strat(*this, result); - } - return result; + VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat, const FixpointAlgorithm<T>& algo) const { + return algo.maxFixpoint(strat, *this); } - VariableAssignment<T> minFixpoint() const { + VariableAssignment<T> minFixpoint(const FixpointAlgorithm<T>& algo) const { VariableAssignment<T> rho = assignment(); VariableAssignment<T> lastRho = assignment(); MaxStrategy<T> strat = strategy(); do { lastRho = rho; strat = strat.improve(*this, rho); - rho = maxFixpoint(strat); + rho = maxFixpoint(strat, algo); } while(lastRho != rho); return rho; } |