2.1.2.5 Initialization with Fibonacci

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
void initFibo(intlist x) {
  int m1 = 1;
  int m2 = 0;
  intlist xi = x;
  while (xi != NULL) {
    xi->data = m1+m2;
    m1 = m2;
    m2 = xi->data;
    xi = xi->next;
  }
}


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

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-initFibo-lsum-prd-01
x(n1) and d(n1)=1
and S(n1)+2=m1+2m2
and m2>=m1 and 2m1+1>=m2>=1


LSUM-PRD
Anon=(2,1)
log/intlist-initFibo-lsum-prd-21
x(n1) and d(n1)=1
and S(n1)+2=m1+2m2
and m2>=m1 and 2m1+1>=m2>=15
and 5m1-3m2+3>=0


LSUM-REL
Anon=(0,1)
log/intlist-initFibo-lsum-rel-01
x(n1) and d(n1)=1
and S(n1)+2=m1+2m2
and m2>=m1 and 2m1+1>=m2>=1


MSET


none


UCONS
Anon=(0,1) or (2,1),
P11 or P21 or P311
TODO
x(n1) and d(n1)=1
and \forall y\in n1 \implies d(y)>=y
and \forall y1,y2\in n1 y1<_1 y2 \implies d(y2)>=d(y1)+1
and \forall y1,y2,y3\in n1 y1<_1 y2<_1 y3 \implies d(y3)=d(y2)+d(y1)