231 struct vm {
232         typedef list<res*> eq; // "cols"
233         list<eqs> eqs; // "rows"
234         // function apply(x,y): try to put x,y at the same row and keep the state valid,
235         // means: require them to be equal.
236         // rules of state validation:
237         // 1. all rows must contain at most one nonvar
238         // 2. nonvars must be the first element in a row
239         // 3. once element was put in a row, it cannot be moved
240         // 4. every element appears at most once in at most one row
241         //
242         // a row that begins with a nonvar will be called an
243         // unbounded row. note that the res* pointers (for vars
244         // or nonvars) are ever dereferenced, serve only as a unique id.
245         // all comparisons are done by comparing those addresses.
246         //
247         // given we have a valid state and we want to update
248         // another equality condition x=y, we have to execute
249         // the following function, called apply(x,y):
250         // 1. if x already appears in row n:
251         //      1.1 if y never appears
252         //              1.1.1 if y is a nonvar
253         //                      1.1.1 if the row n is unbounded, add y to the head of row n
254         //                      1.1.2 if the row n is bounded, fail.
255         //              1.1.2 if y is a var, append it to row n.
256         //      1.2 if y appears at row k
257         //              1.2.1 if n==k, return success.
258         //              1.2.2 if rows n,k are both bounded, fail.
259         //              1.2.3 append all items of the unbounded row to the bounded one
260         //              and delete the old unbounded row. if both rows are unbounded,
261         //              append into row min(n,k). return success.
262         // 2. if x never appears
263         //      2.1 if y never appears, put x,y in a new row and return success.
264         //      otherwise, let n by y's row.
265         //      2.2 if x is a var or row n is unbounded, append x to row n and return success.
266         //      2.3 fail
267         bool apply(res* x, res* y) {
268
269         }
270 };