From 14c0c8bb717a668084cae8cd4b359ffd6fca73b0 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Mon, 22 Oct 2012 14:55:54 +1100 Subject: Try fixing clang to work with the fixed solver. (This may not compile, for an annoying reason. I'll check in again soon with something better-er, or whatever.) --- .../Analyses/IntervalSolver/MaxStrategy.hpp | 99 +++++++++++++++++----- .../Analyses/IntervalSolver/VariableAssignment.hpp | 77 ++++++++++++----- clang/lib/Analysis/Interval.cpp | 42 +++------ 3 files changed, 147 insertions(+), 71 deletions(-) diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp index 57dcdeb..f4026dd 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/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 { - solver_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,10 +88,10 @@ struct DynamicMaxStrategy : public MaxStrategy { } private: - void solve(const MaxExpression& x) const { + void solve(const MaxExpression& x) { if (!_stable.contains(x)) { _stable.insert(x); - solver_log::strategy << indent() << "Stabilise " << x << std::endl; + log::strategy << indent() << "Stabilise " << x << std::endl; stack_depth++; unsigned int val = x.bestStrategy(DependencyAssignment(*this, *_rho, x), @@ -78,7 +99,7 @@ private: stack_depth--; if (val != _values[x]) { - solver_log::strategy << x << " => " << *x.arguments()[val] << std::endl; + log::strategy << x << " => " << *x.arguments()[val] << std::endl; IdSet > oldInfluence = _influence[x]; _influence[x].clear(); @@ -96,15 +117,17 @@ private: solve(_system.maxExpression(*it)); } } else { - solver_log::strategy << indent() << x << " did not change" << std::endl; + log::strategy << indent() << x << " did not change: " + << x << " => " << *x.arguments()[val] << std::endl; } } else { - solver_log::strategy << indent() << x << " is stable" << std::endl; + log::strategy << indent() << x << " is stable: " + << x << " => " << *x.arguments()[_values[x]] << std::endl; } } struct DependencyAssignment : public VariableAssignment{ - DependencyAssignment(const DynamicMaxStrategy& strat, + DependencyAssignment(DynamicMaxStrategy& strat, VariableAssignment& rho, const MaxExpression& expr) : _strat(strat), @@ -116,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) { } @@ -134,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/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp index ba5f650..2a63756 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/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,46 +22,71 @@ 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 { - solver_log::fixpoint << indent() << "Invalidating " << x << std::endl; + 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); _values[x] = infinity(); - - solve(x); + + IdSet > infl = _influence[x]; + _influence[x].clear(); + for (typename IdSet >::iterator + it = infl.begin(), + ei = infl.end(); + it != ei; + ++it) { + invalidate(_system.variable(*it)); + } } } private: - void solve(const Variable& x) const { + void solve(const Variable& x) { if (!_stable.contains(x)) { _stable.insert(x); - solver_log::fixpoint << indent() << "Stabilise " << x << std::endl; + log::fixpoint << indent() << "Stabilise " << x << std::endl; stack_depth++; - if (!_system[x]) - return; - Domain val = _system[x]->evalWithStrat(DependencyAssignment(*this, x), - _strategy); + Domain val = _system[x]->eval(DependencyAssignment(*this, x), + _strategy); stack_depth--; if (val != _values[x]) { - solver_log::fixpoint << x << " = " << val << std::endl; + log::fixpoint << x << " = " << val << std::endl; IdSet > oldInfluence = _influence[x]; _influence[x].clear(); @@ -74,15 +102,17 @@ private: solve(_system.variable(*it)); } } else { - solver_log::fixpoint << indent() << x << " did not change" << std::endl; + log::fixpoint << indent() << x << " did not change: " + << x << " = " << val << std::endl; } } else { - solver_log::fixpoint << indent() << x << " is stable" << std::endl; + log::fixpoint << indent() << x << " is stable: " + << x << " = " << _values[x] << std::endl; } } 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]; @@ -90,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/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp index ac96107..d005048 100644 --- a/clang/lib/Analysis/Interval.cpp +++ b/clang/lib/Analysis/Interval.cpp @@ -702,40 +702,24 @@ void IntervalAnalysis::runOnAllBlocks() { } } - std::vector a; - - a.push_back(&system.constant(-infinity())); - a.push_back(&system.constant(0)); - system[system.variable("x")] = &system.maxExpression(a); - a.clear(); - - system.variable("y"); - - a.push_back(&system.variable("x")); - a.push_back(&system.variable("z")); - EqnExpr* minExpr = &system.expression(new Maximum(), a); - a.clear(); - - a.push_back(&system.constant(-infinity())); - a.push_back(minExpr); - system[system.variable("y")] = &system.maxExpression(a); - a.clear(); - - a.push_back(&system.constant(-infinity())); - a.push_back(&system.variable("y")); - system[system.variable("z")] = &system.maxExpression(a); - - llvm::errs() << toString(system) << "\n"; - system.indexMaxExpressions(); - DynamicMaxStrategy strategy(system); - DynamicVariableAssignment rho(system, strategy); - strategy.setRho(rho); + IdMap result = solve_for(system); for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + EqnVar& var = system.variable(i); + cout << var.name() << " = " << result[var] << endl; + } + + /* + DynamicMaxStrategy strategy(system); + DynamicVariableAssignment rho(system, strategy); + strategy.setRho(rho); + + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { EqnVar& var = system.variable(size - i - 1); llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n"; - } + } + */ } -- cgit v1.2.3 From a1b28d756fe52a53d9d4da4d23853969fd529115 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Tue, 23 Oct 2012 14:40:38 +1100 Subject: Make the recursive solver work properly. If you ignore the intermediate results for the strategy iteration phase then you're in the clear! I think! --- .gitignore | 12 ++++++++ impl/Complete.hpp | 30 +++++++++++++++++--- impl/EquationSystem.hpp | 2 +- impl/Expression.hpp | 10 ++++--- impl/MaxStrategy.hpp | 66 +++++++++++++++++++++++++++++++++++--------- impl/VariableAssignment.hpp | 17 ++++++++++-- impl/gmon.out | Bin 78165 -> 0 bytes impl/main.cpp | 7 +++-- impl/systems/gmon.out | Bin 79219 -> 0 bytes impl/systems/test.eqns | 28 +++++++++---------- impl/test/10.eqns | 9 ++++++ impl/test/10.soln | 9 ++++++ impl/test/7.eqns | 8 ++++++ impl/test/7.soln | 8 ++++++ impl/test/8.eqns | 4 +++ impl/test/8.soln | 4 +++ impl/test/9.eqns | 5 ++++ impl/test/9.soln | 5 ++++ 18 files changed, 182 insertions(+), 42 deletions(-) delete mode 100644 impl/gmon.out delete mode 100644 impl/systems/gmon.out create mode 100644 impl/test/10.eqns create mode 100644 impl/test/10.soln create mode 100644 impl/test/7.eqns create mode 100644 impl/test/7.soln create mode 100644 impl/test/8.eqns create mode 100644 impl/test/8.soln create mode 100644 impl/test/9.eqns create mode 100644 impl/test/9.soln diff --git a/.gitignore b/.gitignore index 3b01757..0173d7a 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,14 @@ /impl/build/* /impl/parser/* +*.log +*.dvi +*.ps +*.aux +*.blg +*.bbl +*.toc +*.lof +*.lot +*.out +*~ +gmon.out diff --git a/impl/Complete.hpp b/impl/Complete.hpp index 8c5559a..38b637e 100644 --- a/impl/Complete.hpp +++ b/impl/Complete.hpp @@ -7,23 +7,38 @@ template T infinity() { } +template +T unknown(const T&) { } template struct Complete { Complete() - : _value(0), _infinity(false) { } + : _value(0), _infinity(false), _unknown(false) { } Complete(const T& value) - : _value(value), _infinity(false) { } + : _value(value), _infinity(false), _unknown(false) { } Complete(const T& value, const bool& infinity) - : _value(value), _infinity(infinity) { + : _value(value), _infinity(infinity), _unknown(false) { assert(value != 0 || infinity == false); } Complete(const Complete& other) - : _value(other._value), _infinity(other._infinity) { } + : _value(other._value), _infinity(other._infinity), _unknown(other._unknown) { } + Complete(const Complete& other, bool unknown) + : _value(other._value), _infinity(other._infinity), _unknown(unknown) { } + + Complete asUnknown() const { + return Complete(*this, true); + } + Complete asKnown() const { + return Complete(*this, false); + } + bool isUnknown() const { + return _unknown; + } Complete& operator=(const Complete& other) { _value = other._value; _infinity = other._infinity; + _unknown = other._unknown; return *this; } Complete& operator+=(const Complete& other) { @@ -98,6 +113,7 @@ struct Complete { private: T _value; bool _infinity; + bool _unknown; }; template @@ -110,6 +126,8 @@ std::istream& operator>>(std::istream& cin, Complete& num) { template std::ostream& operator<<(std::ostream& cout, const Complete& num) { + if (num._unknown) + cout << "(unknown)"; if (num._infinity) { cout << (num._value > 0 ? "inf" : "-inf"); } else { @@ -122,5 +140,9 @@ template<> Complete infinity() { return Complete(1, true); } +template<> +Complete unknown(const Complete& x) { + return Complete(x, true); +} #endif diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp index 2fd24bd..a0ba8a1 100644 --- a/impl/EquationSystem.hpp +++ b/impl/EquationSystem.hpp @@ -31,7 +31,7 @@ struct EquationSystem { delete _expr_to_var; } - MaxExpression& maxExpression(const std::vector*>& arguments) { + MaxExpression& maxExpression(const std::vector*> arguments) { unsigned int id = _max_expressions.size(); Maximum* max = new Maximum(); MaxExpression* expr = new MaxExpression(id, *max, arguments); diff --git a/impl/Expression.hpp b/impl/Expression.hpp index 00bc9cd..0f3717f 100644 --- a/impl/Expression.hpp +++ b/impl/Expression.hpp @@ -143,7 +143,7 @@ struct OperatorExpression : public Expression { template struct MaxExpression : public OperatorExpression { MaxExpression(const unsigned int& id, const Maximum& op, const std::vector*>& arguments) - : OperatorExpression(op, arguments), _id(id) { } + : OperatorExpression(op, arguments), _id(id) {} const MaxExpression* toMaxExpression() const { return this; @@ -161,9 +161,11 @@ struct MaxExpression : public OperatorExpression { i < length; ++i) { const Domain value = this->_arguments[i]->eval(rho, strat); - if (bestValue < value) { - bestValue = value; - bestIndex = i; + if (!value.isUnknown()) { + if (bestValue < value) { + bestValue = value; + bestIndex = i; + } } } return bestIndex; diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp index 96aeef4..96d0492 100644 --- a/impl/MaxStrategy.hpp +++ b/impl/MaxStrategy.hpp @@ -31,7 +31,8 @@ template struct DynamicMaxStrategy : public MaxStrategy { DynamicMaxStrategy( const EquationSystem& system - ) : _system(system), + ) : _frozen(false), + _system(system), _rho(NULL), _values(system.maxExpressionCount(), 0), _stable(system.maxExpressionCount()), @@ -46,23 +47,26 @@ struct DynamicMaxStrategy : public MaxStrategy { } unsigned int get(const MaxExpression& e) const { - solve(e); + if (!_frozen) + solve(e); return _values[e]; } void invalidate(const Variable& v) const { log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; - _stable.filter(_var_influence[v]); - - IdSet > infl = _var_influence[v]; - _var_influence[v].clear(); - - for (typename IdSet >::iterator - it = infl.begin(), - end = infl.end(); - it != end; - ++it) { - solve(_system.maxExpression(*it)); + if (_system[v] && _stable.contains(*_system[v])) { + _stable.remove(*_system[v]); + _stable.filter(_var_influence[v]); + + IdSet > infl = _var_influence[v]; + _var_influence[v].clear(); + for (typename IdSet >::iterator + it = infl.begin(), + end = infl.end(); + it != end; + ++it) { + solve(_system.maxExpression(*it)); + } } } @@ -78,6 +82,7 @@ private: stack_depth--; if (val != _values[x]) { + log::strategy << x << " => " << *x.arguments()[val] << std::endl; IdSet > oldInfluence = _influence[x]; @@ -105,6 +110,16 @@ private: } } + const DynamicMaxStrategy& freeze() const { + _frozen = true; + return *this; + } + + const DynamicMaxStrategy& thaw() const { + _frozen = false; + return *this; + } + struct DependencyAssignment : public VariableAssignment{ DependencyAssignment(const DynamicMaxStrategy& strat, VariableAssignment& rho, @@ -123,6 +138,30 @@ private: const MaxExpression& _expr; }; + struct InvalidatingAssignment : public VariableAssignment{ + InvalidatingAssignment(DynamicVariableAssignment& rho) + : _rho(rho) { + } + ~InvalidatingAssignment() { + for (typename std::set*>::iterator + it = seen.begin(), + ei = seen.end(); + it != ei; + ++it) { + if (!_old_stable.contains(**it)) + _rho.invalidate(**it); + } + } + const Domain& operator[](const Variable& var) const { + seen.insert(&var); + return _rho[var]; + } + private: + DynamicVariableAssignment& _rho; + IdSet > _old_stable; + mutable std::set*> seen; + }; + struct DependencyStrategy : public MaxStrategy { DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression& expr) : _strat(strat), @@ -141,6 +180,7 @@ private: }; private: + mutable bool _frozen; const EquationSystem& _system; mutable DynamicVariableAssignment* _rho; mutable IdMap,unsigned int> _values; diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index ae5efd7..a1f0b5b 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -22,7 +22,7 @@ struct DynamicVariableAssignment : public VariableAssignment { const DynamicMaxStrategy& strat ) : _system(system), _strategy(strat), - _values(system.variableCount(), infinity()), + _values(system.variableCount(), unknown(infinity())), _stable(system.variableCount()), _influence(system.variableCount(), IdSet >(system.variableCount())) @@ -37,9 +37,20 @@ struct DynamicVariableAssignment : public VariableAssignment { log::fixpoint << indent() << "Invalidating " << x << std::endl; if (_stable.contains(x)) { _stable.remove(x); - _values[x] = infinity(); + _values[x] = unknown(infinity()); solve(x); + /* + IdSet > infl = _influence[x]; + _influence[x].clear(); + for (typename IdSet >::iterator + it = infl.begin(), + ei = infl.end(); + it != ei; + ++it) { + invalidate(_system.variable(*it)); + } + */ } } @@ -97,7 +108,9 @@ private: const EquationSystem& _system; const DynamicMaxStrategy& _strategy; mutable IdMap, Domain> _values; +public: mutable IdSet > _stable; +private: mutable IdMap,IdSet > > _influence; }; diff --git a/impl/gmon.out b/impl/gmon.out deleted file mode 100644 index aff812c..0000000 Binary files a/impl/gmon.out and /dev/null differ diff --git a/impl/main.cpp b/impl/main.cpp index e3e0ae3..b547c48 100644 --- a/impl/main.cpp +++ b/impl/main.cpp @@ -147,13 +147,14 @@ int main (int argc, char* argv[]) { 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() << " = " << rho[var] << endl; + if (variables.find(var.name()) != variables.end()) { + cout << var.name() << " = " << rho[var].asKnown() << endl; + } } } else { for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { Variable& var = system.variable(i); - cout << var.name() << " = " << rho[var] << endl; + cout << var.name() << " = " << rho[var].asKnown() << endl; } } diff --git a/impl/systems/gmon.out b/impl/systems/gmon.out deleted file mode 100644 index 3240978..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 fb23f1e..ee90a4b 100644 --- a/impl/systems/test.eqns +++ b/impl/systems/test.eqns @@ -1,16 +1,14 @@ 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)) -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-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[0], inf), min(i-2[0], inf)), 0, negi-2[0])) +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[0], inf), min(i-2[0], inf)), 0, i-2[0])) +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(1, i-3-pre)) +negi-3[0] = max(-inf, add(-1, 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-2[0] = max(-inf, add(1, i-2-pre)) +negi-2[0] = max(-inf, add(-1, negi-2-pre)) diff --git a/impl/test/10.eqns b/impl/test/10.eqns new file mode 100644 index 0000000..39598f4 --- /dev/null +++ b/impl/test/10.eqns @@ -0,0 +1,9 @@ +x = 0 +w = max(x,y,z,u,w) +y = w +z = w +u = a +a = b +b = c +c = d +d = w diff --git a/impl/test/10.soln b/impl/test/10.soln new file mode 100644 index 0000000..20a47ca --- /dev/null +++ b/impl/test/10.soln @@ -0,0 +1,9 @@ +x = 0 +w = 0 +y = 0 +z = 0 +u = 0 +a = 0 +b = 0 +c = 0 +d = 0 diff --git a/impl/test/7.eqns b/impl/test/7.eqns new file mode 100644 index 0000000..1f69268 --- /dev/null +++ b/impl/test/7.eqns @@ -0,0 +1,8 @@ +x = 0 +y = max(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 diff --git a/impl/test/8.eqns b/impl/test/8.eqns new file mode 100644 index 0000000..c9e9c4e --- /dev/null +++ b/impl/test/8.eqns @@ -0,0 +1,4 @@ +x = 0 +w = max(x,y,z) +y = w +z = w diff --git a/impl/test/8.soln b/impl/test/8.soln new file mode 100644 index 0000000..1945057 --- /dev/null +++ b/impl/test/8.soln @@ -0,0 +1,4 @@ +x = 0 +w = 0 +y = 0 +z = 0 diff --git a/impl/test/9.eqns b/impl/test/9.eqns new file mode 100644 index 0000000..b85e118 --- /dev/null +++ b/impl/test/9.eqns @@ -0,0 +1,5 @@ +x = 0 +w = max(x,y,z,u) +y = w +z = w +u = w diff --git a/impl/test/9.soln b/impl/test/9.soln new file mode 100644 index 0000000..616c5e5 --- /dev/null +++ b/impl/test/9.soln @@ -0,0 +1,5 @@ +x = 0 +w = 0 +y = 0 +z = 0 +u = 0 -- cgit v1.2.3 From 0c62b0ba1b307ddc626a62127d835738775bb20d Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Tue, 23 Oct 2012 15:32:35 +1100 Subject: Fix the merge. --- impl/MaxStrategy.hpp | 61 ++++++--------------------------------------- impl/VariableAssignment.hpp | 19 +++++++------- impl/main.cpp | 15 ----------- 3 files changed, 17 insertions(+), 78 deletions(-) diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp index ba7cc11..3ed7972 100644 --- a/impl/MaxStrategy.hpp +++ b/impl/MaxStrategy.hpp @@ -42,38 +42,30 @@ struct DynamicMaxStrategy : public MaxStrategy { _influence(system.maxExpressionCount(), IdSet >(system.maxExpressionCount())), _var_influence(system.variableCount(), - IdSet >(system.maxExpressionCount())), - _frozen(false) + IdSet >(system.maxExpressionCount())) {} - 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 { + // slightly hacky + return const_cast*>(this)->get(e); + } + + unsigned int get(const MaxExpression& e) { if (!_frozen) solve(e); return _values[e]; } - void invalidate(const Variable& v) const { + void invalidate(const Variable& v) { log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; if (_system[v] && _stable.contains(*_system[v])) { _stable.remove(*_system[v]); _stable.filter(_var_influence[v]); - + IdSet > infl = _var_influence[v]; _var_influence[v].clear(); for (typename IdSet >::iterator @@ -203,46 +195,9 @@ private: 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 cfce925..3f4ff70 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -22,8 +22,7 @@ template struct DynamicVariableAssignment : public VariableAssignment { DynamicVariableAssignment( const EquationSystem& system, - DynamicMaxStrategy& strat, - const Domain& value=infinity() + DynamicMaxStrategy& strat ) : _system(system), _strategy(strat), _values(system.variableCount(), unknown(infinity())), @@ -46,7 +45,8 @@ struct DynamicVariableAssignment : public VariableAssignment { } const Domain& operator[](const Variable& var) const { - return _values[var]; + // slightly hacky + return const_cast&>(*this)[var]; } const Domain& operator[](const Variable& var) { @@ -60,7 +60,7 @@ struct DynamicVariableAssignment : public VariableAssignment { if (_stable.contains(x)) { _stable.remove(x); _values[x] = unknown(infinity()); - + solve(x); /* IdSet > infl = _influence[x]; @@ -128,12 +128,11 @@ private: }; const EquationSystem& _system; - const DynamicMaxStrategy& _strategy; - mutable IdMap, Domain> _values; -public: - mutable IdSet > _stable; -private: - mutable IdMap,IdSet > > _influence; + DynamicMaxStrategy& _strategy; + IdMap, Domain> _values; + IdSet > _stable; + IdMap,IdSet > > _influence; + bool _frozen; }; #endif diff --git a/impl/main.cpp b/impl/main.cpp index 02faca5..b547c48 100644 --- a/impl/main.cpp +++ b/impl/main.cpp @@ -140,20 +140,6 @@ 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); @@ -171,7 +157,6 @@ int main (int argc, char* argv[]) { cout << var.name() << " = " << rho[var].asKnown() << endl; } } - */ parser -> free(parser); tokens -> free(tokens); -- cgit v1.2.3 From 8253e957e54d31699b4bd827300bc1fa794c4660 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Tue, 23 Oct 2012 18:03:33 +1100 Subject: Another fix, with a test for what the problem was. --- impl/VariableAssignment.hpp | 13 ++----------- impl/test/11.eqns | 2 ++ impl/test/11.soln | 2 ++ 3 files changed, 6 insertions(+), 11 deletions(-) create mode 100644 impl/test/11.eqns create mode 100644 impl/test/11.soln diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index 3f4ff70..21226ac 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -62,17 +62,8 @@ struct DynamicVariableAssignment : public VariableAssignment { _values[x] = unknown(infinity()); solve(x); - /* - IdSet > infl = _influence[x]; - _influence[x].clear(); - for (typename IdSet >::iterator - it = infl.begin(), - ei = infl.end(); - it != ei; - ++it) { - invalidate(_system.variable(*it)); - } - */ + if (_values[x] == infinity()) + _values[x] = _values[x].asKnown(); } } diff --git a/impl/test/11.eqns b/impl/test/11.eqns new file mode 100644 index 0000000..4edc114 --- /dev/null +++ b/impl/test/11.eqns @@ -0,0 +1,2 @@ +x = y +y = max(-100000, y+1) diff --git a/impl/test/11.soln b/impl/test/11.soln new file mode 100644 index 0000000..cdfcb1f --- /dev/null +++ b/impl/test/11.soln @@ -0,0 +1,2 @@ +x = inf +y = inf -- cgit v1.2.3 From a3860a4cd6ca6a1ee664634ea472b5487535b2b5 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Wed, 24 Oct 2012 10:34:15 +1100 Subject: Add a fix for mutually-recursive infinite things So now it will solve correctly for x = y + 1 y = max(0, x + 1) I also added in tests for this (and a slightly different form with `x` going through another variable, `z`, for indirection). The tests will also stop now after five seconds of execution. If they can't be solved in five seconds then they're considered a failure. --- impl/VariableAssignment.hpp | 19 +++++++++++++++---- impl/test/12.eqns | 2 ++ impl/test/12.soln | 2 ++ impl/test/13.eqns | 3 +++ impl/test/13.soln | 3 +++ impl/test/run | 5 ++++- 6 files changed, 29 insertions(+), 5 deletions(-) create mode 100644 impl/test/12.eqns create mode 100644 impl/test/12.soln create mode 100644 impl/test/13.eqns create mode 100644 impl/test/13.soln diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index 21226ac..19403a8 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -55,15 +55,26 @@ struct DynamicVariableAssignment : public VariableAssignment { return _values[var]; } - void invalidate(const Variable& x) { + void invalidate(const Variable& x, bool also_solve=true) { log::fixpoint << indent() << "Invalidating " << x << std::endl; if (_stable.contains(x)) { _stable.remove(x); _values[x] = unknown(infinity()); - solve(x); - if (_values[x] == infinity()) - _values[x] = _values[x].asKnown(); + IdSet > infl = _influence[x]; + for (typename IdSet >::iterator + it = infl.begin(), + ei = infl.end(); + it != ei; + ++it) { + invalidate(_system.variable(*it), false); + } + + if (also_solve) { + solve(x); + if (_values[x] == infinity()) + _values[x] = _values[x].asKnown(); + } } } diff --git a/impl/test/12.eqns b/impl/test/12.eqns new file mode 100644 index 0000000..91be47b --- /dev/null +++ b/impl/test/12.eqns @@ -0,0 +1,2 @@ +x = y + 1 +y = max(0, x + 1) diff --git a/impl/test/12.soln b/impl/test/12.soln new file mode 100644 index 0000000..cdfcb1f --- /dev/null +++ b/impl/test/12.soln @@ -0,0 +1,2 @@ +x = inf +y = inf diff --git a/impl/test/13.eqns b/impl/test/13.eqns new file mode 100644 index 0000000..ce399ef --- /dev/null +++ b/impl/test/13.eqns @@ -0,0 +1,3 @@ +x = y + 1 +y = max(0, z) +z = x diff --git a/impl/test/13.soln b/impl/test/13.soln new file mode 100644 index 0000000..ff37347 --- /dev/null +++ b/impl/test/13.soln @@ -0,0 +1,3 @@ +x = inf +y = inf +z = inf diff --git a/impl/test/run b/impl/test/run index 0c1886d..826bbde 100644 --- a/impl/test/run +++ b/impl/test/run @@ -7,7 +7,10 @@ FAILED=0 echo "Testing binary: $1 in directory $DIR" while [ -f "$DIR/$NUM.eqns" ] do - OUTPUT=$($1 "$DIR/$NUM.eqns") + OUTPUT=$(timeout 5s $1 "$DIR/$NUM.eqns") + if [ $? -eq 124 ]; then + OUTPUT="did not terminate" + fi DIFF=$(echo "$OUTPUT" | diff - "$DIR/$NUM.soln") if [ ! -z "$DIFF" ]; then echo "==================" -- cgit v1.2.3