Working with Multi-Terminal BDDs (MTBDDs)

Three functions are provided to work with terminals:

Note that bddtrue and bddfalse are not terminals. They are the traditional BDD constants and bdd_is_terminal() returns 0 for them.

#include <iostream>
#include "bddx.h"

void example()
{
  bdd a = bdd_ithvar(0);  // variable a
  bdd b = bdd_ithvar(1);  // variable b

  // Create terminals with values 0, 1, 2, 3
  bdd t0 = bdd_terminal(0);
  bdd t1 = bdd_terminal(1);
  bdd t2 = bdd_terminal(2);
  bdd t3 = bdd_terminal(3);

  // Build an MTBDD.  bdd_ite() is safe to use if it follows the shape
  // of the MTBDD that we want to construct: in this case, the terminals
  // will not need to be combined.
  bdd mtbdd = bdd_ite(a,
                      bdd_ite(b, t1, t2),
                      bdd_ite(b, t3, t0));

  // Check terminal properties
  std::cout << "mtbdd: " << mtbdd << '\n';
  std::cout << "t3 is a terminal: " << bdd_is_terminal(t3) << '\n';
  std::cout << "t3 value: " << bdd_get_terminal(t3) << '\n';
  std::cout << "bddtrue is not a terminal: " << bdd_is_terminal(bddtrue) << '\n';
}

int main()
{
  bdd_init(1000, 100);
  bdd_setvarnum(2);
  example();
  bdd_done();
  return 0;
}

mtbdd: <0:0, 1:0, Terminal(0)><0:0, 1:1, Terminal(3)><0:1, 1:0, Terminal(2)><0:1, 1:1, Terminal(1)>
t3 is a terminal: 1
t3 value: 3
bddtrue is not a terminal: 0

bdd_done() should not be called before all bdd have been destroyed, this is why we run our examples from a function separate from main(). In what follows, we will only show the contents of this function, and assume the same main().

Here is another example that shows that we can build an MTBDD that mixes terminals with bddfalse and bddtrue, and that uses bdd_printdot to obtain a GraphViz description that we can render graphically:

bdd a = bdd_ithvar(0);
bdd b = bdd_ithvar(1);
bdd l0 = bddfalse;
bdd l1 = bddtrue;
bdd l2 = bdd_terminal(2);
bdd l3 = bdd_terminal(3);
bdd mtbdd = bdd_ite(a,
                    bdd_ite(b, l1, l2),
                    bdd_ite(b, l3, l0));
bdd_printdot(mtbdd);

This representation uses gray squares for constants, gray pentagons for terminals, and ellipses for internal nodes. The numbers in parentheses are the BDD node numbers (for the constants 0 and 1, the node numbers are not repeated because they are 0 and 1 too). The numbers displayed before the parentheses are the variable numbers (for internal nodes) or the terminal value (for terminals).

The bddExtCache structure holds the cache. The third argument to bdd_extcache_init (erase_on_gc) specifies whether the cache should be automatically cleared during garbage collection. Set this to 1 (true) by default. Only set this to 0 (false) if you are sure that the cache cannot be used to reference nodes that might be garbage collected.

If the n argument to bdd_extcache_init is negative, it is interpreted as a ratio: the cache size will be bddnodesize / (-n). If n is 0, it defaults to the same size as the standard BDD caches allocated by BuDDy.

Each cache entry contains four integers usually interpreted as (left,right,op,res): given MTBDDs left and right, the result of operation op is res. Functions that implement MTBDD operations will usually take op as an argument. If the callback implementing the operation is using some global data to perform its computation, you may want to update op each time the global data is changing.

BDD bdd_mt_apply2(bdd l, bdd r,
                  int (*termop)(int, int),
                  bddExtCache* cache, int ophash,
                  int applyop_shortcut);

This function applies a binary operation to two MTBDDs. The termop callback receives the integer values of two terminals and returns the integer value of the result terminal.

