From 18a747edd76918e2a1a4fb608b2d3923fcc535fa Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Tue, 16 Oct 2012 13:26:07 +1100 Subject: A quick fix to the solver. --- impl/systems/gmon.out | Bin 79219 -> 75981 bytes impl/systems/test.eqns | 24 ++++++++++-------------- 2 files changed, 10 insertions(+), 14 deletions(-) (limited to 'impl/systems') diff --git a/impl/systems/gmon.out b/impl/systems/gmon.out index 3240978..b5abe0e 100644 Binary files a/impl/systems/gmon.out and b/impl/systems/gmon.out differ diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns index fb23f1e..af18a57 100644 --- a/impl/systems/test.eqns +++ b/impl/systems/test.eqns @@ -1,16 +1,12 @@ i-4[0] = max(-inf, 0) -neg-i4[0] = max(-inf, 0) -neg-i1-pre = max(-inf, guard(add(min(neg-i4[0], inf), min(i-4[0], inf)), 0, neg-i4[0]), guard(add(min(neg-i2-pre, inf), min(i-2-pre, inf)), 0, neg-i2-pre)) -i-1-pre = max(-inf, guard(add(min(neg-i4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(neg-i2-pre, inf), min(i-2-pre, inf)), 0, i-2-pre)) -neg-i3-pre = max(-inf, guard(add(min(neg-i1-pre, inf), min(i-1-pre, 2)), 0, neg-i1-pre)) -i-3-pre = max(-inf, guard(add(min(neg-i1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) -neg-i0-pre = max(-inf, guard(add(min(neg-i1-pre, -3), min(i-1-pre, inf)), 0, min(-3, neg-i1-pre))) -i-0-pre = max(-inf, guard(add(min(neg-i1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) +negi-4[0] = max(-inf, 0) +negi-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, negi-4[0]), guard(add(min(negi-2-pre, inf), min(i-2-pre, inf)), 0, negi-2-pre)) +i-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(negi-2-pre, inf), min(i-2-pre, inf)), 0, i-2-pre)) +negi-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, negi-1-pre)) +i-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) +negi-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, negi-1-pre))) +i-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) i-3[0] = max(-inf, add(0, i-3-pre)) -neg-i3[0] = max(-inf, add(0, neg-i3-pre)) -neg-i2-pre = max(-inf, guard(add(min(neg-i3[0], inf), min(i-3[0], inf)), 0, neg-i3[0])) -i-2-pre = max(-inf, guard(add(min(neg-i3[0], inf), min(i-3[0], inf)), 0, i-3[0])) -x = max(-inf, 0) -y = max(-inf, x, z) -z = max(-inf, y) - +negi-3[0] = max(-inf, add(0, negi-3-pre)) +negi-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, negi-3[0])) +i-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, i-3[0])) -- cgit v1.2.3 From 86ca7448849aaaea6db34b1d2bcf8d99d7d7b12c Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Mon, 22 Oct 2012 14:44:57 +1100 Subject: Okay, the solver is now correct. It runs in two separate passes: - improve strategy (for all) - evaluate fixpoint Unfortunately this loses out on locality at the moment. I really want a local solver, so I'll have to see what I can do about that. --- .gitignore | 1 + impl/Complete.hpp | 6 ++- impl/Expression.hpp | 6 ++- impl/MaxStrategy.hpp | 89 ++++++++++++++++++++++++++++++++++++-------- impl/VariableAssignment.hpp | 47 +++++++++++++++++------ impl/gmon.out | Bin 76225 -> 0 bytes impl/main.cpp | 15 ++++++++ impl/systems/gmon.out | Bin 75981 -> 0 bytes impl/systems/test.eqns | 32 ++++++++++------ impl/test/7.eqns | 8 ++++ impl/test/7.soln | 8 ++++ 11 files changed, 171 insertions(+), 41 deletions(-) delete mode 100644 impl/gmon.out delete mode 100644 impl/systems/gmon.out create mode 100644 impl/test/7.eqns create mode 100644 impl/test/7.soln (limited to 'impl/systems') diff --git a/.gitignore b/.gitignore index 3b01757..93c639b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /impl/build/* /impl/parser/* +gmon.out diff --git a/impl/Complete.hpp b/impl/Complete.hpp index 8c5559a..e3ec15a 100644 --- a/impl/Complete.hpp +++ b/impl/Complete.hpp @@ -40,7 +40,11 @@ struct Complete { return Complete(- _value, _infinity); } Complete operator+(const Complete& other) const { - if (_infinity) { + if (_infinity && other._infinity) { + if (_value > 0 || other._value > 0) + return Complete(1, true); + return Complete(-1, true); + } else if (_infinity) { return *this; } else if (other._infinity) { return other; diff --git a/impl/Expression.hpp b/impl/Expression.hpp index 0d48d70..9c4ac9f 100644 --- a/impl/Expression.hpp +++ b/impl/Expression.hpp @@ -110,6 +110,10 @@ struct OperatorExpression : public Expression { return _operator.eval(argumentValues); } + std::vector*>& arguments() { + return _arguments; + } + const std::vector*>& arguments() const { return _arguments; } @@ -141,7 +145,7 @@ struct OperatorExpression : public Expression { private: const Operator& _operator; protected: - const std::vector*> _arguments; + std::vector*> _arguments; }; template diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp index 96aeef4..f4026dd 100644 --- a/impl/MaxStrategy.hpp +++ b/impl/MaxStrategy.hpp @@ -10,6 +10,9 @@ template struct MaxStrategy { virtual ~MaxStrategy() { } virtual unsigned int get(const MaxExpression& e) const = 0; + virtual unsigned int get(const MaxExpression& e) { + return const_cast(this)->get(e); + } }; unsigned int stack_depth = 1; @@ -38,20 +41,38 @@ struct DynamicMaxStrategy : public MaxStrategy { _influence(system.maxExpressionCount(), IdSet >(system.maxExpressionCount())), _var_influence(system.variableCount(), - IdSet >(system.maxExpressionCount())) + IdSet >(system.maxExpressionCount())), + _frozen(false) {} + void freeze() { + _frozen = true; + } + + void thaw() { + _frozen = false; + } + + bool is_frozen() { + return _frozen; + } + void setRho(DynamicVariableAssignment& rho) { _rho = ρ } unsigned int get(const MaxExpression& e) const { - solve(e); return _values[e]; } - void invalidate(const Variable& v) const { - log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; + unsigned int get(const MaxExpression& e) { + if (!_frozen) + solve(e); + return _values[e]; + } + + void invalidate(const Variable& v) { + log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; _stable.filter(_var_influence[v]); IdSet > infl = _var_influence[v]; @@ -67,7 +88,7 @@ struct DynamicMaxStrategy : public MaxStrategy { } private: - void solve(const MaxExpression& x) const { + void solve(const MaxExpression& x) { if (!_stable.contains(x)) { _stable.insert(x); log::strategy << indent() << "Stabilise " << x << std::endl; @@ -106,7 +127,7 @@ private: } struct DependencyAssignment : public VariableAssignment{ - DependencyAssignment(const DynamicMaxStrategy& strat, + DependencyAssignment(DynamicMaxStrategy& strat, VariableAssignment& rho, const MaxExpression& expr) : _strat(strat), @@ -118,13 +139,13 @@ private: return _rho[var]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; VariableAssignment& _rho; const MaxExpression& _expr; }; struct DependencyStrategy : public MaxStrategy { - DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression& expr) + DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression& expr) : _strat(strat), _expr(expr) { } @@ -136,19 +157,57 @@ private: return _strat._values[e]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; const MaxExpression& _expr; }; -private: +private: const EquationSystem& _system; - mutable DynamicVariableAssignment* _rho; - mutable IdMap,unsigned int> _values; - mutable IdSet > _stable; - mutable IdMap,IdSet > > _influence; - mutable IdMap,IdSet > > _var_influence; + DynamicVariableAssignment* _rho; + IdMap,unsigned int> _values; + IdSet > _stable; + IdMap,IdSet > > _influence; + IdMap,IdSet > > _var_influence; + bool _frozen; }; + +template +IdMap,T> solve_for(const EquationSystem& system) { + IdMap,T> result(system.variableCount(), infinity()); + + DynamicMaxStrategy strategy(system); + DynamicVariableAssignment rho(system, strategy, -infinity()); + strategy.setRho(rho); + + bool changed; + do { + changed = false; + + // improve strategy + rho.freeze(); + strategy.thaw(); + for (unsigned int i = 0; i < system.variableCount(); ++i) { + strategy.get(*system[system.variable(i)]); + } + + // iterate fixpoint + strategy.freeze(); + rho.thaw(); + for (unsigned int i = 0; i < system.variableCount(); ++i) { + Variable& var = system.variable(i); + T val = rho[var]; + if (result[var] != val) { + result[var] = val; + changed = true; + } + } + } while(changed); + + return result; +} + + /*template std::ostream& operator<<(std::ostream& cout, const MaxStrategy& strat) { strat.print(cout); diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index a9247b5..2a63756 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -8,6 +8,9 @@ template struct VariableAssignment { virtual ~VariableAssignment() { } virtual const Domain& operator[](const Variable&) const = 0; + virtual const Domain& operator[](const Variable& x) { + return (*const_cast(this))[x]; + } }; #include "EquationSystem.hpp" @@ -19,21 +22,40 @@ template struct DynamicVariableAssignment : public VariableAssignment { DynamicVariableAssignment( const EquationSystem& system, - const DynamicMaxStrategy& strat + DynamicMaxStrategy& strat, + const Domain& value=infinity() ) : _system(system), _strategy(strat), - _values(system.variableCount(), infinity()), + _values(system.variableCount(), value), _stable(system.variableCount()), _influence(system.variableCount(), - IdSet >(system.variableCount())) + IdSet >(system.variableCount())), + _frozen(false) { } + void freeze() { + _frozen = true; + } + + void thaw() { + _frozen = false; + } + + bool is_frozen() { + return _frozen; + } + const Domain& operator[](const Variable& var) const { - solve(var); return _values[var]; } - void invalidate(const Variable& x) const { + const Domain& operator[](const Variable& var) { + if (!_frozen) + solve(var); + return _values[var]; + } + + void invalidate(const Variable& x) { log::fixpoint << indent() << "Invalidating " << x << std::endl; if (_stable.contains(x)) { _stable.remove(x); @@ -53,7 +75,7 @@ struct DynamicVariableAssignment : public VariableAssignment { private: - void solve(const Variable& x) const { + void solve(const Variable& x) { if (!_stable.contains(x)) { _stable.insert(x); log::fixpoint << indent() << "Stabilise " << x << std::endl; @@ -90,7 +112,7 @@ private: } struct DependencyAssignment : public VariableAssignment { - DependencyAssignment(const DynamicVariableAssignment& assignment, const Variable& var) + DependencyAssignment(DynamicVariableAssignment& assignment, const Variable& var) : _assignment(assignment), _var(var) { } const Domain& operator[](const Variable& x) const { const Domain& result = _assignment[x]; @@ -98,15 +120,16 @@ private: return result; } private: - const DynamicVariableAssignment& _assignment; + DynamicVariableAssignment& _assignment; const Variable& _var; }; const EquationSystem& _system; - const DynamicMaxStrategy& _strategy; - mutable IdMap, Domain> _values; - mutable IdSet > _stable; - mutable IdMap,IdSet > > _influence; + DynamicMaxStrategy& _strategy; + IdMap, Domain> _values; + IdSet > _stable; + IdMap,IdSet > > _influence; + bool _frozen; }; #endif diff --git a/impl/gmon.out b/impl/gmon.out deleted file mode 100644 index f33c245..0000000 Binary files a/impl/gmon.out and /dev/null differ diff --git a/impl/main.cpp b/impl/main.cpp index e3e0ae3..84f17dd 100644 --- a/impl/main.cpp +++ b/impl/main.cpp @@ -140,6 +140,20 @@ int main (int argc, char* argv[]) { log::debug << system << endl; system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n) + IdMap,ZBar> result = solve_for(system); + if (variables.size() > 0) { + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + Variable& var = system.variable(i); + if (variables.find(var.name()) != variables.end()) + cout << var.name() << " = " << result[var] << endl; + } + } else { + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + Variable& var = system.variable(i); + cout << var.name() << " = " << result[var] << endl; + } + } + /* DynamicMaxStrategy strategy(system); DynamicVariableAssignment rho(system, strategy); strategy.setRho(rho); @@ -156,6 +170,7 @@ int main (int argc, char* argv[]) { cout << var.name() << " = " << rho[var] << endl; } } + */ parser -> free(parser); tokens -> free(tokens); diff --git a/impl/systems/gmon.out b/impl/systems/gmon.out deleted file mode 100644 index b5abe0e..0000000 Binary files a/impl/systems/gmon.out and /dev/null differ diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns index af18a57..a3b521d 100644 --- a/impl/systems/test.eqns +++ b/impl/systems/test.eqns @@ -1,12 +1,20 @@ -i-4[0] = max(-inf, 0) -negi-4[0] = max(-inf, 0) -negi-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, negi-4[0]), guard(add(min(negi-2-pre, inf), min(i-2-pre, inf)), 0, negi-2-pre)) -i-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(negi-2-pre, inf), min(i-2-pre, inf)), 0, i-2-pre)) -negi-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, negi-1-pre)) -i-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) -negi-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, negi-1-pre))) -i-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) -i-3[0] = max(-inf, add(0, i-3-pre)) -negi-3[0] = max(-inf, add(0, negi-3-pre)) -negi-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, negi-3[0])) -i-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, i-3[0])) +i-6[0] = max(-inf, 0) +neg-i-6[0] = max(-inf, 0) +neg-i-1-pre = max(-inf, guard(add(min(neg-i-6[0], inf), min(i-6[0], inf)), 0, neg-i-6[0]), guard(add(min(neg-i-2[0], inf), min(i-2[0], inf)), 0, neg-i-2[0])) +i-1-pre = max(-inf, guard(add(min(neg-i-6[0], inf), min(i-6[0], inf)), 0, i-6[0]), guard(add(min(neg-i-2[0], inf), min(i-2[0], inf)), 0, i-2[0])) +neg-i-5-pre = max(-inf, guard(add(min(neg-i-1-pre, inf), min(i-1-pre, 2)), 0, neg-i-1-pre)) +i-5-pre = max(-inf, guard(add(min(neg-i-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) +neg-i-0-pre = max(-inf, guard(add(min(neg-i-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, neg-i-1-pre))) +i-0-pre = max(-inf, guard(add(min(neg-i-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) +neg-i-4-pre = max(-inf, guard(add(min(neg-i-5-pre, inf), min(i-5-pre, 1)), 0, neg-i-5-pre)) +i-4-pre = max(-inf, guard(add(min(neg-i-5-pre, inf), min(i-5-pre, 1)), 0, min(1, i-5-pre))) +neg-i-3-pre = max(-inf, guard(add(min(neg-i-5-pre, -2), min(i-5-pre, inf)), 0, min(-2, neg-i-5-pre))) +i-3-pre = max(-inf, guard(add(min(neg-i-5-pre, -2), min(i-5-pre, inf)), 0, i-5-pre)) +i-4[0] = max(-inf, add(1, i-4-pre)) +neg-i-4[0] = max(-inf, add(-1, neg-i-4-pre)) +neg-i-2-pre = max(-inf, guard(add(min(neg-i-4[0], inf), min(i-4[0], inf)), 0, neg-i-4[0]), guard(add(min(neg-i-3[0], inf), min(i-3[0], inf)), 0, neg-i-3[0])) +i-2-pre = max(-inf, guard(add(min(neg-i-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(neg-i-3[0], inf), min(i-3[0], inf)), 0, i-3[0])) +i-3[0] = max(-inf, 10) +neg-i-3[0] = max(-inf, -10) +i-2[0] = max(-inf, add(1, i-2-pre)) +neg-i-2[0] = max(-inf, add(-1, neg-i-2-pre)) diff --git a/impl/test/7.eqns b/impl/test/7.eqns new file mode 100644 index 0000000..2789f0e --- /dev/null +++ b/impl/test/7.eqns @@ -0,0 +1,8 @@ +x = 0 +y = max(-inf, x, a) +a = b +b = c +c = d +d = e +e = f +f = y diff --git a/impl/test/7.soln b/impl/test/7.soln new file mode 100644 index 0000000..0d85468 --- /dev/null +++ b/impl/test/7.soln @@ -0,0 +1,8 @@ +x = 0 +y = 0 +a = 0 +b = 0 +c = 0 +d = 0 +e = 0 +f = 0 -- cgit v1.2.3