#include <stdbool.h>
#include <ctype.h>
#include <time.h>
+#include <unistd.h>
#include <sylvan.h>
-#include "mc.h"
#include "sokoban.h"
-#include "uthash.h"
+#include "coord.h"
+#include "object.h"
+
+#define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
+#define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
+
+typedef enum {OBJECT, COORD, HYBRID} strategy;
//Global variables
bool DEBUG = false;
void usage(char *prg)
{
- fprintf(stderr,
- "Usage:\n"
+ ERRPRINT("Usage:\n"
"\t%s [opts] [FILE [FILE [...]]]\n"
"\n"
"Options:\n"
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_free(screen);
- //parse_screen(inputstream);
+ //sokoban_print(screen);
time_end_read = clock();
time_start_encode = clock();
- switch(strat){
- case COORD:
- if(DEBUG) fprintf(stderr, "Encoding coordinate based\n");
- break;
- case OBJECT:
- if(DEBUG) fprintf(stderr, "Encoding object based\n");
- break;
- case HYBRID:
- if(DEBUG) fprintf(stderr, "Encoding hybrid based\n");
- break;
- default:
- fprintf(stderr, "Huh?");
- exit(2);
- }
+
+ 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);
+ 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();
- // Future: SMC
- fprintf(stderr, "Reading: %fs\n",
+ //SOLVE???
+
+ sokoban_free(screen);
+ ERRPRINT("Reading: %fs\n",
((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
- fprintf(stderr, "Encoding: %fs\n",
+ ERRPRINT("Encoding: %fs\n",
((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
}
switch(optchar){
case 'c':
strat = COORD;
- if(DEBUG) fprintf(stderr, "Strategy changed to Coordinate based\n");
+ DPRINT("Strategy changed to Coordinate based\n");
break;
case 'd':
DEBUG = true;
- if(DEBUG) fprintf(stderr, "Debug enabled\n");
+ DPRINT("Debug enabled\n");
break;
case 'h':
usage(argv[0]);
return 0;
case 'o':
strat = OBJECT;
- if(DEBUG) fprintf(stderr, "Strategy changed to Object based\n");
+ DPRINT("Strategy changed to Object based\n");
break;
case 'y':
strat = HYBRID;
- if(DEBUG) fprintf(stderr, "Strategy changed to Hybrid\n");
+ DPRINT("Strategy changed to Hybrid\n");
break;
case '?':
if(isprint(optopt)){
- fprintf(stderr, "Unknown option `-%c'.\n", optopt);
+ ERRPRINT("Unknown option `-%c'.\n", optopt);
} else {
- fprintf(stderr, "Unknown option char `-\\x%x'.\n", optopt);
+ ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
}
return 2;
default:
}
if(optind == argc){
- fprintf(stderr, "You have not specified a file, reading from stdin\n");
+ ERRPRINT("You have not specified a file, reading from stdin\n");
solve(stdin);
}
for(int filepathindex = optind; filepathindex < argc; filepathindex++){
char *currentfilepath = argv[filepathindex];
- fprintf(stderr, "Processing: %s\n", currentfilepath);
+ ERRPRINT("Processing: %s\n", currentfilepath);
FILE *currentfile = fopen(currentfilepath, "r");
- if(DEBUG) fprintf(stderr, "Opening file\n");
+ DPRINT("Opening file\n");
solve(currentfile);
- if(DEBUG) fprintf(stderr, "Closing file\n");
+ DPRINT("Closing file\n");
fclose(currentfile);
}
return 0;
repositories / mc1516pa.git / blobdiff