summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--impl/Complete.hpp7
-rw-r--r--impl/EquationSystem.g10
-rw-r--r--impl/EquationSystem.hpp208
-rw-r--r--impl/Expression.hpp154
-rw-r--r--impl/FixpointAlgorithm.hpp125
-rw-r--r--impl/IdMap.hpp1
-rw-r--r--impl/IdSet.hpp2
-rw-r--r--impl/MaxStrategy.hpp218
-rw-r--r--impl/Operator.hpp173
-rw-r--r--impl/Variable.hpp35
-rw-r--r--impl/VariableAssignment.hpp30
-rw-r--r--impl/main.cpp217
-rw-r--r--impl/systems/constant-system.eqns1
-rw-r--r--impl/systems/example.eqns (renamed from impl/systems/size-ten)0
-rw-r--r--impl/systems/generate-fib.py6
-rw-r--r--impl/systems/generate-long.py (renamed from impl/antlr/generate.py)0
-rw-r--r--impl/systems/generate-random.py (renamed from impl/systems/generate-system.py)0
-rw-r--r--impl/systems/long-fib.eqns1001
-rw-r--r--impl/systems/long-fixpoint.eqns (renamed from impl/systems/long-fixpoint)0
-rw-r--r--impl/systems/min-test3
-rw-r--r--impl/systems/minimal.eqns (renamed from impl/systems/small)0
-rw-r--r--impl/systems/random-system1
22 files changed, 1625 insertions, 567 deletions
diff --git a/impl/Complete.hpp b/impl/Complete.hpp
index 64b850a..11f2f83 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) {
@@ -76,7 +81,7 @@ struct Complete {
return other._infinity && ((_value < 0 && other._value < 0) ||
(_value > 0 && other._value > 0));
} else {
- return _value == other._value;
+ return !other._infinity && (_value == other._value);
}
}
bool operator!=(const Complete& other) const {
diff --git a/impl/EquationSystem.g b/impl/EquationSystem.g
index 6b721bb..3a6598a 100644
--- a/impl/EquationSystem.g
+++ b/impl/EquationSystem.g
@@ -11,7 +11,6 @@ tokens {
SUB = '-' ;
MULT = '*' ;
COMMA = ';' ;
- RANGE = 'range' ;
GUARD = 'guard' ;
GREATER_EQUAL = '>=' ;
QUESTION_MARK = '?' ;
@@ -27,15 +26,14 @@ maxExpr : MAXIMUM^ '('! minExpr ( ','! minExpr )* ')'! | minExpr ;
minExpr : MINIMUM^ '('! maxExpr ( ','! maxExpr )* ')'! | expr ;
expr : '(' expr GREATER_EQUAL expr QUESTION_MARK expr ')' -> ^(GUARD expr expr expr)
- | term ( (PLUS | MULT | COMMA)^ expr )* ;
+ | term ( (PLUS | MULT | SUB | COMMA)^ expr )* ;
-term : '[' NUMBER ',' NUMBER ']' -> ^( RANGE NUMBER NUMBER )
+term : NUMBER
| VARIABLE
- | '('! expr ')'!
- | SUB^ term ;
+ | '('! expr ')'! ;
-NUMBER : (SUB) (DIGIT)+ | (DIGIT)+ ;
+NUMBER : (DIGIT)+ ;
VARIABLE: (LETTER) (LETTER | DIGIT)* ;
WHITESPACE : ( '\t' | ' ' | '\u000C' )+
{
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 3c84d30..7fc4542 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -1,89 +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 T operator() (const VariableAssignment<T>& assignment) const {
- return (*_operator)(_arguments, assignment);
+ 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;
}
- template<typename Z>
- friend std::ostream& operator<<(std::ostream&, const Expression<Z>&);
+ void print(std::ostream& cout) const {
+ cout << _value << "!c";
+ }
- 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);
- }
- Expression<T>* argument(unsigned int i) const {
- if (i >= Expression<T>::_arguments.size()) {
- throw "Error";
- }
- return Expression<T>::_arguments[i];
+ std::string name() const {
+ return _name;
}
- virtual T operator() (const VariableAssignment<T>& assignment) const {
- throw "error";
+
+ virtual Domain eval(const VariableAssignment<Domain>& rho) const {
+ return rho[*this];
}
- 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 (best.first < value)
- best = std::pair<T, unsigned int>(value, i);
- }
- std::cerr << "Best strategy: (" << best.first << ", " << best.second << ")" << std::endl;
- return best;
+
+ void print(std::ostream& cout) const {
+ cout << _name << "!v";
}
+
private:
- unsigned int _id;
+ const unsigned int _id;
+ const std::string _name;
};
-template<typename T>
-std::ostream& operator<<(std::ostream& cout, const Expression<T>& expr) {
- if (expr._arguments.size() == 0) {
- cout << expr._operator->op_name;
- } else {
- cout << expr._operator->op_name << "(";
- for (typename std::vector<Expression<T>*>::const_iterator it = expr._arguments.begin();
- it != expr._arguments.end();
+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) {
- cout << (it == expr._arguments.begin() ? "" : ", ");
- cout << **it;
+ argumentValues.push_back((*it)->eval(rho));
+ }
+ return _operator.eval(argumentValues);
+ }
+
+ const std::vector<Expression<Domain>*> arguments() const {
+ return _arguments;
+ }
+
+ const Operator<Domain>& op() const {
+ return _operator;
+ }
+
+ 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];
}
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:
+ const unsigned int _id;
+};
+
+template<typename T>
+std::ostream& operator<<(std::ostream& cout, const Expression<T>& exp) {
+ exp.print(cout);
return cout;
}
-#include "Variable.hpp"
-#include "MaxStrategy.hpp"
+#include "VariableAssignment.hpp"
#endif
diff --git a/impl/FixpointAlgorithm.hpp b/impl/FixpointAlgorithm.hpp
index ed97bec..b39a915 100644
--- a/impl/FixpointAlgorithm.hpp
+++ b/impl/FixpointAlgorithm.hpp
@@ -1,97 +1,92 @@
#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 Domain>
+struct SmartFixpointAlgorithm : public FixpointAlgorithm<Domain> {
+ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
+ DynamicVariableAssignment(const EquationSystem<Domain>& system)
+ : _system(system),
+ _values(system.variableCount(), infinity<Domain>()),
+ _stable(system.variableCount()),
+ _influence(system.variableCount(), IdSet<Variable<Domain> >(system.variableCount())) { }
-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),
- _evaluating(NULL),
- _influence(system.varCount(), IdSet<Variable<T> >(system.varCount())),
- _stable(system.varCount()) {
+ const Domain& operator[](const Variable<Domain>& var) const {
+ solve(var);
+ //std::cout << _values << std::endl;
+ return _values[var];
}
- 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()];
- }
- }
- void solve(const Variable<T>& x) const {
+
+ private:
+
+ void solve(const Variable<Domain>& x) const {
if (!_stable.contains(x)) {
_stable.insert(x);
- const Variable<T>* oldEval = _evaluating;
- _evaluating = &x;
- T t = _strategy(*_system[x], *this);
- _evaluating = oldEval;
+ Domain val = _system[x]->eval(DependencyAssignment(*this, x));
- 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;
+
+ struct DependencyAssignment : public VariableAssignment<Domain> {
+ DependencyAssignment(const DynamicVariableAssignment& assignment, const Variable<Domain>& var)
+ : _assignment(assignment), _var(var) { }
+ const Domain& operator[](const Variable<Domain>& x) const {
+ const Domain& result = _assignment[x];
+ _assignment._influence[x].insert(_var);
+ return result;
+ }
+ private:
+ const DynamicVariableAssignment& _assignment;
+ const Variable<Domain>& _var;
+ };
+
+ const EquationSystem<Domain>& _system;
+ mutable IdMap<Variable<Domain>,Domain> _values;
+ mutable IdSet<Variable<Domain> > _stable;
+ mutable IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
};
- 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..2be9f4c 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -1,100 +1,172 @@
-#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];
+ ~MaxStrategy() {
+ for (int i = 0, length = _system.variableCount();
+ i < length;
+ ++i) {
+ Expression<Domain>* expr = _expressions[_system.variable(i)];
+ if (expr)
+ delete expr;
}
- return *this;
}
- const unsigned int& operator[] (const MaxExpression<T> x) const {
- if (x.id() >= _length) {
- throw "Array out of bounds";
+ 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 _assignment[x.id()];
}
- unsigned int& operator[] (const MaxExpression<T>& x) {
- if (x.id() >= _length) {
- throw "Array out of bounds";
- }
- return _assignment[x.id()];
+
+ unsigned int get(const MaxExpression<Domain>& e) const {
+ return _strategy[e];
}
- VariableAssignment<T> operator() (const EquationSystem<T>& eqns, const VariableAssignment<T>& rho) const {
- return eqns.foreach(*this, rho);
+ unsigned int set(const MaxExpression<Domain>& e, unsigned int i) {
+ _strategy[e] = i;
+ return i;
}
- 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);
+
+ 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 result;
}
- 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;
+
+ unsigned int variableCount() const {
+ return _system.variableCount();
}
- 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;
+ Variable<Domain>& variable(unsigned int i) const {
+ return _system.variable(i);
+ }
+
+ 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);
+ }
+
+
+ struct ImprovementOperator {
+ virtual ~ImprovementOperator() { }
+ virtual bool improve(MaxStrategy<Domain>&, const VariableAssignment<Domain>&) const = 0;
+ };
+ bool improve(const ImprovementOperator& op, const VariableAssignment<Domain>& rho) {
+ return op.improve(*this, rho);
+ }
+
+ struct NaiveImprovementOperator : public ImprovementOperator {
+ bool improve(MaxStrategy<Domain>& strat, const VariableAssignment<Domain>& rho) const {
+ bool changed = false;
+ for (unsigned int i = 0, length = strat._system.maxExpressionCount();
+ i < length;
+ ++i) {
+ MaxExpression<Domain>& expr = strat._system.maxExpression(i);
+ Domain bestValue = MaxStrategyExpression<Domain>(expr, strat._strategy).eval(rho);
+ unsigned int lastIndex= strat.get(expr);
+ unsigned int bestIndex = strat.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, as they form a DAG)
+ 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], strat._strategy).eval(rho);
+ if (bestValue < value) {
+ bestValue = value;
+ bestIndex = j;
+ }
+ }
+ if (bestIndex != lastIndex) {
+ changed = true;
+ strat.set(expr, bestIndex);
+ }
}
+ return changed;
}
- return true;
- }
- bool operator!= (const MaxStrategy& other) const {
- return !(*this == other);
+ };
+
+ struct RepeatedImprovementOperator : public ImprovementOperator {
+ RepeatedImprovementOperator(const ImprovementOperator& op)
+ : _subImprovement(op) { }
+ bool improve(MaxStrategy<Domain>& strat, const VariableAssignment<Domain>& rho) const {
+ if (_subImprovement.improve(strat, rho)) {
+ VariableAssignment<Domain>* rho2 = strat.eval(rho);
+ improve(strat, *rho2);
+ delete rho2;
+ return true;
+ }
+ return false;
+ }
+ private:
+ const ImprovementOperator& _subImprovement;
+ };
+
+ 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 87e4eea..3072abe 100644
--- a/impl/Operator.hpp
+++ b/impl/Operator.hpp
@@ -1,121 +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 {
- Operator(const std::string& name) : op_name(name) { }
virtual ~Operator() { }
- virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& rho) const = 0;
- const std::string op_name;
+
+ virtual Domain eval(const std::vector<Domain>&) const = 0;
+
+ virtual void print(std::ostream&) const = 0;
};
-template<typename T>
-struct Maximum : public Operator<T> {
- Maximum() : Operator<T>("max") { }
- 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 = (value < temporary ? value : temporary);
- //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> {
- Minimum() : Operator<T>("min") { }
- 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 std::string& value, const T& val)
- : Operator<T>(value), _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> {
- Addition() : Operator<T>("add") { }
- 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 Negate: public Operator<T> {
- Negate() : Operator<T>("neg") { }
- T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
- // assert(args.size() == 1);
- return -(*args[0])(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 result;
+ }
+ void print(std::ostream& cout) const {
+ cout << "sub";
}
};
-template<typename T>
-struct Comma: public Operator<T> {
- Comma() : Operator<T>("comma") { }
- 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> {
- Guard() : Operator<T>("guard") { }
- 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/Variable.hpp b/impl/Variable.hpp
deleted file mode 100644
index 35a3991..0000000
--- a/impl/Variable.hpp
+++ /dev/null
@@ -1,35 +0,0 @@
-#ifndef VARIABLE_HPP
-#define VARIABLE_HPP
-
-#include <string>
-#include "Operator.hpp"
-
-template<typename T>
-struct Variable : public Operator<T> {
- Variable(unsigned int id, const std::string& name)
- : Operator<T>(name), _id(id), _name(name) { }
- Variable(const Variable& other)
- : Operator<T>(name), _id(other._id) { }
- unsigned int id() const {
- return _id;
- }
- std::string name() const {
- return _name;
- }
- //T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
- virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment) const {
- //assert(args.size() == 0)
- return assignment[*this];
- }
- private:
- const unsigned int _id;
- const std::string _name;
-};
-
-template<typename T>
-std::ostream& operator<<(std::ostream& cout, const Variable<T>& v) {
- cout << v.name() << "(" << v.id() << ")";
- 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 2006565..6546444 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,124 +16,60 @@ extern "C" {
using namespace std;
template<typename T>
-std::pair<Expression<T>*, Expression<T>*> treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system, bool negative=false) {
+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 - variable
if (num == 0) {
- if (negative) {
- vector<Expression<T>*> firstArgs;
- firstArgs.push_back(system.newExpression(system.newVariable(name + "_u")));
- vector<Expression<T>*> secondArgs;
- secondArgs.push_back(system.newExpression(system.newVariable(name + "_l")));
- return std::pair<Expression<T>*, Expression<T>*>(
- system.newExpression(new Negate<T>(),
- firstArgs),
- system.newExpression(new Negate<T>(),
- secondArgs));
+ // leaf node -> constant or variable
+ if (name == "inf") {
+ return system.constant(infinity<T>());
} else {
- return std::pair<Expression<T>*, Expression<T>*>(
- system.newExpression(system.newVariable(name + "_l")),
- system.newExpression(system.newVariable(name + "_u")));
+ stringstream stream(name);
+ T output;
+ if (stream >> output) {
+ return system.constant(output);
+ } else {
+ return system.variable(name);
+ }
}
}
- // a range itself
- if (name == "RANGE") {
- pANTLR3_BASE_TREE childNode;
- string childName;
- T firstValue, secondValue;
-
- childNode = (pANTLR3_BASE_TREE) node->getChild(node, 0);
- childName = (char*) childNode->getText(childNode)->chars;
- stringstream firstStream(childName);
- if (!(firstStream >> firstValue)) {
- throw "Invalid number.";
- }
- string firstChildName = childName;
-
- childNode = (pANTLR3_BASE_TREE) node->getChild(node, 1);
- childName = (char*) childNode->getText(childNode)->chars;
- stringstream secondStream(childName);
- if (!(secondStream >> secondValue)) {
- throw "Invalid number.";
- }
- string secondChildName = childName;
-
- if (negative) {
- T temp = firstValue;
- string tempname = firstChildName;
-
- firstValue = -secondValue;
- firstChildName = "-" + secondChildName;
-
- secondValue = -temp;
- secondChildName = "-" + tempname;
- }
-
- return std::pair<Expression<T>*, Expression<T>*>(
- system.newExpression(new Constant<T>(firstChildName, firstValue)),
- system.newExpression(new Constant<T>(secondChildName, secondValue)));
- }
-
- if (name == "-") {
- negative = true;
- }
-
- // subexpressions
- std::vector<Expression<T>*> firstArgs;
- std::vector<Expression<T>*> secondArgs;
+ // 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);
- std::pair<Expression<T>*, Expression<T>*> expr = treeToExpression(childNode, system, negative);
- firstArgs.push_back(expr.first);
- secondArgs.push_back(expr.second);
- }
-
- // other operators
- if (name == "-") {
- //if (firstArgs.size() == 1) { // secondArgs.size() == firstArgs.size()
- return std::pair<Expression<T>*, Expression<T>*>(
- firstArgs[0],
- secondArgs[0]);
+ args.push_back(&treeToExpression(childNode, system));
}
if (name == "max") {
- return std::pair<Expression<T>*, Expression<T>*>(
- system.newMaxExpression(firstArgs),
- system.newMaxExpression(secondArgs));
+ return system.maxExpression(args);
} else {
- // we need two because expressions delete their operator
- // bit of a silly design by me
- Operator<T>* firstOp = NULL;
- Operator<T>* secondOp = NULL;
+ Operator<T>* op = NULL;
if (name == "min") {
- firstOp = new Minimum<T>();
- secondOp = new Minimum<T>();
+ op = new Minimum<T>();
} else if (name == "+") {
- firstOp = new Addition<T>();
- secondOp = new Addition<T>();
+ op = new Addition<T>();
+ } else if (name == "-") {
+ if (args.size() == 1) {
+ op = new Negation<T>();
+ } else {
+ op = new Subtraction<T>();
+ }
} else if (name == ";") {
- firstOp = new Comma<T>();
- secondOp = new Comma<T>();
+ op = new Comma<T>();
} else if (name == "GUARD") {
- firstOp = new Guard<T>();
- secondOp = new Guard<T>();
+ 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 std::pair<Expression<T>*, Expression<T>*>(
- system.newExpression(firstOp, firstArgs),
- system.newExpression(secondOp, secondArgs));
+ 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)
@@ -148,36 +81,45 @@ void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
varNode = (pANTLR3_BASE_TREE) node->getChild(node, i);
exprNode = (pANTLR3_BASE_TREE) node->getChild(node, i+1);
- Variable<T>* var;
- vector<Expression<T>*> args;
-
string varName = (char*) varNode->getText(varNode)->chars;
- std::pair<Expression<T>*, Expression<T>*> exprs = treeToExpression(exprNode, system);
-
- var = system.newVariable(varName + "_l");
- args.push_back(system.newExpression(new Constant<T>("-inf", -infinity<T>())));
- args.push_back(exprs.first);
- system[*var] = system.newMaxExpression(args);
- std::cout << var->op_name << " = " << *system[*var] << std::endl;
-
- args.clear();
- var = system.newVariable(varName + "_u");
- args.push_back(system.newExpression(new Constant<T>("-inf", -infinity<T>())));
- args.push_back(exprs.second);
- system[*var] = system.newMaxExpression(args);
- std::cout << var->op_name << " = " << *system[*var] << std::endl;
+ Variable<T>& var = system.variable(varName);
+
+ vector<Expression<T>*> args;
+ args.push_back(&system.constant(-infinity<T>()));
+ args.push_back(&treeToExpression(exprNode, system));
+ system[var] = &system.maxExpression(args);
}
}
typedef Complete<int> ZBar;
int main (int argc, char* argv[]) {
+ if (argc <= 3) {
+ cout << "Usage: " << argv[0] << " filename naive|smart naive|repeat" << endl;
+ exit(1);
+ }
FixpointAlgorithm<ZBar>* algorithm = NULL;
- if (argc > 2 && !strcmp(argv[2], "naive")) {
- algorithm = new NaiveFixpoint<ZBar>();
+ if (!strcmp(argv[2], "naive")) {
+ algorithm = new NaiveFixpointAlgorithm<ZBar>();
cout << "Naive fixpoint" << endl;
+ } else if (!strcmp(argv[2], "smart")) {
+ algorithm = new SmartFixpointAlgorithm<ZBar>();
+ cout << "Smart fixpoint" << endl;
+ } else {
+ cout << "Unknown fixpoint algorithm." << endl;
+ }
+ MaxStrategy<ZBar>::ImprovementOperator* naiveImprovement = new MaxStrategy<ZBar>::NaiveImprovementOperator();
+ MaxStrategy<ZBar>::ImprovementOperator* improvement = NULL;
+ if (!strcmp(argv[3], "repeat")) {
+ improvement = new MaxStrategy<ZBar>::RepeatedImprovementOperator(*naiveImprovement);
+ cout << "Repeated strategy improvement" << endl;
+ } else if (!strcmp(argv[3], "naive")) {
+ improvement = naiveImprovement;
+ cout << "Naive strategy improvement" << endl;
} else {
- algorithm = new RecursiveFixpoint<ZBar>();
- cout << "Recursive fixpoint" << endl;
+ cout << "Unknown strategy improvement algorithm." << endl;
+ }
+ if (!improvement || !algorithm) {
+ exit(1);
}
pANTLR3_INPUT_STREAM input;
@@ -192,18 +134,39 @@ 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>* result = NULL;
+ MaxStrategy<ZBar> strategy(system);
+ bool changed;
+ do {
+ if (result) delete result;
+ result = algorithm->maxFixpoint(strategy);
+ /*for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+ Variable<ZBar>& var = system.variable(i);
+ cout << var.name() << " = " << (*result)[var] << ", ";
+ }
+ cout << endl;*/
+ changed = strategy.improve(*improvement, *result);
+ } while(changed);
+
+ 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;
}
+ delete result;
+ delete algorithm;
+ if (naiveImprovement != improvement)
+ delete improvement;
+ delete naiveImprovement;
+
parser -> free(parser);
tokens -> free(tokens);
lex -> free(lex);
diff --git a/impl/systems/constant-system.eqns b/impl/systems/constant-system.eqns
new file mode 100644
index 0000000..7d4290a
--- /dev/null
+++ b/impl/systems/constant-system.eqns
@@ -0,0 +1 @@
+x = 1
diff --git a/impl/systems/size-ten b/impl/systems/example.eqns
index 9ef3135..9ef3135 100644
--- a/impl/systems/size-ten
+++ b/impl/systems/example.eqns
diff --git a/impl/systems/generate-fib.py b/impl/systems/generate-fib.py
new file mode 100644
index 0000000..0263fff
--- /dev/null
+++ b/impl/systems/generate-fib.py
@@ -0,0 +1,6 @@
+
+print 'x0 = 0'
+print 'x1 = 1'
+for i in xrange(10000):
+ #print 'x' + str(i+2) + " = x" + str(i) + " + x" + str(i+1)
+ print 'x%d = x%d + x%d' % (i+2, i, i+1)
diff --git a/impl/antlr/generate.py b/impl/systems/generate-long.py
index 4513fe2..4513fe2 100644
--- a/impl/antlr/generate.py
+++ b/impl/systems/generate-long.py
diff --git a/impl/systems/generate-system.py b/impl/systems/generate-random.py
index cc67df2..cc67df2 100644
--- a/impl/systems/generate-system.py
+++ b/impl/systems/generate-random.py
diff --git a/impl/systems/long-fib.eqns b/impl/systems/long-fib.eqns
new file mode 100644
index 0000000..08a29d6
--- /dev/null
+++ b/impl/systems/long-fib.eqns
@@ -0,0 +1,1001 @@
+x0 = 0
+x1 = 1
+x2 = x0 + x1
+x3 = x1 + x2
+x4 = x2 + x3
+x5 = x3 + x4
+x6 = x4 + x5
+x7 = x5 + x6
+x8 = x6 + x7
+x9 = x7 + x8
+x10 = x8 + x9
+x11 = x9 + x10
+x12 = x10 + x11
+x13 = x11 + x12
+x14 = x12 + x13
+x15 = x13 + x14
+x16 = x14 + x15
+x17 = x15 + x16
+x18 = x16 + x17
+x19 = x17 + x18
+x20 = x18 + x19
+x21 = x19 + x20
+x22 = x20 + x21
+x23 = x21 + x22
+x24 = x22 + x23
+x25 = x23 + x24
+x26 = x24 + x25
+x27 = x25 + x26
+x28 = x26 + x27
+x29 = x27 + x28
+x30 = x28 + x29
+x31 = x29 + x30
+x32 = x30 + x31
+x33 = x31 + x32
+x34 = x32 + x33
+x35 = x33 + x34
+x36 = x34 + x35
+x37 = x35 + x36
+x38 = x36 + x37
+x39 = x37 + x38
+x40 = x38 + x39
+x41 = x39 + x40
+x42 = x40 + x41
+x43 = x41 + x42
+x44 = x42 + x43
+x45 = x43 + x44
+x46 = x44 + x45
+x47 = x45 + x46
+x48 = x46 + x47
+x49 = x47 + x48
+x50 = x48 + x49
+x51 = x49 + x50
+x52 = x50 + x51
+x53 = x51 + x52
+x54 = x52 + x53
+x55 = x53 + x54
+x56 = x54 + x55
+x57 = x55 + x56
+x58 = x56 + x57
+x59 = x57 + x58
+x60 = x58 + x59
+x61 = x59 + x60
+x62 = x60 + x61
+x63 = x61 + x62
+x64 = x62 + x63
+x65 = x63 + x64
+x66 = x64 + x65
+x67 = x65 + x66
+x68 = x66 + x67
+x69 = x67 + x68
+x70 = x68 + x69
+x71 = x69 + x70
+x72 = x70 + x71
+x73 = x71 + x72
+x74 = x72 + x73
+x75 = x73 + x74
+x76 = x74 + x75
+x77 = x75 + x76
+x78 = x76 + x77
+x79 = x77 + x78
+x80 = x78 + x79
+x81 = x79 + x80
+x82 = x80 + x81
+x83 = x81 + x82
+x84 = x82 + x83
+x85 = x83 + x84
+x86 = x84 + x85
+x87 = x85 + x86
+x88 = x86 + x87
+x89 = x87 + x88
+x90 = x88 + x89
+x91 = x89 + x90
+x92 = x90 + x91
+x93 = x91 + x92
+x94 = x92 + x93
+x95 = x93 + x94
+x96 = x94 + x95
+x97 = x95 + x96
+x98 = x96 + x97
+x99 = x97 + x98
+x100 = x98 + x99
+x101 = x99 + x100
+x102 = x100 + x101
+x103 = x101 + x102
+x104 = x102 + x103
+x105 = x103 + x104
+x106 = x104 + x105
+x107 = x105 + x106
+x108 = x106 + x107
+x109 = x107 + x108
+x110 = x108 + x109
+x111 = x109 + x110
+x112 = x110 + x111
+x113 = x111 + x112
+x114 = x112 + x113
+x115 = x113 + x114
+x116 = x114 + x115
+x117 = x115 + x116
+x118 = x116 + x117
+x119 = x117 + x118
+x120 = x118 + x119
+x121 = x119 + x120
+x122 = x120 + x121
+x123 = x121 + x122
+x124 = x122 + x123
+x125 = x123 + x124
+x126 = x124 + x125
+x127 = x125 + x126
+x128 = x126 + x127
+x129 = x127 + x128
+x130 = x128 + x129
+x131 = x129 + x130
+x132 = x130 + x131
+x133 = x131 + x132
+x134 = x132 + x133
+x135 = x133 + x134
+x136 = x134 + x135
+x137 = x135 + x136
+x138 = x136 + x137
+x139 = x137 + x138
+x140 = x138 + x139
+x141 = x139 + x140
+x142 = x140 + x141
+x143 = x141 + x142
+x144 = x142 + x143
+x145 = x143 + x144
+x146 = x144 + x145
+x147 = x145 + x146
+x148 = x146 + x147
+x149 = x147 + x148
+x150 = x148 + x149
+x151 = x149 + x150
+x152 = x150 + x151
+x153 = x151 + x152
+x154 = x152 + x153
+x155 = x153 + x154
+x156 = x154 + x155
+x157 = x155 + x156
+x158 = x156 + x157
+x159 = x157 + x158
+x160 = x158 + x159
+x161 = x159 + x160
+x162 = x160 + x161
+x163 = x161 + x162
+x164 = x162 + x163
+x165 = x163 + x164
+x166 = x164 + x165
+x167 = x165 + x166
+x168 = x166 + x167
+x169 = x167 + x168
+x170 = x168 + x169
+x171 = x169 + x170
+x172 = x170 + x171
+x173 = x171 + x172
+x174 = x172 + x173
+x175 = x173 + x174
+x176 = x174 + x175
+x177 = x175 + x176
+x178 = x176 + x177
+x179 = x177 + x178
+x180 = x178 + x179
+x181 = x179 + x180
+x182 = x180 + x181
+x183 = x181 + x182
+x184 = x182 + x183
+x185 = x183 + x184
+x186 = x184 + x185
+x187 = x185 + x186
+x188 = x186 + x187
+x189 = x187 + x188
+x190 = x188 + x189
+x191 = x189 + x190
+x192 = x190 + x191
+x193 = x191 + x192
+x194 = x192 + x193
+x195 = x193 + x194
+x196 = x194 + x195
+x197 = x195 + x196
+x198 = x196 + x197
+x199 = x197 + x198
+x200 = x198 + x199
+x201 = x199 + x200
+x202 = x200 + x201
+x203 = x201 + x202
+x204 = x202 + x203
+x205 = x203 + x204
+x206 = x204 + x205
+x207 = x205 + x206
+x208 = x206 + x207
+x209 = x207 + x208
+x210 = x208 + x209
+x211 = x209 + x210
+x212 = x210 + x211
+x213 = x211 + x212
+x214 = x212 + x213
+x215 = x213 + x214
+x216 = x214 + x215
+x217 = x215 + x216
+x218 = x216 + x217
+x219 = x217 + x218
+x220 = x218 + x219
+x221 = x219 + x220
+x222 = x220 + x221
+x223 = x221 + x222
+x224 = x222 + x223
+x225 = x223 + x224
+x226 = x224 + x225
+x227 = x225 + x226
+x228 = x226 + x227
+x229 = x227 + x228
+x230 = x228 + x229
+x231 = x229 + x230
+x232 = x230 + x231
+x233 = x231 + x232
+x234 = x232 + x233
+x235 = x233 + x234
+x236 = x234 + x235
+x237 = x235 + x236
+x238 = x236 + x237
+x239 = x237 + x238
+x240 = x238 + x239
+x241 = x239 + x240
+x242 = x240 + x241
+x243 = x241 + x242
+x244 = x242 + x243
+x245 = x243 + x244
+x246 = x244 + x245
+x247 = x245 + x246
+x248 = x246 + x247
+x249 = x247 + x248
+x250 = x248 + x249
+x251 = x249 + x250
+x252 = x250 + x251
+x253 = x251 + x252
+x254 = x252 + x253
+x255 = x253 + x254
+x256 = x254 + x255
+x257 = x255 + x256
+x258 = x256 + x257
+x259 = x257 + x258
+x260 = x258 + x259
+x261 = x259 + x260
+x262 = x260 + x261
+x263 = x261 + x262
+x264 = x262 + x263
+x265 = x263 + x264
+x266 = x264 + x265
+x267 = x265 + x266
+x268 = x266 + x267
+x269 = x267 + x268
+x270 = x268 + x269
+x271 = x269 + x270
+x272 = x270 + x271
+x273 = x271 + x272
+x274 = x272 + x273
+x275 = x273 + x274
+x276 = x274 + x275
+x277 = x275 + x276
+x278 = x276 + x277
+x279 = x277 + x278
+x280 = x278 + x279
+x281 = x279 + x280
+x282 = x280 + x281
+x283 = x281 + x282
+x284 = x282 + x283
+x285 = x283 + x284
+x286 = x284 + x285
+x287 = x285 + x286
+x288 = x286 + x287
+x289 = x287 + x288
+x290 = x288 + x289
+x291 = x289 + x290
+x292 = x290 + x291
+x293 = x291 + x292
+x294 = x292 + x293
+x295 = x293 + x294
+x296 = x294 + x295
+x297 = x295 + x296
+x298 = x296 + x297
+x299 = x297 + x298
+x300 = x298 + x299
+x301 = x299 + x300
+x302 = x300 + x301
+x303 = x301 + x302
+x304 = x302 + x303
+x305 = x303 + x304
+x306 = x304 + x305
+x307 = x305 + x306
+x308 = x306 + x307
+x309 = x307 + x308
+x310 = x308 + x309
+x311 = x309 + x310
+x312 = x310 + x311
+x313 = x311 + x312
+x314 = x312 + x313
+x315 = x313 + x314
+x316 = x314 + x315
+x317 = x315 + x316
+x318 = x316 + x317
+x319 = x317 + x318
+x320 = x318 + x319
+x321 = x319 + x320
+x322 = x320 + x321
+x323 = x321 + x322
+x324 = x322 + x323
+x325 = x323 + x324
+x326 = x324 + x325
+x327 = x325 + x326
+x328 = x326 + x327
+x329 = x327 + x328
+x330 = x328 + x329
+x331 = x329 + x330
+x332 = x330 + x331
+x333 = x331 + x332
+x334 = x332 + x333
+x335 = x333 + x334
+x336 = x334 + x335
+x337 = x335 + x336
+x338 = x336 + x337
+x339 = x337 + x338
+x340 = x338 + x339
+x341 = x339 + x340
+x342 = x340 + x341
+x343 = x341 + x342
+x344 = x342 + x343
+x345 = x343 + x344
+x346 = x344 + x345
+x347 = x345 + x346
+x348 = x346 + x347
+x349 = x347 + x348
+x350 = x348 + x349
+x351 = x349 + x350
+x352 = x350 + x351
+x353 = x351 + x352
+x354 = x352 + x353
+x355 = x353 + x354
+x356 = x354 + x355
+x357 = x355 + x356
+x358 = x356 + x357
+x359 = x357 + x358
+x360 = x358 + x359
+x361 = x359 + x360
+x362 = x360 + x361
+x363 = x361 + x362
+x364 = x362 + x363
+x365 = x363 + x364
+x366 = x364 + x365
+x367 = x365 + x366
+x368 = x366 + x367
+x369 = x367 + x368
+x370 = x368 + x369
+x371 = x369 + x370
+x372 = x370 + x371
+x373 = x371 + x372
+x374 = x372 + x373
+x375 = x373 + x374
+x376 = x374 + x375
+x377 = x375 + x376
+x378 = x376 + x377
+x379 = x377 + x378
+x380 = x378 + x379
+x381 = x379 + x380
+x382 = x380 + x381
+x383 = x381 + x382
+x384 = x382 + x383
+x385 = x383 + x384
+x386 = x384 + x385
+x387 = x385 + x386
+x388 = x386 + x387
+x389 = x387 + x388
+x390 = x388 + x389
+x391 = x389 + x390
+x392 = x390 + x391
+x393 = x391 + x392
+x394 = x392 + x393
+x395 = x393 + x394
+x396 = x394 + x395
+x397 = x395 + x396
+x398 = x396 + x397
+x399 = x397 + x398
+x400 = x398 + x399
+x401 = x399 + x400
+x402 = x400 + x401
+x403 = x401 + x402
+x404 = x402 + x403
+x405 = x403 + x404
+x406 = x404 + x405
+x407 = x405 + x406
+x408 = x406 + x407
+x409 = x407 + x408
+x410 = x408 + x409
+x411 = x409 + x410
+x412 = x410 + x411
+x413 = x411 + x412
+x414 = x412 + x413
+x415 = x413 + x414
+x416 = x414 + x415
+x417 = x415 + x416
+x418 = x416 + x417
+x419 = x417 + x418
+x420 = x418 + x419
+x421 = x419 + x420
+x422 = x420 + x421
+x423 = x421 + x422
+x424 = x422 + x423
+x425 = x423 + x424
+x426 = x424 + x425
+x427 = x425 + x426
+x428 = x426 + x427
+x429 = x427 + x428
+x430 = x428 + x429
+x431 = x429 + x430
+x432 = x430 + x431
+x433 = x431 + x432
+x434 = x432 + x433
+x435 = x433 + x434
+x436 = x434 + x435
+x437 = x435 + x436
+x438 = x436 + x437
+x439 = x437 + x438
+x440 = x438 + x439
+x441 = x439 + x440
+x442 = x440 + x441
+x443 = x441 + x442
+x444 = x442 + x443
+x445 = x443 + x444
+x446 = x444 + x445
+x447 = x445 + x446
+x448 = x446 + x447
+x449 = x447 + x448
+x450 = x448 + x449
+x451 = x449 + x450
+x452 = x450 + x451
+x453 = x451 + x452
+x454 = x452 + x453
+x455 = x453 + x454
+x456 = x454 + x455
+x457 = x455 + x456
+x458 = x456 + x457
+x459 = x457 + x458
+x460 = x458 + x459
+x461 = x459 + x460
+x462 = x460 + x461
+x463 = x461 + x462
+x464 = x462 + x463
+x465 = x463 + x464
+x466 = x464 + x465
+x467 = x465 + x466
+x468 = x466 + x467
+x469 = x467 + x468
+x470 = x468 + x469
+x471 = x469 + x470
+x472 = x470 + x471
+x473 = x471 + x472
+x474 = x472 + x473
+x475 = x473 + x474
+x476 = x474 + x475
+x477 = x475 + x476
+x478 = x476 + x477
+x479 = x477 + x478
+x480 = x478 + x479
+x481 = x479 + x480
+x482 = x480 + x481
+x483 = x481 + x482
+x484 = x482 + x483
+x485 = x483 + x484
+x486 = x484 + x485
+x487 = x485 + x486
+x488 = x486 + x487
+x489 = x487 + x488
+x490 = x488 + x489
+x491 = x489 + x490
+x492 = x490 + x491
+x493 = x491 + x492
+x494 = x492 + x493
+x495 = x493 + x494
+x496 = x494 + x495
+x497 = x495 + x496
+x498 = x496 + x497
+x499 = x497 + x498
+x500 = x498 + x499
+x501 = x499 + x500
+x502 = x500 + x501
+x503 = x501 + x502
+x504 = x502 + x503
+x505 = x503 + x504
+x506 = x504 + x505
+x507 = x505 + x506
+x508 = x506 + x507
+x509 = x507 + x508
+x510 = x508 + x509
+x511 = x509 + x510
+x512 = x510 + x511
+x513 = x511 + x512
+x514 = x512 + x513
+x515 = x513 + x514
+x516 = x514 + x515
+x517 = x515 + x516
+x518 = x516 + x517
+x519 = x517 + x518
+x520 = x518 + x519
+x521 = x519 + x520
+x522 = x520 + x521
+x523 = x521 + x522
+x524 = x522 + x523
+x525 = x523 + x524
+x526 = x524 + x525
+x527 = x525 + x526
+x528 = x526 + x527
+x529 = x527 + x528
+x530 = x528 + x529
+x531 = x529 + x530
+x532 = x530 + x531
+x533 = x531 + x532
+x534 = x532 + x533
+x535 = x533 + x534
+x536 = x534 + x535
+x537 = x535 + x536
+x538 = x536 + x537
+x539 = x537 + x538
+x540 = x538 + x539
+x541 = x539 + x540
+x542 = x540 + x541
+x543 = x541 + x542
+x544 = x542 + x543
+x545 = x543 + x544
+x546 = x544 + x545
+x547 = x545 + x546
+x548 = x546 + x547
+x549 = x547 + x548
+x550 = x548 + x549
+x551 = x549 + x550
+x552 = x550 + x551
+x553 = x551 + x552
+x554 = x552 + x553
+x555 = x553 + x554
+x556 = x554 + x555
+x557 = x555 + x556
+x558 = x556 + x557
+x559 = x557 + x558
+x560 = x558 + x559
+x561 = x559 + x560
+x562 = x560 + x561
+x563 = x561 + x562
+x564 = x562 + x563
+x565 = x563 + x564
+x566 = x564 + x565
+x567 = x565 + x566
+x568 = x566 + x567
+x569 = x567 + x568
+x570 = x568 + x569
+x571 = x569 + x570
+x572 = x570 + x571
+x573 = x571 + x572
+x574 = x572 + x573
+x575 = x573 + x574
+x576 = x574 + x575
+x577 = x575 + x576
+x578 = x576 + x577
+x579 = x577 + x578
+x580 = x578 + x579
+x581 = x579 + x580
+x582 = x580 + x581
+x583 = x581 + x582
+x584 = x582 + x583
+x585 = x583 + x584
+x586 = x584 + x585
+x587 = x585 + x586
+x588 = x586 + x587
+x589 = x587 + x588
+x590 = x588 + x589
+x591 = x589 + x590
+x592 = x590 + x591
+x593 = x591 + x592
+x594 = x592 + x593
+x595 = x593 + x594
+x596 = x594 + x595
+x597 = x595 + x596
+x598 = x596 + x597
+x599 = x597 + x598
+x600 = x598 + x599
+x601 = x599 + x600
+x602 = x600 + x601
+x603 = x601 + x602
+x604 = x602 + x603
+x605 = x603 + x604
+x606 = x604 + x605
+x607 = x605 + x606
+x608 = x606 + x607
+x609 = x607 + x608
+x610 = x608 + x609
+x611 = x609 + x610
+x612 = x610 + x611
+x613 = x611 + x612
+x614 = x612 + x613
+x615 = x613 + x614
+x616 = x614 + x615
+x617 = x615 + x616
+x618 = x616 + x617
+x619 = x617 + x618
+x620 = x618 + x619
+x621 = x619 + x620
+x622 = x620 + x621
+x623 = x621 + x622
+x624 = x622 + x623
+x625 = x623 + x624
+x626 = x624 + x625
+x627 = x625 + x626
+x628 = x626 + x627
+x629 = x627 + x628
+x630 = x628 + x629
+x631 = x629 + x630
+x632 = x630 + x631
+x633 = x631 + x632
+x634 = x632 + x633
+x635 = x633 + x634
+x636 = x634 + x635
+x637 = x635 + x636
+x638 = x636 + x637
+x639 = x637 + x638
+x640 = x638 + x639
+x641 = x639 + x640
+x642 = x640 + x641
+x643 = x641 + x642
+x644 = x642 + x643
+x645 = x643 + x644
+x646 = x644 + x645
+x647 = x645 + x646
+x648 = x646 + x647
+x649 = x647 + x648
+x650 = x648 + x649
+x651 = x649 + x650
+x652 = x650 + x651
+x653 = x651 + x652
+x654 = x652 + x653
+x655 = x653 + x654
+x656 = x654 + x655
+x657 = x655 + x656
+x658 = x656 + x657
+x659 = x657 + x658
+x660 = x658 + x659
+x661 = x659 + x660
+x662 = x660 + x661
+x663 = x661 + x662
+x664 = x662 + x663
+x665 = x663 + x664
+x666 = x664 + x665
+x667 = x665 + x666
+x668 = x666 + x667
+x669 = x667 + x668
+x670 = x668 + x669
+x671 = x669 + x670
+x672 = x670 + x671
+x673 = x671 + x672
+x674 = x672 + x673
+x675 = x673 + x674
+x676 = x674 + x675
+x677 = x675 + x676
+x678 = x676 + x677
+x679 = x677 + x678
+x680 = x678 + x679
+x681 = x679 + x680
+x682 = x680 + x681
+x683 = x681 + x682
+x684 = x682 + x683
+x685 = x683 + x684
+x686 = x684 + x685
+x687 = x685 + x686
+x688 = x686 + x687
+x689 = x687 + x688
+x690 = x688 + x689
+x691 = x689 + x690
+x692 = x690 + x691
+x693 = x691 + x692
+x694 = x692 + x693
+x695 = x693 + x694
+x696 = x694 + x695
+x697 = x695 + x696
+x698 = x696 + x697
+x699 = x697 + x698
+x700 = x698 + x699
+x701 = x699 + x700
+x702 = x700 + x701
+x703 = x701 + x702
+x704 = x702 + x703
+x705 = x703 + x704
+x706 = x704 + x705
+x707 = x705 + x706
+x708 = x706 + x707
+x709 = x707 + x708
+x710 = x708 + x709
+x711 = x709 + x710
+x712 = x710 + x711
+x713 = x711 + x712
+x714 = x712 + x713
+x715 = x713 + x714
+x716 = x714 + x715
+x717 = x715 + x716
+x718 = x716 + x717
+x719 = x717 + x718
+x720 = x718 + x719
+x721 = x719 + x720
+x722 = x720 + x721
+x723 = x721 + x722
+x724 = x722 + x723
+x725 = x723 + x724
+x726 = x724 + x725
+x727 = x725 + x726
+x728 = x726 + x727
+x729 = x727 + x728
+x730 = x728 + x729
+x731 = x729 + x730
+x732 = x730 + x731
+x733 = x731 + x732
+x734 = x732 + x733
+x735 = x733 + x734
+x736 = x734 + x735
+x737 = x735 + x736
+x738 = x736 + x737
+x739 = x737 + x738
+x740 = x738 + x739
+x741 = x739 + x740
+x742 = x740 + x741
+x743 = x741 + x742
+x744 = x742 + x743
+x745 = x743 + x744
+x746 = x744 + x745
+x747 = x745 + x746
+x748 = x746 + x747
+x749 = x747 + x748
+x750 = x748 + x749
+x751 = x749 + x750
+x752 = x750 + x751
+x753 = x751 + x752
+x754 = x752 + x753
+x755 = x753 + x754
+x756 = x754 + x755
+x757 = x755 + x756
+x758 = x756 + x757
+x759 = x757 + x758
+x760 = x758 + x759
+x761 = x759 + x760
+x762 = x760 + x761
+x763 = x761 + x762
+x764 = x762 + x763
+x765 = x763 + x764
+x766 = x764 + x765
+x767 = x765 + x766
+x768 = x766 + x767
+x769 = x767 + x768
+x770 = x768 + x769
+x771 = x769 + x770
+x772 = x770 + x771
+x773 = x771 + x772
+x774 = x772 + x773
+x775 = x773 + x774
+x776 = x774 + x775
+x777 = x775 + x776
+x778 = x776 + x777
+x779 = x777 + x778
+x780 = x778 + x779
+x781 = x779 + x780
+x782 = x780 + x781
+x783 = x781 + x782
+x784 = x782 + x783
+x785 = x783 + x784
+x786 = x784 + x785
+x787 = x785 + x786
+x788 = x786 + x787
+x789 = x787 + x788
+x790 = x788 + x789
+x791 = x789 + x790
+x792 = x790 + x791
+x793 = x791 + x792
+x794 = x792 + x793
+x795 = x793 + x794
+x796 = x794 + x795
+x797 = x795 + x796
+x798 = x796 + x797
+x799 = x797 + x798
+x800 = x798 + x799
+x801 = x799 + x800
+x802 = x800 + x801
+x803 = x801 + x802
+x804 = x802 + x803
+x805 = x803 + x804
+x806 = x804 + x805
+x807 = x805 + x806
+x808 = x806 + x807
+x809 = x807 + x808
+x810 = x808 + x809
+x811 = x809 + x810
+x812 = x810 + x811
+x813 = x811 + x812
+x814 = x812 + x813
+x815 = x813 + x814
+x816 = x814 + x815
+x817 = x815 + x816
+x818 = x816 + x817
+x819 = x817 + x818
+x820 = x818 + x819
+x821 = x819 + x820
+x822 = x820 + x821
+x823 = x821 + x822
+x824 = x822 + x823
+x825 = x823 + x824
+x826 = x824 + x825
+x827 = x825 + x826
+x828 = x826 + x827
+x829 = x827 + x828
+x830 = x828 + x829
+x831 = x829 + x830
+x832 = x830 + x831
+x833 = x831 + x832
+x834 = x832 + x833
+x835 = x833 + x834
+x836 = x834 + x835
+x837 = x835 + x836
+x838 = x836 + x837
+x839 = x837 + x838
+x840 = x838 + x839
+x841 = x839 + x840
+x842 = x840 + x841
+x843 = x841 + x842
+x844 = x842 + x843
+x845 = x843 + x844
+x846 = x844 + x845
+x847 = x845 + x846
+x848 = x846 + x847
+x849 = x847 + x848
+x850 = x848 + x849
+x851 = x849 + x850
+x852 = x850 + x851
+x853 = x851 + x852
+x854 = x852 + x853
+x855 = x853 + x854
+x856 = x854 + x855
+x857 = x855 + x856
+x858 = x856 + x857
+x859 = x857 + x858
+x860 = x858 + x859
+x861 = x859 + x860
+x862 = x860 + x861
+x863 = x861 + x862
+x864 = x862 + x863
+x865 = x863 + x864
+x866 = x864 + x865
+x867 = x865 + x866
+x868 = x866 + x867
+x869 = x867 + x868
+x870 = x868 + x869
+x871 = x869 + x870
+x872 = x870 + x871
+x873 = x871 + x872
+x874 = x872 + x873
+x875 = x873 + x874
+x876 = x874 + x875
+x877 = x875 + x876
+x878 = x876 + x877
+x879 = x877 + x878
+x880 = x878 + x879
+x881 = x879 + x880
+x882 = x880 + x881
+x883 = x881 + x882
+x884 = x882 + x883
+x885 = x883 + x884
+x886 = x884 + x885
+x887 = x885 + x886
+x888 = x886 + x887
+x889 = x887 + x888
+x890 = x888 + x889
+x891 = x889 + x890
+x892 = x890 + x891
+x893 = x891 + x892
+x894 = x892 + x893
+x895 = x893 + x894
+x896 = x894 + x895
+x897 = x895 + x896
+x898 = x896 + x897
+x899 = x897 + x898
+x900 = x898 + x899
+x901 = x899 + x900
+x902 = x900 + x901
+x903 = x901 + x902
+x904 = x902 + x903
+x905 = x903 + x904
+x906 = x904 + x905
+x907 = x905 + x906
+x908 = x906 + x907
+x909 = x907 + x908
+x910 = x908 + x909
+x911 = x909 + x910
+x912 = x910 + x911
+x913 = x911 + x912
+x914 = x912 + x913
+x915 = x913 + x914
+x916 = x914 + x915
+x917 = x915 + x916
+x918 = x916 + x917
+x919 = x917 + x918
+x920 = x918 + x919
+x921 = x919 + x920
+x922 = x920 + x921
+x923 = x921 + x922
+x924 = x922 + x923
+x925 = x923 + x924
+x926 = x924 + x925
+x927 = x925 + x926
+x928 = x926 + x927
+x929 = x927 + x928
+x930 = x928 + x929
+x931 = x929 + x930
+x932 = x930 + x931
+x933 = x931 + x932
+x934 = x932 + x933
+x935 = x933 + x934
+x936 = x934 + x935
+x937 = x935 + x936
+x938 = x936 + x937
+x939 = x937 + x938
+x940 = x938 + x939
+x941 = x939 + x940
+x942 = x940 + x941
+x943 = x941 + x942
+x944 = x942 + x943
+x945 = x943 + x944
+x946 = x944 + x945
+x947 = x945 + x946
+x948 = x946 + x947
+x949 = x947 + x948
+x950 = x948 + x949
+x951 = x949 + x950
+x952 = x950 + x951
+x953 = x951 + x952
+x954 = x952 + x953
+x955 = x953 + x954
+x956 = x954 + x955
+x957 = x955 + x956
+x958 = x956 + x957
+x959 = x957 + x958
+x960 = x958 + x959
+x961 = x959 + x960
+x962 = x960 + x961
+x963 = x961 + x962
+x964 = x962 + x963
+x965 = x963 + x964
+x966 = x964 + x965
+x967 = x965 + x966
+x968 = x966 + x967
+x969 = x967 + x968
+x970 = x968 + x969
+x971 = x969 + x970
+x972 = x970 + x971
+x973 = x971 + x972
+x974 = x972 + x973
+x975 = x973 + x974
+x976 = x974 + x975
+x977 = x975 + x976
+x978 = x976 + x977
+x979 = x977 + x978
+x980 = x978 + x979
+x981 = x979 + x980
+x982 = x980 + x981
+x983 = x981 + x982
+x984 = x982 + x983
+x985 = x983 + x984
+x986 = x984 + x985
+x987 = x985 + x986
+x988 = x986 + x987
+x989 = x987 + x988
+x990 = x988 + x989
+x991 = x989 + x990
+x992 = x990 + x991
+x993 = x991 + x992
+x994 = x992 + x993
+x995 = x993 + x994
+x996 = x994 + x995
+x997 = x995 + x996
+x998 = x996 + x997
+x999 = x997 + x998
+x1000 = x998 + x999
diff --git a/impl/systems/long-fixpoint b/impl/systems/long-fixpoint.eqns
index 5838910..5838910 100644
--- a/impl/systems/long-fixpoint
+++ b/impl/systems/long-fixpoint.eqns
diff --git a/impl/systems/min-test b/impl/systems/min-test
deleted file mode 100644
index a05a662..0000000
--- a/impl/systems/min-test
+++ /dev/null
@@ -1,3 +0,0 @@
-x1 = min(1, x1)
-x2 = min(x2+1, x3)
-x3 = 0
diff --git a/impl/systems/small b/impl/systems/minimal.eqns
index 3c40ed9..3c40ed9 100644
--- a/impl/systems/small
+++ b/impl/systems/minimal.eqns
diff --git a/impl/systems/random-system b/impl/systems/random-system
deleted file mode 100644
index 506c18a..0000000
--- a/impl/systems/random-system
+++ /dev/null
@@ -1 +0,0 @@
-x = max()
generated by cgit v1.2.3 (git 2.46.2) at 2024-12-25 19:08:41 +0000