modelchecker/coord.c

   1 #include <argp.h>
   2 #include <inttypes.h>
   3 #include <locale.h>
   4 #include <stdio.h>
   5 #include <stdlib.h>
   6 #include <string.h>
   7 #include <sys/time.h>
   8
   9 #ifdef HAVE_PROFILER
  10 #include <gperftools/profiler.h>
  11 #endif
  12
  13 #include <sylvan.h>
  14 #include <llmsset.h>
  15 #include <lace.h>
  16
  17 #include "coord.h"
  18 #include "sokoban.h"
  19
  20
  21 /*
  22  * Each coordinate has three related boolean variables. The combination of those boolean variables
  23  * defines tiles:
  24  * 000: Wall
  25  * 001: Free
  26  * 010: Box
  27  * 100: Box on target
  28  * 011: Target
  29  * 101: Agent
  30  * 110: Agent on target
  31  * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
  32  * tiles in the shrinked screen.
  33  */
  34
  35 BDD encode_screen(sokoban_screen *screen)
  36 {
  37         int num_tiles;
  38         num_tiles = HASH_COUNT(screen);
  39         printf("Number of tiles: %d\n", num_tiles);
  40         return sylvan_true;
  41 }
  42
  43 BDD encode_rel(sokoban_screen *screen)
  44 {
  45         int num_tiles;
  46         num_tiles = HASH_COUNT(screen);
  47         printf("Number of tiles: %d\n", num_tiles);
  48         return sylvan_true;
  49 }
  50
  51 void test()
  52 {
  53
  54         printf("Test!\n");
  55         BDD a = sylvan_true;
  56         BDD b = sylvan_not(a);
  57         if (b == sylvan_false){
  58                 printf("BDD works!\n");
  59         } else {
  60                 printf("BDD does not work!\n");
  61         }
  62         LACE_ME;
  63         BDD c = sylvan_ithvar(1);
  64         if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
  65         if (sylvan_var(c) == 1) printf("Var works 2\n");
  66 }