diff options
Diffstat (limited to 'impl')
| -rw-r--r-- | impl/Complete.hpp | 6 | ||||
| -rw-r--r-- | impl/Expression.hpp | 14 | ||||
| -rw-r--r-- | impl/MaxStrategy.hpp | 76 | ||||
| -rw-r--r-- | impl/VariableAssignment.hpp | 36 | ||||
| -rw-r--r-- | impl/main.cpp | 15 | ||||
| -rw-r--r-- | impl/systems/test.eqns | 32 |
6 files changed, 146 insertions, 33 deletions
diff --git a/impl/Complete.hpp b/impl/Complete.hpp index 38b637e..336ab24 100644 --- a/impl/Complete.hpp +++ b/impl/Complete.hpp @@ -55,7 +55,11 @@ struct Complete { return Complete<T>(- _value, _infinity); } Complete operator+(const Complete& other) const { - if (_infinity) { + if (_infinity && other._infinity) { + if (_value > 0 || other._value > 0) + return Complete<T>(1, true); + return Complete<T>(-1, true); + } else if (_infinity) { return *this; } else if (other._infinity) { return other; diff --git a/impl/Expression.hpp b/impl/Expression.hpp index 0f3717f..cba9582 100644 --- a/impl/Expression.hpp +++ b/impl/Expression.hpp @@ -27,6 +27,10 @@ struct Expression { return NULL; } + virtual MaxExpression<Domain>* toMaxExpression() { + return NULL; + } + virtual Domain eval(const VariableAssignment<Domain>&) const = 0; virtual Domain eval(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>&) const { @@ -106,6 +110,10 @@ struct OperatorExpression : public Expression<Domain> { return _operator.eval(argumentValues); } + std::vector<Expression<Domain>*>& arguments() { + return _arguments; + } + const std::vector<Expression<Domain>*>& arguments() const { return _arguments; } @@ -137,7 +145,7 @@ struct OperatorExpression : public Expression<Domain> { private: const Operator<Domain>& _operator; protected: - const std::vector<Expression<Domain>*> _arguments; + std::vector<Expression<Domain>*> _arguments; }; template<typename Domain> @@ -145,6 +153,10 @@ 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) {} + MaxExpression* toMaxExpression() { + return this; + } + const MaxExpression* toMaxExpression() const { return this; } diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp index 96d0492..ba7cc11 100644 --- a/impl/MaxStrategy.hpp +++ b/impl/MaxStrategy.hpp @@ -10,6 +10,9 @@ template<typename Domain> struct MaxStrategy { virtual ~MaxStrategy() { } virtual unsigned int get(const MaxExpression<Domain>& e) const = 0; + virtual unsigned int get(const MaxExpression<Domain>& e) { + return const_cast<const MaxStrategy*>(this)->get(e); + } }; unsigned int stack_depth = 1; @@ -39,9 +42,22 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> { _influence(system.maxExpressionCount(), IdSet<MaxExpression<Domain> >(system.maxExpressionCount())), _var_influence(system.variableCount(), - IdSet<MaxExpression<Domain> >(system.maxExpressionCount())) + IdSet<MaxExpression<Domain> >(system.maxExpressionCount())), + _frozen(false) {} + void freeze() { + _frozen = true; + } + + void thaw() { + _frozen = false; + } + + bool is_frozen() { + return _frozen; + } + void setRho(DynamicVariableAssignment<Domain>& rho) { _rho = ρ } @@ -71,7 +87,7 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> { } private: - void solve(const MaxExpression<Domain>& x) const { + void solve(const MaxExpression<Domain>& x) { if (!_stable.contains(x)) { _stable.insert(x); log::strategy << indent() << "Stabilise " << x << std::endl; @@ -121,7 +137,7 @@ private: } struct DependencyAssignment : public VariableAssignment<Domain>{ - DependencyAssignment(const DynamicMaxStrategy& strat, + DependencyAssignment(DynamicMaxStrategy& strat, VariableAssignment<Domain>& rho, const MaxExpression<Domain>& expr) : _strat(strat), @@ -133,7 +149,7 @@ private: return _rho[var]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; VariableAssignment<Domain>& _rho; const MaxExpression<Domain>& _expr; }; @@ -163,7 +179,7 @@ private: }; struct DependencyStrategy : public MaxStrategy<Domain> { - DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr) + DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr) : _strat(strat), _expr(expr) { } @@ -175,20 +191,58 @@ private: return _strat._values[e]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; const MaxExpression<Domain>& _expr; }; private: mutable bool _frozen; const EquationSystem<Domain>& _system; - mutable DynamicVariableAssignment<Domain>* _rho; - mutable IdMap<MaxExpression<Domain>,unsigned int> _values; - mutable IdSet<MaxExpression<Domain> > _stable; - mutable IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence; - mutable IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence; + DynamicVariableAssignment<Domain>* _rho; + IdMap<MaxExpression<Domain>,unsigned int> _values; + IdSet<MaxExpression<Domain> > _stable; + IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence; + IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence; + bool _frozen; }; + +template<typename T> +IdMap<Variable<T>,T> solve_for(const EquationSystem<T>& system) { + IdMap<Variable<T>,T> result(system.variableCount(), infinity<T>()); + + DynamicMaxStrategy<T> strategy(system); + DynamicVariableAssignment<T> rho(system, strategy, -infinity<T>()); + 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<T>& var = system.variable(i); + T val = rho[var]; + if (result[var] != val) { + result[var] = val; + changed = true; + } + } + } while(changed); + + return result; +} + + /*template<typename Domain> std::ostream& operator<<(std::ostream& cout, const MaxStrategy<Domain>& strat) { strat.print(cout); diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index a1f0b5b..cfce925 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -8,6 +8,9 @@ template<typename Domain> struct VariableAssignment { virtual ~VariableAssignment() { } virtual const Domain& operator[](const Variable<Domain>&) const = 0; + virtual const Domain& operator[](const Variable<Domain>& x) { + return (*const_cast<const VariableAssignment*>(this))[x]; + } }; #include "EquationSystem.hpp" @@ -19,21 +22,40 @@ template<typename Domain> struct DynamicVariableAssignment : public VariableAssignment<Domain> { DynamicVariableAssignment( const EquationSystem<Domain>& system, - const DynamicMaxStrategy<Domain>& strat + DynamicMaxStrategy<Domain>& strat, + const Domain& value=infinity<Domain>() ) : _system(system), _strategy(strat), _values(system.variableCount(), unknown(infinity<Domain>())), _stable(system.variableCount()), _influence(system.variableCount(), - IdSet<Variable<Domain> >(system.variableCount())) + IdSet<Variable<Domain> >(system.variableCount())), + _frozen(false) { } + void freeze() { + _frozen = true; + } + + void thaw() { + _frozen = false; + } + + bool is_frozen() { + return _frozen; + } + const Domain& operator[](const Variable<Domain>& var) const { - solve(var); return _values[var]; } - void invalidate(const Variable<Domain>& x) const { + const Domain& operator[](const Variable<Domain>& var) { + if (!_frozen) + solve(var); + return _values[var]; + } + + void invalidate(const Variable<Domain>& x) { log::fixpoint << indent() << "Invalidating " << x << std::endl; if (_stable.contains(x)) { _stable.remove(x); @@ -56,7 +78,7 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> { private: - void solve(const Variable<Domain>& x) const { + void solve(const Variable<Domain>& x) { if (!_stable.contains(x)) { _stable.insert(x); log::fixpoint << indent() << "Stabilise " << x << std::endl; @@ -93,7 +115,7 @@ private: } struct DependencyAssignment : public VariableAssignment<Domain> { - DependencyAssignment(const DynamicVariableAssignment& assignment, const Variable<Domain>& var) + DependencyAssignment(DynamicVariableAssignment& assignment, const Variable<Domain>& var) : _assignment(assignment), _var(var) { } const Domain& operator[](const Variable<Domain>& x) const { const Domain& result = _assignment[x]; @@ -101,7 +123,7 @@ private: return result; } private: - const DynamicVariableAssignment& _assignment; + DynamicVariableAssignment& _assignment; const Variable<Domain>& _var; }; diff --git a/impl/main.cpp b/impl/main.cpp index b547c48..02faca5 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<Variable<ZBar>,ZBar> result = solve_for(system); + if (variables.size() > 0) { + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + Variable<ZBar>& 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<ZBar>& var = system.variable(i); + cout << var.name() << " = " << result[var] << endl; + } + } + /* DynamicMaxStrategy<ZBar> strategy(system); DynamicVariableAssignment<ZBar> rho(system, strategy); strategy.setRho(rho); @@ -157,6 +171,7 @@ int main (int argc, char* argv[]) { cout << var.name() << " = " << rho[var].asKnown() << endl; } } + */ parser -> free(parser); tokens -> free(tokens); diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns index ee90a4b..a3b521d 100644 --- a/impl/systems/test.eqns +++ b/impl/systems/test.eqns @@ -1,14 +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[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-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)) -negi-2[0] = max(-inf, add(-1, negi-2-pre)) +neg-i-2[0] = max(-inf, add(-1, neg-i-2-pre)) |