lurd solver

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 85c6303..b50a1a4 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -40,6 +40,73 @@ void usage(char *prg)
                "\t         when no file is specified stdin will be used\n", prg);
 }
 
+int lurd_solve(FILE *inputstream, char *lurd){
+
+       sokoban_screen *screen = parse_screen(inputstream, false);
+       if (screen == NULL) printf("Something went wrong...\n");
+
+       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);
+
+       state *init = encode_screen(screen);
+    state *goal = encode_goal(screen);
+    if (goal == NULL) printf("WRONG\n");
+       rels *rls = encode_rel(screen);
+       BDD new = init->bdd;
+    trans_t *t = NULL;
+
+    while (*lurd != '\n'){
+        printf("We're here1\n");
+        switch(*lurd){
+        case 'l':
+            printf("We're here2\n");
+            t = rls->rell;
+            while (t != NULL){
+                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+                t = t->next_rel;
+            }
+            lurd++;
+            break;
+        case 'u':
+            t = rls->relu;
+            while (t != NULL){
+                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+                t = t->next_rel;
+            }
+            lurd++;
+            break;
+        case 'r':
+            t = rls->relr;
+            while (t != NULL){
+                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+                t = t->next_rel;
+            }
+            lurd++;
+            break;
+        case 'd':
+            t = rls->reld;
+            while (t != NULL){
+                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+                t = t->next_rel;
+            }
+            lurd++;
+            break;
+        default: lurd++;
+        }
+
+    }
+
+    double check = 0;
+    if (goal != NULL) {
+        check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
+    }
+    if (check > 0) return 1;
+    else return 0;
+}
+
 void solve(FILE *inputstream)
 {
        clock_t time_start_read, time_end_read;
@@ -179,7 +246,10 @@ int main(int argc, char **argv)
 
        if(optind == argc){
                ERRPRINT("You have not specified a file, reading from stdin\n");
-               solve(stdin);
+               //solve(stdin);
+        char lrd[] = "ll\n";
+        if (lurd_solve(stdin, lrd) == 1) printf ("The given lurd solves the given screen\n");
+        else printf ("The given lurd can not solve the given screen\n");
        }
 
        for(int filepathindex = optind; filepathindex < argc; filepathindex++){