Next: , Previous: Sentinel, Up: Computing on data


2.1.1.4 List equality

C code Spl encoding
#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) and
 * acyclic(y) and l[y]==_l and data(y) and
 * disjoint(x,y) */
int equal(intlist x, intlist y) {
  intlist xi = x;
  intlist yi = y;
  while (xi != NULL && yi != NULL &&
         xi->data == yi->data) {
    xi = xi->next;
    yi = yi->next;
  }
  if (xi==NULL && yi==NULL)
    return 1;
  else
    return 0;
}
var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, y:real, yi:real, z:real,
    _l:int, _k:int, S:int;
begin
  assume (x == 2); 
  xi = _null; yi = _null; z= _null;
  xi = x;
  yi = y;
  while (xi != _null and yi != _null and
         xi * _data == yi * _data) do
    z = xi * _next;
    xi = _null;
    xi = z;
    z = _null;
    z = yi * _next;
    yi = _null;
    yi = z;
    z = _null;
  done;
  if (xi == _null and yi == _null) then
    _k = 1;
  else
    _k = 0;
  endif;
end

Results

Domain Param. Log file Interesting constraint
LSUM-PRD Anon=(0,1) log/intlist-equal-lsum-prd-01/ x(n1) and y(n3) and d(n1)=d(n3) and S(n1)=S(n3) and l=l[n1]=l[n3]
LSUM-REL Anon=(0,1) log/intlist-equal-lsum-rel-01/ same as above
MSET TODO x(n1) and y(n2) and M[n1]=M[n2] and l=l[n1]=l[n2]
UCONS Anon=(0,1), P13 TODO x(n1) and y(n2) and d(n1)=d(n2) and \forall y1 \in n1, y2\in n2 y1=y2 \implies d(y1)=d(y2)