#include <stdio.h>
#include <assert.h>

#include "cbmcLLRBContext.h"

void meta(struct Context*, enum Code);

/* cbmc built in functions */
int nondet_int(); 

/* functions for verification */
void printTree(struct Node* node, int n) {
    if (node != 0) {
        printTree(node->left, n+1);
        for (int i=0;i<n;i++)
            printf("  ");
        printf("key=%d value=%d color=%s\t%p\n", node->key, node->value,/* n, */node->color==0? "R":"B", node);
        printTree(node->right, n+1);
    }
}

unsigned int minHeight(struct Node* node, unsigned int height) {
    if ((node->left == NULL) && (node->right == NULL)) return height;
    if (node->left  == NULL) return minHeight(node->right, height+1);
    if (node->right == NULL) return minHeight(node->left, height+1);

    unsigned int left_min  = minHeight(node->left, height+1);
    unsigned int right_min = minHeight(node->right, height+1);

    if (left_min < right_min) {
        return left_min;
    } else {
        return right_min;
    }
}

unsigned int maxHeight(struct Node* node, unsigned int height) {
    if ((node->left == NULL) && (node->right == NULL)) return height;
    if (node->left  == NULL) return maxHeight(node->right, height+1);
    if (node->right == NULL) return maxHeight(node->left, height+1);

    unsigned int left_max  = maxHeight(node->left, height+1);
    unsigned int right_max = maxHeight(node->right, height+1);

    if (left_max > right_max) {
        return left_max;
    } else {
        return right_max;
    }
}

void enumerateInputs(struct Context* context, struct Node* node) {
    if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) {
        return meta(context, Exit);
    }

    node->key     = nondet_int();
    node->value   = node->key;
    context->next = VerifySpecification;
    context->loopCount++;

    return meta(context, Put);
}

void enumerateInputs_stub(struct Context* context) {
    return enumerateInputs(context, &context->data[Node]->node);
}


void verifySpecification(struct Context* context, struct Tree* tree) {
    assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
    return meta(context, EnumerateInputs);
}

void verifySpecification_stub(struct Context* context) {
    return verifySpecification(context, &context->data[Tree]->tree);
}


int main(int argc, char const* argv[]) {
    startCode(EnumerateInputs);
    return 0;
}