Next: , Previous: First not null, Up: Computing on data


2.1.1.2 Get maximum

C code Spl encoding
#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x)  */
int listMax(intlist x) {
  intlist xi = x;
  int max = x->data;
  while (xi != NULL) {
    if (max < xi->data) 
      max = xi->data;
    xi = xi->next;
  }
  return max;
}
var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, y:real,
    _l:int, _k:int, S:int, max:int;
begin
  assume (x == 0); 
  xi = _null; y = _null;
  xi = x;
  max = x * _data;
  while xi != _null do
    if (max+1 <= xi* _data) then
      max = xi * _data;
    endif;
    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-getMax-lsum-prd-01 x(n1) and xi(n2) and d(n1)<=max and l=l[n1]+l[n2]
LSUM-REL Anon=(0,1) log/intlist-getMax-lsum-rel-01 same as above
MSET none
UCONS Anon=(0,1), P11 TODO x(n1) and d(n1)<=max and \forall y \in n1 \implies d(y)<=max