//@Description Sketches a remove method from a doubly linked list.

int N=4;

struct node{
	bit val;
	node prev;
	node next;
}


generator node newNode(bit val){ /* automatically rewritten */
	node n = new node();
	n.val = val;
	n.prev = null;
	n.next = null;
	return n;	
}

struct list{
	node head;
	node tail;		
}


generator node rhsNode(list l, node n1){ /* automatically rewritten */
	return {| ( l(.head | .tail) | n1(.next | .prev)? ) | null  |};
}

generator void assign(list l, node n1){ /* automatically rewritten */
	node rhs = rhsNode(l, n1);	
	{|  l(.head | .tail)  | n1(.prev | .next | .prev.next | .next.prev)   |} = rhs;	
}


generator bit cond(list l, node na){ /* automatically rewritten */	
	node n1 = rhsNode(l, na);
	node n2 = rhsNode(l, na);
	return {|  n1 (== | !=) n2 | ??  |}  ;	
}

void addHead(list l, node n){ /* automatically rewritten */
	
	if(cond(l,n)){
		//assign(l, n);
		n.next = l.head;
		l.head.prev = n;
		l.head = n;
	}
	if(cond(l,n)){
		l.head = n;
		l.tail = n;	
	}
	
	/*
	repeat(??){
		if(cond(l, n)){ assign(l, n, l.head, n); }
	}
	*/
	
}

void addNext(list l, node cur, node n){ /* automatically rewritten */
	
	n.next = cur.next;
	cur.next = n;
	if(cond(l, ?? ? n : cur)){ n.next.prev = n; }
	n.prev = cur;
	if(l.tail == cur){ l.tail = n; }
	
	/*
	repeat(4){
		if(cond(l, ?? ? n : cur)){ assign(l, ?? ? n : cur); }
	}
	*/
	
	
}


void remove(list l, node n){ 	
	repeat(4){
		if(cond(l,n)){assign(l, n);} 	
	}
}


generator list newList(){ /* automatically rewritten */
	list l = new list();
	l.head = null;
	l.tail = null;	
	return l;
}


harness void main(bit[N] elems, int addP, bit addV, int rem){ /* automatically rewritten */
	list l = newList();
	node[N] nodes;
	node prevn = null;
	for(int i=0; i<N; ++i){
		node n = newNode(elems[i]);
		addHead(l, n);
		assert n.next == prevn;
		prevn = n;
		nodes[N-1-i] = n;
	}
	
	assert l.head != null;
	assert l.tail != null;
	
	{
		node t = l.head;
		for(int i=0; i<N; ++i){
			assert t == nodes[i];
			t = t.next;		
		}
	}
	
	
	if(addP < N && rem < N && addP != rem){
		node n = newNode(addV);
		addNext(l, nodes[addP], n);
		remove(l, nodes[rem]);
		int j=0;
		node t = l.head;
		node prevt = null;
		for(int i=0; i<N; ++i){
			if(j!= rem){
				assert t == nodes[j];
				prevt = t;
				t = t.next;				
			}
			if(j == addP){
				assert t == n;
				prevt = t;
				t = t.next;	
			}
			++j;
		}
		assert prevt == l.tail;
	}
	
	
	{
		node t = l.tail;
		node prevt = null;
		for(int i=0; i<N; ++i){
			assert t != null;
			prevt = t;
			t = t.prev;	
		}
		assert prevt == l.head;
	}
	
	
}