From d0ee02a16e9266da088b78ab8d2982f1c215fa1b Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Sun, 10 Apr 2016 09:57:30 +0100 Subject: [PATCH] bimap helper added --- modelchecker/coord.c | 49 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 46 insertions(+), 3 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index f6e2234..c74c2fe 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -46,8 +46,8 @@ typedef struct { } bddvar_xy_map; typedef struct { - xy_bddvar_map f; - bddvar_xy_map t; + xy_bddvar_map *f; + bddvar_xy_map *t; } bimap; xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map) @@ -82,7 +82,6 @@ xy_bddvar_map *create_xy_bddvar_map(sokoban_screen *screen) memset(f, 0, sizeof(xy_bddvar_map)); f->key.x = r->coord.x; f->key.y = r->coord.y; - printf("test!: %d %d\n", r->coord.x, r->coord.y); f->value.var[0] = varcount; f->value.var[1] = varcount + 1; f->value.var[2] = varcount + 2; @@ -114,6 +113,41 @@ bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen) return bddxy; } +bimap *create_bimap_helper(sokoban_screen *screen) +{ + int varcount = 0; + sokoban_screen *r; + xy_bddvar_map *xybdd = NULL; + bddvar_xy_map *bddxy = NULL; + for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ + xy_bddvar_map *f = NULL; + f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map)); + memset(f, 0, sizeof(xy_bddvar_map)); + f->key.x = r->coord.x; + f->key.y = r->coord.y; + f->value.var[0] = varcount; + f->value.var[1] = varcount + 1; + f->value.var[2] = varcount + 2; + HASH_ADD(hh, xybdd, key, sizeof(xy), f); + + for (int i = 0; i <3; i++){ + bddvar_xy_map *t = NULL; + t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map)); + memset(t, 0, sizeof(bddvar_xy_map)); + t->key = varcount + i; + t->value.x = r->coord.x; + t->value.y = r->coord.y; + HASH_ADD(hh, bddxy, key, sizeof(int), t); + } + varcount = varcount + 3; + } + bimap *bm = NULL; + bm = (bimap *)malloc(sizeof(bimap)); + bm->f = xybdd; + bm->t = bddxy; + return bm; +} + /* * Each coordinate has three related boolean variables. The combination of those boolean variables * defines tiles: @@ -276,7 +310,16 @@ BDD encode_screen(sokoban_screen *screen) printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]); printf("Test2: %d %d\n", m2->value.x, m2->value.y); */ + /* + bimap *bm = NULL; + bm = create_bimap_helper(screen); + xy_bddvar_map *m = getxy(1, 1, bm->f); + bddvar_xy_map *m2 = getbdd(2, bm->t); + printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]); + printf("Test2: %d %d\n", m2->value.x, m2->value.y); printf("%d tiles were encoded\n", tile_index); + if (bm != NULL) printf ("WORKS!\n"); + */ return state; } -- 2.20.1