Previous: Partial reset, Up: Initializing data


2.1.2.7 Sum of lists

C code Spl encoding
#include "intlist.h"

/* acyclic(x) and _l==l[x] and data(x) and
 * acyclic(y) and _l==l[y] and data(y) and
 * acyclic(z) and _l==l[z] and data(z) and
 * disjoint(x,y,z) */
void initSum(intlist x, 
             intlist y,
             intlist z) {
  intlist xi = x;
  intlist yi = y;
  intlist zi = z;
  while (xi != NULL && yi != NULL && zi != NULL) {
    zi->data = xi->data + yi->data;
    xi = xi->next;
    yi = yi->next;
    zi = zi->next;
  }
}
var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, y:real, yi:real, z:real, zi:real, zii:real,
    _l:int, _k:int, S: int, T:int;
begin
  assume (x == 4); 
  xi = _null; yi = _null; zi = _null; zii = _null;
  xi = x;
  yi = y;
  zi = z;
  while xi != _null and yi != _null and 
        zi != _null do
    zi = (xi * _data + yi * _data) / _data;
    zii = xi * _next;
    xi = _null;
    xi = zii;
    zii = _null;
    zii = yi * _next;
    yi = _null;
    yi = zii;
    zii = _null;
    zii = zi * _next;
    zi = _null;
    zi = zii;
    zii = _null;
  done;
end


Results

Domain Param. Log file Interesting constraint
LSUM-PRD Anon=(0,1) log/intlist-initSum-lsum-prd-01 x(n1) and y(n2) and z(n3) and d(n3)=d(n1)+d(n2) and S(n3)=S(n1)+S(n2)
LSUM-REL Anon=(0,1) log/intlist-initSum-lsum-rel-01 x(n1) and y(n2) and z(n3) and d(n3)=d(n1)+d(n2) and S(n3)=S(n1)+S(n2)
MSET TODO TODO TODO
UCONS Anon=(0,3) TODO x(n1) and y(n2) and z(n3) and and \forall y1\in n1, y2\in n2, y3\in n3 y1=y2=y3 \implies d(y3)=d(y1)+d(y2)