some checks

[mc1516pa.git] / modelchecker / main.c

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 45831e7..7cc1070 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);
@@ -47,9 +48,9 @@ void solve(FILE *inputstream)
        time_start_read = clock();
        sokoban_screen *screen = parse_screen(inputstream);
        if (screen == NULL) printf("Something went wrong...\n");
-       sokoban_print(screen);
-
+       //sokoban_print(screen);
        time_end_read = clock();
+
        time_start_encode = clock();
 
        lace_init(0, 1000000);
@@ -58,28 +59,60 @@ void solve(FILE *inputstream)
     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");
-                       break;
-               case OBJECT:
-                       DPRINT("Encoding object based\n");
-                       break;
-               case HYBRID:
-                       DPRINT("Encoding hybrid based\n");
-                       break;
-               default:
-                       ERRPRINT("Huh?");
-                       exit(2);
+       state *init = encode_screen(screen);
+       rels *rls = encode_rel(screen);
+
+       BDD old = sylvan_false;
+       BDD new = init->bdd;
+       int iteration = 0;
+       while(new != old){
+               old = new;
+               ERRPRINT("Iteration %d\n", iteration++);
+        trans_t *t = rls->rell;
+
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        t = rls->relu;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        t = rls->relr;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        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(old, init->vars.varset));
+               //sylvan_printdot_nc(old);
+       //switch(strat){
+       //      case COORD:
+       //              DPRINT("Encoding coordinate based\n");
+       //              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);
+       //}
        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",