#include <sylvan.h>
#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);
time_start_read = clock();
sokoban_screen *screen = parse_screen(inputstream);
if (screen == NULL) printf("Something went wrong...\n");
- sokoban_print(screen);
- sokoban_free(screen);
-
+ //sokoban_print(screen);
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:
- 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){
+ ERRPRINT("Iteration %d\n", iteration++);
+ old = new;
+ new = sylvan_or(new, sylvan_relnext(new, rls->rell->bdd, rls->rell->varset.varset));
+ new = sylvan_or(new, sylvan_relnext(new, rls->relu->bdd, rls->relu->varset.varset));
+ new = sylvan_or(new, sylvan_relnext(new, rls->relr->bdd, rls->relr->varset.varset));
+ new = sylvan_or(new, sylvan_relnext(new, rls->reld->bdd, rls->reld->varset.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",