zdd.h

   1 #include <stdint.h>
   2 #include <gmp.h>
   3
   4 void zdd_init();
   5 void zdd_check();
   6 uint16_t zdd_vmax();
   7 uint16_t zdd_set_vmax(int i);
   8 // Call before computing a new ZDD on the stack.
   9 void zdd_push();
  10 void zdd_pop();
  11 // Print all nodes.
  12 void zdd_dump();
  13 // Getters and setters.
  14 uint32_t zdd_v(uint32_t n);
  15 uint32_t zdd_lo(uint32_t n);
  16 uint32_t zdd_hi(uint32_t n);
  17 uint32_t zdd_root();
  18 uint32_t zdd_set_hi(uint32_t n, uint32_t hi);
  19 uint32_t zdd_set_lo(uint32_t n, uint32_t lo);
  20 uint32_t zdd_set_hilo(uint32_t n, uint32_t hilo);
  21 uint32_t zdd_set_root(uint32_t root);
  22 uint32_t zdd_add_node(uint32_t v, int offlo, int offhi);
  23 uint32_t zdd_abs_node(uint32_t v, uint32_t lo, uint32_t hi);
  24 uint32_t zdd_last_node();
  25 uint32_t zdd_next_node();
  26 void zdd_count(mpz_ptr);
  27 // Returns number of nodes.
  28 uint32_t zdd_size();
  29
  30 // Need to have set vmax to call these:
  31
  32 // Constructs ZDD of all sets.
  33 uint32_t zdd_powerset();
  34
  35 // Runs callback on every set in ZDD.
  36 void zdd_forall(void (*fn)(int *, int));
  37
  38 // Runs callback on largest set in ZDD. If there are several candidates,
  39 // runs on lexicographically smallest.
  40 void zdd_forlargest(void (*fn)(int *, int));
  41
  42 // Construct ZDD of sets containing exactly 1 of the elements in the given list.
  43 void zdd_contains_exactly_1(const int *a, int count);
  44
  45 // Construct ZDD of sets containing at most 1 of the elements in the given
  46 // list.
  47 void zdd_contains_at_most_1(const int *a, int count);
  48
  49 // Construct ZDD of sets containing at least 1 of the elements in the given
  50 // list.
  51 void zdd_contains_at_least_1(const int *a, int count);
  52
  53 // Construct ZDD of sets not containing any elements from the given list.
  54 void zdd_contains_0(const int *a, int count);
  55
  56 // Construct ZDD of sets containing exactly n of the elements in the
  57 // given list.
  58 void zdd_contains_exactly_n(int n, const int *a, int count);
  59
  60 // Replace top two ZDDs on the stack with their intersection.
  61 uint32_t zdd_intersection();