// This program is an example of the use of binary decision diagrams (BDD's).
// Since BDD's implement the BooleanAlgebra interface, all the boolean algebra
// operators ("&", "|", "^", "~", and "mux") can be used on BDD's.
import jazz.circuit.*;
import jazz.circuit.bdd.*;

// Function defined over any boolean algebra.
fun fbool(u, v, w) = (~u | v) & (v ^ w);

// Create three BDD variables "x", "y", and "z" such that "x < y < z".
var vars = Bdd.newVars(3)(["x", "y", "z"]);
var x = vars[0];
var y = vars[1];
var z = vars[2];

// Build the BDD that computes "fbool" by giving the three BDD variables as
// argument to "fbool" (this is legal since "fbool" is defined for any boolean
// algebra and BDD's implement the BooleanAlgebra interface).
var bdd = fbool(x, y, z);

// Display the BDD as a canonical set of Jazz equations (the "%a" format calls
// the "toString()" method of the BDD).
@ print("bdd(%a, %a, %a) = %a\n\n", x, y, z, bdd);

// Build a function "bdd2fun" that can be used to build a function that
// computes the BDD for x, y, and z over any particular boolean algebra given
// the "zero" and "one" constants of the algebra.
fun bdd2fun(zero, one)(x, y, z) =
  Bdd.toFunction(3)(vars)(1)([bdd])(zero, one)([x, y, z])[0];

// Build the function that computes the bdd for booleans (since zero=false,
// and one=true for this boolean algebra)
var fbool' = bdd2fun(false, true);

// Check that "fbool" and "fbool'" compute the same function over booleans
{
  var bools = [false, true];
  
  for (i < 2) {
    for (j < 2) {
      for (k < 2) {
        var u = bools[i];
        var v = bools[j];
        var w = bools[k];
        var fb = fbool(u, v, w);
        var fb' = fbool'(u, v, w);
        
        assert(fb == fb');
        @ print("fbool'(%a, %a, %a) = %a\n", u, v, w, fb);
      }
    }
  }
}

// Check that "fper" computes the same thing as "fbool" for a few sets of
// three periodic numbers chosen at random.
{
  // Build the function that computes the BDD for periodics (since zero=#(0),
  // and one=#(1) for this boolean algebra).
  var fper = bdd2fun(#(0), #(1));
  
  // Returns a random periodic number.
  fun random() = (per) (Integer.random(25) / (1 + 2 * Integer.random(35)));
  
  @ print("\n");
  for (i < 5) {
    var u = random();
    var v = random();
    var w = random();
    var fb = fbool(u, v, w);
    var fp = fper(u, v, w);
  
    assert(fb == fp);
    @ print("fper(%a, %a, %a) = %a\n", u, v, w, fb);
  }
}

// Create a new bdd from "fbool'", which is essentially the restriction of
// "fbool" to booleans (since "fbool" was defined over any boolean algebra),
// and thus implements the truth table of "fbool".
var bdd' = Bdd.fromFunction(3)(vars)(f)
{
  fun f(v) = fbool'(v[0], v[1], v[2]);
}

// Formally check that the two BDD's are indeed equal (that is to say, that
// they compute the same function).
assert(bdd == bdd');
@ print("\n(bdd == bdd')\n\n");

// Create a device computing the BDD over nets.
device Test {
  input in1: Net;
  input in2: Net;
  input in3: Net;
  
  output out: Net;

  var zero = Net.constant(#(0));
  var one = Net.constant(#(1));
  
  out = bdd2fun(zero, one)(in1, in2, in3);
}

export Test();