Quick Start
After installing Ruby-BDD, you may run the examples provided in the distribution if you're curious. The knight.rb example checks if a knight on a chess board can reach every position on the board (it's not really the knight's tour). The queens.rb example solves the N-queens problem. The milner_scheduler.rb example is Milner's scheduler, a token based scheduler.
A more interesting use is the interactive mode of ruby. Run irb from the command line prompt (not from cygwin if you installed Ruby for Windows).
There are two ways of accessing boolean variables, either you declare a number of them and call BDD.get_var(number) or you want to name them, which is only some sugar in the binding. Let's load the module and declare some variables.
prompt>irb
irb(main):001:0>
In the interactive mode, the interpreter prints the returned value after every command. The binding computes a string representation of the BDD. Let's try other formula. You can see the BDDs themselves by calling show.
irb(main):001:0> require 'bdd'
=> true
irb(main):002:0> a=var('a')
=> #<BDD:2 "a">
irb(main):003:0> b=var('b')
=> #<BDD:4 "b">
irb(main):004:0> c=var('c')
=> #<BDD:6 "c">
irb(main):005:0>
The two assignments of d are only for testing the operators. The third encodes something very common, namely only one of a, b, or c should be set. It's a kind of generalized 'xor' on n variables. This particular function is supported by the binding as the nxor function. We can check that it gives exactly what we want by looking at the satisfying assignments of these boolean variables. This is done through an iterator in Ruby.
irb(main):005:0> d=(a & b)| c >> b
=> #<BDD:9 "b | (!b & !c)">
irb(main):006:0> d=(a & b.not) >> c
=> #<BDD:12 "(a & b | (!b & c)) | !a">
irb(main):007:0> d=(a & b.not & c.not)|(a.not & b & c.not)|(a.not & b.not & c)
=> #<BDD:23 "(a & (!b & !c)) | (!a & (b & !c) | (!b & c))">
irb(main):008:0> e=BDD.nxor(a,b,c)
=> #<BDD:23 "(a & (!b & !c)) | (!a & (b & !c) | (!b & c))">
irb(main):009:0> d == e
=> true
irb(main):010:0>
The iteration gives vectors of booleans (true/false) corresponding to the assignments of the boolean variables, of nil for 'does not matter'. The method to_keys translates back to names to read the result more easily.
irb(main):010:0> d.each {|v| puts v.to_keys.inspect }
["!a", "!b", "c"]
["!a", "b", "!c"]
["a", "!b", "!c"]
=> #<BDD:23 "(a & (!b & !c)) | (!a & (b & !c) | (!b & c))">
irb(main):011:0>