From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Wed, 20 Apr 2016 17:53:11 +0000 (+0200)
Subject: lurd solver
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=7b36d26b43604aa30cd19f6d5345a9d881aff000;p=mc1516pa.git

lurd solver
---

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 85c6303..b50a1a4 100644
--- 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++){