From 97d0e60c5370a856bad627590764d70abde9f7a5 Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Tue, 12 Apr 2016 01:16:54 +0100 Subject: [PATCH] some clean-up --- modelchecker/coord.c | 300 ------------------------------------------- 1 file changed, 300 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 85b1867..b96eef0 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -17,12 +17,6 @@ #include "coord.h" #include "sokoban.h" -/* - * Global TODOs for now: - * - update the helper maps so it is a single bimap - * - make a data structure for relations - * - encode relations as a set of four relations for each move - */ typedef struct { int x; @@ -69,51 +63,6 @@ bddvar_xy_map *getbdd(int key, bddvar_xy_map *map) return r; } -/* -xy_bddvar_map *create_xy_bddvar_map(sokoban_screen *screen) -{ - int varcount = 0; - sokoban_screen *r; - xy_bddvar_map *xybdd = NULL; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ - xy_bddvar_map *f = NULL; - //bddvar_xy_map *t = 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); - varcount = varcount + 3; - } - return xybdd; -} - -bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen) -{ - int varcount = 0; - sokoban_screen *r; - bddvar_xy_map *bddxy = NULL; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ - for (int i = 0; i <3; i++){ - bddvar_xy_map *f = NULL; - //bddvar_xy_map *t = NULL; - - f = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map)); - memset(f, 0, sizeof(bddvar_xy_map)); - f->key = varcount + i; - f->value.x = r->coord.x; - f->value.y = r->coord.y; - HASH_ADD(hh, bddxy, key, sizeof(int), f); - } - varcount = varcount + 3; - } - return bddxy; -} -*/ bimap *create_bimap_helper(sokoban_screen *screen) { @@ -269,39 +218,6 @@ state *encode_screen(sokoban_screen *screen) return fullState; } -int -test_relprod() -{ - LACE_ME; - - BDDVAR vars[] = {0,2,4}; - BDDVAR all_vars[] = {4,5}; - - BDDSET vars_set = sylvan_set_fromarray(vars, 3); - BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 2); - - BDD s, t, next, prev; - BDD zeroes, ones; - - // transition relation: 000 --> 111 and !000 --> 000 - t = sylvan_false; - //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1,0,1,0,1})); - //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0})); - //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,1,0,2,0})); - t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0})); - - s = sylvan_cube(vars_set, (uint8_t[]){0,0,1}); - zeroes = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); - ones = sylvan_cube(vars_set, (uint8_t[]){0,0,1}); - - next = sylvan_relnext(s, t, all_vars_set); - prev = sylvan_relprev(t, next, all_vars_set); - if (next == zeroes) printf("Pass 1\n"); - if (prev == ones || prev == zeroes) printf("Pass 2\n"); - - return 0; -} - BDD create_single_rel(sokoban_screen *screen, direction dir) { LACE_ME; @@ -565,222 +481,6 @@ rels *encode_rel(sokoban_screen *screen) //left relation tl = create_single_rel(screen, LEFT); - /* - for (unsigned int i = 0; i < HASH_COUNT(screen); i++){ - printf("i:%d\n", i); - bddxy = getbdd(i*3, bm->t); - x = bddxy->value.x; - y = bddxy->value.y; - if (check_space(x, y, LEFT, 1, bm) == 0){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - if (tmp_scr->tile == AGENT){ - //1 1 0 0 1 1 (1 0 1 -> 1 0 1) - BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 6); - uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT){ - //1 1 1 1 0 0 (1 1 0 -> 1 1 0) - BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 6); - uint8_t rel_enc[6] = {1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - } - else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen); - xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f); - int deltai = bddvar->value.var[0]; - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 0 1 1 1 0 0 0 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 0 1 1 1 0 0 1 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 1 1 0 1 0 1 0 0 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 1 1 0 1 0 1 1 0 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){ - //(0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){ - //(1 1 0 0 0 0 1 1 0 0 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){ - //(0 0 1 1 0 0 1 1 1 1 0 0) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){ - //(1 1 0 0 0 0 1 1 1 1 0 0) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - } - else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen); - sokoban_screen *tmp_scr_g = get_coord(x - 2, y, screen); - xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f); - int deltai = bddvar->value.var[0]; - bddvar = getxy(x - 2, y, bm->f); - int gammai = bddvar->value.var[0]; - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 0 1 1 1 0 0 0 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 0 1 1 1 0 0 1 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 1 1 0 1 0 1 0 0 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 1 1 0 1 0 1 1 0 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){ - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){ - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ - //free box agent -> box agent free - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ - //(free targbox agent -> box targagent free) - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ - //(target box agent -> targbox agent free) - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ - //(target targbox agent -> targbox targagent free) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ - //(free box targagent -> box agent target) - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ - //(free targbox targagent -> box targagent target) - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ - //(target box targagent -> targbox agent target) - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ - //(target targbox targagent -> targbox targagent target) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - } - } - */ //up relation BDD tu = create_single_rel(screen, UP); -- 2.20.1