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 BDD encode_screen(sokoban_screen *screen)
  22 {
  23         int num_tiles;
  24         num_tiles = HASH_COUNT(screen);
  25         printf("Number of tiles: %d\n", num_tiles);
  26         return sylvan_true;
  27 }
  28
  29 BDD encode_rel(sokoban_screen *screen)
  30 {
  31         int num_tiles;
  32         num_tiles = HASH_COUNT(screen);
  33         printf("Number of tiles: %d\n", num_tiles);
  34         return sylvan_true;
  35 }
  36
  37 void test()
  38 {
  39
  40         printf("Test!\n");
  41         BDD a = sylvan_true;
  42         BDD b = sylvan_not(a);
  43         if (b == sylvan_false){
  44                 printf("BDD works!\n");
  45         } else {
  46                 printf("BDD does not work!\n");
  47         }
  48         LACE_ME;
  49         BDD c = sylvan_ithvar(1);
  50         if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
  51         if (sylvan_var(c) == 1) printf("Var works 2\n");
  52 }