//@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);
}