From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 6 Apr 2016 15:00:03 +0000 (+0200)
Subject: fixed makefile, made lace stub, updated headers
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=2be3ea1fc484406a2865426c9b02ad7e9ff703ba;p=mc1516pa.git

fixed makefile, made lace stub, updated headers
---

diff --git a/modelchecker/Makefile b/modelchecker/Makefile
index 97496e7..ab7ffb8 100644
--- a/modelchecker/Makefile
+++ b/modelchecker/Makefile
@@ -1,11 +1,16 @@
 PROGRAM:=main
-OBJS:=sokoban.o mc.o
+OBJS:=sokoban.o # Here comes coord.o and object.o
 
-CFLAGS=-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11 \
+CFLAGS:=-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11\
 	-I./sylvan/src
+LDLIBS:=-lm -lpthread -lrt
+LDFLAGS:=./sylvan/src/libsylvan.a
 
 $(PROGRAM): $(PROGRAM).o $(OBJS)
-	$(CC) $< $(OBJS) -o $@
+	$(CC) $(CFLAGS) $< $(OBJS) $(LDFLAGS) $(LDLIBS) -o $@
+
+%.o: %.c %.h
+	$(CC) $(CFLAGS) -c -o $@ $<
 
 clean:
 	$(RM) -v $(PROGRAM).o $(PROGRAM) $(OBJS)
diff --git a/modelchecker/main.c b/modelchecker/main.c
index 9d93ef2..1fd9e93 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -2,20 +2,24 @@
 #include <stdbool.h>
 #include <ctype.h>
 #include <time.h>
+#include <unistd.h>
 
 #include <sylvan.h>
 
-#include "mc.h"
 #include "sokoban.h"
 
+#define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
+#define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
+
+typedef enum {OBJECT, COORD, HYBRID} strategy;
+
 //Global variables
 bool DEBUG = false;
 strategy strat = HYBRID;
 
 void usage(char *prg)
 {
-	fprintf(stderr,
-		"Usage:\n"
+	ERRPRINT("Usage:\n"
 		"\t%s [opts] [FILE [FILE [...]]]\n"
 		"\n"
 		"Options:\n"
@@ -44,30 +48,38 @@ void solve(FILE *inputstream)
 	if (screen == NULL) printf("Something went wrong...\n");
 	sokoban_print(screen);
 	sokoban_free(screen);
-	//parse_screen(inputstream);
-	time_end_read = clock();
 
+	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???
 	switch(strat){
-	case COORD:
-		if(DEBUG) fprintf(stderr, "Encoding coordinate based\n");
-		break;
-	case OBJECT:
-		if(DEBUG) fprintf(stderr, "Encoding object based\n");
-		break;
-	case HYBRID:
-		if(DEBUG) fprintf(stderr, "Encoding hybrid based\n");
-		break;
-	default:
-		fprintf(stderr, "Huh?");
-		exit(2);
+		case COORD:
+			DPRINT("Encoding coordinate based\n");
+			break;
+		case OBJECT:
+			DPRINT("Encoding object based\n");
+			break;
+		case HYBRID:
+			DPRINT("Encoding hybrid based\n");
+			break;
+		default:
+			ERRPRINT("Huh?");
+			exit(2);
 	}
 	time_end_encode = clock();
 
-	// Future: SMC
-	fprintf(stderr, "Reading: %fs\n",
+	//SOLVE???
+
+	ERRPRINT("Reading: %fs\n",
 		((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
-	fprintf(stderr, "Encoding: %fs\n",
+	ERRPRINT("Encoding: %fs\n",
 		((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
 }
 
@@ -79,28 +91,28 @@ int main(int argc, char **argv)
 		switch(optchar){
 		case 'c':
 			strat = COORD;
-			if(DEBUG) fprintf(stderr, "Strategy changed to Coordinate based\n");
+			DPRINT("Strategy changed to Coordinate based\n");
 			break;
 		case 'd':
 			DEBUG = true;
-			if(DEBUG) fprintf(stderr, "Debug enabled\n");
+			DPRINT("Debug enabled\n");
 			break;
 		case 'h':
 			usage(argv[0]);
 			return 0;
 		case 'o':
 			strat = OBJECT;
-			if(DEBUG) fprintf(stderr, "Strategy changed to Object based\n");
+			DPRINT("Strategy changed to Object based\n");
 			break;
 		case 'y':
 			strat = HYBRID;
-			if(DEBUG) fprintf(stderr, "Strategy changed to Hybrid\n");
+			DPRINT("Strategy changed to Hybrid\n");
 			break;
 		case '?':
 			if(isprint(optopt)){
-				fprintf(stderr, "Unknown option `-%c'.\n", optopt);
+				ERRPRINT("Unknown option `-%c'.\n", optopt);
 			} else {
-				fprintf(stderr, "Unknown option char `-\\x%x'.\n", optopt);
+				ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
 			}
 			return 2;
 		default:
@@ -109,17 +121,17 @@ int main(int argc, char **argv)
 	}
 
 	if(optind == argc){
-		fprintf(stderr, "You have not specified a file, reading from stdin\n");
+		ERRPRINT("You have not specified a file, reading from stdin\n");
 		solve(stdin);
 	}
 
 	for(int filepathindex = optind; filepathindex < argc; filepathindex++){
 		char *currentfilepath = argv[filepathindex];
-		fprintf(stderr, "Processing: %s\n", currentfilepath);
+		ERRPRINT("Processing: %s\n", currentfilepath);
 		FILE *currentfile = fopen(currentfilepath, "r");
-		if(DEBUG) fprintf(stderr, "Opening file\n");
+		DPRINT("Opening file\n");
 		solve(currentfile);
-		if(DEBUG) fprintf(stderr, "Closing file\n");
+		DPRINT("Closing file\n");
 		fclose(currentfile);
 	}
 	return 0;
diff --git a/modelchecker/mc.c b/modelchecker/mc.c
deleted file mode 100644
index 09bfc54..0000000
--- a/modelchecker/mc.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "mc.h"
-
diff --git a/modelchecker/mc.h b/modelchecker/mc.h
deleted file mode 100644
index fd90291..0000000
--- a/modelchecker/mc.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef MC_H
-#define MC_H
-
-typedef enum {OBJECT, COORD, HYBRID} strategy;
-
-#endif