2.1.2.1 Initialization modulo 2

The encoding of this example in Spl has been changed in order to replace the boolean variable by an integer variable. The test used in the if statement is has been changed to avoid non equality constraints.

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
void initMod2(intlist x) {
  intlist xi = x;
  bool k = true;
  while (xi != NULL) {
    if (k) xi->data = 1;
    else   xi->data = 0;
    xi = xi->next;
    k = not(k);
  }
}


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, y:real,
    _l:int, _k: int;
begin
  assume (x == 0); 
  xi = _null; y = _null;
   _k = 0;
  xi = x;
  while xi != _null do
    if (_k<=0) then
      xi = 0 / _data;
      _k = 1;
    else
      xi = 1 / _data;
      _k = 0;
    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-initMod2-lsum-prd-01
x(n1) and 0<= d(n1)<= 1 and S(n1)>=0


LSUM-REL
Anon=(0,1)
log/intlist-initMod2-lsum-rel-11
x(n1) and xi(n2) and d(n1)=0 and 0<=k<=1
and 2*S(n1)+_k>=_l and _l>=S(n1)+1


LSUM-REL
Anon=(1,1)
log/intlist-initMod2-lsum-rel-11
x(n1) and xi(n2) and d(n1)=0 and 0<=k<=1
and 2*S(n1)+1=l[n1]


MSET


none


UCONS
Anon=(1,1),
P12
TODO
x(n1) and xi(n2) and d(n1)=0 and 0<=k<=1
and \forall y1 <_1 y2 \in n1 \implies d(y1)+d(y2)=1
and _l=l[n1]+l[n2]