2.1.3.1 Copy a list (1)

Copy the data in the list into an equal length list.

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) and
 * acyclic(y) and l[y]==_l and data(y) and
 * disjoint(x,y) */
void listCopy(intlist x, intlist y) {
  intlist xi = x;
  intlist yi = y;
  while (xi != NULL) {
    yi->data = xi->data;
    xi = xi->next;
    yi = yi->next;
  }
}


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

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,2)
log/intlist-copy-eq-prd-02
x(n1) and y(n2) and d(n1)=d(n2)
and d(n1)+S(n1) = d(n2)+S(n2) = S

LSUM-REL
Anon=(0,2)
log/intlist-copy-eq-rel-02
x(n1) and y(n2) and d(n1)=d(n2)
and d(n1)+S(n1) = d(n2)+S(n2) = S

MSET
Anon=(0,2)
TODO
TODO

UCONS
TODO
Anon=(0,2),
P21
x(n1) and y(n2) and d(n1)=d(n2)
and \forall y1\in n1, y2\in n2 y1=y2 \implies d(y1)=d(y2)