From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 21 Apr 2016 18:57:54 +0000 (+0200)
Subject: cleaned up code
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=313c58c1cd85852f33ff7ca7c638ccb3066d5069;p=mc1516pa.git
cleaned up code
---
diff --git a/modelchecker/Makefile b/modelchecker/Makefile
index e284a57..2463f37 100644
--- a/modelchecker/Makefile
+++ b/modelchecker/Makefile
@@ -1,7 +1,7 @@
PROGRAM:=main
-OBJS:=sokoban.o coord.o object.o deque.o
+OBJS:=sokoban.o coord.o
-CFLAGS:=-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11\
+CFLAGS:=-O3 -g -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11\
-I./sylvan/src
LDLIBS:=-lm -lpthread -lrt
LDFLAGS:=./sylvan/src/libsylvan.a
diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 6325091..42ad6ce 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -6,7 +6,6 @@
#include "coord.h"
#include "sokoban.h"
-#include "deque.h"
typedef struct {
@@ -123,7 +122,6 @@ int check_space(int x, int y, direction d, int delta, bimap *bm)
* It seems that the move variable is not necessary since non-deterministic moves can be emvedded
* directly in transition relations.
*/
-
state *encode_screen(sokoban_screen *screen)
{
LACE_ME;
@@ -142,272 +140,51 @@ state *encode_screen(sokoban_screen *screen)
fullState->vars.varset = varset;
fullState->vars.size = HASH_COUNT(screen) * 3;
int tile_index = 0;
- sokoban_screen *r;
- for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+ for(sokoban_screen *r=screen; r != NULL; r = r->hh.next){
switch(r->tile){
case FREE: //001
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 1;
- tile_index++;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 1;
break;
case WALL: //000
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
break;
case BOX: //010
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 0;
break;
case TARGET: //011
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 1;
- tile_index++;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 1;
break;
case AGENT: //101
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
-
- st_enc[tile_index] = 1;
- tile_index++;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 1;
break;
case TARGAGENT: //110
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 0;
break;
case TARGBOX: //100
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
break;
}
}
s = sylvan_cube(varset, st_enc);
fullState->bdd = s;
- printf("Initial state encoded\n");
return fullState;
}
-lurd_t *lappend(lurd_t *l, char c){
- lurd_t *temp_lrd = NULL;
- if (l == NULL){
- temp_lrd = (lurd_t *)malloc(sizeof(lurd_t));
- temp_lrd->c = c;
- temp_lrd->next = NULL;
- l = temp_lrd;
- }
- else {
- temp_lrd = l;
- while (temp_lrd->next != NULL){
- temp_lrd = temp_lrd->next;
- }
- temp_lrd->next = (lurd_t *)malloc(sizeof(lurd_t));
- temp_lrd->next->c = c;
- temp_lrd->next->next = NULL;
- }
- return l;
-}
-
-int check_goal(BDD s, BDD g, BDDSET vars){
- LACE_ME;
- if(sylvan_satcount(sylvan_and(s, g), vars) > 0) return 1;
- else return 0;
-}
-
-int check_visited(BDD s, BDD v, BDDSET vars){
- LACE_ME;
- if(sylvan_satcount(sylvan_and(s, v), vars) > 0) return 1;
- else return 0;
-}
-
-state_t *explstate(state *init, rels *rls, state *g){
- LACE_ME;
- deque *state_queue = create();
- trans_t *t = NULL;
- state_t *tmp_state = (state_t *)malloc(sizeof(state_t));
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- //state_t *new_state = (state_t *)malloc(sizeof(state_t));
- BDD visited = init->bdd;
- BDD new;
- tmp_state->bdd = init->bdd;
- tmp_state->vars = init->vars;
- tmp_state->lrd = lrd;
- state_queue = enq(tmp_state, state_queue);
-
- while (isEmpty(state_queue) == 0){
- tmp_state = get_front(state_queue);
- state_queue = deq(state_queue);
- new = tmp_state->bdd;
- t = rls->rell;
- while (t != NULL){
- new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
- if (new != sylvan_false && new != tmp_state->bdd) break;
- t = t->next_rel;
- }
- if (new != sylvan_false && new != tmp_state->bdd){
- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'l');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- printf("GOAL\n");
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'l');
- new_state->lrd = lrd;
- return new_state;
- }
- }
- }
-
- t = rls->relu;
- while (t != NULL){
- new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
- if (new != sylvan_false && new != tmp_state->bdd) break;
- t = t->next_rel;
- }
- if (new != sylvan_false && new != tmp_state->bdd){
- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'u');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- printf("GOAL\n");
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'u');
- new_state->lrd = lrd;
- return new_state;
- }
- }
- }
-
- t = rls->relr;
- while (t != NULL){
- new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
- if (new != sylvan_false && new != tmp_state->bdd) break;
- t = t->next_rel;
- }
- if (new != sylvan_false && new != tmp_state->bdd){
- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
-
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'r');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- printf("GOAL\n");
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
-
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'r');
- new_state->lrd = lrd;
- return new_state;
- }
- }
- }
-
-
- t = rls->reld;
- while (t != NULL){
- new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
- if (new != sylvan_false && new != tmp_state->bdd) break;
- t = t->next_rel;
- }
- if (new != sylvan_false && new != tmp_state->bdd){
- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
-
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
-
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'd');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- printf("GOAL\n");
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
-
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'd');
- new_state->lrd = lrd;
- return new_state;
- }
- }
- }
-
-
- }
-
- return NULL;
-}
-
state *encode_goal(sokoban_screen *screen){
- int boxes = 0;
- int targets = 0;
-
LACE_ME;
BDDVAR vars[HASH_COUNT(screen) * 3];
@@ -424,83 +201,50 @@ state *encode_goal(sokoban_screen *screen){
fullState->vars.varset = varset;
fullState->vars.size = HASH_COUNT(screen) * 3;
int tile_index = 0;
- sokoban_screen *r;
- for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+ for(sokoban_screen *r=screen; r != NULL; r=r->hh.next){
switch(r->tile){
case FREE: //001 -> any
- st_enc[tile_index] = 2;
- tile_index++;
- st_enc[tile_index] = 2;
- tile_index++;
- st_enc[tile_index] = 2;
- tile_index++;
+ st_enc[tile_index++] = 2;
+ st_enc[tile_index++] = 2;
+ st_enc[tile_index++] = 2;
break;
case WALL: //000 -> stays the same
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
break;
case BOX: //010 -> any
- boxes++;
- st_enc[tile_index] = 2;
- tile_index++;
- st_enc[tile_index] = 2;
- tile_index++;
- st_enc[tile_index] = 2;
- tile_index++;
+ st_enc[tile_index++] = 2;
+ st_enc[tile_index++] = 2;
+ st_enc[tile_index++] = 2;
break;
case TARGET: //011 -> targbox
- targets++;
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
break;
case AGENT: //101 -> any
- st_enc[tile_index] = 2;
- tile_index++;
- st_enc[tile_index] = 2;
- tile_index++;
- st_enc[tile_index] = 2;
- tile_index++;
+ st_enc[tile_index++] = 2;
+ st_enc[tile_index++] = 2;
+ st_enc[tile_index++] = 2;
break;
case TARGAGENT: //110 -> targbox
- targets++;
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
break;
case TARGBOX: //100 -> stays the same
- targets++;
- boxes++;
- st_enc[tile_index] = 1;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
- st_enc[tile_index] = 0;
- tile_index++;
+ st_enc[tile_index++] = 1;
+ st_enc[tile_index++] = 0;
+ st_enc[tile_index++] = 0;
break;
}
}
s = sylvan_cube(varset, st_enc);
fullState->bdd = s;
- printf("Goal state encoded\n");
- if (targets == 0 || (boxes != targets)) return NULL;
- else return fullState;
-
+ return fullState;
}
-//test
-//int countTrans(trans_t *trs);
-
trans_t *create_single_rel(sokoban_screen *screen, direction dir)
{
LACE_ME;
@@ -571,9 +315,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
trs_current->next_rel = trs;
trs = trs_current;
- }
-
- else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
+ } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
unsigned int deltai = bddvar->value.var[0];
//Agent Free -> Free Agent
@@ -737,11 +479,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
trs_current->varset.size = 12;
trs_current->next_rel = trs;
trs = trs_current;
-
-
- }
-
- else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
+ } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
unsigned int deltai = bddvar->value.var[0];
bddvar = getxy(x + xgamma, y + ygamma, bm->f);
@@ -1367,47 +1105,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
}
trs_current = trs;
-
- //test
- /*
- switch(dir){
- case LEFT:
- if (trs_current != NULL) printf("LEFT ok!\n");
- else printf ("LEFT is empty\n");
- printf("Num of trans relations:%d\n", countTrans(trs));
- break;
- case UP:
- if (trs_current != NULL) printf("UP ok!\n");
- else printf ("UP is empty\n");
- printf("Num of trans relations:%d\n", countTrans(trs));
- break;
- case RIGHT:
- if (trs_current != NULL) printf("RIGHT ok!\n");
- else printf ("RIGHT is empty\n");
- printf("Num of trans relations:%d\n", countTrans(trs));
- break;
- case DOWN:
- if (trs_current != NULL) printf("DOWN ok!\n");
- else printf ("DOWN is empty\n");
- printf("Num of trans relations:%d\n", countTrans(trs));
- break;
- }
- */
return trs;
}
-//test
-/*
-int countTrans(trans_t *trs)
-{
- int counter = 0;
- while (trs != NULL){
- counter++;
- trs = trs->next_rel;
- }
- return counter;
-}
-*/
rels *encode_rel(sokoban_screen *screen)
{
LACE_ME;
@@ -1416,14 +1116,8 @@ rels *encode_rel(sokoban_screen *screen)
//left relation
tl = create_single_rel(screen, LEFT);
-
- //up relation
trans_t *tu = create_single_rel(screen, UP);
-
- //right relation
trans_t *tr = create_single_rel(screen, RIGHT);
-
- //down relation
trans_t *td = create_single_rel(screen, DOWN);
rels *rls = NULL;
@@ -1435,17 +1129,3 @@ rels *encode_rel(sokoban_screen *screen)
return rls;
}
-
-int test_trans(state *s, trans_t *t)
-{
- LACE_ME;
- BDD next = sylvan_false;
- while (t != NULL){
- next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
- if (next == s->bdd) printf("Same\n");
- if (next != s->bdd && next != sylvan_false) printf("Different\n");
- if (next == sylvan_false) printf("False\n");
- t = t->next_rel;
- }
- return 1;
-}
diff --git a/modelchecker/coord.h b/modelchecker/coord.h
index 014579f..15f6c76 100644
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -40,21 +40,7 @@ typedef struct {
typedef enum { LEFT, UP, RIGHT, DOWN } direction;
state *encode_screen(sokoban_screen *screen);
-
rels *encode_rel(sokoban_screen *screen);
-
-int test_trans(state *s, trans_t *t);
-
state *encode_goal(sokoban_screen *screen);
-int check_goal(BDD s, BDD g, BDDSET vars);
-
-int check_visited(BDD s, BDD v, BDDSET vars);
-
-lurd_t *lappend(lurd_t *l, char c);
-
-state_t *explstate(state *init, rels *rls, state *g);
-
-int test_relprod();
-
#endif
diff --git a/modelchecker/deque.c b/modelchecker/deque.c
deleted file mode 100644
index 12ad6fc..0000000
--- a/modelchecker/deque.c
+++ /dev/null
@@ -1,71 +0,0 @@
-#include <argp.h>
-#include <stdio.h>
-#include <stdlib.h>
-#include <sylvan.h>
-#include <lace.h>
-
-#include "deque.h"
-
-deque *create()
-{
- deque *d;
- d = (deque *)malloc(sizeof(deque));
- d->front = NULL;
- d->rear = NULL;
- d->count = 0;
-
- return d;
-}
-
-deque *enq(state_t *s, deque *d)
-{
- if (d->rear == NULL){
- d->rear = (node_t *)malloc(sizeof(node_t));
- d->rear->ptr = NULL;
- d->rear->s = s;
- d->front = d->rear;
- }
- else {
- node_t *temp = (node_t *)malloc(sizeof(node_t));
- d->rear->ptr = temp;
- temp->s = s;
- temp->ptr = NULL;
- d->rear = temp;
- }
- d->count++;
-
- return d;
-}
-
-deque *deq(deque *d)
-{
- node_t *front_tmp = d->front;
-
- if (front_tmp == NULL){
- return d;
- }
- else if (front_tmp->ptr != NULL){
- front_tmp = front_tmp->ptr;
- free(d->front);
- d->front = front_tmp;
- }
- else {
- free(d->front);
- d->front = NULL;
- d->rear = NULL;
- }
- d->count--;
- return d;
-}
-
-int isEmpty(deque *d)
-{
- if (d->front != NULL && d->rear != NULL) return 0;
- else return 1;
-}
-
-state_t *get_front(deque *d)
-{
- if (isEmpty(d) == 0) return d->front->s;
- else return NULL;
-}
diff --git a/modelchecker/deque.h b/modelchecker/deque.h
deleted file mode 100644
index 16125ea..0000000
--- a/modelchecker/deque.h
+++ /dev/null
@@ -1,28 +0,0 @@
-#ifndef DEQUE_H
-#define DEQUE_H
-#include <stdio.h>
-#include <stdbool.h>
-#include "coord.h"
-
-typedef struct node {
- state_t *s;
- struct node *ptr;
-} node_t;
-
-typedef struct {
- node_t *front;
- node_t *rear;
- int count;
-} deque;
-
-deque *create();
-
-deque *enq(state_t *s, deque *d);
-
-deque *deq(deque *d);
-
-int isEmpty(deque *d);
-
-state_t *get_front(deque *d);
-
-#endif
diff --git a/modelchecker/main.c b/modelchecker/main.c
index 79bb46d..07a665c 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -8,7 +8,6 @@
#include "sokoban.h"
#include "coord.h"
-#include "object.h"
#define DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as);
#define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC);
@@ -48,7 +47,7 @@ int solve(FILE *inputstream, char *lurd)
//Read screen
time_start_read = clock();
- sokoban_screen *screen = parse_screen(inputstream, false);
+ sokoban_screen *screen = parse_screen(inputstream, true);
if (screen == NULL) {
printf("Something went wrong encoding the screen\n");
return 2;
@@ -130,7 +129,7 @@ int solve(FILE *inputstream, char *lurd)
REPORT("Goal encoding: %fs\n", time_end_goal, time_start_goal);
REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel);
REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve);
-
+ DPRINT("Iterations needed: %d\n", iteration);
if(!found){
printf("no solution\n");
diff --git a/modelchecker/object.c b/modelchecker/object.c
deleted file mode 100644
index 362802d..0000000
--- a/modelchecker/object.c
+++ /dev/null
@@ -1,202 +0,0 @@
-#include <sylvan.h>
-#include <stdbool.h>
-
-#include "object.h"
-#include "sokoban.h"
-
-#define MAX_BOX 50
-#define EPRINTF(fmt, as...) fprintf(stderr, fmt, ##as)
-
-typedef enum {UP, DOWN, LEFT, RIGHT} direction;
-
-int ilog2(int x)
-{
- int l = 1;
- while((x >>= 1) >= 1)
- l++;
- return l;
-}
-
-void get_screen_metrics(sokoban_screen *screen,
- int *boxes,
- int *mx, int *my,
- int *agentx, int *agenty,
- int *boxxes, int *boxyes)
-{
- *boxes = 0;
- *mx = 0;
- *my = 0;
- *agentx = 0;
- *agenty = 0;
- sokoban_screen *r;
- for(r=screen; r != NULL; r = r->hh.next){
- *mx = r->coord.x > *mx ? r->coord.x : *mx;
- *my = r->coord.y > *my ? r->coord.x : *my;
- switch(r->tile){
- case TARGAGENT:
- case AGENT:
- *agentx = r->coord.x;
- *agenty = r->coord.y;
- break;
- case TARGBOX:
- case BOX:
- boxxes[*boxes] = r->coord.x;
- boxyes[*boxes] = r->coord.y;
- *boxes += 1;
- break;
- default:;
- }
- }
-}
-
-//LSB first
-BDD encode_int(BDD state, int x, int bx, int *variablenum)
-{
- LACE_ME;
- char *encoding = malloc(bx);
- for(int i = 0; i<bx; i++){
- if((x & (1<<i)) > 0){
- state = sylvan_and(state, sylvan_ithvar(*variablenum*2));
- } else {
- state = sylvan_and(state, sylvan_nithvar(*variablenum*2));
- }
- *variablenum += 1;
- }
- free(encoding);
- return state;
-}
-
-BDD encode_position(BDD state, int x, int y, int bx, int by, int *variablenum)
-{
- state = encode_int(state, x, bx, variablenum);
- return encode_int(state, y, by, variablenum);
-}
-
-BDD encode_transition(sokoban_screen *scr, BDD state, int bx, int by, int *varnum, direction dir)
-{
- LACE_ME;
- //Increase the position
- int oldvarnum = *varnum;
-
- //RIGHT
- if(dir == RIGHT){
- state = sylvan_and(state,
- sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1)));
- *varnum += 1;
- for(int i = 1; i<bx; i++){
- state = sylvan_and(state,
- sylvan_xor(sylvan_ithvar(*varnum*2-1),
- sylvan_xor(sylvan_ithvar(*varnum*2),
- sylvan_ithvar(*varnum*2+1))));
- *varnum += 1;
- }
- } else if(dir == LEFT){
- //TODO
- *varnum += bx;
- }else {
- *varnum += bx;
- }
-
- //DOWN
- if(dir == DOWN){
- state = sylvan_and(state,
- sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1)));
- *varnum += 1;
- for(int i = 1; i<by; i++){
- state = sylvan_and(state,
- sylvan_xor(sylvan_ithvar(*varnum*2-1),
- sylvan_xor(sylvan_ithvar(*varnum*2),
- sylvan_ithvar(*varnum*2+1))));
- *varnum += 1;
- }
- } else if(dir == UP){
- //TODO
- *varnum += by;
- } else {
- *varnum += by;
- }
-
- //Check wether it is a valid position
- BDD legalpos = sylvan_false;
- for(sokoban_screen *r=scr; r != NULL; r = r->hh.next){
- int x = r->coord.x;
- int y = r->coord.y;
- *varnum = oldvarnum;
-
- BDD currentx = sylvan_true;
- for(int i = 0; i<bx; i++){
- if((x & (1<<i)) > 0){
- currentx = sylvan_and(currentx, sylvan_ithvar(*varnum*2+1));
- } else {
- currentx = sylvan_and(currentx, sylvan_nithvar(*varnum*2+1));
- }
- *varnum += 1;
- }
-
- BDD currenty = sylvan_true;
- for(int i = 0; i<by; i++){
- if((y & (1<<i)) > 0){
- currenty = sylvan_and(currenty, sylvan_ithvar(*varnum*2+1));
- } else {
- currenty = sylvan_and(currenty, sylvan_nithvar(*varnum*2+1));
- }
- *varnum += 1;
- }
- legalpos = sylvan_or(legalpos,
- sylvan_and(currentx, currenty));
- }
-
- return sylvan_and(state, legalpos);
-}
-
-/*
- * We have variables numbered 1...
- * Per coordinate we need k=bitsx+bitsy variables
- *
- * agent: 0 till k
- * box_i: k+k*i till k+k*(i+1)
- * We start with the agent
- */
-BDD solve_object(sokoban_screen *scr)
-{
- LACE_ME;
- int nboxes, mx, my, wx, wy, agentx, agenty;
- int varnum = 0;
- int boxx[MAX_BOX];
- int boxy[MAX_BOX];
-
- get_screen_metrics(scr, &nboxes, &mx, &my, &agentx, &agenty, boxx, boxy);
-
- EPRINTF("Max x: %d, thus %d bits\n", mx, (wx = ilog2(mx)));
- EPRINTF("Max y: %d, thus %d bits\n", my, (wy = ilog2(my)));
- EPRINTF("%d boxes\n", nboxes);
-
- BDD init = encode_position(sylvan_true, agentx, agenty, wx, wy, &varnum);
- for(int i = 0; i<nboxes; i++){
- init = encode_position(init, boxx[i], boxy[i], wx, wy, &varnum);
- }
-
- varnum = 0;
- BDD trans_r = encode_transition(scr, sylvan_true, mx, my, &varnum, RIGHT);
- varnum = 0;
- BDD trans_l = encode_transition(scr, sylvan_true, mx, my, &varnum, LEFT);
- varnum = 0;
- BDD trans_d = encode_transition(scr, sylvan_true, mx, my, &varnum, DOWN);
- varnum = 0;
- BDD trans_u = encode_transition(scr, sylvan_true, mx, my, &varnum, UP);
-
- BDD old = sylvan_false;
- BDD new = init;
- int iteration = 0;
- while(new != old){
- EPRINTF("Iteration %d\n", iteration++);
- old = new;
- new = sylvan_or(new, sylvan_relnext(new, trans_d, false));
- new = sylvan_or(new, sylvan_relnext(new, trans_r, false));
- new = sylvan_or(new, sylvan_relnext(new, trans_u, false));
- new = sylvan_or(new, sylvan_relnext(new, trans_l, false));
- sylvan_printdot_nc(old);
- }
-
- return init;
-}
diff --git a/modelchecker/object.h b/modelchecker/object.h
deleted file mode 100644
index af00378..0000000
--- a/modelchecker/object.h
+++ /dev/null
@@ -1,10 +0,0 @@
-#ifndef OBJECT_H
-#define OBJECT_H
-
-#include <sylvan.h>
-
-#include "sokoban.h"
-
-BDD solve_object(sokoban_screen *screen);
-
-#endif