#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);
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);
-
+ //sokoban_print(screen);
time_end_read = clock();
+
time_start_encode = clock();
lace_init(0, 1000000);
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);
+ 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;
+ }
+ }
+ }
+ 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",