Basic Usage

Table of Contents

• Creating BDDs
  • Constants
  • Variables
• Combining BDDs
  • Negation
  • Binary Operators
  • If-Then-Else Operator
  • Restricting Variables
  • Quantification
• Satisfying Assignments
• Predicates
  • Boolean Constants
  • Single Variables
  • Cubes
  • Equality
• BDD Information
  • Counting Operations
  • Support
  • Graphical Output

To play around with the examples below, please take a look at examples/basic.cpp.

Creating BDDs

Constants

The Boolean constants true and false can be obtained directly with the adiar::bdd_true and adiar::bdd_false functions.

  adiar::bdd top = adiar::bdd_true();

Alternatively, boolean constants can also be created directly from a value of type bool.

  adiar::bdd bot = false;

Variables

For a single variable, e.g. x_i, parse the label i to adiar::bdd_ithvar.

  adiar::bdd x0 = adiar::bdd_ithvar(0);

  adiar::bdd x1 = adiar::bdd_ithvar(1);

  adiar::bdd x2 = adiar::bdd_ithvar(2);

For the negation of a single variable, use adiar::bdd_nithvar

Combining BDDs

Negation

Use adiar::bdd_not or the ~ operator. For example, res below is equivalent to adiar::bdd_nithvar of 0.

  adiar::bdd _ = adiar::bdd_not(x0);

  adiar::bdd _ = x0;

Binary Operators

Use adiar::bdd_apply with an adiar::bool_op.

  adiar::bdd f = adiar::bdd_apply(x0, x1, adiar::xor_op);

Alternatively, there is a specializations of adiar::bdd_apply for each adiar::bool_op and for and, or, and xor one can also use the &, |, and ^ operators.

  adiar::bdd f = adiar::bdd_xor(x0, x1);

  adiar::bdd f = x0 ^ x1;

  adiar::bdd f = bot;
  f ^= x0;
  f ^= x1;

If-Then-Else Operator

Use adiar::bdd_ite.

  adiar::bdd g = adiar::bdd_ite(x0, x1, x2);

In other BDD packages, this function is good for manually constructing a BDD bottom-up. But, here you should use adiar::bdd_builder instead (see Manual Construction).

Restricting Variables

Use adiar::bdd_restrict. For example, res below is equivalent to ~x1.

  int i = 1;
  adiar::bdd _ = adiar::bdd_restrict(f, i, true); // ~x0

Specifically to restrict the top variable, you can use adiar::bdd_low and adiar::bdd_high.

See also the Function Objects tutorial for better ways to use this operation.

Quantification

Use adiar::bdd_exists and adiar::bdd_forall. For example, res below is equivalent to adiar::bdd_true().

  int i = 1;
  adiar::bdd _ = adiar::bdd_exists(f, i); // true

See also the Function Objects tutorial for better ways to use these operations.

Satisfying Assignments

To get the number of satisfying assignments, use adiar::bdd_satcount. Its second (optional) argument is the total number of variables (including the possibly suppressed ones in the BDD).

  size_t varcount = 3;
  size_t _ = adiar::bdd_satcount(f, varcount); // 4

To get a cube of the lexicographical minimal or maximal assignment, use adiar::bdd_satmin and adiar::bdd_satmax respectively.

  adiar::bdd f_min = adiar::bdd_satmin(f); // ~i & j

  adiar::bdd f_max = adiar::bdd_satmax(f); // i & ~j

Predicates

Boolean Constants

Use adiar::bdd_isconst to check whether a BDD is a constant Boolean value.

  bool _ = adiar::bdd_isconst(top); // true

  bool _ = adiar::bdd_isconst(bot); // true

  bool _ = adiar::bdd_isconst(x0); // false

Use adiar::bdd_istrue and adiar::bdd_isfalse to check for it being specifically \(\top\) or \(\bot\), respectively.

Single Variables

Use adiar::bdd_isvar check whether a BDD represents a formula of exactly one variable, i.e. a literal.

  bool _ = adiar::bdd_isvar(top); // false

  bool _ = adiar::bdd_isvar(x0); // true

  bool _ = adiar::bdd_isvar(~x0); // true

Use adiar::bdd_isithvar, and adiar::bdd_isnithvar to check whether a BDD represents a formula of a positive or negative variable, respectively.

Cubes

To check whether a BDD represents a cube, i.e. where all the variables in its support have a fixed value, use adiar::bdd_iscube.

  bool _ = adiar::bdd_iscube(f); // false

  bool _ = adiar::bdd_iscube(f_min); // true

Equality

Use adiar::bdd_equal and adiar::bdd_unequal or the == and != operators.

  bool _ = adiar::bdd_equal(f, g); // false

  bool _ = f == (x1 ^ x0); // true

BDD Information

Counting Operations

Use adiar::bdd_nodecount to get the number of BDD nodes.

  size_t _ = adiar::bdd_nodecount(f); // 3

Use adiar::bdd_varcount to get the number of variables present in the BDD.

  size_t _ = adiar::bdd_varcount(f); // 2

Use adiar::bdd_pathcount to get the number of paths to true.

  size_t _ = adiar::bdd_pathcount(f); // 2

Support

The top (smallest) variable present in the BDD can be obtained with adiar::bdd_topvar (adiar::bdd_minvar).

  size_t _ = adiar::bdd_topvar(f); // 0

On the other hand, the last variable present in the BDD can be obtained with adiar::bdd_maxvar.

  size_t _ = adiar::bdd_maxvar(f); // 1

Graphical Output

The BDD can be exported to the DOT format with adiar::bdd_printdot. The second argument can either be an output stream, e.g. std::cout, or a filename.

  adiar::bdd_printdot(f, "./f.dot");