/*
Author: Yihao Yan

See challenge 3 of: http://etaps2015.verifythis.org/challenges

-----------------
Problem description:

Dancing links is a technique introduced in 1979 by Hitotumatu and
Noshita and later popularized by Knuth. The technique can be used to
efficiently implement a search for all solutions of the exact cover
problem, which in its turn can be used to solve Tiling, Sudoku,
N-Queens, and other problems.

Suppose x points to a node of a doubly linked list; let L[x] and R[x]
point to the predecessor and successor of that node. Then the operations
L[R[x]] := L[x];
R[L[x]] := R[x];
remove x from the list. The subsequent operations
L[R[x]] := x;
R[L[x]] := x;
will put x back into the list again.

-----------------
Verification task:

Implement the data structure with these operations, and specify and
verify that they behave in the way described above.

-----------------
Result: 
After deleting Node n, all the node remains the same except the left of n 
(if there is any) or the right of n (if there is any). Also, the right of the left of
n points at the right of n; the left of the right of n points at the left of n.

Then after insertion, the list is restored, which means every node in the list is 
the same with the orignial.

Therefore, the delete and insert functions behave correctly

-----------------
command:civl verify dancingLinks.c

*/

#include <stdlib.h>
#include <stdbool.h>
#include <assert.h>
#include <time.h>

#ifdef _CIVL
#include <civlc.cvh>
$input int N=10;
$assume (N >= 3);
#else
int N=10;
#endif

struct Node {
  struct Node *left;
  struct Node *right;
};

void insert(struct Node *x) {
  x->right->left = x;
  x->left->right = x;
}

void delete(struct Node *x) {
  x->right->left = x->left;
  x->left->right = x->right;
}

//initilize a linkedlist
struct Node* init(int n) {
  struct Node *head = (struct Node *)malloc(sizeof(struct Node));
  struct Node *temp = head;

  temp->left = NULL;
  while(n > 1) {
    struct Node *new = (struct Node *)malloc(sizeof(struct Node));

    temp->right = new;
    new->left = temp;
    temp = temp->right;
    n--;
  }
  temp->right = NULL;
  return head;
}

struct Node* getNode(struct Node* list, int index) {
  struct Node *result = list;

  while(index >1) {
    result = result->right;
    index--;
  }
  return result;
}

void initNodeArray(struct Node** array, struct Node* list, int n) {
  struct Node *cur = list;
  int index=0;

  while(n > 0) {
    array[index++] = cur;
    cur = cur->right;
    n--;
  }
}

void verifyDelete(struct Node *list, struct Node **nodeArray, int index, int n) {
  struct Node *temp1 = list;

  for(int i=0; i<index-1; i++) {
    assert(temp1 == nodeArray[i]);
    assert(temp1->left == (nodeArray[i])->left);
    if(i != index-2) {
      assert(temp1->right == (nodeArray[i])->right);
    } else {
      if(index == n) {
        assert(temp1->right == NULL);
      } else {
        assert(temp1->right == nodeArray[index]);
      }
    }
    temp1 = temp1->right;
  }

  for(int j=index; j<=n-1; j++) {
    assert(temp1 == nodeArray[j]);
    assert(temp1->right == (nodeArray[j])->right);
    if(j == index) {
      if(index == 1) {
        assert(temp1->left == NULL);
      } else {
        assert(temp1->left == nodeArray[index-2]);
      }
    } else {
      assert(temp1->left == (nodeArray[j])->left);
    }
    temp1 = temp1->right;
  }
}

void verifyInsert(struct Node *list, struct Node **nodeArray, int index, int n) {
  struct Node *temp1 = list;

  for(int k=0;k < n; k++) {
    assert(temp1 == nodeArray[k]);
    assert(temp1->left == (nodeArray[k])->left);
    assert(temp1->right == (nodeArray[k])->right);
    temp1 = temp1->right;
  }
}

int main() {
  // size of the linked list
#ifdef _CIVL
  int n = $choose_int(N-2)+3;
#else
  srand(time(NULL));
  int n = rand()%(N-2)+3;
#endif

  struct Node *list = init(n);
  // the index of the node which will be deleted
#ifdef _CIVL
  int index = $choose_int(n-2)+2;
#else
  int index = rand()%(N-2)+2;
#endif

  struct Node *x = getNode(list, index);
  struct Node *nodeArray[n];

  initNodeArray(nodeArray, list, n);
  delete(x);
  verifyDelete(list, nodeArray, index, n);
  insert(x);
  verifyInsert(list, nodeArray, index, n);

  int t = n;
  struct Node *temp1 = list;

  while(t >0) {
    struct Node *temp2 = temp1;

    temp1 = temp1->right;
    free(temp2);
    t--;
  }
  return 0;
}