Parameters:

• l, r: The two input MTBDDs
• termop: Callback function int f(int left_val, int right_val)
• cache: External cache for memoization
• ophash: Unique identifier for this operation (for cache keying)
• applyop_shortcut: If ≥0, use BDD shortcuts (e.g., bddop_and)

Without shortcuts, the operation will perform a recursive traversal of l and r until it reaches two terminals to combine with termop. MTBDD should not contain bddtrue or bddfalse in this case.

If applyop_shortcut is set to an operation like bddop_and or bddop_or that knows how to deal with both constants (bddtrue and bddfalse), then the MTBDD may use those constants. The recursion will terminate earlier each time one side is a constant. In that case the result is computed using the semantics of the operation passed to applyop_shortcut.

bdd bdd_mt_apply2_leaves(bdd l, bdd r,
                         int (*termop)(int l_bdd, int l_val,
                                       int r_bdd, int r_val),
                         bddExtCache* cache, int ophash,
                         int applyop_shortcut);

Similar to bdd_mt_apply2, but the callback receives both the BDD node number and the terminal value. This allows distinguishing between bddtrue=/=bddfalse (they have BDD number 1 and 0 respectively) and actual terminals.

You should use this variant when the MTBDD mixes terminals and constants, and when applyop_shortcut will not always be able to remove all constants. For instance, if applyop_shortcut is set to work like an implication (bddop_imp), only the following short-cuts are used: \(\top \rightarrow b = b\), \(\bot \rightarrow b = \top\), \(b \rightarrow b = \top\), \(b \rightarrow \top = \top\). What isn't implemented is a reduction for \(b \rightarrow \bot\) because how to complement \(b\) actually depends on the semantics of the terminals it contains.

This example uses paths_mt_of(), described later, to iterate over all the paths in the MTBDDs.

bdd a = bdd_ithvar(0);
bdd b = bdd_ithvar(1);
bdd t1 = bdd_terminal(1);
bdd t2 = bdd_terminal(2);
bdd t3 = bdd_terminal(3);

bdd x = bdd_ite(a, t1, t2);
bdd y = bdd_ite(a, t3, bdd_ite(b, t1, t3));

std::cout << "MTBDD for x:\n";
for (auto [path, term]: paths_mt_of(x))
  std::cout << "  " << path << " -> " << bdd_get_terminal(term) << '\n';

std::cout << "MTBDD for y:\n";
for (auto [path, term]: paths_mt_of(y))
  std::cout << "  " << path << " -> " << bdd_get_terminal(term) << '\n';

bddExtCache cache;
bdd_extcache_init(&cache, 100, true);

// Add terminal values
bdd sum = bdd_mt_apply2(x, y,
                        [](int a, int b) { return a + b; },
                        &cache, 1, -1);

std::cout << "MTBDD for sum:\n";
for (auto [path, term]: paths_mt_of(sum))
  std::cout << "  " << path << " -> " << bdd_get_terminal(term) << '\n';

bdd_extcache_done(&cache);

MTBDD for x:
  <0:0> -> 2
  <0:1> -> 1
MTBDD for y:
  <0:0, 1:0> -> 3
  <0:0, 1:1> -> 1
  <0:1> -> 3
MTBDD for sum:
  <0:0, 1:0> -> 5
  <0:0, 1:1> -> 3
  <0:1> -> 4

bdd bdd_mt_apply1(bdd r, int (*termop)(int),
                  bdd replace_false, bdd replace_true,
                  bddExtCache* cache, int ophash);

Apply a unary operation to all terminals of an MTBDD. The termop callback receives a terminal value and returns the new terminal value.

Parameters:

• r: Input MTBDD
• termop: Callback function int f(int val)
• replace_false: BDD to substitute for bddfalse leaves
• replace_true: BDD to substitute for bddtrue leaves
• cache: External cache
• ophash: Unique operation identifier

