From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Thu, 7 Apr 2016 09:04:47 +0000 (+0100)
Subject: started with bdd encoding
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=363cf737b04fbeab89362b6252b97db10d25ca02;p=mc1516pa.git

started with bdd encoding
---

diff --git a/modelchecker/Makefile b/modelchecker/Makefile
index ab7ffb8..7984b1b 100644
--- a/modelchecker/Makefile
+++ b/modelchecker/Makefile
@@ -1,5 +1,5 @@
 PROGRAM:=main
-OBJS:=sokoban.o # Here comes coord.o and object.o
+OBJS:=sokoban.o coord.o
 
 CFLAGS:=-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11\
 	-I./sylvan/src
diff --git a/modelchecker/coord.c b/modelchecker/coord.c
new file mode 100644
index 0000000..4c19a60
--- /dev/null
+++ b/modelchecker/coord.c
@@ -0,0 +1,52 @@
+#include <argp.h>
+#include <inttypes.h>
+#include <locale.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <sys/time.h>
+
+#ifdef HAVE_PROFILER
+#include <gperftools/profiler.h>
+#endif
+
+#include <sylvan.h>
+#include <llmsset.h>
+#include <lace.h>
+
+#include "coord.h"
+#include "sokoban.h"
+
+
+BDD encode_screen(sokoban_screen *screen)
+{
+	int num_tiles;
+	num_tiles = HASH_COUNT(screen);
+	printf("Number of tiles: %d\n", num_tiles);
+	return sylvan_true;
+}
+
+BDD encode_rel(sokoban_screen *screen)
+{
+	int num_tiles;
+	num_tiles = HASH_COUNT(screen);
+	printf("Number of tiles: %d\n", num_tiles);
+	return sylvan_true;
+}
+
+void test()
+{
+
+	printf("Test!\n");
+	BDD a = sylvan_true;
+	BDD b = sylvan_not(a);
+	if (b == sylvan_false){
+		printf("BDD works!\n");
+	} else {
+		printf("BDD does not work!\n");
+	}
+	LACE_ME;
+	BDD c = sylvan_ithvar(1);
+	if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
+	if (sylvan_var(c) == 1) printf("Var works 2\n");
+}
diff --git a/modelchecker/coord.h b/modelchecker/coord.h
new file mode 100644
index 0000000..2580d60
--- /dev/null
+++ b/modelchecker/coord.h
@@ -0,0 +1,10 @@
+#ifndef COORD_H
+#define COORD_H
+
+#include "sokoban.h"
+
+BDD encode_screen(sokoban_screen *screen);
+
+BDD encode_rel(sokoban_screen *screen);
+
+#endif
diff --git a/modelchecker/main.c b/modelchecker/main.c
index 1fd9e93..45831e7 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -7,6 +7,7 @@
 #include <sylvan.h>
 
 #include "sokoban.h"
+#include "coord.h"
 
 #define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
 #define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
@@ -47,18 +48,20 @@ void solve(FILE *inputstream)
 	sokoban_screen *screen = parse_screen(inputstream);
 	if (screen == NULL) printf("Something went wrong...\n");
 	sokoban_print(screen);
-	sokoban_free(screen);
 
 	time_end_read = clock();
 	time_start_encode = clock();
-	
+
 	lace_init(0, 1000000);
 	lace_startup(0, NULL, NULL);
 	LACE_ME;
     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
     sylvan_init_bdd(6);
-	
-	//ENCODE???
+
+	encode_screen(screen);
+
+	sokoban_free(screen);
+
 	switch(strat){
 		case COORD:
 			DPRINT("Encoding coordinate based\n");