The Interactive BDD Environment ------------------------------- IBEN provides an interactive interface to Jørn Lind-Nielsen's BUDDY BDD package. IBEN is ported from David Longs BDD package with minor modifications to accommodate differences between the packages. The program reads commands from standard input and writes to standard output. The only command line option to the program is -i, which means "interactive mode". This causes iben to use the readline package. Readline provides line editing and a command history. Iben uses the semicolon as a command separator (like Pascal), not as a command terminator (like C). This means that lines do not have to be terminated in interactive mode. The available commands are (some commands are not implemented in the BUDDY version - these are marked with "--" characters): Creating variables: vars ... Create some new boolean variables and assign them to the identifiers given by s. Variable assignment: := Evaluates an expression and assigns the result to . Any previous definition of is lost. The syntax of expressions is defined below. Clear: clear all clear ... Deletes all definitions or the definitions of the specified identifiers. The first form also restarts the BDD package. Printing: print Print all satisfying assignments. show Show the BDD representing the expression as a graph. This requires access to ghostview. Sizes: size ... Print the number of BDD nodes used in representing the given expressions. Getting satisfying assignments: satisfy Find and print a satisfying assignment for the expression. Getting valuation counts: satcount Prints the number of valuations that make the expressions TRUE. Setting the node limit: limit limit none Set the BDD node limit to the indicated number of nodes, or get rid of the node limit. If the number of nodes gets bigger than during an operation, the operation will be aborted. Help: View this file Timing things: timer timer off The first form either starts the timer, or prints the elapsed CPU time since the timer was started and since the last timer command. The second form prints the elapsed times and also stops the timer. Including files: load were is the filename in double quotes, e.g. load "myfile" This can be used as a simple procedure call mechanism. Quitting: quit In interactive mode quit will terminate the program. Expression syntax: a boolean variable 0 FALSE 1 TRUE ( ) & * conjunction | + disjunction = equivalence ^ exclusive or => implies ! ~ negation exists ( ) existential quantification over variables, e.g. exists x & y (a) will perform existential quantification of x and y in a. forall ( ) universal quantification over variables (see exists) subst ( ) with the variables in replaced by their associated expressions Variable association syntax: [ / / ... ] an association between pairs of variables. Typically used for simultaneous substitution. For instance subst [ x / y ] (f) will replace all occurrences of y in f with x.