bdd bdd_mt_apply1_leaves(bdd r, int (*termop)(int bdd, int val),
                         bddExtCache* cache, int ophash);

Similar to bdd_mt_apply1, but the callback receives both the BDD node number and the terminal value, allowing it to handle constants specially. The callback can return any BDD (not just a terminal).

bdd a = bdd_ithvar(0);
bdd t1 = bdd_terminal(1);
bdd t2 = bdd_terminal(2);
bdd x = bdd_ite(a, t1, t2);

std::cout << "before:  " << x << '\n';

bddExtCache cache;
bdd_extcache_init(&cache, 100, true);

// Increment all terminals by 10
bdd y = bdd_mt_apply1(x,
                      [](int v) { return v + 10; },
                      bddfalse, bddtrue,
                      &cache, 1);

bdd_extcache_done(&cache);

std::cout << "after:  " << y << '\n';

before:  <0:0, Terminal(2)><0:1, Terminal(1)>
after:  <0:0, Terminal(12)><0:1, Terminal(11)>

void bdd_mt_quantify_prepare(bdd varset);
void bdd_mt_quantify_prepare(bdd output_vars, bdd quant_vars);
void bdd_mt_quantify_prepare(bdd output_vars, bdd quant1_vars, bdd quant2_vars);

The one-argument version prepares for quantification by specifying which variables should be quantified.

The two-argument overload also marks quant_vars as variables to be quantified, but it additionally marks output_vars as a set of output variables. This is typically used for synthesis with partial observation: in this context quant_vars are input variables that will be universally quantified, but the game solving algorithm also needs to distinguish output variables from input variables, even if they are not quantified in the MTBDD.

The three-argument overload is used with bdd_mt_quantify2 to allow two types of quantifications to be performed in the same pass over the MTBDD. Variables in quant1_vars will be quantified using a first type of quantification, variables in quant2_vars will use a second type. Those quantifications will be performed bottom-up following variable order. Again, output_vars is not used for quantification, but it is used to distinguish output variables from input variables during synthesis.

int bdd_mt_quantify_to_bool(bdd r, int (*termop)(int),
                            bddExtCache* cache, int ophash);

Quantify all variables in r and return a Boolean result (0 or 1). The termop callback evaluates each terminal to 0 or 1.

The variables passed to any argument of bdd_mt_quantify_prepare are considered as existential variables, so their quantification will be the OR of their children. Other variables will be quantified universally, so their quantification will be the AND of their children.

In this example, the MTBDD encodes a game between two players a and b (two BDD variables). Each path leads to an integer terminal. The question is: regardless of the choice made by player a, can player b make a choice that reaches an odd number?

This is expressed as \(\forall a, \exists b, \mathrm{odd}(\mathit{game}(a,b))\): player a is universal, player b is existential.

bdd a = bdd_ithvar(0);  // player a (universal)
bdd b = bdd_ithvar(1);  // player b (existential)

// Game outcomes:
//   a=0, b=0 -> 4 (even)
//   a=0, b=1 -> 7 (odd)
//   a=1, b=0 -> 3 (odd)
//   a=1, b=1 -> 2 (even)
bdd game = bdd_ite(a,
                   bdd_ite(b, bdd_terminal(2), bdd_terminal(3)),
                   bdd_ite(b, bdd_terminal(7), bdd_terminal(4)));

std::cout << "Game MTBDD:\n";
for (auto [path, term]: paths_mt_of(game))
  std::cout << "  " << path << " -> " << bdd_get_terminal(term)
            << (bdd_get_terminal(term) % 2 ? " (odd)" : " (even)") << '\n';

bddExtCache cache;
bdd_extcache_init(&cache, 100, true);

// Player b is existential, player a is universal
bdd_mt_quantify_prepare(b);

// termop returns 1 if terminal is odd, 0 otherwise
int result = bdd_mt_quantify_to_bool(game,
                                     [](int v) { return v & 1; },
                                     &cache, 1);

