X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=bcf8c7b6106bb1ebda1dc159d2722d3fe2452e57;hb=b3851097adbafa74d01e05b25ba550a814a5767d;hp=e954c073f79fedc82ca930a780b3d836172df3a7;hpb=a2b59cab025a7ec42afb0f51e057361f590e8b3f;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index e954c07..bcf8c7b 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -46,7 +46,7 @@ void solve(FILE *inputstream)
 	clock_t time_start_encode, time_end_encode;
 
 	time_start_read = clock();
-	sokoban_screen *screen = parse_screen(inputstream);
+	sokoban_screen *screen = parse_screen(inputstream, false);
 	if (screen == NULL) printf("Something went wrong...\n");
 	//sokoban_print(screen);
 	time_end_read = clock();
@@ -58,28 +58,83 @@ void solve(FILE *inputstream)
 	LACE_ME;
     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
     sylvan_init_bdd(6);
-	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);
+
+	state *init = encode_screen(screen);
+    state *goal = encode_goal(screen);
+	rels *rls = encode_rel(screen);
+    /*
+    printf("Doing left\n");
+    test_trans(init, rls->rell);
+    printf("Doing up\n");
+    test_trans(init, rls->relu);
+    printf("Doing right\n");
+    test_trans(init, rls->relr);
+    printf("Doing down\n");
+    test_trans(init, rls->reld);
+    */
+
+	BDD old = sylvan_false;
+	BDD new = init->bdd;
+	int iteration = 0;
+    if (goal != NULL){
+        while(new != old){
+            old = new;
+            ERRPRINT("Iteration %d\n", iteration++);
+            trans_t *t = rls->rell;
+
+            //for testing
+            /*
+              BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9);
+              BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0});
+              BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0}));
+              BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1}));
+              if (new == teststate2) printf("Wrong!\n");
+            */
+            while (t != NULL){
+                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+                t = t->next_rel;
+                //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
+            }
+
+            t = rls->relu;
+            while (t != NULL){
+                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+                t = t->next_rel;
+                //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
+            }
+
+
+            t = rls->relr;
+            while (t != NULL){
+                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+                t = t->next_rel;
+                //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
+            }
+
+
+            t = rls->reld;
+            while (t != NULL){
+                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+                t = t->next_rel;
+                //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
+            }
+            double check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
+            if (check > 0){
+                printf("Solution is found after %d iteration(s)!\n", iteration);
+                break;
+            }
+        }
+        printf("Solution is not found after %d iteration(s)\n", iteration);
+    }
+    else printf("No solution found!\n");
+	//ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
+//	sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);
+//	sylvan_printdot_nc(old);
 	time_end_encode = clock();
 
 	//SOLVE???
 
+	sokoban_free(screen);
 	ERRPRINT("Reading: %fs\n",
 		((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
 	ERRPRINT("Encoding: %fs\n",