summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--impl/Complete.hpp7
-rw-r--r--impl/EquationSystem.hpp208
-rw-r--r--impl/Expression.hpp143
-rw-r--r--impl/FixpointAlgorithm.hpp127
-rw-r--r--impl/IdMap.hpp1
-rw-r--r--impl/IdSet.hpp2
-rw-r--r--impl/MaxStrategy.hpp175
-rw-r--r--impl/Operator.hpp166
-rw-r--r--impl/VariableAssignment.hpp30
-rw-r--r--impl/main.cpp84
10 files changed, 539 insertions, 404 deletions
diff --git a/impl/Complete.hpp b/impl/Complete.hpp
index 1cf40af..22e060a 100644
--- a/impl/Complete.hpp
+++ b/impl/Complete.hpp
@@ -5,9 +5,14 @@
#include <istream>
template<typename T>
+T infinity() { }
+
+template<typename T>
struct Complete {
Complete()
: _value(0), _infinity(false) { }
+ Complete(const T& value)
+ : _value(value), _infinity(false) { }
Complete(const T& value, const bool& infinity)
: _value(value), _infinity(infinity) {
if (value == 0 && infinity == true) {
@@ -69,7 +74,7 @@ struct Complete {
}
}
bool operator>(const Complete& other) const {
- return !(*this < other || *this == other);
+ return other < *this;
}
bool operator==(const Complete& other) const {
if (_infinity) {
diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp
index 13319e0..50a0e45 100644
--- a/impl/EquationSystem.hpp
+++ b/impl/EquationSystem.hpp
@@ -1,141 +1,145 @@
#ifndef EQUATION_SYSTEM_HPP
#define EQUATION_SYSTEM_HPP
+#include <vector>
+#include <set>
#include <map>
-
-template<typename T>
-struct EquationSystem;
-
-#include "IdSet.hpp"
+#include "Operator.hpp"
#include "Expression.hpp"
-#include "FixpointAlgorithm.hpp"
+#include "VariableAssignment.hpp"
-template<typename T>
-struct MaxStrategy;
-
-template<typename T>
+template<typename Domain>
struct EquationSystem {
- virtual ~EquationSystem() {
- for (int i = 0, size = _expressions.size(); i < size; ++i) {
- delete _expressions[i];
- }
- for (int i = 0, size = _vars.size(); i < size; ++i) {
- delete _vars[i];
+ virtual ~EquationSystem() { }
+ virtual const Expression<Domain>* operator[](const Variable<Domain>&) const = 0;
+ virtual VariableAssignment<Domain>* eval(const VariableAssignment<Domain>& rho) const = 0;
+ virtual unsigned int variableCount() const = 0;
+ virtual Variable<Domain>& variable(unsigned int) const = 0;
+ virtual StableVariableAssignment<Domain>* assignment(const Domain& value) const = 0;
+ virtual bool equalAssignments(const VariableAssignment<Domain>&, const VariableAssignment<Domain>&) const = 0;
+
+ virtual void print(std::ostream& cout) const = 0;
+};
+
+template<typename Domain>
+struct ConcreteEquationSystem : public EquationSystem<Domain> {
+ virtual ~ConcreteEquationSystem() {
+ for (typename std::set<Expression<Domain>*>::iterator it = _expressions.begin();
+ it != _expressions.end();
+ ++it) {
+ delete *it;
}
- }
- Variable<T>* newVariable(const std::string& name) {
- typename std::map<const std::string, Variable<T>*>::iterator it = _var_names.find(name);
- if (it == _var_names.end()) {
- Variable<T>* newVar = new Variable<T>(_vars.size(), name);
- _vars.push_back(newVar);
- _var_names[name] = newVar;
- return _vars[_vars.size()-1];
- } else {
- return it->second;
+ for (typename std::set<Operator<Domain>*>::iterator it = _operators.begin();
+ it != _operators.end();
+ ++it) {
+ delete *it;
}
}
- const std::vector<Variable<T>*> vars() const {
- return _vars;
+
+ MaxExpression<Domain>& maxExpression(const std::vector<Expression<Domain>*>& arguments) {
+ unsigned int id = _max_expressions.size();
+ Maximum<Domain>* max = new Maximum<Domain>();
+ MaxExpression<Domain>* expr = new MaxExpression<Domain>(id, *max, arguments);
+ _operators.insert(max);
+ _max_expressions.push_back(expr);
+ _expressions.insert(expr);
+ return *expr;
}
- const Variable<T>* getVar(unsigned int i) const {
- return _vars[i];
+ MaxExpression<Domain>& maxExpression(unsigned int i) const {
+ return *_max_expressions[i];
}
- unsigned int varCount() const {
- return _vars.size();
+ unsigned int maxExpressionCount() const {
+ return _max_expressions.size();
}
- Expression<T>* newExpression(Operator<T>* op, const std::vector<Expression<T>*>& args=std::vector<Expression<T>*>()) {
- Expression<T>* expr = new Expression<T>(op, args);
- _expressions.push_back(expr);
- return expr;
+ Expression<Domain>& expression(Operator<Domain>* op, const std::vector<Expression<Domain>*>& arguments) {
+ Expression<Domain>* expr = new OperatorExpression<Domain>(*op, arguments);
+ _operators.insert(op);
+ _expressions.insert(expr);
+ return *expr;
}
- MaxExpression<T>* newMaxExpression(const std::vector<Expression<T>*>& args) {
- MaxExpression<T>* expr = new MaxExpression<T>(args);
- expr->id(_max_expressions.size());
- _max_expressions.push_back(expr);
- _expressions.push_back(expr);
- return expr;
+ Variable<Domain>& variable(const std::string& name) {
+ if (_variable_names.find(name) == _variable_names.end()) {
+ // not found - create a new variable and whatnot
+ unsigned int id = _variables.size();
+ Variable<Domain>* var = new Variable<Domain>(id, name);
+ _variables.push_back(var);
+ _right_sides.push_back(NULL);
+ _expressions.insert(var);
+ _variable_names[name] = var;
+ return *var;
+ } else {
+ return *_variable_names[name];
+ }
}
- unsigned int maxCount() const {
- return _max_expressions.count();
+ Variable<Domain>& variable(unsigned int id) const {
+ return *_variables[id];
}
- const MaxExpression<T>* getMax(unsigned int i) const {
- return _max_expressions[i];
+ unsigned int variableCount() const {
+ return _variables.size();
}
- MaxStrategy<T> strategy() const {
- return MaxStrategy<T>(_max_expressions.size());
+ Constant<Domain>& constant(const Domain& value) {
+ Constant<Domain>* constant = new Constant<Domain>(value);
+ _expressions.insert(constant);
+ return *constant;
}
- VariableAssignment<T> assignment() const {
- return VariableAssignment<T>(_vars.size());
+ Expression<Domain>* operator[](const Variable<Domain>& var) const {
+ return _right_sides[var.id()];
}
-
- Expression<T>*& operator[] (const Variable<T>& v) {
- if (_right_expressions.size() <= v.id()) {
- _right_expressions.resize(v.id()+1);
- }
- return _right_expressions[v.id()];
- }
- const Expression<T>* operator[] (const Variable<T>& v) const {
- if (_right_expressions.size() <= v.id()) {
- throw "Out of range";
- }
- return _right_expressions[v.id()];
+ Expression<Domain>*& operator[](const Variable<Domain>& var) {
+ return _right_sides[var.id()];
}
- template<typename F>
- VariableAssignment<T> foreach(F op, const VariableAssignment<T>& rho) const {
- VariableAssignment<T> result(_vars.size());
- for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
- result[*_vars[i]] = op(*_right_expressions[i], rho);
- }
- return result;
+ StableVariableAssignment<Domain>* assignment(const Domain& value) const {
+ return new StableVariableAssignment<Domain>(_variables.size(), value);
}
-
- VariableAssignment<T> operator() (const VariableAssignment<T>& rho) const {
- VariableAssignment<T> result(_vars.size());
- for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
- result[*_vars[i]] = (*_right_expressions[i])(rho);
+ VariableAssignment<Domain>* eval(const VariableAssignment<Domain>& rho) const {
+ StableVariableAssignment<Domain>* result = this->assignment(-infinity<Domain>());
+ for (unsigned int i = 0, length = _variables.size();
+ i < length;
+ ++i) {
+ const Variable<Domain>& var = *_variables[i];
+ const Expression<Domain>& expr = * (*this)[var];
+ (*result)[var] = expr.eval(rho);
}
return result;
}
- VariableAssignment<T> maxFixpoint() const {
- unsigned int size = _vars.size();
- VariableAssignment<T> newResult(size, infinity<T>());
- VariableAssignment<T> result(0);
- do {
- result = newResult;
- newResult = (*this)(result);
- } while (newResult != result);
- return result;
+ virtual bool equalAssignments(const VariableAssignment<Domain>& l, const VariableAssignment<Domain>& r) const {
+ for (unsigned int i = 0, length = _variables.size();
+ i < length;
+ ++i) {
+ const Variable<Domain>& var = *_variables[i];
+ if (l[var] != r[var])
+ return false;
+ }
+ return true;
}
- VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat, const FixpointAlgorithm<T>& algo) const {
- return algo.maxFixpoint(strat, *this);
+ void print(std::ostream& cout) const {
+ for (unsigned int i = 0, length = _variables.size();
+ i < length;
+ ++i) {
+ cout << *_variables[i] << " = " << *_right_sides[i] << std::endl;
+ }
}
- VariableAssignment<T> minFixpoint(const FixpointAlgorithm<T>& algo) const {
- VariableAssignment<T> rho = assignment();
- VariableAssignment<T> lastRho(0);
- MaxStrategy<T> strat = strategy();
- do {
- lastRho = rho;
- strat = strat.improve(*this, rho);
- rho = maxFixpoint(strat, algo);
- } while(lastRho != rho);
- return rho;
- }
private:
- std::map<const std::string, Variable<T>*> _var_names;
- std::vector<Variable<T>*> _vars;
- std::vector<MaxExpression<T>*> _max_expressions;
- std::vector<Expression<T>*> _expressions;
- std::vector<Expression<T>*> _right_expressions;
+ std::set<Operator<Domain>*> _operators;
+ std::set<Expression<Domain>*> _expressions;
+ std::vector<Variable<Domain>*> _variables;
+ std::map<std::string, Variable<Domain>*> _variable_names;
+ std::vector<MaxExpression<Domain>*> _max_expressions;
+ std::vector<Expression<Domain>*> _right_sides;
};
-#include "MaxStrategy.hpp"
+template<typename T>
+std::ostream& operator<<(std::ostream& cout, const EquationSystem<T>& system) {
+ system.print(cout);
+ return cout;
+}
#endif
diff --git a/impl/Expression.hpp b/impl/Expression.hpp
index d3dfcf3..72318e4 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -1,68 +1,125 @@
#ifndef EXPRESSION_HPP
#define EXPRESSION_HPP
-#include <iostream>
-#include "VariableAssignment.hpp"
+#include <string>
+#include <vector>
+#include <sstream>
+#include "IdMap.hpp"
#include "Operator.hpp"
-template<typename T>
-struct Variable;
-template<typename T>
-struct MaxStrategy;
-
-int ExpressionCount;
+template<typename Domain>
+struct VariableAssignment;
-template<typename T>
+template<typename Domain>
struct Expression {
- Expression(Operator<T>* op, const std::vector< Expression<T>* >& args)
- : _operator(op), _arguments(args) { }
- virtual ~Expression() {
- if (!dynamic_cast<Variable<T>*>(_operator)) {
- delete _operator;
- }
+ virtual ~Expression() { }
+
+ virtual Domain eval(const VariableAssignment<Domain>&) const = 0;
+
+ virtual void print(std::ostream&) const = 0;
+};
+
+template<typename Domain>
+struct Constant : public Expression<Domain> {
+ Constant(const Domain& value)
+ : _value(value) { }
+
+ virtual Domain eval(const VariableAssignment<Domain>&) const {
+ return _value;
}
- virtual T operator() (const VariableAssignment<T>& assignment) const {
- return (*_operator)(_arguments, assignment);
+
+ void print(std::ostream& cout) const {
+ cout << _value;
}
- protected:
- Operator<T>* _operator;
- std::vector< Expression<T>* > _arguments;
+
+ private:
+ Domain _value;
};
-template<typename T>
-struct MaxExpression : public Expression<T> {
- MaxExpression(const std::vector< Expression<T>* >& args)
- : Expression<T>(new Maximum<T>, args) { }
+template<typename Domain>
+struct Variable : public Expression<Domain> {
+ Variable(const unsigned int& id, const std::string& name)
+ : _id(id), _name(name) { }
+
unsigned int id() const {
return _id;
}
- unsigned int id(unsigned int id) {
- return (_id = id);
+ std::string name() const {
+ return _name;
}
- Expression<T>* argument(unsigned int i) const {
- if (i >= Expression<T>::_arguments.size()) {
- throw "Error";
+
+ virtual Domain eval(const VariableAssignment<Domain>& rho) const {
+ return rho[*this];
+ }
+
+ void print(std::ostream& cout) const {
+ cout << name();
+ }
+
+ private:
+ const unsigned int _id;
+ const std::string _name;
+};
+
+template<typename Domain>
+struct OperatorExpression : public Expression<Domain> {
+ OperatorExpression(const Operator<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
+ : _operator(op), _arguments(arguments) { }
+
+ virtual Domain eval(const VariableAssignment<Domain>& rho) const {
+ std::vector<Domain> argumentValues;
+ for (typename std::vector<Expression<Domain>*>::const_iterator it = _arguments.begin();
+ it != _arguments.end();
+ ++it) {
+ argumentValues.push_back((*it)->eval(rho));
}
- return Expression<T>::_arguments[i];
+ return _operator.eval(argumentValues);
+ }
+
+ const std::vector<Expression<Domain>*> arguments() const {
+ return _arguments;
}
- virtual T operator() (const VariableAssignment<T>& assignment) const {
- throw "error";
+
+ const Operator<Domain>& op() const {
+ return _operator;
}
- std::pair<T, unsigned int> bestStrategy(const VariableAssignment<T>& rho, const MaxStrategy<T>& strat) const {
- std::pair<T, unsigned int> best = std::pair<T, unsigned int>(-infinity<T>(), 0);
- for (unsigned int i = 0, size = Expression<T>::_arguments.size(); i < size; ++i) {
- T value = strat(*Expression<T>::_arguments[i], rho);
- if (value > best.first)
- best = std::pair<T, unsigned int>(value, i);
+
+ void print(std::ostream& cout) const {
+ cout << _operator << "(";
+ for (unsigned int i = 0, length = _arguments.size();
+ i < length;
+ ++i) {
+ if (i > 0)
+ cout << ", ";
+ cout << *_arguments[i];
}
- std::cerr << "Best strategy: (" << best.first << ", " << best.second << ")" << std::endl << std::endl;
- return best;
+ cout << ")";
+ }
+
+ private:
+ const Operator<Domain>& _operator;
+ const std::vector<Expression<Domain>*> _arguments;
+};
+
+template<typename Domain>
+struct MaxExpression : public OperatorExpression<Domain> {
+ MaxExpression(const unsigned int& id, const Maximum<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
+ : OperatorExpression<Domain>(op, arguments), _id(id) { }
+
+ unsigned int id() const {
+ return _id;
}
+
private:
- unsigned int _id;
+ const unsigned int _id;
};
-#include "Variable.hpp"
-#include "MaxStrategy.hpp"
+template<typename T>
+std::ostream& operator<<(std::ostream& cout, const Expression<T>& exp) {
+ exp.print(cout);
+ return cout;
+}
+
+#include "VariableAssignment.hpp"
#endif
diff --git a/impl/FixpointAlgorithm.hpp b/impl/FixpointAlgorithm.hpp
index ed97bec..f199476 100644
--- a/impl/FixpointAlgorithm.hpp
+++ b/impl/FixpointAlgorithm.hpp
@@ -1,97 +1,100 @@
#ifndef FIXPOINT_ALGORITHM_HPP
#define FIXPOINT_ALGORITHM_HPP
+#include "IdSet.hpp"
+#include "IdMap.hpp"
#include "VariableAssignment.hpp"
+#include "EquationSystem.hpp"
-template<typename T>
-struct EquationSystem;
-template<typename T>
-struct MaxStrategy;
-
-template<typename T>
+template<typename Domain>
struct FixpointAlgorithm {
- virtual VariableAssignment<T> maxFixpoint(const MaxStrategy<T>&, const EquationSystem<T>&) const = 0;
+ virtual ~FixpointAlgorithm() { }
+ virtual VariableAssignment<Domain>* maxFixpoint(const EquationSystem<Domain>&) const = 0;
};
-#include "EquationSystem.hpp"
-#include "MaxStrategy.hpp"
-
-template<typename T>
-struct NaiveFixpoint : public FixpointAlgorithm<T> {
- virtual VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat, const EquationSystem<T>& system) const {
- unsigned int size = system.varCount();
- VariableAssignment<T> newResult(size, infinity<T>());
- VariableAssignment<T> result(0);
+template<typename Domain>
+struct NaiveFixpointAlgorithm : public FixpointAlgorithm<Domain> {
+ virtual VariableAssignment<Domain>* maxFixpoint(const EquationSystem<Domain>& system) const {
+ VariableAssignment<Domain>* rho = NULL;
+ VariableAssignment<Domain>* result = system.assignment(infinity<Domain>());
do {
- result = newResult;
- newResult = strat(system, result);
- } while (newResult != result);
+ if (rho) delete rho;
+ rho = result;
+ result = system.eval(*rho);
+ } while (!system.equalAssignments(*rho, *result));
+ if (rho) delete rho;
return result;
}
};
-
-template<typename T>
-struct RecursiveFixpoint : public FixpointAlgorithm<T> {
- // this is a "VariableAssignment" which actually performs a recursive
- // call to determine what value to return
- struct EvaluatingVariableAssignment : public VariableAssignment<T> {
- EvaluatingVariableAssignment(const MaxStrategy<T>& strategy, const EquationSystem<T>& system)
- : VariableAssignment<T>(system.varCount(), infinity<T>()),
- _strategy(strategy), _system(system),
+template<typename Domain>
+struct SmartFixpointAlgorithm : public FixpointAlgorithm<Domain> {
+ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
+ DynamicVariableAssignment(const EquationSystem<Domain>& system)
+ : _system(system),
_evaluating(NULL),
- _influence(system.varCount(), IdSet<Variable<T> >(system.varCount())),
- _stable(system.varCount()) {
- }
- virtual T& operator[] (const Variable<T>& x) const {
- if (_evaluating == NULL) {
- solve(x);
- return VariableAssignment<T>::_assignment[x.id()];
- } else {
- solve(x);
- _influence[x].insert(*_evaluating);
- return VariableAssignment<T>::_assignment[x.id()];
+ _values(system.variableCount(), -infinity<Domain>()),
+ _stable(system.variableCount()),
+ _haveValue(system.variableCount()),
+ _influence(system.variableCount(), IdSet<Variable<Domain> >(system.variableCount())),
+ _id(0) { }
+
+ const Domain& operator[](const Variable<Domain>& var) const {
+ _id++;
+ solve(var);
+ for (unsigned int i = 0; i < _id; ++i) {
+ std::cout << " ";
+ }
+ std::cout << "operator[] " << var.name() << " => " << _values[var] << std::endl;
+ _id--;
+ if (_evaluating) {
+ _influence[var].insert(*_evaluating);
}
+ return _values[var];
}
- void solve(const Variable<T>& x) const {
+
+ private:
+ void solve(const Variable<Domain>& x) const {
if (!_stable.contains(x)) {
_stable.insert(x);
+ for (unsigned int i = 0; i < _id; ++i) {
+ std::cout << " ";
+ }
+ std::cout << "solve(" << x.name() << ") " << &x << " " << _evaluating << std::endl;
+ std::cout << _stable << std::endl;
- const Variable<T>* oldEval = _evaluating;
+ const Variable<Domain>* oldEval = _evaluating;
_evaluating = &x;
- T t = _strategy(*_system[x], *this);
+ Domain val = _system[x]->eval(*this);
_evaluating = oldEval;
- if (t != VariableAssignment<T>::_assignment[x.id()]) {
- IdSet<Variable<T> > oldInfluence = _influence[x];
- _influence[x].clear(); // clear out our idea of what x influences
- VariableAssignment<T>::_assignment[x.id()] = t;
+ if (val != _values[x]) {
+ IdSet<Variable<Domain> > oldInfluence = _influence[x];
+ _influence[x].clear();
+ _values[x] = val;
- _stable.filter(oldInfluence); // whatever x influences needs to be re-evaluated
+ _stable.filter(oldInfluence);
- for (typename IdSet<Variable<T> >::iterator it = oldInfluence.begin();
+ for (typename IdSet<Variable<Domain> >::iterator it = oldInfluence.begin();
it != oldInfluence.end();
++it) {
- solve(*_system.getVar(*it));
+ solve(_system.variable(*it));
}
}
}
}
- private:
- const MaxStrategy<T>& _strategy;
- const EquationSystem<T>& _system;
- mutable const Variable<T>* _evaluating;
- mutable IdMap<Variable<T>, IdSet<Variable<T> > > _influence;
- mutable IdSet<Variable<T> > _stable;
+
+ const EquationSystem<Domain>& _system;
+ mutable const Variable<Domain>* _evaluating;
+ mutable IdMap<Variable<Domain>,Domain> _values;
+ mutable IdSet<Variable<Domain> > _stable;
+ mutable IdSet<Variable<Domain> > _haveValue;
+ mutable IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
+ mutable unsigned int _id;
};
- virtual VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat, const EquationSystem<T>& system) const {
- EvaluatingVariableAssignment assignment(strat, system);
- VariableAssignment<T> result(system.varCount());
- for (unsigned int i = 0; i < system.varCount(); ++i) {
- result[*system.getVar(i)] = assignment[*system.getVar(i)];
- }
- return result;
+ virtual VariableAssignment<Domain>* maxFixpoint(const EquationSystem<Domain>& system) const {
+ return new DynamicVariableAssignment(system);
}
};
diff --git a/impl/IdMap.hpp b/impl/IdMap.hpp
index b3a87fb..b265e37 100644
--- a/impl/IdMap.hpp
+++ b/impl/IdMap.hpp
@@ -58,7 +58,6 @@ struct IdMap {
return !(*this == other);
}
-
template<typename Q,typename Z>
friend std::ostream& operator<<(std::ostream& cout, const IdMap<Q, Z>& rho);
diff --git a/impl/IdSet.hpp b/impl/IdSet.hpp
index 6f6fd3f..8c64051 100644
--- a/impl/IdSet.hpp
+++ b/impl/IdSet.hpp
@@ -91,7 +91,7 @@ class IdSet {
void absorb(const IdSet& other) {
if (_length == other._length) {
- for (unsigned int i = 0; i < _length; ++i) {
+ for (unsigned int i = 0; i < DIV_ROUND_UP(_length, CELL_SIZE); ++i) {
_values[i] |= other._values[i];
}
} else {
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index aa49c9d..5d139fe 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -1,100 +1,129 @@
-#ifndef MAX_STRATEGY_HPP
-#define MAX_STRATEGY_HPP
+#ifndef MAX_EXPRESSION_HPP
+#define MAX_EXPRESSION_HPP
-#include <iostream>
#include "Expression.hpp"
#include "EquationSystem.hpp"
-#include "VariableAssignment.hpp"
-
-template<typename T>
-struct MaxStrategy {
- MaxStrategy()
- : _length(0), _assignment(NULL) { }
- MaxStrategy(unsigned int length)
- : _length(length), _assignment(new unsigned int[length]) {
- for (unsigned int i = 0; i < length; ++i) {
- _assignment[i] = 0;
+
+template<typename Domain>
+struct MaxStrategyExpression : public Expression<Domain> {
+ MaxStrategyExpression(const Expression<Domain>& expr, const IdMap<MaxExpression<Domain>,unsigned int>& strategy)
+ : _expr(expr), _strategy(strategy) { }
+
+ virtual Domain eval(const VariableAssignment<Domain>& rho) const {
+ // relies on implementation details - BAD BAD BAD, maybe
+ const OperatorExpression<Domain>* opExpr = dynamic_cast<const OperatorExpression<Domain>*>(&_expr);
+ if (opExpr) {
+ const MaxExpression<Domain>* maxExpr = dynamic_cast<const MaxExpression<Domain>*>(opExpr);
+ const std::vector<Expression<Domain>*> args = opExpr->arguments();
+ if (maxExpr) {
+ unsigned int i = _strategy[*maxExpr];
+ return MaxStrategyExpression(*args[i], _strategy).eval(rho);
+ } else {
+ std::vector<Domain> argumentValues;
+ for (typename std::vector<Expression<Domain>*>::const_iterator it = args.begin();
+ it != args.end();
+ ++it) {
+ argumentValues.push_back(MaxStrategyExpression(**it, _strategy).eval(rho));
+ }
+ return opExpr->op().eval(argumentValues);
+ }
+ } else {
+ return _expr.eval(rho);
}
}
- MaxStrategy(const MaxStrategy& other)
- : _length(other._length), _assignment(new unsigned int[other._length]) {
- for (unsigned int i = 0; i < other._length; ++i) {
- _assignment[i] = other._assignment[i];
- }
+
+ void print(std::ostream& cout) const {
+ cout << _expr;
}
+ private:
+ const Expression<Domain>& _expr;
+ const IdMap<MaxExpression<Domain>,unsigned int>& _strategy;
+};
- virtual ~MaxStrategy() {
- delete[] _assignment;
+template<typename Domain>
+struct MaxStrategy : public EquationSystem<Domain> {
+ MaxStrategy(const ConcreteEquationSystem<Domain>& system)
+ : _system(system), _expressions(system.variableCount(), NULL), _strategy(system.maxExpressionCount(), 0) {
}
- MaxStrategy<T>& operator=(const MaxStrategy& other) {
- if (_length != other._length) {
- _length = other._length;
- delete[] _assignment;
- _assignment = new unsigned int[_length];
- }
- for (unsigned int i = 0; i < _length; ++i) {
- _assignment[i] = other._assignment[i];
+ const Expression<Domain>* operator[](const Variable<Domain>& v) const {
+ if (_expressions[v] == NULL) {
+ Expression<Domain>* expression = new MaxStrategyExpression<Domain>(*_system[v], _strategy);
+ _expressions[v] = expression;
+ return expression;
+ } else {
+ return _expressions[v];
}
- return *this;
}
- const unsigned int& operator[] (const MaxExpression<T> x) const {
- if (x.id() >= _length) {
- throw "Array out of bounds";
- }
- return _assignment[x.id()];
+ unsigned int get(const MaxExpression<Domain>& e) const {
+ return _strategy[e];
+ }
+ unsigned int set(const MaxExpression<Domain>& e, unsigned int i) {
+ _strategy[e] = i;
+ return i;
}
- unsigned int& operator[] (const MaxExpression<T>& x) {
- if (x.id() >= _length) {
- throw "Array out of bounds";
+
+ VariableAssignment<Domain>* eval(const VariableAssignment<Domain>& rho) const {
+ StableVariableAssignment<Domain>* result = this->assignment(-infinity<Domain>());
+ for (unsigned int i = 0, length = _system.variableCount();
+ i < length;
+ ++i) {
+ const Variable<Domain>& var = _system.variable(i);
+ const Expression<Domain>& expr = * (*this)[var];
+ (*result)[var] = expr.eval(rho);
}
- return _assignment[x.id()];
+ return result;
}
- VariableAssignment<T> operator() (const EquationSystem<T>& eqns, const VariableAssignment<T>& rho) const {
- return eqns.foreach(*this, rho);
+
+ unsigned int variableCount() const {
+ return _system.variableCount();
}
- T operator() (const Expression<T>& expr, const VariableAssignment<T>& rho) const {
- const MaxExpression<T>* max = dynamic_cast<const MaxExpression<T>*>(&expr);
- if (max == NULL) {
- return expr(rho);
- } else {
- return (*this)(*max->argument(_assignment[max->id()]), rho);
- }
+
+ Variable<Domain>& variable(unsigned int i) const {
+ return _system.variable(i);
}
- MaxStrategy<T> improve(const EquationSystem<T>& s, const VariableAssignment<T>& rho) const {
- MaxStrategy<T> newStrategy(*this);
- for (unsigned int i = 0; i < _length; ++i) {
- const MaxExpression<T>& expr = *s.getMax(i);
- const T oldValue = (*this)(expr, rho);
-
- // this relies on the fact that deeper MaxExpressions have a lower id
- // than the MaxExpressions containing them. This means that we know that
- // we have enough of a strategy to work with what we have within us
- std::pair<const T,unsigned int> best = expr.bestStrategy(rho, newStrategy);
-
- if (best.first > oldValue)
- newStrategy[expr] = best.second;
- }
- return newStrategy;
+
+ StableVariableAssignment<Domain>* assignment(const Domain& v) const {
+ return _system.assignment(v);
+ }
+
+ bool equalAssignments(const VariableAssignment<Domain>& l, const VariableAssignment<Domain>& r) const {
+ return _system.equalAssignments(l, r);
}
- bool operator== (const MaxStrategy& other) const {
- if (_length != other._length)
- return false;
- for (unsigned int i = 0; i < _length; ++i) {
- if (_assignment[i] != other._assignment[i]) {
- return false;
+ void improve(const VariableAssignment<Domain>& rho) {
+ for (unsigned int i = 0, length = _system.maxExpressionCount();
+ i < length;
+ ++i) {
+ MaxExpression<Domain>& expr = _system.maxExpression(i);
+ Domain bestValue = MaxStrategyExpression<Domain>(expr, _strategy).eval(rho);
+ unsigned int bestIndex = this->get(expr);
+
+ // this relies on the fact that an expression will only be proessed after the expressions
+ // it depends on (which should always be true)
+ const std::vector<Expression<Domain>*> args = expr.arguments();
+ for (unsigned int j = 0, length = args.size();
+ j < length;
+ ++j) {
+ const Domain value = MaxStrategyExpression<Domain>(*args[j], _strategy).eval(rho);
+ if (bestValue < value) {
+ bestValue = value;
+ bestIndex = j;
+ }
}
+ this->set(expr, bestIndex);
}
- return true;
}
- bool operator!= (const MaxStrategy& other) const {
- return !(*this == other);
+
+ void print(std::ostream& cout) const {
+ cout << _system << std::endl;
}
+
private:
- unsigned int _length;
- unsigned int* _assignment;
+ const ConcreteEquationSystem<Domain>& _system;
+ mutable IdMap<Variable<Domain>,Expression<Domain>*> _expressions;
+ IdMap<MaxExpression<Domain>,unsigned int> _strategy;
};
#endif
diff --git a/impl/Operator.hpp b/impl/Operator.hpp
index 5f7cd1e..3072abe 100644
--- a/impl/Operator.hpp
+++ b/impl/Operator.hpp
@@ -1,116 +1,126 @@
#ifndef OPERATOR_HPP
#define OPERATOR_HPP
-template<typename T>
-T infinity() { }
-template<>
-float infinity() {
- return INFINITY;
-}
-
#include <vector>
-#include "IdSet.hpp"
-
-template<typename T>
-struct Variable;
-
-template<typename T>
-struct VariableAssignment;
-template<typename T>
-struct Expression;
-template<typename T>
+template<typename Domain>
struct Operator {
virtual ~Operator() { }
- virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& rho) const = 0;
+
+ virtual Domain eval(const std::vector<Domain>&) const = 0;
+
+ virtual void print(std::ostream&) const = 0;
};
-template<typename T>
-struct Maximum : public Operator<T> {
- virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment) const {
- T value = -infinity<T>();
- for (typename std::vector< Expression<T>* >::const_iterator it = args.begin();
- it != args.end();
+
+template<typename Domain>
+struct Maximum : public Operator<Domain> {
+ virtual Domain eval(const std::vector<Domain>& arguments) const {
+ Domain result = -infinity<Domain>();
+ for (typename std::vector<Domain>::const_iterator it = arguments.begin();
+ it != arguments.end();
++it) {
- T temporary = (**it)(assignment);
- value = (temporary > value ? temporary : value);
- //if (value == infinity<T>()) break;
+ result = (result < *it ? *it : result);
}
- return value;
+ return result;
+ }
+ void print(std::ostream& cout) const {
+ cout << "max";
}
};
-template<typename T>
-struct Minimum : public Operator<T> {
- virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment) const {
- T value = infinity<T>();
- for (typename std::vector< Expression<T>* >::const_iterator it = args.begin();
- it != args.end();
+
+template<typename Domain>
+struct Minimum : public Operator<Domain> {
+ virtual Domain eval(const std::vector<Domain>& arguments) const {
+ Domain result = infinity<Domain>();
+ for (typename std::vector<Domain>::const_iterator it = arguments.begin();
+ it != arguments.end();
++it) {
- T temporary = (**it)(assignment);
- value = (temporary < value ? temporary : value);
- //if (value == -infinity<T>()) break;
+ result = (*it < result ? *it : result);
}
- return value;
+ return result;
+ }
+ void print(std::ostream& cout) const {
+ cout << "min";
}
};
-template<typename T>
-struct Constant : public Operator<T> {
- Constant(const T& val)
- : _value(val) { }
- T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
- return _value;
+template<typename Domain>
+struct Negation : public Operator<Domain> {
+ virtual Domain eval(const std::vector<Domain>& arguments) const {
+ if (arguments.size() > 1)
+ throw "Too many arguments to a negation.";
+ return -arguments[0];
+ }
+ void print(std::ostream& cout) const {
+ cout << "-";
}
- private:
- const T _value;
};
-template<typename T>
-struct Addition: public Operator<T> {
- T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
- T sum = (*args[0])(ass);
- for (unsigned int i = 1, size = args.size(); i < size; ++i) {
- sum += (*args[i])(ass);
+template<typename Domain>
+struct Addition : public Operator<Domain> {
+ virtual Domain eval(const std::vector<Domain>& arguments) const {
+ Domain result = 0;
+ for (typename std::vector<Domain>::const_iterator it = arguments.begin();
+ it != arguments.end();
+ ++it) {
+ result += *it;
}
- return sum;
+ return result;
+ }
+ void print(std::ostream& cout) const {
+ cout << "add";
}
};
-template<typename T>
-struct Subtraction: public Operator<T> {
- T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
- T sum = (*args[0])(ass);
- for (unsigned int i = 1, size = args.size(); i < size; ++i) {
- sum -= (*args[i])(ass);
+template<typename Domain>
+struct Subtraction : public Operator<Domain> {
+ virtual Domain eval(const std::vector<Domain>& arguments) const {
+ Domain result = 0;
+ for (typename std::vector<Domain>::const_iterator it = arguments.begin();
+ it != arguments.end();
+ ++it) {
+ if (it == arguments.begin())
+ result = *it;
+ else
+ result -= *it;
}
- return sum;
+ return result;
+ }
+ void print(std::ostream& cout) const {
+ cout << "sub";
}
};
-template<typename T>
-struct Comma: public Operator<T> {
- T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
- if ((*args[0])(ass) == -infinity<T>()) {
- std::cout << "Comma - neg inf" << std::endl;
- return -infinity<T>();
- } else {
- std::cout << "Comma - finite" << std::endl;
- return (*args[1])(ass);
+template<typename Domain>
+struct Comma : public Operator<Domain> {
+ virtual Domain eval(const std::vector<Domain>& arguments) const {
+ if (arguments[0] == -infinity<Domain>()) {
+ return -infinity<Domain>();
}
+ return arguments[1];
+ }
+ void print(std::ostream& cout) const {
+ cout << "comma";
}
};
-template<typename T>
-struct Guard: public Operator<T> {
- T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
- if ((*args[0])(ass) < (*args[1])(ass)) {
- return -infinity<T>();
- } else {
- return (*args[2])(ass);
+template<typename Domain>
+struct Guard : public Operator<Domain> {
+ virtual Domain eval(const std::vector<Domain>& arguments) const {
+ if (arguments[0] < arguments[1]) {
+ return -infinity<Domain>();
}
+ return arguments[2];
+ }
+ void print(std::ostream& cout) const {
+ cout << "guard";
}
};
-#include "VariableAssignment.hpp"
-#include "Expression.hpp"
+template<typename T>
+std::ostream& operator<<(std::ostream& cout, const Operator<T>& op) {
+ op.print(cout);
+ return cout;
+}
#endif
diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index 9d8137a..e0f7dc8 100644
--- a/impl/VariableAssignment.hpp
+++ b/impl/VariableAssignment.hpp
@@ -1,17 +1,29 @@
#ifndef VARIABLE_ASSIGNMENT_HPP
#define VARIABLE_ASSIGNMENT_HPP
-#include "Variable.hpp"
+#include "Expression.hpp"
#include "IdMap.hpp"
-template<typename T>
-struct VariableAssignment : public IdMap<Variable<T>,T> {
- VariableAssignment(unsigned int length)
- : IdMap<Variable<T>,T>(length, -infinity<T>()) { }
- VariableAssignment(unsigned int length, const T& initial)
- : IdMap<Variable<T>,T>(length, initial) { }
- VariableAssignment(const VariableAssignment& other)
- : IdMap<Variable<T>,T>(other) { }
+template<typename Domain>
+struct VariableAssignment {
+ virtual ~VariableAssignment() { }
+ virtual const Domain& operator[](const Variable<Domain>&) const = 0;
+};
+
+template<typename Domain>
+struct StableVariableAssignment
+: public VariableAssignment<Domain>, public IdMap<Variable<Domain>, Domain> {
+ StableVariableAssignment(unsigned int length)
+ : IdMap<Variable<Domain>,Domain>(length, -infinity<Domain>()) { }
+ StableVariableAssignment(unsigned int length, const Domain& value)
+ : IdMap<Variable<Domain>,Domain>(length, value) { }
+
+ const Domain& operator[](const Variable<Domain>& var) const {
+ return IdMap<Variable<Domain>,Domain>::operator[](var);
+ }
+ Domain& operator[](const Variable<Domain>& var) {
+ return IdMap<Variable<Domain>,Domain>::operator[](var);
+ }
};
#endif
diff --git a/impl/main.cpp b/impl/main.cpp
index 530556f..b03a4f2 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -1,15 +1,12 @@
#include <iostream>
#include <vector>
-#include <map>
-#include <string>
#include <sstream>
-#include <math.h>
-
-#include "Operator.hpp"
+#include "Complete.hpp"
#include "Expression.hpp"
-#include "MaxStrategy.hpp"
+#include "Operator.hpp"
#include "EquationSystem.hpp"
-#include "Complete.hpp"
+#include "MaxStrategy.hpp"
+#include "FixpointAlgorithm.hpp"
extern "C" {
#include "EquationSystemParser.h"
@@ -19,36 +16,35 @@ extern "C" {
using namespace std;
template<typename T>
-Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
+Expression<T>& treeToExpression(pANTLR3_BASE_TREE node, ConcreteEquationSystem<T>& system) {
ANTLR3_UINT32 num = node->getChildCount(node);
-
string name = (char*) node->getText(node)->chars;
- // leaf node - constant or variable
if (num == 0) {
+ // leaf node -> constant or variable
if (name == "inf") {
- return system.newExpression(new Constant<T>(infinity<T>()));
+ return system.constant(infinity<T>());
} else {
stringstream stream(name);
T output;
if (stream >> output) {
- return system.newExpression(new Constant<T>(output));
+ return system.constant(output);
} else {
- return system.newExpression(system.newVariable(name));
+ return system.variable(name);
}
}
}
- // other operators
+ // anything that's not a constant/variable
std::vector<Expression<T>*> args;
pANTLR3_BASE_TREE childNode;
for (unsigned int i = 0; i < num; ++i) {
childNode = (pANTLR3_BASE_TREE) node->getChild(node, i);
- args.push_back(treeToExpression(childNode, system));
+ args.push_back(&treeToExpression(childNode, system));
}
if (name == "max") {
- return system.newMaxExpression(args);
+ return system.maxExpression(args);
} else {
Operator<T>* op = NULL;
if (name == "min") {
@@ -56,21 +52,24 @@ Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& syste
} else if (name == "+") {
op = new Addition<T>();
} else if (name == "-") {
- op = new Subtraction<T>();
+ if (args.size() == 1) {
+ op = new Negation<T>();
+ } else {
+ op = new Subtraction<T>();
+ }
} else if (name == ";") {
op = new Comma<T>();
} else if (name == "GUARD") {
op = new Guard<T>();
} else {
- std::cerr << "Unknown leaf node type: " << name << std::endl;
- throw "Unknown leaf node type";
+ throw "Parse error: Unknown operator";
}
- return system.newExpression(op, args);
+ return system.expression(op, args);
}
}
template<typename T>
-void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
+void treeToSystem(pANTLR3_BASE_TREE node, ConcreteEquationSystem<T>& system) {
ANTLR3_UINT32 num = node->getChildCount(node);
if (num % 2 == 1)
@@ -83,12 +82,12 @@ void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
exprNode = (pANTLR3_BASE_TREE) node->getChild(node, i+1);
string varName = (char*) varNode->getText(varNode)->chars;
- Variable<T>* var = system.newVariable(varName);
+ Variable<T>& var = system.variable(varName);
vector<Expression<T>*> args;
- args.push_back(system.newExpression(new Constant<T>(-infinity<T>())));
- args.push_back(treeToExpression(exprNode, system));
- system[*var] = system.newMaxExpression(args);
+ args.push_back(&system.constant(-infinity<T>()));
+ args.push_back(&treeToExpression(exprNode, system));
+ system[var] = &system.maxExpression(args);
}
}
@@ -96,11 +95,11 @@ typedef Complete<int> ZBar;
int main (int argc, char* argv[]) {
FixpointAlgorithm<ZBar>* algorithm = NULL;
if (argc > 2 && !strcmp(argv[2], "naive")) {
- algorithm = new NaiveFixpoint<ZBar>();
+ algorithm = new NaiveFixpointAlgorithm<ZBar>();
cout << "Naive fixpoint" << endl;
} else {
- algorithm = new RecursiveFixpoint<ZBar>();
- cout << "Recursive fixpoint" << endl;
+ algorithm = new SmartFixpointAlgorithm<ZBar>();
+ cout << "Smart fixpoint" << endl;
}
pANTLR3_INPUT_STREAM input;
@@ -115,16 +114,33 @@ int main (int argc, char* argv[]) {
EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
- EquationSystem<ZBar> system;
+ ConcreteEquationSystem<ZBar> system;
treeToSystem<ZBar>(ret.tree, system);
// DO MORE HERE
- VariableAssignment<ZBar> rho = system.minFixpoint(*algorithm);
- std::cout << rho << std::endl;
+ cout << system << endl;
+ VariableAssignment<ZBar>* prev = NULL;
+ VariableAssignment<ZBar>* result = system.assignment(-infinity<ZBar>());
+ MaxStrategy<ZBar> strategy(system);
+ do {
+ if (prev) delete prev;
+ prev = result;
+ strategy.improve(*prev);
+ for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+ Variable<ZBar>& var = system.variable(i);
+ cout << var.name() << " = " << (*result)[var] << ", ";
+ }
+ cout << endl;
+ result = algorithm->maxFixpoint(strategy);
+ } while(!system.equalAssignments(*prev, *result));
+ if (prev) delete prev;
+
+ VariableAssignment<ZBar>* rho = result;
- const std::vector<Variable<ZBar>*> vars = system.vars();
- for (unsigned int i = 0, size = vars.size(); i < size; ++i) {
- cout << vars[i]->name() << " = " << rho[*vars[i]] << endl;
+ cout << endl;
+ for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+ Variable<ZBar>& var = system.variable(i);
+ cout << var.name() << " = " << (*rho)[var] << endl;
}
parser -> free(parser);
generated by cgit v1.2.3 (git 2.46.2) at 2024-12-25 07:10:52 +0000