Iben

Semantics & Verification, Spring 2006

---

Even though there is no miniproject concerning BDDs, you can have a look at the tool IBEN for manipulation with BDDs. We will be using the tool in the last tutorial (Tutorial 14). Iben can be run e.g. from the command line on borg (/pack/FS/pack/iben-1.1/bin/iben) and it is extremely easy to use. Here is a very short manual and a small demo:

iben> vars x y (This declares two boolean variables x (the 0th variable) and y (the first variable))
iben> satisfy x & y
<0:1, 1:1> (This says that the only satisfying assignment is one in which the 0th variable, namely x, is true, and so is the first one, namely y.)
iben> vars z (This declares the variable z with index 2)
iben> satisfy x & y & !z
<0:1, 1:1, 2:0>
iben> satisfy x + (!x & y & !z)
<0:0, 1:1, 2:0><0:1> (This says that there are two families of satisfying assignments. In the second one, the only thing that matters is that x is true.)
iben> show x + (!x & y & !z) (This shows the resulting ROBDD as a postscript file.)