summaryrefslogtreecommitdiff
path: root/impl
diff options
context:
space:
mode:
Diffstat (limited to 'impl')
-rw-r--r--impl/Expression.hpp3
-rw-r--r--impl/MaxStrategy.hpp62
-rw-r--r--impl/VariableAssignment.hpp7
-rw-r--r--impl/main.cpp3
-rw-r--r--impl/systems/test.eqns24
-rw-r--r--impl/test/1.eqns2
-rw-r--r--impl/test/10.soln10
-rw-r--r--impl/test/14.eqns3
-rw-r--r--impl/test/14.soln3
-rw-r--r--impl/test/7.soln4
-rw-r--r--impl/test/8.soln2
-rw-r--r--impl/test/9.soln4
-rw-r--r--impl/test/run6
13 files changed, 51 insertions, 82 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 5534597..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,24 +39,13 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
_values(system.maxExpressionCount(), 0),
_stable(system.maxExpressionCount()),
_influence(system.maxExpressionCount(),
- IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
- _var_influence(system.variableCount(),
- IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
- _changed(false)
+ IdSet<MaxExpression<Domain> >(system.maxExpressionCount()))
{}
void setRho(DynamicVariableAssignment<Domain>& rho) {
_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];
@@ -70,9 +59,8 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
void invalidate(const Variable<Domain>& v) {
log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl;
- //log::debug << indent() << " var-influence sets " << _var_influence << std::endl;
- IdSet<MaxExpression<Domain> > infl = _var_influence[v];
+ IdSet<MaxExpression<Domain> > infl = _influence[*_system[v]];
for (typename IdSet<MaxExpression<Domain> >::iterator
it = infl.begin(),
end = infl.end();
@@ -102,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));
@@ -153,8 +141,8 @@ private:
}
const Domain operator[](const Variable<Domain>& var) {
// solve the strategy for this variable, too
+ // recursive magic!
_strat.solve(*_strat._system[var]);
- _strat._var_influence[var].insert(_expr);
_strat._influence[*_strat._system[var]].insert(_expr);
return _rho[var];
}
@@ -190,8 +178,6 @@ private:
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 _changed;
};
@@ -205,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
generated by cgit v1.2.3 (git 2.50.1) at 2025-10-31 01:06:19 +0000