Parameterise fixpoint and strategy improvement

(command-line arguments specify which to use)

Also:
 - Fix up Complete<T> to work comparing `inf` to 1 (stupid bug)
 - Clean up the systems/ folder a bit
 - Change the printed output to differentiate variables and constants
   (!v/!c, respectively)
 - Perform a slight optimisation to the strategy-iteration process

15 files changed, 1109 insertions, 41 deletions

diff --git a/impl/Complete.hpp b/impl/Complete.hpp
index 22e060a..11f2f83 100644
--- a/impl/Complete.hpp
+++ b/impl/Complete.hpp
@@ -81,7 +81,7 @@ struct Complete {
       return other._infinity && ((_value < 0 && other._value < 0) ||
                                  (_value > 0 && other._value > 0));
     } else {
-      return _value == other._value;
+      return !other._infinity && (_value == other._value);
     }
   }
   bool operator!=(const Complete& other) const {
diff --git a/impl/Expression.hpp b/impl/Expression.hpp
index 72318e4..7fc4542 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -29,7 +29,7 @@ struct Constant : public Expression<Domain> {
   }
 
   void print(std::ostream& cout) const {
-    cout << _value;
+    cout << _value << "!c";
   }
 
   private:
@@ -53,7 +53,7 @@ struct Variable : public Expression<Domain> {
   }
 
   void print(std::ostream& cout) const {
-    cout << name();
+    cout << _name << "!v";
   }
 
   private:
diff --git a/impl/FixpointAlgorithm.hpp b/impl/FixpointAlgorithm.hpp
index 4c84ff2..b39a915 100644
--- a/impl/FixpointAlgorithm.hpp
+++ b/impl/FixpointAlgorithm.hpp
@@ -32,14 +32,13 @@ struct SmartFixpointAlgorithm : public FixpointAlgorithm<Domain> {
   struct DynamicVariableAssignment : public VariableAssignment<Domain> {
     DynamicVariableAssignment(const EquationSystem<Domain>& system)
       : _system(system),
-        _evaluating(NULL),
         _values(system.variableCount(), infinity<Domain>()),
         _stable(system.variableCount()),
-        _haveValue(system.variableCount()),
         _influence(system.variableCount(), IdSet<Variable<Domain> >(system.variableCount())) { }
 
     const Domain& operator[](const Variable<Domain>& var) const {
       solve(var);
+      //std::cout << _values << std::endl;
       return _values[var];
     }
 
@@ -81,10 +80,8 @@ struct SmartFixpointAlgorithm : public FixpointAlgorithm<Domain> {
     };
 
     const EquationSystem<Domain>& _system;
-    mutable const Variable<Domain>* _evaluating;
     mutable IdMap<Variable<Domain>,Domain> _values;
     mutable IdSet<Variable<Domain> > _stable;
-    mutable IdSet<Variable<Domain> > _haveValue;
     mutable IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
   };
 
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index 06f61b7..2be9f4c 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -46,6 +46,16 @@ struct MaxStrategy : public EquationSystem<Domain> {
     : _system(system), _expressions(system.variableCount(), NULL), _strategy(system.maxExpressionCount(), 0) {
   }
 
+  ~MaxStrategy() {
+    for (int i = 0, length = _system.variableCount();
+         i < length;
+         ++i) {
+      Expression<Domain>* expr = _expressions[_system.variable(i)];
+      if (expr)
+        delete expr;
+    }
+  }
+
   const Expression<Domain>* operator[](const Variable<Domain>& v) const {
     if (_expressions[v] == NULL) {
       Expression<Domain>* expression = new MaxStrategyExpression<Domain>(*_system[v], _strategy);
@@ -92,29 +102,62 @@ struct MaxStrategy : public EquationSystem<Domain> {
     return _system.equalAssignments(l, r);
   }
 
-  void improve(const VariableAssignment<Domain>& rho) {
-    for (unsigned int i = 0, length = _system.maxExpressionCount();
-         i < length;
-         ++i) {
-      MaxExpression<Domain>& expr = _system.maxExpression(i);
-      Domain bestValue = MaxStrategyExpression<Domain>(expr, _strategy).eval(rho);
-      unsigned int bestIndex = this->get(expr);
-
-      // this relies on the fact that an expression will only be proessed after the expressions
-      // it depends on (which should always be true, as they form a DAG)
-      const std::vector<Expression<Domain>*> args = expr.arguments();
-      for (unsigned int j = 0, length = args.size();
-           j < length;
-           ++j) {
-        const Domain value = MaxStrategyExpression<Domain>(*args[j], _strategy).eval(rho);
-        if (bestValue < value) {
-          bestValue = value;
-          bestIndex = j;
+
+  struct ImprovementOperator {
+    virtual ~ImprovementOperator() { }
+    virtual bool improve(MaxStrategy<Domain>&, const VariableAssignment<Domain>&) const = 0;
+  };
+  bool improve(const ImprovementOperator& op, const VariableAssignment<Domain>& rho) {
+    return op.improve(*this, rho);
+  }
+
+  struct NaiveImprovementOperator : public ImprovementOperator {
+    bool improve(MaxStrategy<Domain>& strat, const VariableAssignment<Domain>& rho) const {
+      bool changed = false;
+      for (unsigned int i = 0, length = strat._system.maxExpressionCount();
+           i < length;
+           ++i) {
+        MaxExpression<Domain>& expr = strat._system.maxExpression(i);
+        Domain bestValue = MaxStrategyExpression<Domain>(expr, strat._strategy).eval(rho);
+        unsigned int lastIndex= strat.get(expr);
+        unsigned int bestIndex = strat.get(expr);
+
+        // this relies on the fact that an expression will only be proessed after the expressions
+        // it depends on (which should always be true, as they form a DAG)
+        const std::vector<Expression<Domain>*> args = expr.arguments();
+        for (unsigned int j = 0, length = args.size();
+             j < length;
+             ++j) {
+          const Domain value = MaxStrategyExpression<Domain>(*args[j], strat._strategy).eval(rho);
+          if (bestValue < value) {
+            bestValue = value;
+            bestIndex = j;
+          }
+        }
+        if (bestIndex != lastIndex) {
+          changed = true;
+          strat.set(expr, bestIndex);
         }
       }
-      this->set(expr, bestIndex);
+      return changed;
     }
-  }
+  };
+    
+  struct RepeatedImprovementOperator : public ImprovementOperator {
+    RepeatedImprovementOperator(const ImprovementOperator& op)
+      : _subImprovement(op) { }
+    bool improve(MaxStrategy<Domain>& strat, const VariableAssignment<Domain>& rho) const {
+      if (_subImprovement.improve(strat, rho)) {
+        VariableAssignment<Domain>* rho2 = strat.eval(rho);
+        improve(strat, *rho2);
+        delete rho2;
+        return true;
+      }
+      return false;
+    }
+    private:
+    const ImprovementOperator& _subImprovement;
+  };
 
   void print(std::ostream& cout) const {
     cout << _system << std::endl;
diff --git a/impl/main.cpp b/impl/main.cpp
index 40cae42..6546444 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -93,13 +93,33 @@ void treeToSystem(pANTLR3_BASE_TREE node, ConcreteEquationSystem<T>& system) {
 
 typedef Complete<int> ZBar;
 int main (int argc, char* argv[]) {
+  if (argc <= 3) {
+    cout << "Usage: " << argv[0] << " filename naive|smart naive|repeat" << endl;
+    exit(1);
+  }
   FixpointAlgorithm<ZBar>* algorithm = NULL;
-  if (argc > 2 && !strcmp(argv[2], "naive")) {
+  if (!strcmp(argv[2], "naive")) {
     algorithm = new NaiveFixpointAlgorithm<ZBar>();
     cout << "Naive fixpoint" << endl;
-  } else {
+  } else if (!strcmp(argv[2], "smart")) {
     algorithm = new SmartFixpointAlgorithm<ZBar>();
     cout << "Smart fixpoint" << endl;
+  } else {
+    cout << "Unknown fixpoint algorithm." << endl;
+  }
+  MaxStrategy<ZBar>::ImprovementOperator* naiveImprovement = new MaxStrategy<ZBar>::NaiveImprovementOperator();
+  MaxStrategy<ZBar>::ImprovementOperator* improvement = NULL;
+  if (!strcmp(argv[3], "repeat")) {
+    improvement = new MaxStrategy<ZBar>::RepeatedImprovementOperator(*naiveImprovement);
+    cout << "Repeated strategy improvement" << endl;
+  } else if (!strcmp(argv[3], "naive")) {
+    improvement = naiveImprovement;
+    cout << "Naive strategy improvement" << endl;
+  } else {
+    cout << "Unknown strategy improvement algorithm." << endl;
+  }
+  if (!improvement || !algorithm) {
+    exit(1);
   }
 
   pANTLR3_INPUT_STREAM input;
@@ -119,21 +139,19 @@ int main (int argc, char* argv[]) {
   // DO MORE HERE
 
   cout << system << endl;
-  VariableAssignment<ZBar>* prev = NULL;
-  VariableAssignment<ZBar>* result = system.assignment(-infinity<ZBar>());
+  VariableAssignment<ZBar>* result = NULL;
   MaxStrategy<ZBar> strategy(system);
+  bool changed;
   do {
-    if (prev) delete prev;
-    prev = result;
+    if (result) delete result;
+    result = algorithm->maxFixpoint(strategy);
     /*for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
       cout << var.name() << " = " << (*result)[var] << ", ";
     }
     cout << endl;*/
-    strategy.improve(*prev);
-    result = algorithm->maxFixpoint(strategy);
-  } while(!system.equalAssignments(*prev, *result));
-  if (prev) delete prev;
+    changed = strategy.improve(*improvement, *result);
+  } while(changed);
 
   VariableAssignment<ZBar>* rho = result;
 
@@ -143,6 +161,12 @@ int main (int argc, char* argv[]) {
     cout << var.name() << " = " << (*rho)[var] << endl;
   }
 
+  delete result;
+  delete algorithm;
+  if (naiveImprovement != improvement)
+    delete improvement;
+  delete naiveImprovement;
+
   parser -> free(parser);
   tokens -> free(tokens);
   lex -> free(lex);
diff --git a/impl/systems/constant-system.eqns b/impl/systems/constant-system.eqns
new file mode 100644
index 0000000..7d4290a
--- /dev/null
+++ b/impl/systems/constant-system.eqns
@@ -0,0 +1 @@
+x = 1
diff --git a/impl/systems/size-ten b/impl/systems/example.eqns
index 71ee74a..71ee74a 100644
--- a/impl/systems/size-ten
+++ b/impl/systems/example.eqns
diff --git a/impl/systems/generate-fib.py b/impl/systems/generate-fib.py
new file mode 100644
index 0000000..0263fff
--- /dev/null
+++ b/impl/systems/generate-fib.py
@@ -0,0 +1,6 @@
+
+print 'x0 = 0'
+print 'x1 = 1'
+for i in xrange(10000):
+  #print 'x' + str(i+2) + " = x" + str(i) + " + x" + str(i+1)
+  print 'x%d = x%d + x%d' % (i+2, i, i+1)
diff --git a/impl/antlr/generate.py b/impl/systems/generate-long.py
index 4513fe2..4513fe2 100644
--- a/impl/antlr/generate.py
+++ b/impl/systems/generate-long.py
diff --git a/impl/systems/generate-system.py b/impl/systems/generate-random.py
index cc67df2..cc67df2 100644
--- a/impl/systems/generate-system.py
+++ b/impl/systems/generate-random.py
diff --git a/impl/systems/long-fib.eqns b/impl/systems/long-fib.eqns
new file mode 100644
index 0000000..08a29d6
--- /dev/null
+++ b/impl/systems/long-fib.eqns
@@ -0,0 +1,1001 @@
+x0 = 0
+x1 = 1
+x2 = x0 + x1
+x3 = x1 + x2
+x4 = x2 + x3
+x5 = x3 + x4
+x6 = x4 + x5
+x7 = x5 + x6
+x8 = x6 + x7
+x9 = x7 + x8
+x10 = x8 + x9
+x11 = x9 + x10
+x12 = x10 + x11
+x13 = x11 + x12
+x14 = x12 + x13
+x15 = x13 + x14
+x16 = x14 + x15
+x17 = x15 + x16
+x18 = x16 + x17
+x19 = x17 + x18
+x20 = x18 + x19
+x21 = x19 + x20
+x22 = x20 + x21
+x23 = x21 + x22
+x24 = x22 + x23
+x25 = x23 + x24
+x26 = x24 + x25
+x27 = x25 + x26
+x28 = x26 + x27
+x29 = x27 + x28
+x30 = x28 + x29
+x31 = x29 + x30
+x32 = x30 + x31
+x33 = x31 + x32
+x34 = x32 + x33
+x35 = x33 + x34
+x36 = x34 + x35
+x37 = x35 + x36
+x38 = x36 + x37
+x39 = x37 + x38
+x40 = x38 + x39
+x41 = x39 + x40
+x42 = x40 + x41
+x43 = x41 + x42
+x44 = x42 + x43
+x45 = x43 + x44
+x46 = x44 + x45
+x47 = x45 + x46
+x48 = x46 + x47
+x49 = x47 + x48
+x50 = x48 + x49
+x51 = x49 + x50
+x52 = x50 + x51
+x53 = x51 + x52
+x54 = x52 + x53
+x55 = x53 + x54
+x56 = x54 + x55
+x57 = x55 + x56
+x58 = x56 + x57
+x59 = x57 + x58
+x60 = x58 + x59
+x61 = x59 + x60
+x62 = x60 + x61
+x63 = x61 + x62
+x64 = x62 + x63
+x65 = x63 + x64
+x66 = x64 + x65
+x67 = x65 + x66
+x68 = x66 + x67
+x69 = x67 + x68
+x70 = x68 + x69
+x71 = x69 + x70
+x72 = x70 + x71
+x73 = x71 + x72
+x74 = x72 + x73
+x75 = x73 + x74
+x76 = x74 + x75
+x77 = x75 + x76
+x78 = x76 + x77
+x79 = x77 + x78
+x80 = x78 + x79
+x81 = x79 + x80
+x82 = x80 + x81
+x83 = x81 + x82
+x84 = x82 + x83
+x85 = x83 + x84
+x86 = x84 + x85
+x87 = x85 + x86
+x88 = x86 + x87
+x89 = x87 + x88
+x90 = x88 + x89
+x91 = x89 + x90
+x92 = x90 + x91
+x93 = x91 + x92
+x94 = x92 + x93
+x95 = x93 + x94
+x96 = x94 + x95
+x97 = x95 + x96
+x98 = x96 + x97
+x99 = x97 + x98
+x100 = x98 + x99
+x101 = x99 + x100
+x102 = x100 + x101
+x103 = x101 + x102
+x104 = x102 + x103
+x105 = x103 + x104
+x106 = x104 + x105
+x107 = x105 + x106
+x108 = x106 + x107
+x109 = x107 + x108
+x110 = x108 + x109
+x111 = x109 + x110
+x112 = x110 + x111
+x113 = x111 + x112
+x114 = x112 + x113
+x115 = x113 + x114
+x116 = x114 + x115
+x117 = x115 + x116
+x118 = x116 + x117
+x119 = x117 + x118
+x120 = x118 + x119
+x121 = x119 + x120
+x122 = x120 + x121
+x123 = x121 + x122
+x124 = x122 + x123
+x125 = x123 + x124
+x126 = x124 + x125
+x127 = x125 + x126
+x128 = x126 + x127
+x129 = x127 + x128
+x130 = x128 + x129
+x131 = x129 + x130
+x132 = x130 + x131
+x133 = x131 + x132
+x134 = x132 + x133
+x135 = x133 + x134
+x136 = x134 + x135
+x137 = x135 + x136
+x138 = x136 + x137
+x139 = x137 + x138
+x140 = x138 + x139
+x141 = x139 + x140
+x142 = x140 + x141
+x143 = x141 + x142
+x144 = x142 + x143
+x145 = x143 + x144
+x146 = x144 + x145
+x147 = x145 + x146
+x148 = x146 + x147
+x149 = x147 + x148
+x150 = x148 + x149
+x151 = x149 + x150
+x152 = x150 + x151
+x153 = x151 + x152
+x154 = x152 + x153
+x155 = x153 + x154
+x156 = x154 + x155
+x157 = x155 + x156
+x158 = x156 + x157
+x159 = x157 + x158
+x160 = x158 + x159
+x161 = x159 + x160
+x162 = x160 + x161
+x163 = x161 + x162
+x164 = x162 + x163
+x165 = x163 + x164
+x166 = x164 + x165
+x167 = x165 + x166
+x168 = x166 + x167
+x169 = x167 + x168
+x170 = x168 + x169
+x171 = x169 + x170
+x172 = x170 + x171
+x173 = x171 + x172
+x174 = x172 + x173
+x175 = x173 + x174
+x176 = x174 + x175
+x177 = x175 + x176
+x178 = x176 + x177
+x179 = x177 + x178
+x180 = x178 + x179
+x181 = x179 + x180
+x182 = x180 + x181
+x183 = x181 + x182
+x184 = x182 + x183
+x185 = x183 + x184
+x186 = x184 + x185
+x187 = x185 + x186
+x188 = x186 + x187
+x189 = x187 + x188
+x190 = x188 + x189
+x191 = x189 + x190
+x192 = x190 + x191
+x193 = x191 + x192
+x194 = x192 + x193
+x195 = x193 + x194
+x196 = x194 + x195
+x197 = x195 + x196
+x198 = x196 + x197
+x199 = x197 + x198
+x200 = x198 + x199
+x201 = x199 + x200
+x202 = x200 + x201
+x203 = x201 + x202
+x204 = x202 + x203
+x205 = x203 + x204
+x206 = x204 + x205
+x207 = x205 + x206
+x208 = x206 + x207
+x209 = x207 + x208
+x210 = x208 + x209
+x211 = x209 + x210
+x212 = x210 + x211
+x213 = x211 + x212
+x214 = x212 + x213
+x215 = x213 + x214
+x216 = x214 + x215
+x217 = x215 + x216
+x218 = x216 + x217
+x219 = x217 + x218
+x220 = x218 + x219
+x221 = x219 + x220
+x222 = x220 + x221
+x223 = x221 + x222
+x224 = x222 + x223
+x225 = x223 + x224
+x226 = x224 + x225
+x227 = x225 + x226
+x228 = x226 + x227
+x229 = x227 + x228
+x230 = x228 + x229
+x231 = x229 + x230
+x232 = x230 + x231
+x233 = x231 + x232
+x234 = x232 + x233
+x235 = x233 + x234
+x236 = x234 + x235
+x237 = x235 + x236
+x238 = x236 + x237
+x239 = x237 + x238
+x240 = x238 + x239
+x241 = x239 + x240
+x242 = x240 + x241
+x243 = x241 + x242
+x244 = x242 + x243
+x245 = x243 + x244
+x246 = x244 + x245
+x247 = x245 + x246
+x248 = x246 + x247
+x249 = x247 + x248
+x250 = x248 + x249
+x251 = x249 + x250
+x252 = x250 + x251
+x253 = x251 + x252
+x254 = x252 + x253
+x255 = x253 + x254
+x256 = x254 + x255
+x257 = x255 + x256
+x258 = x256 + x257
+x259 = x257 + x258
+x260 = x258 + x259
+x261 = x259 + x260
+x262 = x260 + x261
+x263 = x261 + x262
+x264 = x262 + x263
+x265 = x263 + x264
+x266 = x264 + x265
+x267 = x265 + x266
+x268 = x266 + x267
+x269 = x267 + x268
+x270 = x268 + x269
+x271 = x269 + x270
+x272 = x270 + x271
+x273 = x271 + x272
+x274 = x272 + x273
+x275 = x273 + x274
+x276 = x274 + x275
+x277 = x275 + x276
+x278 = x276 + x277
+x279 = x277 + x278
+x280 = x278 + x279
+x281 = x279 + x280
+x282 = x280 + x281
+x283 = x281 + x282
+x284 = x282 + x283
+x285 = x283 + x284
+x286 = x284 + x285
+x287 = x285 + x286
+x288 = x286 + x287
+x289 = x287 + x288
+x290 = x288 + x289
+x291 = x289 + x290
+x292 = x290 + x291
+x293 = x291 + x292
+x294 = x292 + x293
+x295 = x293 + x294
+x296 = x294 + x295
+x297 = x295 + x296
+x298 = x296 + x297
+x299 = x297 + x298
+x300 = x298 + x299
+x301 = x299 + x300
+x302 = x300 + x301
+x303 = x301 + x302
+x304 = x302 + x303
+x305 = x303 + x304
+x306 = x304 + x305
+x307 = x305 + x306
+x308 = x306 + x307
+x309 = x307 + x308
+x310 = x308 + x309
+x311 = x309 + x310
+x312 = x310 + x311
+x313 = x311 + x312
+x314 = x312 + x313
+x315 = x313 + x314
+x316 = x314 + x315
+x317 = x315 + x316
+x318 = x316 + x317
+x319 = x317 + x318
+x320 = x318 + x319
+x321 = x319 + x320
+x322 = x320 + x321
+x323 = x321 + x322
+x324 = x322 + x323
+x325 = x323 + x324
+x326 = x324 + x325
+x327 = x325 + x326
+x328 = x326 + x327
+x329 = x327 + x328
+x330 = x328 + x329
+x331 = x329 + x330
+x332 = x330 + x331
+x333 = x331 + x332
+x334 = x332 + x333
+x335 = x333 + x334
+x336 = x334 + x335
+x337 = x335 + x336
+x338 = x336 + x337
+x339 = x337 + x338
+x340 = x338 + x339
+x341 = x339 + x340
+x342 = x340 + x341
+x343 = x341 + x342
+x344 = x342 + x343
+x345 = x343 + x344
+x346 = x344 + x345
+x347 = x345 + x346
+x348 = x346 + x347
+x349 = x347 + x348
+x350 = x348 + x349
+x351 = x349 + x350
+x352 = x350 + x351
+x353 = x351 + x352
+x354 = x352 + x353
+x355 = x353 + x354
+x356 = x354 + x355
+x357 = x355 + x356
+x358 = x356 + x357
+x359 = x357 + x358
+x360 = x358 + x359
+x361 = x359 + x360
+x362 = x360 + x361
+x363 = x361 + x362
+x364 = x362 + x363
+x365 = x363 + x364
+x366 = x364 + x365
+x367 = x365 + x366
+x368 = x366 + x367
+x369 = x367 + x368
+x370 = x368 + x369
+x371 = x369 + x370
+x372 = x370 + x371
+x373 = x371 + x372
+x374 = x372 + x373
+x375 = x373 + x374
+x376 = x374 + x375
+x377 = x375 + x376
+x378 = x376 + x377
+x379 = x377 + x378
+x380 = x378 + x379
+x381 = x379 + x380
+x382 = x380 + x381
+x383 = x381 + x382
+x384 = x382 + x383
+x385 = x383 + x384
+x386 = x384 + x385
+x387 = x385 + x386
+x388 = x386 + x387
+x389 = x387 + x388
+x390 = x388 + x389
+x391 = x389 + x390
+x392 = x390 + x391
+x393 = x391 + x392
+x394 = x392 + x393
+x395 = x393 + x394
+x396 = x394 + x395
+x397 = x395 + x396
+x398 = x396 + x397
+x399 = x397 + x398
+x400 = x398 + x399
+x401 = x399 + x400
+x402 = x400 + x401
+x403 = x401 + x402
+x404 = x402 + x403
+x405 = x403 + x404
+x406 = x404 + x405
+x407 = x405 + x406
+x408 = x406 + x407
+x409 = x407 + x408
+x410 = x408 + x409
+x411 = x409 + x410
+x412 = x410 + x411
+x413 = x411 + x412
+x414 = x412 + x413
+x415 = x413 + x414
+x416 = x414 + x415
+x417 = x415 + x416
+x418 = x416 + x417
+x419 = x417 + x418
+x420 = x418 + x419
+x421 = x419 + x420
+x422 = x420 + x421
+x423 = x421 + x422
+x424 = x422 + x423
+x425 = x423 + x424
+x426 = x424 + x425
+x427 = x425 + x426
+x428 = x426 + x427
+x429 = x427 + x428
+x430 = x428 + x429
+x431 = x429 + x430
+x432 = x430 + x431
+x433 = x431 + x432
+x434 = x432 + x433
+x435 = x433 + x434
+x436 = x434 + x435
+x437 = x435 + x436
+x438 = x436 + x437
+x439 = x437 + x438
+x440 = x438 + x439
+x441 = x439 + x440
+x442 = x440 + x441
+x443 = x441 + x442
+x444 = x442 + x443
+x445 = x443 + x444
+x446 = x444 + x445
+x447 = x445 + x446
+x448 = x446 + x447
+x449 = x447 + x448
+x450 = x448 + x449
+x451 = x449 + x450
+x452 = x450 + x451
+x453 = x451 + x452
+x454 = x452 + x453
+x455 = x453 + x454
+x456 = x454 + x455
+x457 = x455 + x456
+x458 = x456 + x457
+x459 = x457 + x458
+x460 = x458 + x459
+x461 = x459 + x460
+x462 = x460 + x461
+x463 = x461 + x462
+x464 = x462 + x463
+x465 = x463 + x464
+x466 = x464 + x465
+x467 = x465 + x466
+x468 = x466 + x467
+x469 = x467 + x468
+x470 = x468 + x469
+x471 = x469 + x470
+x472 = x470 + x471
+x473 = x471 + x472
+x474 = x472 + x473
+x475 = x473 + x474
+x476 = x474 + x475
+x477 = x475 + x476
+x478 = x476 + x477
+x479 = x477 + x478
+x480 = x478 + x479
+x481 = x479 + x480
+x482 = x480 + x481
+x483 = x481 + x482
+x484 = x482 + x483
+x485 = x483 + x484
+x486 = x484 + x485
+x487 = x485 + x486
+x488 = x486 + x487
+x489 = x487 + x488
+x490 = x488 + x489
+x491 = x489 + x490
+x492 = x490 + x491
+x493 = x491 + x492
+x494 = x492 + x493
+x495 = x493 + x494
+x496 = x494 + x495
+x497 = x495 + x496
+x498 = x496 + x497
+x499 = x497 + x498
+x500 = x498 + x499
+x501 = x499 + x500
+x502 = x500 + x501
+x503 = x501 + x502
+x504 = x502 + x503
+x505 = x503 + x504
+x506 = x504 + x505
+x507 = x505 + x506
+x508 = x506 + x507
+x509 = x507 + x508
+x510 = x508 + x509
+x511 = x509 + x510
+x512 = x510 + x511
+x513 = x511 + x512
+x514 = x512 + x513
+x515 = x513 + x514
+x516 = x514 + x515
+x517 = x515 + x516
+x518 = x516 + x517
+x519 = x517 + x518
+x520 = x518 + x519
+x521 = x519 + x520
+x522 = x520 + x521
+x523 = x521 + x522
+x524 = x522 + x523
+x525 = x523 + x524
+x526 = x524 + x525
+x527 = x525 + x526
+x528 = x526 + x527
+x529 = x527 + x528
+x530 = x528 + x529
+x531 = x529 + x530
+x532 = x530 + x531
+x533 = x531 + x532
+x534 = x532 + x533
+x535 = x533 + x534
+x536 = x534 + x535
+x537 = x535 + x536
+x538 = x536 + x537
+x539 = x537 + x538
+x540 = x538 + x539
+x541 = x539 + x540
+x542 = x540 + x541
+x543 = x541 + x542
+x544 = x542 + x543
+x545 = x543 + x544
+x546 = x544 + x545
+x547 = x545 + x546
+x548 = x546 + x547
+x549 = x547 + x548
+x550 = x548 + x549
+x551 = x549 + x550
+x552 = x550 + x551
+x553 = x551 + x552
+x554 = x552 + x553
+x555 = x553 + x554
+x556 = x554 + x555
+x557 = x555 + x556
+x558 = x556 + x557
+x559 = x557 + x558
+x560 = x558 + x559
+x561 = x559 + x560
+x562 = x560 + x561
+x563 = x561 + x562
+x564 = x562 + x563
+x565 = x563 + x564
+x566 = x564 + x565
+x567 = x565 + x566
+x568 = x566 + x567
+x569 = x567 + x568
+x570 = x568 + x569
+x571 = x569 + x570
+x572 = x570 + x571
+x573 = x571 + x572
+x574 = x572 + x573
+x575 = x573 + x574
+x576 = x574 + x575
+x577 = x575 + x576
+x578 = x576 + x577
+x579 = x577 + x578
+x580 = x578 + x579
+x581 = x579 + x580
+x582 = x580 + x581
+x583 = x581 + x582
+x584 = x582 + x583
+x585 = x583 + x584
+x586 = x584 + x585
+x587 = x585 + x586
+x588 = x586 + x587
+x589 = x587 + x588
+x590 = x588 + x589
+x591 = x589 + x590
+x592 = x590 + x591
+x593 = x591 + x592
+x594 = x592 + x593
+x595 = x593 + x594
+x596 = x594 + x595
+x597 = x595 + x596
+x598 = x596 + x597
+x599 = x597 + x598
+x600 = x598 + x599
+x601 = x599 + x600
+x602 = x600 + x601
+x603 = x601 + x602
+x604 = x602 + x603
+x605 = x603 + x604
+x606 = x604 + x605
+x607 = x605 + x606
+x608 = x606 + x607
+x609 = x607 + x608
+x610 = x608 + x609
+x611 = x609 + x610
+x612 = x610 + x611
+x613 = x611 + x612
+x614 = x612 + x613
+x615 = x613 + x614
+x616 = x614 + x615
+x617 = x615 + x616
+x618 = x616 + x617
+x619 = x617 + x618
+x620 = x618 + x619
+x621 = x619 + x620
+x622 = x620 + x621
+x623 = x621 + x622
+x624 = x622 + x623
+x625 = x623 + x624
+x626 = x624 + x625
+x627 = x625 + x626
+x628 = x626 + x627
+x629 = x627 + x628
+x630 = x628 + x629
+x631 = x629 + x630
+x632 = x630 + x631
+x633 = x631 + x632
+x634 = x632 + x633
+x635 = x633 + x634
+x636 = x634 + x635
+x637 = x635 + x636
+x638 = x636 + x637
+x639 = x637 + x638
+x640 = x638 + x639
+x641 = x639 + x640
+x642 = x640 + x641
+x643 = x641 + x642
+x644 = x642 + x643
+x645 = x643 + x644
+x646 = x644 + x645
+x647 = x645 + x646
+x648 = x646 + x647
+x649 = x647 + x648
+x650 = x648 + x649
+x651 = x649 + x650
+x652 = x650 + x651
+x653 = x651 + x652
+x654 = x652 + x653
+x655 = x653 + x654
+x656 = x654 + x655
+x657 = x655 + x656
+x658 = x656 + x657
+x659 = x657 + x658
+x660 = x658 + x659
+x661 = x659 + x660
+x662 = x660 + x661
+x663 = x661 + x662
+x664 = x662 + x663
+x665 = x663 + x664
+x666 = x664 + x665
+x667 = x665 + x666
+x668 = x666 + x667
+x669 = x667 + x668
+x670 = x668 + x669
+x671 = x669 + x670
+x672 = x670 + x671
+x673 = x671 + x672
+x674 = x672 + x673
+x675 = x673 + x674
+x676 = x674 + x675
+x677 = x675 + x676
+x678 = x676 + x677
+x679 = x677 + x678
+x680 = x678 + x679
+x681 = x679 + x680
+x682 = x680 + x681
+x683 = x681 + x682
+x684 = x682 + x683
+x685 = x683 + x684
+x686 = x684 + x685
+x687 = x685 + x686
+x688 = x686 + x687
+x689 = x687 + x688
+x690 = x688 + x689
+x691 = x689 + x690
+x692 = x690 + x691
+x693 = x691 + x692
+x694 = x692 + x693
+x695 = x693 + x694
+x696 = x694 + x695
+x697 = x695 + x696
+x698 = x696 + x697
+x699 = x697 + x698
+x700 = x698 + x699
+x701 = x699 + x700
+x702 = x700 + x701
+x703 = x701 + x702
+x704 = x702 + x703
+x705 = x703 + x704
+x706 = x704 + x705
+x707 = x705 + x706
+x708 = x706 + x707
+x709 = x707 + x708
+x710 = x708 + x709
+x711 = x709 + x710
+x712 = x710 + x711
+x713 = x711 + x712
+x714 = x712 + x713
+x715 = x713 + x714
+x716 = x714 + x715
+x717 = x715 + x716
+x718 = x716 + x717
+x719 = x717 + x718
+x720 = x718 + x719
+x721 = x719 + x720
+x722 = x720 + x721
+x723 = x721 + x722
+x724 = x722 + x723
+x725 = x723 + x724
+x726 = x724 + x725
+x727 = x725 + x726
+x728 = x726 + x727
+x729 = x727 + x728
+x730 = x728 + x729
+x731 = x729 + x730
+x732 = x730 + x731
+x733 = x731 + x732
+x734 = x732 + x733
+x735 = x733 + x734
+x736 = x734 + x735
+x737 = x735 + x736
+x738 = x736 + x737
+x739 = x737 + x738
+x740 = x738 + x739
+x741 = x739 + x740
+x742 = x740 + x741
+x743 = x741 + x742
+x744 = x742 + x743
+x745 = x743 + x744
+x746 = x744 + x745
+x747 = x745 + x746
+x748 = x746 + x747
+x749 = x747 + x748
+x750 = x748 + x749
+x751 = x749 + x750
+x752 = x750 + x751
+x753 = x751 + x752
+x754 = x752 + x753
+x755 = x753 + x754
+x756 = x754 + x755
+x757 = x755 + x756
+x758 = x756 + x757
+x759 = x757 + x758
+x760 = x758 + x759
+x761 = x759 + x760
+x762 = x760 + x761
+x763 = x761 + x762
+x764 = x762 + x763
+x765 = x763 + x764
+x766 = x764 + x765
+x767 = x765 + x766
+x768 = x766 + x767
+x769 = x767 + x768
+x770 = x768 + x769
+x771 = x769 + x770
+x772 = x770 + x771
+x773 = x771 + x772
+x774 = x772 + x773
+x775 = x773 + x774
+x776 = x774 + x775
+x777 = x775 + x776
+x778 = x776 + x777
+x779 = x777 + x778
+x780 = x778 + x779
+x781 = x779 + x780
+x782 = x780 + x781
+x783 = x781 + x782
+x784 = x782 + x783
+x785 = x783 + x784
+x786 = x784 + x785
+x787 = x785 + x786
+x788 = x786 + x787
+x789 = x787 + x788
+x790 = x788 + x789
+x791 = x789 + x790
+x792 = x790 + x791
+x793 = x791 + x792
+x794 = x792 + x793
+x795 = x793 + x794
+x796 = x794 + x795
+x797 = x795 + x796
+x798 = x796 + x797
+x799 = x797 + x798
+x800 = x798 + x799
+x801 = x799 + x800
+x802 = x800 + x801
+x803 = x801 + x802
+x804 = x802 + x803
+x805 = x803 + x804
+x806 = x804 + x805
+x807 = x805 + x806
+x808 = x806 + x807
+x809 = x807 + x808
+x810 = x808 + x809
+x811 = x809 + x810
+x812 = x810 + x811
+x813 = x811 + x812
+x814 = x812 + x813
+x815 = x813 + x814
+x816 = x814 + x815
+x817 = x815 + x816
+x818 = x816 + x817
+x819 = x817 + x818
+x820 = x818 + x819
+x821 = x819 + x820
+x822 = x820 + x821
+x823 = x821 + x822
+x824 = x822 + x823
+x825 = x823 + x824
+x826 = x824 + x825
+x827 = x825 + x826
+x828 = x826 + x827
+x829 = x827 + x828
+x830 = x828 + x829
+x831 = x829 + x830
+x832 = x830 + x831
+x833 = x831 + x832
+x834 = x832 + x833
+x835 = x833 + x834
+x836 = x834 + x835
+x837 = x835 + x836
+x838 = x836 + x837
+x839 = x837 + x838
+x840 = x838 + x839
+x841 = x839 + x840
+x842 = x840 + x841
+x843 = x841 + x842
+x844 = x842 + x843
+x845 = x843 + x844
+x846 = x844 + x845
+x847 = x845 + x846
+x848 = x846 + x847
+x849 = x847 + x848
+x850 = x848 + x849
+x851 = x849 + x850
+x852 = x850 + x851
+x853 = x851 + x852
+x854 = x852 + x853
+x855 = x853 + x854
+x856 = x854 + x855
+x857 = x855 + x856
+x858 = x856 + x857
+x859 = x857 + x858
+x860 = x858 + x859
+x861 = x859 + x860
+x862 = x860 + x861
+x863 = x861 + x862
+x864 = x862 + x863
+x865 = x863 + x864
+x866 = x864 + x865
+x867 = x865 + x866
+x868 = x866 + x867
+x869 = x867 + x868
+x870 = x868 + x869
+x871 = x869 + x870
+x872 = x870 + x871
+x873 = x871 + x872
+x874 = x872 + x873
+x875 = x873 + x874
+x876 = x874 + x875
+x877 = x875 + x876
+x878 = x876 + x877
+x879 = x877 + x878
+x880 = x878 + x879
+x881 = x879 + x880
+x882 = x880 + x881
+x883 = x881 + x882
+x884 = x882 + x883
+x885 = x883 + x884
+x886 = x884 + x885
+x887 = x885 + x886
+x888 = x886 + x887
+x889 = x887 + x888
+x890 = x888 + x889
+x891 = x889 + x890
+x892 = x890 + x891
+x893 = x891 + x892
+x894 = x892 + x893
+x895 = x893 + x894
+x896 = x894 + x895
+x897 = x895 + x896
+x898 = x896 + x897
+x899 = x897 + x898
+x900 = x898 + x899
+x901 = x899 + x900
+x902 = x900 + x901
+x903 = x901 + x902
+x904 = x902 + x903
+x905 = x903 + x904
+x906 = x904 + x905
+x907 = x905 + x906
+x908 = x906 + x907
+x909 = x907 + x908
+x910 = x908 + x909
+x911 = x909 + x910
+x912 = x910 + x911
+x913 = x911 + x912
+x914 = x912 + x913
+x915 = x913 + x914
+x916 = x914 + x915
+x917 = x915 + x916
+x918 = x916 + x917
+x919 = x917 + x918
+x920 = x918 + x919
+x921 = x919 + x920
+x922 = x920 + x921
+x923 = x921 + x922
+x924 = x922 + x923
+x925 = x923 + x924
+x926 = x924 + x925
+x927 = x925 + x926
+x928 = x926 + x927
+x929 = x927 + x928
+x930 = x928 + x929
+x931 = x929 + x930
+x932 = x930 + x931
+x933 = x931 + x932
+x934 = x932 + x933
+x935 = x933 + x934
+x936 = x934 + x935
+x937 = x935 + x936
+x938 = x936 + x937
+x939 = x937 + x938
+x940 = x938 + x939
+x941 = x939 + x940
+x942 = x940 + x941
+x943 = x941 + x942
+x944 = x942 + x943
+x945 = x943 + x944
+x946 = x944 + x945
+x947 = x945 + x946
+x948 = x946 + x947
+x949 = x947 + x948
+x950 = x948 + x949
+x951 = x949 + x950
+x952 = x950 + x951
+x953 = x951 + x952
+x954 = x952 + x953
+x955 = x953 + x954
+x956 = x954 + x955
+x957 = x955 + x956
+x958 = x956 + x957
+x959 = x957 + x958
+x960 = x958 + x959
+x961 = x959 + x960
+x962 = x960 + x961
+x963 = x961 + x962
+x964 = x962 + x963
+x965 = x963 + x964
+x966 = x964 + x965
+x967 = x965 + x966
+x968 = x966 + x967
+x969 = x967 + x968
+x970 = x968 + x969
+x971 = x969 + x970
+x972 = x970 + x971
+x973 = x971 + x972
+x974 = x972 + x973
+x975 = x973 + x974
+x976 = x974 + x975
+x977 = x975 + x976
+x978 = x976 + x977
+x979 = x977 + x978
+x980 = x978 + x979
+x981 = x979 + x980
+x982 = x980 + x981
+x983 = x981 + x982
+x984 = x982 + x983
+x985 = x983 + x984
+x986 = x984 + x985
+x987 = x985 + x986
+x988 = x986 + x987
+x989 = x987 + x988
+x990 = x988 + x989
+x991 = x989 + x990
+x992 = x990 + x991
+x993 = x991 + x992
+x994 = x992 + x993
+x995 = x993 + x994
+x996 = x994 + x995
+x997 = x995 + x996
+x998 = x996 + x997
+x999 = x997 + x998
+x1000 = x998 + x999
diff --git a/impl/systems/long-fixpoint b/impl/systems/long-fixpoint.eqns
index 5838910..5838910 100644
--- a/impl/systems/long-fixpoint
+++ b/impl/systems/long-fixpoint.eqns
diff --git a/impl/systems/min-test b/impl/systems/min-test
deleted file mode 100644
index a05a662..0000000
--- a/impl/systems/min-test
+++ /dev/null
@@ -1,3 +0,0 @@
-x1 = min(1, x1)
-x2 = min(x2+1, x3)
-x3 = 0
diff --git a/impl/systems/small b/impl/systems/minimal.eqns
index 3c40ed9..3c40ed9 100644
--- a/impl/systems/small
+++ b/impl/systems/minimal.eqns
diff --git a/impl/systems/random-system b/impl/systems/random-system
deleted file mode 100644
index 506c18a..0000000
--- a/impl/systems/random-system
+++ /dev/null
@@ -1 +0,0 @@
-x = max()