examples/muddy/bdd.sig

147 (* Structure bdd provide an interface to J��rn Linds <jl@it.dtu.dk>
156    for small test examples and up to 1000000 nodes for large examples.
157    A cache size of 10000 seems to work good even for large examples,
167    [setvarnum num] is used to define the number of variables used in
168    the bdd package. It may be called more than one time, but only to
169    increase the number of variables. num is the number of variables to
173    package to its initial state.
218    [toSet_ r] converts the bdd r to a varSet; no checks are performed
219    to check that r really represents a varSet therefore it should be
243    [appex x y opr varset] equivalent to 'exist varset (apply x y opr)'
246    [appall x y opr varset] equivalent to 'forall varset (apply x y opr)'
249    [DIFF(x,y)] equivalent to 'apply x y Diff', but this is nice for
252    [IMP(x,y)] equivalent to 'apply x y Imp', but this is nice for infix.
254    [LESSTH(x,y)] equivalent to 'apply x y Lessth', but this is nice for
257    [BIIMP(x,y)] equivalent to 'apply x y Biimp', but this is nice for
260    [OR(x,y)] equivalent to 'apply x y Or', but this is nice for infix.
262    [INVIMP(x,y)] equivalent to 'apply x y Invimp', but this is nice for
265    [NAND(x,y)] equivalent to 'apply x y Nand', but this is nice for infix.
267    [NOR(x,y)] equivalent to 'apply x y Nor', but this is nice for infix.
269    [AND(x,y)] equivalent to 'apply x y And', but this is nice for infix.
271    [XOR(x,y)] equivalent to 'apply x y Xor', but this is nice for infix.
275    [ITE x y z] equivalent to 'OR(AND(x, y), AND(NOT x, z))'; but more
278    Type [pairSet] is used to represet substitutions of variables with
289    assignment [(x1,true), (x3,false), (x2, true)] corresponds to the
292    [restrict r assign] ... restrict the variables in assign to TRUE or
296    if r is equal to FALSE.
298    [simplify r dom] tries to simplify r by restricting it to domain d,
307    [enableReorder()] Re-enables reordering after a call to
337    [setCacheratio n] sets the cache ratio to n.  For example, if n is
341    [verbosegc(SOME(pregc,postgc))] instructs BuDDy to print