zdd.h

   1 #include <stdint.h>
   2 #include <gmp.h>
   3
   4 // Usage:
   5 // 1. Call zdd_init() first.
   6 // 2. Call zdd_set_vmax() with the number of variables (number of elements).
   7 //    Following Knuth, the variables are 1-indexed.
   8 // 3. Construct ZDDs by using functions such as zdd_contains_exactly_1, or
   9 //    manually with the getters and setters. If done manually, call zdd_push()
  10 //    between trees.
  11 // 4. Call zdd_intersection() to take the last two trees off the stack and
  12 //    replace them with their intersection.
  13 // 5. Now it depends on the application. For a puzzle solver, there is
  14 //    typically a unique solution which can be read by traversing the HI edges:
  15 //      for(i = zdd_root; i != 1; i = zdd_hi(i)) {
  16 //        printf("%d\n", zdd_v(i));
  17 //      }
  18 //    Or compute statistics on the family of sets with zdd_count() and friends.
  19
  20 void zdd_init();
  21 void zdd_check();
  22 uint16_t zdd_vmax();
  23 uint16_t zdd_set_vmax(int i);
  24 // Call before computing a new ZDD on the stack.
  25 void zdd_push();
  26 void zdd_pop();
  27 // Print all nodes.
  28 void zdd_dump();
  29 // Getters and setters.
  30 uint32_t zdd_v(uint32_t n);
  31 uint32_t zdd_lo(uint32_t n);
  32 uint32_t zdd_hi(uint32_t n);
  33 uint32_t zdd_root();
  34 uint32_t zdd_set_hi(uint32_t n, uint32_t hi);
  35 uint32_t zdd_set_lo(uint32_t n, uint32_t lo);
  36 uint32_t zdd_set_hilo(uint32_t n, uint32_t hilo);
  37 uint32_t zdd_set_root(uint32_t root);
  38 uint32_t zdd_add_node(uint32_t v, int offlo, int offhi);
  39 uint32_t zdd_abs_node(uint32_t v, uint32_t lo, uint32_t hi);
  40 uint32_t zdd_last_node();
  41 uint32_t zdd_next_node();
  42 // Count number of sets in ZDD.
  43 void zdd_count(mpz_ptr);
  44 // Count number of sets in ZDD, as well as sum of sizes of all sets.
  45 // (The 0- and 1- power sums.)
  46 void zdd_count_1(mpz_ptr z0, mpz_ptr z1);
  47 // Count number of sets in ZDD, the sum of sizes of all sets, and the sum
  48 // of their squares. (The 0-, 1- and 2- power sums.)
  49 void zdd_count_2(mpz_ptr z0, mpz_ptr z1, mpz_ptr z2);
  50 // Returns number of nodes.
  51 uint32_t zdd_size();
  52
  53 // Need to have set vmax to call these:
  54
  55 // Constructs ZDD of all sets.
  56 uint32_t zdd_powerset();
  57
  58 // Runs callback on every set in ZDD.
  59 void zdd_forall(void (*fn)(int *, int));
  60
  61 // Runs callback on largest set in ZDD. If there are several candidates,
  62 // runs on lexicographically smallest.
  63 void zdd_forlargest(void (*fn)(int *, int));
  64
  65 // Construct ZDD of sets containing exactly 1 of the elements in the given list.
  66 void zdd_contains_exactly_1(const int *a, int count);
  67
  68 // Construct ZDD of sets containing at most 1 of the elements in the given
  69 // list.
  70 void zdd_contains_at_most_1(const int *a, int count);
  71
  72 // Construct ZDD of sets containing at least 1 of the elements in the given
  73 // list.
  74 void zdd_contains_at_least_1(const int *a, int count);
  75
  76 // Construct ZDD of sets not containing any elements from the given list.
  77 void zdd_contains_0(const int *a, int count);
  78
  79 // Construct ZDD of sets containing exactly n of the elements in the
  80 // given list.
  81 void zdd_contains_exactly_n(int n, const int *a, int count);
  82
  83 // Replace top two ZDDs on the stack with their intersection.
  84 uint32_t zdd_intersection();