pragma options "--bnd-unroll-amnt 8";

int DAGNODES = 4;
int N = 4;

int VISITING_LEFT = -2;
int VISITING_RIGHT = -3;
int UNVISITED = -1;


struct node{
    node l;
    node r;
    int flag;       
    int id;
}

bit unvisited(node n){  
    return n!=null && n.flag == UNVISITED;
}

void setx(node n){
    n.flag = UNVISITED;
}

bit lv(node n){ 
    return n!=null && n.flag == VISITING_LEFT;
}

void setlv(node n){
    n.flag = VISITING_LEFT;
}

bit rv(node n){ 
    return n!=null && n.flag == VISITING_RIGHT;
}

void setrv(node n){
    n.flag = VISITING_RIGHT;
}

bit done(node n){  
    return n==null || n.flag ≥0;
}

void setFlag(node n, int i){
    
    n.flag = i;
}

node newNode(){
    node n = new node();
    n.l = null;
    n.r = null;
    n.flag = UNVISITED;    
    return n;
}

struct dag{
    node[DAGNODES] nodes;   
    int size;
}

dag newDag(){
    dag d = new dag();
    for(int i=0; i<DAGNODES; ++i){
        d.nodes[i] = null;  
    }
    d.size = 0;
    return d;
}

node addNode(int fid, int mid, dag d){
        node n = newNode();     
        if(fid ≥ 0 && fid < d.size){ 
            n.l = d.nodes[fid];
        }else{
            n.l = null; 
        }
        if(mid ≥ 0 && mid < d.size){ 
            n.r = d.nodes[mid];
        }else{
            n.r = null; 
        }
        d.nodes[d.size] = n;
        n.id = d.size;
        d.size = d.size + 1;
        return n;
}

void dfs(dag d){    
    int count = 0;
    for(int i=0; i<d.size; ++i){
        node cur = d.nodes[i];
        if(unvisited(cur)){
            assert cur.id == i;
            node prev = null;           
            while(cur != null){             
                node tp = prev;
                node tc = cur;
                assert unvisited(cur);
                bit b1 = done(cur.l);
                bit b2 = done(cur.r);
                bit b3 = lv(prev);
                bit b4 = rv(prev);          
                if(!b1){
                    cur = tc.l;                 
                    if(??){ prev = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ {| tp.l | tp.r |} = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ {| tc.l | tc.r |} = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }                    
                    if(??){ setFlag({| tc | tp | tp.l | tp.r | tc.l | tc.r |},  VISITING_LEFT ); }
                }
                if(b1 && !b2){
                    cur = tc.r;
                    if(??){ prev = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ {| tp.l | tp.r |} = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ {| tc.l | tc.r |} =  {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }                   
                    if(??){ setFlag({| tc | tp | tp.l | tp.r | tc.l | tc.r |}, VISITING_RIGHT ); }                 
                }
                if(b1 && b2 && b3){
                    if(??){ cur  = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){  prev  = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ {| tp.l | tp.r | tc.l | tc.r |} = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ setFlag(({| tc | tp | tp.l | tp.r | tc.l | tc.r |}), count); ++count; }
                }
                if(b1 && b2 && b4){
                    if(??){ cur  = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){  prev  = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ {| tp.l | tp.r | tc.l | tc.r |} = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ setFlag(({| tc | tp | tp.l | tp.r | tc.l | tc.r |}), count); ++count; }                    
                }
                if(b1 && b2){
                    if(??){ cur  = {| tc | tp | tp.l | tp.r | tc.l | tc.r |}; }
                    if(??){ setFlag(({| tc | tp | tp.l | tp.r | tc.l | tc.r |}), count); ++count; }
                }
                if(cur != null){ setx(cur); }
                if(prev != null){ 
                    assert rv(prev) || lv(prev); 
                }
            }           
        }
    }
        
}


void swap(dag d, int i, int j){
    
    i = i % d.size;
    j = j%d.size;
    
    node ni = d.nodes[i];
    node nj = d.nodes[j];
    
    ni.id = j;
    nj.id = i;
    d.nodes[i] = nj;
    d.nodes[j] = ni;        
}

harness void main(int[N] rs, int[N] ls, int i, int j){  

    dag d = newDag();
    
    for(int i=0; i<N; ++i){
        addNode(rs[i], ls[i], d);   
    }
    
    swap(d, 0,2);
    swap(d, 1,3);
    swap(d, i, j);
    
    dfs(d);
    
    for(int i=0; i<N; ++i){
        node t = d.nodes[i];
        if(t.l != null){
            ls[i] = t.l.id;
        }else{
            ls[i] = -1; 
        }
        if(t.r != null){
            rs[i] =  t.r.id;
        }else{
            rs[i] = -1;
        }
    }
    
    
    for(int i=0; i<N; ++i){
        node t = d.nodes[i];
        if(t.l != null){
            assert t.l.flag < t.flag;   
            assert ls[i] == t.l.id;
        }else{
            assert ls[i] == -1; 
        }   
        if(t.r != null){
            assert t.r.flag < t.flag;   
            assert rs[i] == t.r.id;
        }else{
            assert rs[i] == -1;
        }
    }   
}