2.1.1.3 Sentinel

In its original version Halbwach-Peron-08, this program uses a test xi->data!=m. We changed it into xi->data<=m because we are not using a numerical domain fairly representing non equality constraints.

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
intlist sentinel(intlist x, int m) {
  intlist xi = x;
  while (xi != NULL && xi->data <= m) {
    xi = xi->next;
  }
  return xi;
}


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, m:int;
begin
  assume (x == 0); 
  xi = _null; y = _null;
  xi = x;
  while (xi != _null and xi * _data <= m) do
    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-sentinel-lsum-prd
x(n1) and xi(n2) and d(n1)<=m and d(n2)>=m+1
and l=l[n1]+l[n2]


LSUM-PRD
Anon=(0,1), m=2
log/intlist-sentinel-lsum-prd-2
x(n1) and xi(n2) and d(n1)<=2 and d(n2)>=3
and l=l[n1]+l[n2]


LSUM-REL
Anon=(0,1)
log/intlist-sentinel-lsum-rel
x(n1) and xi(n2) and d(n1)<=m and d(n2)>=m+1
and l=l[n1]+l[n2]


LSUM-REL
Anon=(0,1), m=2
log/intlist-sentinel-lsum-rel-2
x(n1) and xi(n2) and d(n1)<=2
and 2l[n1]>=S[n1] and d(n2)>=3
and l=l[n1]+l[n2]


MSET


none


UCONS
Anon=(0,1), P11
TODO
x(n1) and xi(n2) and d(n1)<=m and d(n2)>=m+1
and \forall y \in n1 \implies d(y)<=m