//@Description Sketch to reverse a list. pragma options "--bnd-unroll-amnt 6"; int N = 6; struct node{ node next; bit val; } struct list{ node head; node tail; } generator list cat(list l1, list l2){ /* automatically rewritten */ if(l1.head == null){ return l2; }else{ if(l2.head == null){ return l1; }else{ l1.tail.next = l2.head; l1.tail = l2.tail; return l1; } } } generator node popHead(list l){ /* automatically rewritten */ assert l.head != null; node n = l.head; l.head = l.head.next; if(l.head == null){ assert l.tail == n; l.tail = null; } return n; } list reverse(list l){ /* automatically rewritten */ if(l.head == null){ return l; }else{ node n = popHead(l); list l2 = new list(); l2.head = n; l2.tail = n; n.next = null; return cat( reverse(l) , l2 ); } } generator node hole(list l1, list l2){ /* automatically rewritten */ return {| null | ( (l1 | l2)(.head | .tail) )(.next)? |} ; } generator node holeB(list l1, list l2, node n){ /* automatically rewritten */ return (?? ? hole(l1, l2) : n); } generator bit cond(list l1, list l2){ /* automatically rewritten */ node n1 = hole(l1, l2); node n2 = hole(l1, l2); return {| n1 (== | !=) n2 | ?? |}; } list reverseSK(list l){ /* automatically rewritten */ list nl = new list(); nl.head = null; nl.tail = null; bit c = cond(l, nl); node tmp = null; while(c){ if(cond(l, nl)){ {| tmp | l.head |l.head.next | nl.head | nl.head.next | nl.tail |} = holeB(l, nl, tmp);}// 83 * 10 * 6 = 4980 if(cond(l, nl)){ {| tmp | l.head |l.head.next | nl.head | nl.head.next | nl.tail |} = holeB(l, nl, tmp);} if(cond(l, nl)){ {| tmp | l.head |l.head.next | nl.head | nl.head.next | nl.tail |} = holeB(l, nl, tmp);} if(cond(l, nl)){ {| tmp | l.head |l.head.next | nl.head | nl.head.next | nl.tail |} = holeB(l, nl, tmp);} if(cond(l, nl)){ {| tmp | l.head |l.head.next | nl.head | nl.head.next | nl.tail |} = holeB(l, nl, tmp);} c = cond(l, nl); } return nl; } list populate(bit[N] elems, int n){ /* automatically rewritten */ list l = new list(); node prev = null; for(int i=0; i<n; ++i){ node t = new node(); t.val = elems[i]; if(prev != null){ prev.next = t; } prev = t; if(i==0){ l.head = t; } } l.tail = prev; return l; } bit[N] serialize(list l, int n){ /* automatically rewritten */ bit[N] out = 0; node t = l.head; node prev = null; for(int i=0; i<n; ++i){ assert t != null; out[i] = t.val; prev = t; t = t.next; } assert prev == l.tail; assert t == null; return out; } bit[N] spec(bit[N] elems, int n){ if(n ≥ N){ n = N-1; } list l = populate(elems, n); l = reverse(l); return serialize(l, n); } bit[N] sketch(bit[N] elems, int n) implements spec{ if(n ≥ N){ n = N-1; } list l = populate(elems, n); l = reverseSK(l); return serialize(l, n); }