std::cout << "\nQuestion: forall a, exists b, odd(game(a,b))?\n";
std::cout << "Answer: " << (result ? "YES" : "NO") << '\n';

// Let's swap the roles of the players
bdd_mt_quantify_prepare(a);

result = bdd_mt_quantify_to_bool(game,
                                 [](int v) { return v & 1; },
                                 &cache, 2);

std::cout << "\nQuestion: exists a, forall b, odd(game(a,b))?\n";
std::cout << "Answer: " << (result ? "YES" : "NO") << '\n';

bdd_extcache_done(&cache);

Game MTBDD:
  <0:0, 1:0> -> 4 (even)
  <0:0, 1:1> -> 7 (odd)
  <0:1, 1:0> -> 3 (odd)
  <0:1, 1:1> -> 2 (even)

Question: forall a, exists b, odd(game(a,b))?
Answer: YES

Question: exists a, forall b, odd(game(a,b))?
Answer: NO

The nature of the quantifiers is indicated by bdd_mt_quantify_prepare, but their order is the order of the BDD variables.

int bdd_mt_quantify_to_trival(bdd r, int (*termop)(int),
                              bddExtCache* cache, int ophash,
                              int iteration);

Like bdd_mt_quantify_to_bool, but termop returns one of three values:

• 0: false
• 2: unknown
• 3: true

The iteration parameter is used for cache management: "unknown" results are only reused within the same iteration. This function is typically used to compute attractors in two-player games, where false and true are stable values that indicate that the vertex is in the attractor of player 0 or 1, and "unknown" values will be changed after some iterations.

bdd bdd_mt_quantify(bdd r,
                    int (*termop)(int),
                    int (*leavesop)(int, int, int, int),
                    bddExtCache* cache, int quanthash,
                    int applyhash, int applyop);

Quantify variables in r and return the resulting BDD. Call bdd_mt_quantify_prepare first to specify which variables should be quantified. If the two-argument version of bdd_mt_quantify_prepare is used, only the second argument is used.

Parameters:

• r: Input MTBDD
• termop: Callback applied to each terminal, allowing optional renaming. Receives a terminal value and returns the (possibly new) terminal value.
• leavesop: Callback passed to bdd_mt_apply2_leaves for combining the low and high children at quantified variables (use a conjunction to implement universal quantification, a disjunction to implement existential quantification, or xor to implement unique quantification).
• cache: External cache for memoization
• quanthash: Unique identifier for the quantification operation (for cache keying)
• applyhash: Unique identifier for the apply operation (for cache keying)
• applyop: If ≥0, use BDD shortcuts (e.g., bddop_or for existential quantification)

Unlike bdd_mt_quantify_to_bool which returns an integer result after quantifying all variables, this function returns a BDD. When used with the two-argument version of bdd_mt_quantify_prepare, only the variables in quant_vars are quantified away; the output_vars are preserved as existential variables in game-solving contexts.

In this example, we interpret the 32-bit terminal values as bit sets. Using quantification with OR computes unions, while quantification with AND computes intersections.

bdd a = bdd_ithvar(0);
bdd b = bdd_ithvar(1);

bdd x = bdd_ite(a,
                bdd_ite(b, bdd_terminal(0b0011), bdd_terminal(0b0101)),
                bdd_ite(b, bdd_terminal(0b1001), bdd_terminal(0b1100)));

std::cout << "MTBDD x (bit sets):\n";
for (auto [path, term]: paths_mt_of(x))
  std::cout << "  " << path << " -> 0b"
            << std::bitset<4>(bdd_get_terminal(term)) << '\n';

bddExtCache cache;
bdd_extcache_init(&cache, 100, true);

