diff options
Diffstat (limited to 'impl')
-rw-r--r-- | impl/Complete.hpp | 30 | ||||
-rw-r--r-- | impl/EquationSystem.hpp | 2 | ||||
-rw-r--r-- | impl/Expression.hpp | 10 | ||||
-rw-r--r-- | impl/MaxStrategy.hpp | 66 | ||||
-rw-r--r-- | impl/VariableAssignment.hpp | 17 | ||||
-rw-r--r-- | impl/gmon.out | bin | 78165 -> 0 bytes | |||
-rw-r--r-- | impl/main.cpp | 7 | ||||
-rw-r--r-- | impl/systems/gmon.out | bin | 79219 -> 0 bytes | |||
-rw-r--r-- | impl/systems/test.eqns | 28 | ||||
-rw-r--r-- | impl/test/10.eqns | 9 | ||||
-rw-r--r-- | impl/test/10.soln | 9 | ||||
-rw-r--r-- | impl/test/7.eqns | 8 | ||||
-rw-r--r-- | impl/test/7.soln | 8 | ||||
-rw-r--r-- | impl/test/8.eqns | 4 | ||||
-rw-r--r-- | impl/test/8.soln | 4 | ||||
-rw-r--r-- | impl/test/9.eqns | 5 | ||||
-rw-r--r-- | impl/test/9.soln | 5 |
17 files changed, 170 insertions, 42 deletions
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<typename T> T infinity() { } +template<typename T> +T unknown(const T&) { } template<typename T> 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<typename Z> @@ -110,6 +126,8 @@ std::istream& operator>>(std::istream& cin, Complete<Z>& num) { template<typename Z> std::ostream& operator<<(std::ostream& cout, const Complete<Z>& num) { + if (num._unknown) + cout << "(unknown)"; if (num._infinity) { cout << (num._value > 0 ? "inf" : "-inf"); } else { @@ -122,5 +140,9 @@ template<> Complete<int> infinity() { return Complete<int>(1, true); } +template<> +Complete<int> unknown(const Complete<int>& x) { + return Complete<int>(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<Domain>& maxExpression(const std::vector<Expression<Domain>*>& arguments) { + 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); 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<Domain> { 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) { } + : OperatorExpression<Domain>(op, arguments), _id(id) {} const MaxExpression* toMaxExpression() const { return this; @@ -161,9 +161,11 @@ struct MaxExpression : public OperatorExpression<Domain> { 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<typename Domain> struct DynamicMaxStrategy : public MaxStrategy<Domain> { DynamicMaxStrategy( const EquationSystem<Domain>& system - ) : _system(system), + ) : _frozen(false), + _system(system), _rho(NULL), _values(system.maxExpressionCount(), 0), _stable(system.maxExpressionCount()), @@ -46,23 +47,26 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> { } unsigned int get(const MaxExpression<Domain>& e) const { - solve(e); + if (!_frozen) + solve(e); return _values[e]; } void invalidate(const Variable<Domain>& v) const { log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; - _stable.filter(_var_influence[v]); - - IdSet<MaxExpression<Domain> > infl = _var_influence[v]; - _var_influence[v].clear(); - - for (typename IdSet<MaxExpression<Domain> >::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<MaxExpression<Domain> > infl = _var_influence[v]; + _var_influence[v].clear(); + for (typename IdSet<MaxExpression<Domain> >::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<MaxExpression<Domain> > 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<Domain>{ DependencyAssignment(const DynamicMaxStrategy& strat, VariableAssignment<Domain>& rho, @@ -123,6 +138,30 @@ private: const MaxExpression<Domain>& _expr; }; + struct InvalidatingAssignment : public VariableAssignment<Domain>{ + InvalidatingAssignment(DynamicVariableAssignment<Domain>& rho) + : _rho(rho) { + } + ~InvalidatingAssignment() { + for (typename std::set<const Variable<Domain>*>::iterator + it = seen.begin(), + ei = seen.end(); + it != ei; + ++it) { + if (!_old_stable.contains(**it)) + _rho.invalidate(**it); + } + } + const Domain& operator[](const Variable<Domain>& var) const { + seen.insert(&var); + return _rho[var]; + } + private: + DynamicVariableAssignment<Domain>& _rho; + IdSet<Variable<Domain> > _old_stable; + mutable std::set<const Variable<Domain>*> seen; + }; + struct DependencyStrategy : public MaxStrategy<Domain> { DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr) : _strat(strat), @@ -141,6 +180,7 @@ private: }; private: + mutable bool _frozen; const EquationSystem<Domain>& _system; mutable DynamicVariableAssignment<Domain>* _rho; mutable IdMap<MaxExpression<Domain>,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<Domain> { const DynamicMaxStrategy<Domain>& strat ) : _system(system), _strategy(strat), - _values(system.variableCount(), infinity<Domain>()), + _values(system.variableCount(), unknown(infinity<Domain>())), _stable(system.variableCount()), _influence(system.variableCount(), IdSet<Variable<Domain> >(system.variableCount())) @@ -37,9 +37,20 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> { log::fixpoint << indent() << "Invalidating " << x << std::endl; if (_stable.contains(x)) { _stable.remove(x); - _values[x] = infinity<Domain>(); + _values[x] = unknown(infinity<Domain>()); solve(x); + /* + IdSet<Variable<Domain> > infl = _influence[x]; + _influence[x].clear(); + for (typename IdSet<Variable<Domain> >::iterator + it = infl.begin(), + ei = infl.end(); + it != ei; + ++it) { + invalidate(_system.variable(*it)); + } + */ } } @@ -97,7 +108,9 @@ private: const EquationSystem<Domain>& _system; const DynamicMaxStrategy<Domain>& _strategy; mutable IdMap<Variable<Domain>, Domain> _values; +public: mutable IdSet<Variable<Domain> > _stable; +private: mutable IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence; }; diff --git a/impl/gmon.out b/impl/gmon.out Binary files differdeleted file mode 100644 index aff812c..0000000 --- a/impl/gmon.out +++ /dev/null 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<ZBar>& 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<ZBar>& 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 Binary files differdeleted file mode 100644 index 3240978..0000000 --- a/impl/systems/gmon.out +++ /dev/null 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 |