diff options
Diffstat (limited to 'impl')
-rw-r--r-- | impl/Expression.hpp | 3 | ||||
-rw-r--r-- | impl/MaxStrategy.hpp | 55 | ||||
-rw-r--r-- | impl/VariableAssignment.hpp | 7 | ||||
-rw-r--r-- | impl/main.cpp | 3 | ||||
-rw-r--r-- | impl/systems/test.eqns | 24 | ||||
-rw-r--r-- | impl/test/1.eqns | 2 | ||||
-rw-r--r-- | impl/test/10.soln | 10 | ||||
-rw-r--r-- | impl/test/14.eqns | 3 | ||||
-rw-r--r-- | impl/test/14.soln | 3 | ||||
-rw-r--r-- | impl/test/7.soln | 4 | ||||
-rw-r--r-- | impl/test/8.soln | 2 | ||||
-rw-r--r-- | impl/test/9.soln | 4 | ||||
-rw-r--r-- | impl/test/run | 6 |
13 files changed, 50 insertions, 76 deletions
diff --git a/impl/Expression.hpp b/impl/Expression.hpp index dcf7201..619bc7e 100644 --- a/impl/Expression.hpp +++ b/impl/Expression.hpp @@ -197,8 +197,7 @@ struct MaxExpression : public OperatorExpression<Domain> { return this->_arguments[strat.get(*this)]->eval(rho, strat); } - unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const { - unsigned int bestIndex = const_cast<const MaxStrategy<Domain>&>(strat).get(*this); + unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat, unsigned int bestIndex) const { Domain bestValue = this->_arguments[bestIndex]->eval(rho, strat); for (unsigned int i = 0, length = this->_arguments.size(); diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp index 71ea4f4..6fee921 100644 --- a/impl/MaxStrategy.hpp +++ b/impl/MaxStrategy.hpp @@ -20,7 +20,7 @@ unsigned int stack_depth = 1; std::string indent() { std::string result = ""; for (unsigned int i = 0; i < stack_depth; ++i) { - result += '\t'; + result += ' '; } return result; } @@ -39,22 +39,13 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> { _values(system.maxExpressionCount(), 0), _stable(system.maxExpressionCount()), _influence(system.maxExpressionCount(), - IdSet<MaxExpression<Domain> >(system.maxExpressionCount())), - _changed(false) + IdSet<MaxExpression<Domain> >(system.maxExpressionCount())) {} void setRho(DynamicVariableAssignment<Domain>& rho) { _rho = ρ } - void hasChanged(bool c) { - _changed = c; - } - - bool hasChanged() const { - return _changed; - } - unsigned int get(const MaxExpression<Domain>& e) const { log::strategy << indent() << "Look up " << e << std::endl; return _values[e]; @@ -99,32 +90,32 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> { private: void solve(const MaxExpression<Domain>& x) { if (!_stable.contains(x)) { + std::cerr << indent() << x.id() << std::endl; _stable.insert(x); log::strategy << indent() << "Stabilise " << x << std::endl; stack_depth++; DependencyAssignment assignment(*this, *_rho, x); DependencyStrategy depStrat(*this, x); - unsigned int val = x.bestStrategy(assignment, depStrat); + unsigned int val = x.bestStrategy(assignment, depStrat, _values[x]); stack_depth--; if (val != _values[x]) { + std::cerr << indent() << "-" << std::endl; log::strategy << x << " => " << *x.arguments()[val] << std::endl; - IdSet<MaxExpression<Domain> > oldInfluence = _influence[x]; - //_influence[x].clear(); _values[x] = val; - _changed = true; _rho->invalidate(*_system.varFromExpr(x)); //_rho->stabilise(); - _stable.filter(oldInfluence); - + IdSet<MaxExpression<Domain> > infl = _influence[x]; + _stable.filter(infl); + for (typename IdSet<MaxExpression<Domain> >::iterator - it = oldInfluence.begin(), - end = oldInfluence.end(); + it = infl.begin(), + end = infl.end(); it != end; ++it) { solve(_system.maxExpression(*it)); @@ -150,6 +141,7 @@ private: } const Domain operator[](const Variable<Domain>& var) { // solve the strategy for this variable, too + // recursive magic! _strat.solve(*_strat._system[var]); _strat._influence[*_strat._system[var]].insert(_expr); return _rho[var]; @@ -186,7 +178,6 @@ private: IdMap<MaxExpression<Domain>,unsigned int> _values; IdSet<MaxExpression<Domain> > _stable; IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence; - bool _changed; }; @@ -200,28 +191,12 @@ struct Solver { } Domain solve(Variable<Domain>& var) { - MaxExpression<Domain>& rhs = *_system[var]; - - // _rho automatically keeps up to date with changes made to the - // strategy, so you don't need to stabilise it - + MaxExpression<Domain>& rhs = *_system[var]; + // this will automatically work sufficiently to get the final + // strategy for this variable's RHS _strategy.get(rhs); - - /* - do { - _strategy.hasChanged(false); - - log::debug << "Stabilise assignment (toplevel)" << std::endl; - _rho.stabilise(); - - log::debug << "Improve strategy (toplevel)" << std::endl; - // improve strategy - _strategy.get(rhs); - log::debug << (_strategy.hasChanged() ? "Strategy has changed - loop again" : "Strategy has not changed - terminate") << std::endl; - } while (_strategy.hasChanged()); - */ - + // this will automatically solve for the value of the RHS, if required return _rho[var]; } private: diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index 2e081e6..e575d60 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -34,13 +34,6 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> { return _values[var]; } - /*void stabilise() { - if (!_unstable.empty()) { - Variable<Domain>& var = _system.variable(*_unstable.begin()); - solve(var); - } - }*/ - void invalidate(const Variable<Domain>& x) { if (!_unstable.contains(x)) { log::fixpoint << indent() << "Invalidating " << x << std::endl; diff --git a/impl/main.cpp b/impl/main.cpp index 1fed389..be9cc82 100644 --- a/impl/main.cpp +++ b/impl/main.cpp @@ -159,8 +159,7 @@ int main (int argc, char* argv[]) { } } else { for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { - Variable<ZBar>& var = system.variable(i); - solver.solve(var); + solver.solve(system.variable(i)); } } clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &finish); diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns index a3b521d..a320049 100644 --- a/impl/systems/test.eqns +++ b/impl/systems/test.eqns @@ -1,19 +1,19 @@ 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)) +neg-i-1-pre = max(-inf, neg-i-6[0], neg-i-2[0]) +i-1-pre = max(-inf, i-6[0], i-2[0]) +neg-i-5-pre = max(-inf, neg-i-1-pre) +i-5-pre = max(-inf, min(2, i-1-pre)) +neg-i-0-pre = max(-inf, min(-3, neg-i-1-pre)) +i-0-pre = max(-inf, i-1-pre) +neg-i-4-pre = max(-inf, neg-i-5-pre) +i-4-pre = max(-inf, min(1, i-5-pre)) +neg-i-3-pre = max(-inf, min(-2, neg-i-5-pre)) +i-3-pre = max(-inf, 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])) +neg-i-2-pre = max(-inf, neg-i-4[0], neg-i-3[0]) +i-2-pre = max(-inf, i-4[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)) diff --git a/impl/test/1.eqns b/impl/test/1.eqns index 0cdfd24..34c51de 100644 --- a/impl/test/1.eqns +++ b/impl/test/1.eqns @@ -1,3 +1,3 @@ -x = max(0, min(-1 + x, y)) y = max(0, 5 + x, x) z = max(0, 1 + z, 0 + x) +x = max(0, min(-1 + x, y)) diff --git a/impl/test/10.soln b/impl/test/10.soln index 20a47ca..238b7d5 100644 --- a/impl/test/10.soln +++ b/impl/test/10.soln @@ -1,9 +1,9 @@ -x = 0 -w = 0 -y = 0 -z = 0 -u = 0 a = 0 b = 0 c = 0 d = 0 +u = 0 +w = 0 +x = 0 +y = 0 +z = 0 diff --git a/impl/test/14.eqns b/impl/test/14.eqns new file mode 100644 index 0000000..6c28481 --- /dev/null +++ b/impl/test/14.eqns @@ -0,0 +1,3 @@ +x = 0 +y = max(x, z) +z = y + 1 diff --git a/impl/test/14.soln b/impl/test/14.soln new file mode 100644 index 0000000..c0301bb --- /dev/null +++ b/impl/test/14.soln @@ -0,0 +1,3 @@ +x = 0 +y = inf +z = inf diff --git a/impl/test/7.soln b/impl/test/7.soln index 0d85468..2c9b183 100644 --- a/impl/test/7.soln +++ b/impl/test/7.soln @@ -1,8 +1,8 @@ -x = 0 -y = 0 a = 0 b = 0 c = 0 d = 0 e = 0 f = 0 +x = 0 +y = 0 diff --git a/impl/test/8.soln b/impl/test/8.soln index 1945057..73d26df 100644 --- a/impl/test/8.soln +++ b/impl/test/8.soln @@ -1,4 +1,4 @@ -x = 0 w = 0 +x = 0 y = 0 z = 0 diff --git a/impl/test/9.soln b/impl/test/9.soln index 616c5e5..7116cf4 100644 --- a/impl/test/9.soln +++ b/impl/test/9.soln @@ -1,5 +1,5 @@ -x = 0 +u = 0 w = 0 +x = 0 y = 0 z = 0 -u = 0 diff --git a/impl/test/run b/impl/test/run index 169edda..d15fb68 100644 --- a/impl/test/run +++ b/impl/test/run @@ -7,15 +7,17 @@ FAILED=0 echo "Testing binary: $1 in directory $DIR" while [ -f "$DIR/$NUM.eqns" ] do + cat "$DIR/$NUM.soln" | sort > "/tmp/$NUM.soln.tmp" + mv "/tmp/$NUM.soln.tmp" "$DIR/$NUM.soln" 2> /dev/null OUTPUT=$(timeout 5s $1 "$DIR/$NUM.eqns" 2> /dev/null) if [ $? -eq 124 ]; then OUTPUT="did not terminate" fi - DIFF=$(echo "$OUTPUT" | diff - "$DIR/$NUM.soln") + DIFF=$(echo "$OUTPUT" | sort | diff - "$DIR/$NUM.soln") if [ ! -z "$DIFF" ]; then echo "==================" echo "Test #$NUM failed:" - echo "$OUTPUT" | sdiff - "$DIR/$NUM.soln" + echo "$OUTPUT" | sort | sdiff - "$DIR/$NUM.soln" echo FAILED=$(($FAILED + 1)) fi |