made a stub for object oriented appearch

diff --git a/modelchecker/Makefile b/modelchecker/Makefile
index 7984b1b..0de3de3 100644 (file)
--- a/modelchecker/Makefile
+++ b/modelchecker/Makefile
@@ -1,5 +1,5 @@
 PROGRAM:=main
-OBJS:=sokoban.o coord.o
+OBJS:=sokoban.o coord.o object.o
 
 CFLAGS:=-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11\
        -I./sylvan/src

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 45831e7..02cda40 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -8,6 +8,7 @@
 
 #include "sokoban.h"
 #include "coord.h"
+#include "object.h"
 
 #define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
 #define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
@@ -57,25 +58,24 @@ void solve(FILE *inputstream)
        LACE_ME;
     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
     sylvan_init_bdd(6);
-
-       encode_screen(screen);
-
-       sokoban_free(screen);
-
        switch(strat){
                case COORD:
                        DPRINT("Encoding coordinate based\n");
+                       encode_screen(screen);
                        break;
                case OBJECT:
                        DPRINT("Encoding object based\n");
+                       solve_object(screen);
                        break;
                case HYBRID:
                        DPRINT("Encoding hybrid based\n");
+                       DPRINT("Not implemented yet...\n");
                        break;
                default:
                        ERRPRINT("Huh?");
                        exit(2);
        }
+       sokoban_free(screen);
        time_end_encode = clock();
 
        //SOLVE???

diff --git a/modelchecker/object.c b/modelchecker/object.c
new file mode 100644 (file)
index 0000000..5829ed3
--- /dev/null
+++ b/modelchecker/object.c
@@ -0,0 +1,11 @@
+#include <sylvan.h>
+
+#include "object.h"
+#include "sokoban.h"
+
+BDD solve_object(sokoban_screen *screen)
+{
+       BDD state = sylvan_false;
+       return state;
+       (void) screen; //To avoid not used error
+}

diff --git a/modelchecker/object.h b/modelchecker/object.h
new file mode 100644 (file)
index 0000000..af00378
--- /dev/null
+++ b/modelchecker/object.h
@@ -0,0 +1,10 @@
+#ifndef OBJECT_H
+#define OBJECT_H
+
+#include <sylvan.h>
+
+#include "sokoban.h"
+
+BDD solve_object(sokoban_screen *screen);
+
+#endif

diff --git a/modelchecker/sokoban.h b/modelchecker/sokoban.h
index 30466e3..6b8823d 100644 (file)
--- a/modelchecker/sokoban.h
+++ b/modelchecker/sokoban.h
@@ -1,5 +1,7 @@
 #ifndef SOKOBAN_H
 #define SOKOBAN_H
+#include <stdio.h>
+
 #include "uthash.h"
 
 typedef enum {FREE, WALL, BOX, TARGET, AGENT, TARGAGENT, TARGBOX} sokoban_tile;