Okay, the solver is now correct.

It runs in two separate passes:
 - improve strategy (for all)
 - evaluate fixpoint

Unfortunately this loses out on locality at the moment.

I really want a local solver, so I'll have to see what I can do about
that.

1 files changed, 20 insertions, 12 deletions

diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns
index af18a57..a3b521d 100644
--- a/impl/systems/test.eqns
+++ b/impl/systems/test.eqns
@@ -1,12 +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-pre, inf), min(i-2-pre, inf)), 0, negi-2-pre))
-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-pre, inf), min(i-2-pre, inf)), 0, i-2-pre))
-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(0, i-3-pre))
-negi-3[0] = max(-inf, add(0, 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))
+neg-i-2[0] = max(-inf, add(-1, neg-i-2-pre))