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