From 2c22cee1f8fa87c527449a8bdc668ea311fdaf64 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Fri, 27 Apr 2012 13:33:58 +1000 Subject: Bit more work. maxFixpoint should be working now. --- impl/EquationSystem.hpp | 79 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 impl/EquationSystem.hpp (limited to 'impl/EquationSystem.hpp') diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp new file mode 100644 index 0000000..065a1a2 --- /dev/null +++ b/impl/EquationSystem.hpp @@ -0,0 +1,79 @@ +#ifndef EQUATION_SYSTEM_HPP +#define EQUATION_SYSTEM_HPP + +#include "Expression.hpp" + +template +struct EquationSystem { + EquationSystem () + : _max_id(0) { } + virtual ~EquationSystem() { + for (int i = 0, size = _vars.size(); i < size; ++i) { + delete _vars[i]; + } + } + Variable* newVariable(const std::string&) { + _vars.push_back(new Variable(_vars.size())); + return _vars[_vars.size()-1]; + } + unsigned int varCount() const { + return _vars.size(); + } + MaxExpression* newMaxExpression(const std::vector*>& args) { + MaxExpression* expr = new MaxExpression(args); + expr->id(_max_id++); + return expr; + } + unsigned int maxCount() const { + return _max_id; + } + + Expression*& operator[] (const Variable& v) { + if (_expressions.size() <= v.id()) { + _expressions.resize(v.id()+1); + } + return _expressions[v.id()]; + } + const Expression*& operator[] (const Variable& v) const { + if (_expressions.size() <= v.id()) { + throw "Out of range"; + } + return _expressions[v.id()]; + } + + template + VariableAssignment foreach(F op, const VariableAssignment& v) { + VariableAssignment result(_vars.size()); + for (unsigned int i = 0, size = _vars.size(); i < size; ++i) { + result[_vars[i]] = op(_expressions[i], v); + } + } + + VariableAssignment operator() (const VariableAssignment& rho) { + VariableAssignment result(_vars.size()); + for (unsigned int i = 0, size = _vars.size(); i < size; ++i) { + result[*_vars[i]] = (*_expressions[i])(rho); + } + return result; + } + + VariableAssignment maxFixpoint() { + unsigned int size = _vars.size(); + VariableAssignment result(size, infinity()); + for (unsigned int i = 0; i < size; ++i) { + result = (*this)(result); + } + result = result.expand((*this)(result), -infinity()); + for (unsigned int i = 0; i < size-1; ++i) { + result = (*this)(result); + } + return result; + } + private: + unsigned int _max_id; + std::vector*> _vars; + std::vector*> _expressions; +}; + + +#endif -- cgit v1.2.3