// leavesop for combining terminals: these receive bdd numbers and
// values, but in this example the MTBDD does not contain bddtrue or
// bddfalse, so we do not need the bdd numbers.
auto combine_or = [](int, int lval, int, int rval) {
  return bdd_terminal_as_int(lval | rval);
};
auto combine_and = [](int, int lval, int, int rval) {
  return bdd_terminal_as_int(lval & rval);
};
auto combine_xor = [](int, int lval, int, int rval) {
  return bdd_terminal_as_int(lval ^ rval);
};
// We won't change the leaves.
auto term_id = [](int v) { return v; };

// Quantify variable 'b', building the union of its leaves
bdd_mt_quantify_prepare(b);
bdd union_b = bdd_mt_quantify(x, term_id, combine_or,
                              &cache, 1, 2, bddop_or);

std::cout << "\nAfter existential quantification of b (union):\n";
for (auto [path, term]: paths_mt_of(union_b))
  std::cout << "  " << path << " -> 0b"
            << std::bitset<4>(bdd_get_terminal(term)) << '\n';

// Quantify variable 'b' building the intersection of its leaves
bdd_mt_quantify_prepare(b);
bdd inter_b = bdd_mt_quantify(x, term_id, combine_and,
                              &cache, 3, 4, bddop_and);

std::cout << "\nAfter universal quantification of b (intersection):\n";
for (auto [path, term]: paths_mt_of(inter_b))
  std::cout << "  " << path << " -> 0b"
            << std::bitset<4>(bdd_get_terminal(term)) << '\n';

// Quantify variable 'b' building the xor of its leaves
bdd_mt_quantify_prepare(b);
bdd xor_b = bdd_mt_quantify(x, term_id, combine_xor,
                              &cache, 5, 6, bddop_xor);

std::cout << "\nAfter unique quantification of b (xor):\n";
for (auto [path, term]: paths_mt_of(xor_b))
  std::cout << "  " << path << " -> 0b"
            << std::bitset<4>(bdd_get_terminal(term)) << '\n';

bdd_extcache_done(&cache);

MTBDD x (bit sets):
  <0:0, 1:0> -> 0b1100
  <0:0, 1:1> -> 0b1001
  <0:1, 1:0> -> 0b0101
  <0:1, 1:1> -> 0b0011

After existential quantification of b (union):
  <0:0> -> 0b1101
  <0:1> -> 0b0111

After universal quantification of b (intersection):
  <0:0> -> 0b1000
  <0:1> -> 0b0001

After unique quantification of b (xor):
  <0:0> -> 0b0101
  <0:1> -> 0b0110

bdd bdd_mt_quantify2(bdd r,
                     int (*termop)(int),
                     int (*leavesop1)(int, int, int, int),
                     int (*leavesop2)(int, int, int, int),
                     bddExtCache* cache, int quanthash,
                     int applyhash1, int applyop1,
                     int applyhash2, int applyop2);

Like bdd_mt_quantify, but performs two different quantifications depending on the variable. Call the three-argument version of bdd_mt_quantify_prepare first to classify variables into output variables, quant1_vars, and quant2_vars. Variables in quant1_vars will be quantified using leavesop1 / applyop1, and variables in quant2_vars will use leavesop2 / applyop2.

Parameters:

• r: Input MTBDD
• termop: Callback applied to each terminal, allowing optional renaming
• leavesop1: Callback for combining children at quant1_vars variables
• leavesop2: Callback for combining children at quant2_vars variables
• cache: External cache for memoization
• quanthash: Unique identifier for the quantification (for cache keying)
• applyhash1, applyop1: Cache key and BDD shortcut for leavesop1
• applyhash2, applyop2: Cache key and BDD shortcut for leavesop2

In this example, we have three BDD variables: a (output), b (quantified existentially via OR), and c (quantified universally via AND). The terminal values are bit sets, so the existential quantification computes the union while the universal quantification computes the intersection.

We show how the ∃b∀c quantification can be done using two calls to bdd_mt_quantify(), or how it can be done with a single call to bdd_mt_quantify2().

bdd a = bdd_ithvar(0);  // output variable
bdd b = bdd_ithvar(1);  // quant1: existential (OR)
bdd c = bdd_ithvar(2);  // quant2: universal (AND)

