2.1.4.7 Dispatch lists

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and _l==l[x] and data(x) */
void dispatch(intlist x, 
             intlist xgtv,
             intlist xlev,
             int v) {
  intlist xi = x;
  intlist y;
  xgtv=NULL;  xlev=NULL;
  while (xi != NULL) {
    y=xi;
    xi=xi->next;
    if (y->data<=v) {
      y->next = xlev;
      xlev = y;
    }else {
      y->next = xgtv;
      xgtv = y;
    }
  }
}


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xgtv:real, xi:real, xlev:real, y:real, z:real, 
    _l:int, _k:int, S: int, v:int;
begin
  assume (x == 0); 
  xgtv = _null; xi = _null; xlev = _null; y = _null; z = _null;
  xi = x;
  x = _null;
  while xi != _null do
    y = xi;
    z = xi * _next;
    xi = _null;
    xi = z;
    z = _null;
    y = _null/_next;
    if (y * _data <= v) then
      y = xlev / _next;
      z = xlev;
      xlev = _null;
      xlev = y;
    else
      y = xgtv / _next;
      z = xgtv;
      xgtv = _null;
      xgtv = y;
    endif;
    z = _null;
    y = _null;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-dispatch-lsum-prd-01
x(null) and y(n1) and z(n2) and
_l=l[n1]+l[n2] and l[n1]>=1 and l[n2]>=1 and
S=S[n1]+S[n2] and v>=d(n2) and v+1<=d(n1)

LSUM-REL
Anon=(0,1)
log/intlist-dispatch-lsum-rel-01
x(null) and y(n1) and z(n2) and
_l=l[n1]+l[n2] and l[n1]>=1 and l[n2]>=1 and
S=S[n1]+S[n2] and v>=d(n2) and v+1<=d(n1)

LSUM-PRD
Anon=(0,1), v=5
log/intlist-dispatch-lsum-prd-01
x(null) and y(n1) and z(n2) and
_l=l[n1]+l[n2] and l[n1]>=1 and l[n2]>=1 and
S=S[n1]+S[n2] and 5>=d(n2) and 6<=d(n1)

LSUM-REL
Anon=(0,1), v=5
log/intlist-dispatch-lsum-rel-01
x(null) and y(n1) and z(n2) and
_l=l[n1]+l[n2] and l[n1]>=1 and l[n2]>=1 and
S=S[n1]+S[n2] and 5>=d(n2) and 6<=d(n1) and
S[n1]>=6l[n1] and S[n2]<=5l[n2]

MSET
TODO
TODO
x(null) and y(n1) and z(n2) and
_l=l[n1]+l[n2] and l[n1]>=1 and l[n2]>=1 and
M[n1]+M[n2]=M

UCONS
TODO
TODO
x(null) and y(n1) and z(n2) and
_l=l[n1]+l[n2] and l[n1]>=1 and l[n2]>=1 and
\forall y1\in n1 \implies d(y1)>=v+1 and
\forall y1\in n2 \implies d(y1)<=v