BTW. I’m pretty happy with the current state of the code once it has been debugged. Especially how I was finally able to express generating a Bdd from randomly selected truth table (genRandomBdd) vs generating a Bdd from the k’th truth table (genKthBdd) without having to generate a random 2^n bit integer, which may be larger than Long.MaxVal.
def clauseToBdd(clause: Clause, ident: BddTerm, op: BinaryOperation): Bdd = {
// interpreting clause as an OR so that clause is CNF rather than DNF
def conv(i: Int): Bdd = Bdd(i)
treeReduce(clause, ident: Bdd, conv, (acc: Bdd, b: Bdd) => op(acc, b))
}
def cnfClauseToBdd(cnfClause: Clause): Bdd = clauseToBdd(cnfClause, BddFalse, Or)
def dnfClauseToBdd(dnfClause: Clause): Bdd = clauseToBdd(dnfClause, BddTrue, And)
// Interpret a list of Clauses as an And of Ors where each clause is a disjunction
def cnfToBdd(cnf: TraversableOnce[Clause]): Bdd = {
treeReduce(cnf, BddTrue, cnfClauseToBdd, { (acc: Bdd, b: Bdd) => And(acc, b) })
}
// Interpret a list of Clauses as an Or of Ands where each clause is a conjunction
def dnfToBdd(dnf: TraversableOnce[Clause]): Bdd = {
treeReduce(dnf, BddFalse, dnfClauseToBdd, { (acc: Bdd, b: Bdd) => Or(acc, b) })
}
def genBddFromBitMask(n: Int, f: Int => Boolean): Bdd = {
val dnf = for {
truthTableRow <- (0 until (1 << n)).iterator
if f(truthTableRow)
} yield minTerm(n, truthTableRow)
dnfToBdd(dnf)
}
val prng = scala.util.Random
// Generate randomly selected BDD of n variables.
// In terms of truth table, this is equivalent to choosing a number between 0 and 2^n-1 where
// each 1 in k'th position of the binary representation indicates a T in the k'th row
// of the truth table, but we don't really generate such an integer as it may be larger
// than Long.MaxValue
def genRandomBdd(n: Int): Bdd = {
genBddFromBitMask(n, _ => (0 == prng.nextInt(2)))
}
// if the 1 bits of the binary representation of k denote the True
// rows in the truth table, with the least significant bit representing
// variable x1. (there is no x0)
// k is interpreted as a 2^n-bit binary number. 0 <= k < 2^(2^n)
def genKthBdd(n: Int, k: Long): Bdd = {
// we interpret k as a 'function' mapping the range 0<=i<2^n to Boolean
// whose value is true if there is a 1 in the ith position of k,
// considering the 0'th position as the least significant bit.
genBddFromBitMask(n, truthTableRow => (k & (1 << truthTableRow)) != 0)
}