bdd x = bdd_ite(a,
                bdd_ite(b,
                        bdd_ite(c, bdd_terminal(0b0011),
                                   bdd_terminal(0b0101)),
                        bdd_ite(c, bdd_terminal(0b1001),
                                   bdd_terminal(0b1100))),
                bdd_ite(b,
                        bdd_ite(c, bdd_terminal(0b1010),
                                   bdd_terminal(0b0110)),
                        bdd_ite(c, bdd_terminal(0b1111),
                                   bdd_terminal(0b0001))));

std::cout << "MTBDD x (bit sets):\n";
for (auto [path, term]: paths_mt_of(x))
  std::cout << "  " << path << " -> 0b"
            << std::bitset<4>(bdd_get_terminal(term)) << '\n';

bddExtCache cache;
bdd_extcache_init(&cache, 100, true);

auto combine_or = [](int, int lval, int, int rval) {
  return bdd_terminal_as_int(lval | rval);
};
auto combine_and = [](int, int lval, int, int rval) {
  return bdd_terminal_as_int(lval & rval);
};
auto term_id = [](int v) { return v; };

// First, we demonstrate quantification in two steps
std::cout << "\n-- two calls to bdd_mt_quantify()\n\n";
// Quantify c universally (AND)
bdd_mt_quantify_prepare(c);
bdd result = bdd_mt_quantify(x, term_id, combine_and,
                             &cache, 100, 1, bddop_and);
std::cout << "After ∀c:\n";
for (auto [path, term]: paths_mt_of(result))
  std::cout << "  " << path << " -> 0b"
            << std::bitset<4>(bdd_get_terminal(term)) << '\n';

// Quantify b existentially (OR)
bdd_mt_quantify_prepare(b);
result = bdd_mt_quantify(result, term_id, combine_or,
                         &cache, 101, 2, bddop_or);
std::cout << "\nAfter ∃b ∀c:\n";
for (auto [path, term]: paths_mt_of(result))
  std::cout << "  " << path << " -> 0b"
            << std::bitset<4>(bdd_get_terminal(term)) << '\n';

// Now, combine both in a single step.  (This only works
// because the quantifications are following the variable order.)
std::cout << "\n-- one call to bdd_mt_quantify2()\n\n";
// 'a' is marked as 'output', but it is simply ignored by
// bdd_mt_quantify_prepare
bdd_mt_quantify_prepare(a, b, c);
result = bdd_mt_quantify2(x, term_id,
                          combine_or, combine_and,
                          &cache, 102,
                          2, bddop_or,
                          1, bddop_and);

std::cout << "After ∃b ∀c:\n";
for (auto [path, term]: paths_mt_of(result))
  std::cout << "  " << path << " -> 0b"
            << std::bitset<4>(bdd_get_terminal(term)) << '\n';

bdd_extcache_done(&cache);

MTBDD x (bit sets):
  <0:0, 1:0, 2:0> -> 0b0001
  <0:0, 1:0, 2:1> -> 0b1111
  <0:0, 1:1, 2:0> -> 0b0110
  <0:0, 1:1, 2:1> -> 0b1010
  <0:1, 1:0, 2:0> -> 0b1100
  <0:1, 1:0, 2:1> -> 0b1001
  <0:1, 1:1, 2:0> -> 0b0101
  <0:1, 1:1, 2:1> -> 0b0011

-- two calls to bdd_mt_quantify()

After ∀c:
  <0:0, 1:0> -> 0b0001
  <0:0, 1:1> -> 0b0010
  <0:1, 1:0> -> 0b1000
  <0:1, 1:1> -> 0b0001

After ∃b ∀c:
  <0:0> -> 0b0011
  <0:1> -> 0b1001

-- one call to bdd_mt_quantify2()

After ∃b ∀c:
  <0:0> -> 0b0011
  <0:1> -> 0b1001

