/*
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.

command: civl verify dancingLinks.c

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.

*/

#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;
}