2.1.4.4 Delete on condition

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
void delAllGeV(intlist x, int v) {
  intlist z;
  intlist y = null;
  intlist xi = x;
  while (xi != NULL) {
    if (xi->data >= v) {
      z = xi;
      xi = xi->next;
      free (z);
      if (y==NULL)
	x = xi;
      else
	y->next = xi;
    }
    else {
      y = xi;
      xi = xi->next;
    }
  }
}


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, y:real, z:real,
    _l:int, _k:int, S:int, v: int;
begin
  assume (x == 0); 
  y = _null; xi = _null; z = _null;
  xi = x;
  while xi != _null do
    if (xi* _data >= v) then
      z = xi;
      xi = _null;
      xi = z * _next;
      if (y == _null) then
        x = _null;
        x = xi;
      else
        y = _null / _next;
        y = xi / _next;     
      endif;
      z = _free;
      z = _null;
    else
      y = _null;
      y = xi;
      z = xi * _next;
      xi = _null;
      xi = z;
      z = _null;
    endif;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-delAllGeV-lsum-prd-01
x(n1) and xi(n2) and l[n2]=1 and l>=l[n1]+1 and
S(n2)=0 and d(n1)+1<=v and d(n2)+1<=v

LSUM-PRD
Anon=(0,1), v=5
log/intlist-delAllGe5-lsum-prd-01
x(n1) and xi(n2) and l[n2]=1 and l>=l[n1]+1 and
S(n2)=0 and d(n1)+1<=5 and d(n2)+1<=5 and
S >= d(n1)+d(n2)+S(n1)

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

LSUM-REL
Anon=(0,1), v=5
log/intlist-delAllGe5-lsum-rel-01
x(n1) and xi(n2) and l[n2]=1 and l>=l[n1]+1 and
S(n2)=0 and d(n1)+1<=5 and d(n2)+1<=5 and
4l[n1] >= S(n1)+4

MSET


none

UCONS
Anon=(0,1)
TODO
x(n1) and xi(n2)  and l[n2]=1 and l>=l[n1]+1 and
d(n1)+1<=v  and d(n2)+1<=v and
\forall y1\in n1 \implies d(y1)+1<=v