The quantification is bottom-up, so inner variables (c, variable 2) are processed first (AND), then outer variables (b, variable 1) are processed second (OR).

Since quant1_vars and quant2_vars can contain multiple variables that need not be adjacent, bdd_mt_quantify2() allows executing arbitrary nesting of quantifiers as long as they follow the variable order.

Also, please note how the hash keys 1, 2, 100, 101, and 102 are used in this code: the combine_and=/=apply_and operation is using hash key 1, while combine_or=/=apply_or is using hash key 2. When these operations are performed inside bdd_mt_quantify2(), they can reuse results that were cached when they were applied during previous calls to bdd_mt_quantify(). The top-level operations, i.e., the two calls to bdd_mt_quantify() and bdd_mt_quantify2() are distinct operations with different hash keys (100, 101, 102) so that they do not share their cached results.

std::tuple<bool, int, int> bdd_mt_quantified_low_high(int bdd);

For a node in an MTBDD, return whether the node's variable appears among the arguments of bdd_mt_quantify_prepare, as well as their low/high children.

In MTBDD-based synthesis, this is used to interpret the MTBDD as a game. bdd_mt_quantify_prepare's first argument is used to mark output variables. Then bdd_mt_quantified_low_high will return the type of the current node as well as its successors.

The successors can also be obtained with bdd_low() and bdd_high(), however calling functions across shared libraries is expensive. So this interface groups three results behind a single call.

int bdd_mt_apply1_synthesis(bdd& r,
                            int (*opleaf)(int* bdd, int term),
                            bddExtCache* cache, int ophash);

Perform synthesis traversal on an MTBDD. The opleaf callback is called for each terminal; it may modify the BDD node (via *bdd) and should return a Boolean indicating realizability.

Call bdd_mt_quantify_prepare first to indicate which variables are existential. When using the two-argument version of this function, only the first argument will be considered.

Returns 1 if there is a strategy for the existential player to force the MTBDD to reach a realizable terminal, regardless of the choices performed by the universal player.

The MTBDD r is modified in place to contain the winning strategy (if it exists) or just some partial simplification. A strategy is an MTBDD where each existential node has exactly one child that is bddfalse (indicating that the strategy is to take the other child).

Additionally, branches where the universal player can reach bddfalse will be simplified to bddfalse, since those branches are losing from the point of view of the existential player.

int bdd_mt_apply1_synthesis_with_choice(bdd* ptr_r,
                                        int (*choice)(int),
                                        int (*opleaf)(int* bdd, int term),
                                        bddExtCache* cache, int ophash);

Like bdd_mt_apply1_synthesis, but with an additional choice callback that selects which branch to explore at existential nodes. This allows for implementing specific strategy selection policies.

Function choice() is called on existential nodes, and should return the BDD number of the child to select.

Iterate over all paths that lead to a non-false leaf, returning pairs of (path condition, terminal).

for (auto [path, terminal]: paths_mt_of(mtbdd))
  if (terminal == bddtrue)
    std::cout << path << " -> bddtrue\n";
  else
    std::cout << path << " -> " << bdd_get_terminal(terminal) << '\n';

Like paths_mt_of, but also includes paths leading to bddfalse.

Iterate over terminals only (without computing path conditions). Useful when you only need the set of terminals. However, the terminals may be listed twice if they appear on multiple paths.

for (bdd terminal: silent_paths_mt_of(mtbdd))
  if (terminal == bddtrue)
    std::cout << "bddtrue\n";
  else
    std::cout << bdd_get_terminal(terminal) << '\n';

Collect all distinct leaves (terminals and constants) of an MTBDD, or of a vector of MTBDDs. These functions are linear in the (collective) size of the MTBDD(s), and will return each terminal only once, bddfalse included.

std::vector<bdd> leaves_of(const bdd& mtbdd);
std::vector<bdd> leaves_of(const std::vector<bdd>& mtbdds);