2.1.4.8 Copy and reverse

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
intlist copyRevList(intlist x) {
  intlist xi = x;
  intlist y, z = NULL;
  while (xi != NULL) {
    z = new();
    z->data = xi->data;
    z->next = y;
    y = z;
    xi = xi->next;
  }
  return y;
}


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

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,2)
log/intlist-copyRev-lsum-prd-02
x(n1) and y(n2) and l[n1]=l=l[n2]>=1
and S=S[n1]=S[n2]

LSUM-REL
Anon=(0,2)
log/intlist-copyRev-lsum-rel-02
x(n1) and y(n2) and l[n1]=l=l[n2]>=1
and S=S[n1]=S[n2]

MSET
Anon=(0,2)
TODO
x(n1) and y(n2) and l[n1]=l=l[n2]>=1
and M=M[n1]=M[n2]

UCONS
Anon=(0,2)
TODO
x(n1) and y(n2) and l[n1]=l=l[n2]>=1
and \forall y1\in n1, y2\in n2 y1=l-y2 \implies d(y1)=d(y2)