X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=02cda40f09ee0bedcbc35eb59b93a76c02b246ee;hb=b29982e8181d823142ce12b6d582181937fba7ad;hp=45831e7d2cbadddfbf0995db630f35066226d2bf;hpb=3350e67ad7c96bf9b821c0d691a58eb141a13e17;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 45831e7..02cda40 100644
--- 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???