tclbdd

Check-in [97123e476e]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Finish draft of man page for tclbdd(n)
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:97123e476e049011bc18a58402e21aebe5e456b2
User & Date: kbk 2014-07-05 19:33:39
Context
2014-07-10
03:30
progress toward a man page for tclfddd check-in: 337aa1f548 user: kbk tags: trunk
2014-07-05
19:33
Finish draft of man page for tclbdd(n) check-in: 97123e476e user: kbk tags: trunk
2014-07-01
03:26
Begin writing a man page for tclbdd, and make some comments truthful check-in: 780b74afbb user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to doc/tclbdd.n.

183
184
185
186
187
188
189
190
191
192

193
194
195
196
197
198
199
200
201
202
...
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
...
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
...
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
...
428
429
430
431
432
433
434




















































435
436
437
438
439
440
441
442






































443
444
445
446
447
448
449
450

451


452













453
454
455
456
457
458
In addition to the BDD's representing variables, two predefined BDD's are
always available: \fB0\fR is the BDD whose value is always false and \fB1\fR
is the BDD whose value is always true.
.SH "COPYING AND NEGATING"
.PP
A BDD name may be assigned to another BDD, or to its logical complement, by
the \fB:=\fR and \fB~\fR methods:
.PP
.nf
\fIsystem\fR \fB:=\fR \fIresultBdd\fR \fIbdd\fR

\fIsystem\fR \fB~\fR \fIresultBdd\fR \fIbdd\fR
.fi
.PP
After these methods execute, \fIresultBdd\fR will designate either the same
Boolean function as \fIbdd\fR, or its logical negation.
.SH "BINARY OPERATORS"
.PP
Pairs of BDD's may be combined with binary operators. The resulting function
is assigned a new name (overwriting any other function of the same name 
in  \fIsystem\fR). The available operators are;
................................................................................
This method is a combination of a binary operator and the \fBexists\fR
quantifier. It first computes the value of 
the given binary operation applied to \fIbdd1\fR
and \fIbdd2\fR. It then eliminates the variables in \fIvarList\fR by
setting \fIresultBdd\fR to a Boolean formula which is true only for free 
variable combinations that make the value true for at least one combination 
of values of the variables in \fIvarList\fR.
.PP
The evaluation of both the binary operator and the quanitifier is done in the
same pass.
.PP
The binary operator may be any of the eleven operators, \fB!=\fR, \fB&\fR,
\fB<\fR, \fB<=\fR, \fB==\fR, \fB>\fR, \fB>=\fR, \fB^\fR, \fBnand\fR,
\fBnor\fR, and \fB|\fR.
.TP
................................................................................
This method is a combination of a binary operator and the \fBforall\fR
quantifier. It first computes the value of 
the given binary operation applied to \fIbdd1\fR
and \fIbdd2\fR. It then eliminates the variables in \fIvarList\fR by
setting \fIresultBdd\fR to a Boolean formula which is true only for free 
variable combinations that make the value true for every possible combination 
of values of the variables in \fIvarList\fR.
.PP
The evaluation of both the binary operator and the quanitifier is done in the
same pass.
.PP
The binary operator may be any of the eleven operators, \fB!=\fR, \fB&\fR,
\fB<\fR, \fB<=\fR, \fB==\fR, \fB>\fR, \fB>=\fR, \fB^\fR, \fBnand\fR,
\fBnor\fR, and \fB|\fR.
.SH "VARIABLE AND EXPRESSION SUBSTITUTION IN BDDs"
Three methods are provided that allow BDD's to be rewritten with changes of
variables or with restrictive assumptions.
.TP
................................................................................
Returns a representation of the given BDD as a Tcl list. This method is
intended only for testing the BDD library.
.TP
\fIsystem\fR \fBprofile\fR \fIbdd\fR
Computes the number of nodes at each level of the given BDD. This function
returns a list of integers. The nth element of the list is the number of nodes
at level n (equivalently, testing the value of variable number n).
.PP
This function is provided so that the programmer can test whether the order
of variables chosen to represent a given formula yields a compact representation
as a BDD, in order to choose among possible variable orderings. (Choice of
variable order, in some cases, may yield a BDD whose size grows exponentially
while in others it yields a BDD whose size grows only linearly.)
.TP
\fIsystem\fR \fBsatcount\fR \fIbdd\fR
................................................................................
is nonzero.
.TP
\fIsystem\fR \fBsatisfiable\fR \fIbdd\fR
Returns 1 if the given BDD is a tautology, that is, if it is true for every
combination of variable values.
Returns 0 if the given BDD is sometimes false. This method
runs in constant time.




















































.SH "DELETING BDDs"
.TP
\fIsystem\fR \fBunset\fR \fIbdd\fR
Forgets the value of the given BDD and makes its name undefined.
.SH "ENUMERATING SATISFYING VARIABLE ASSIGNMENTS"
'\" foreach_sat and bdd::foreach_fullsat
.SH "FUNCTIONS FOR FDDD SUPPORT"
'\" load, project, replace






































.SH "MISCELLANEOUS FUNCTIONS"
.TP
\fIsystem\fR \fBgc\fR
Performs garbage collection on the memory representing the given system of
BDD's. When BDD's are overwritten, their memory is retained for a short 
while because other BDD's under construction often reconstruct exactly the
same node structure. This method arranges that all such memory is freed.
.SH "SEE ALSO"

.SH "KEYWORDS"


.SH "REFERENCES"













.SH "COPYRIGHT"
Copyright (c) 2014 by Kevin B. Kenny.
'\" Local Variables:
'\" mode: nroff
'\" End:
'\"







|
<

>

|
<







 







|







 







|


|







 







|







 







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>




<
<

<
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>








>

>
>

>
>
>
>
>
>
>
>
>
>
>
>
>






183
184
185
186
187
188
189
190

191
192
193
194

195
196
197
198
199
200
201
...
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
...
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
...
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
...
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489


490

491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
In addition to the BDD's representing variables, two predefined BDD's are
always available: \fB0\fR is the BDD whose value is always false and \fB1\fR
is the BDD whose value is always true.
.SH "COPYING AND NEGATING"
.PP
A BDD name may be assigned to another BDD, or to its logical complement, by
the \fB:=\fR and \fB~\fR methods:
.TP

\fIsystem\fR \fB:=\fR \fIresultBdd\fR \fIbdd\fR
.TP
\fIsystem\fR \fB~\fR \fIresultBdd\fR \fIbdd\fR
.IP

After these methods execute, \fIresultBdd\fR will designate either the same
Boolean function as \fIbdd\fR, or its logical negation.
.SH "BINARY OPERATORS"
.PP
Pairs of BDD's may be combined with binary operators. The resulting function
is assigned a new name (overwriting any other function of the same name 
in  \fIsystem\fR). The available operators are;
................................................................................
This method is a combination of a binary operator and the \fBexists\fR
quantifier. It first computes the value of 
the given binary operation applied to \fIbdd1\fR
and \fIbdd2\fR. It then eliminates the variables in \fIvarList\fR by
setting \fIresultBdd\fR to a Boolean formula which is true only for free 
variable combinations that make the value true for at least one combination 
of values of the variables in \fIvarList\fR.
.IP
The evaluation of both the binary operator and the quanitifier is done in the
same pass.
.PP
The binary operator may be any of the eleven operators, \fB!=\fR, \fB&\fR,
\fB<\fR, \fB<=\fR, \fB==\fR, \fB>\fR, \fB>=\fR, \fB^\fR, \fBnand\fR,
\fBnor\fR, and \fB|\fR.
.TP
................................................................................
This method is a combination of a binary operator and the \fBforall\fR
quantifier. It first computes the value of 
the given binary operation applied to \fIbdd1\fR
and \fIbdd2\fR. It then eliminates the variables in \fIvarList\fR by
setting \fIresultBdd\fR to a Boolean formula which is true only for free 
variable combinations that make the value true for every possible combination 
of values of the variables in \fIvarList\fR.
.IP
The evaluation of both the binary operator and the quanitifier is done in the
same pass.
.IP
The binary operator may be any of the eleven operators, \fB!=\fR, \fB&\fR,
\fB<\fR, \fB<=\fR, \fB==\fR, \fB>\fR, \fB>=\fR, \fB^\fR, \fBnand\fR,
\fBnor\fR, and \fB|\fR.
.SH "VARIABLE AND EXPRESSION SUBSTITUTION IN BDDs"
Three methods are provided that allow BDD's to be rewritten with changes of
variables or with restrictive assumptions.
.TP
................................................................................
Returns a representation of the given BDD as a Tcl list. This method is
intended only for testing the BDD library.
.TP
\fIsystem\fR \fBprofile\fR \fIbdd\fR
Computes the number of nodes at each level of the given BDD. This function
returns a list of integers. The nth element of the list is the number of nodes
at level n (equivalently, testing the value of variable number n).
.IP
This function is provided so that the programmer can test whether the order
of variables chosen to represent a given formula yields a compact representation
as a BDD, in order to choose among possible variable orderings. (Choice of
variable order, in some cases, may yield a BDD whose size grows exponentially
while in others it yields a BDD whose size grows only linearly.)
.TP
\fIsystem\fR \fBsatcount\fR \fIbdd\fR
................................................................................
is nonzero.
.TP
\fIsystem\fR \fBsatisfiable\fR \fIbdd\fR
Returns 1 if the given BDD is a tautology, that is, if it is true for every
combination of variable values.
Returns 0 if the given BDD is sometimes false. This method
runs in constant time.
.SH "ENUMERATING SATISFYING VARIABLE ASSIGNMENTS"
The package provides a function for enumerating the variable assignments
that satisfy the Boolean function represented by a BDD:
.TP
\fIsystem\fR \fBforeach_sat\fR \fIvariable\fR \fIbdd\fR \fIscript\fR
This call iterates over the satisfying assigments for \fIbdd\fR. For each
assignment, it places a description of the variable values in the 
Tcl variable \fIvariable\fR and evaluates \fIscript\fR. 
.IP
The content of \fIvariable\fR will be a Tcl list of integers in alternating
pairs. The first of the integers will be the variable number that was passed
to [\fIsystem\fR \fBnthvar\fR] or [\fIsystem\fR \fBnotnthvar\fR] to define
the variable. The second will be the value of the variable: 1 if true and
0 if false.
.IP
\fIVariables with "don't care" values are omitted from the list.\fR That
is, a list such as
.CS
0 1 2 0 5 1
.CE
means, "any set of variable values such that variable 0 is true, variable 2 
is false, and variable 5 is true. Any set of values for variables 1, 3 and 4
is acceptable."
.IP
\fBbreak\fR, \fBcontinue\fR and \fBreturn\fR commands appearing within the
script have their natural meaning of terminating the loop prematurely,
advancing prematurely to the next value, and returning from the calling 
procedure.
.IP
For callers that require complete variable enumeration, rather than the
abbreviated form provided by the \fBforeach_sat\fR method, the library
provides a call to expand a term from \fBforeach_sat\fR:
.TP
\fBbdd::foreach_fullsat\fR \fIvariable varList term script\fR
This call expands the term \fIterm\fR, making sure that assignments are
present for all the variables in \fIvarList\fR. It places the list of values,
in the order in which the variable numbers appear in \fIvarList\fR, into
\fIvariable\fR, and evaluates \fIscript\fR for each combination.
.IP
All the variables present in \fIterm\fR must appear in \fIvarList\fR.
.IP
\fBbreak\fR, \fBcontinue\fR and \fIreturn\fR operations that appear in
\fIscript\fR have their natural meaning. In addition, because 
\fBbdd::foreach_fullsat\fR so often appears nested directly 
within [\fIsystem\fR \fBforeach_sat\fR], the special call:
.CS
return -level 0 -code 6
.CE
executed within \fIscript\fR has the effect, not only of breaking the
loop requested by \fBbdd::foreach_fullsat\fR but also of making
\fBbdd::foreach_fullsat\fR have the effect of performing a \fBbreak\fR
and terminating the execution of the enclosing loop as well.
.SH "DELETING BDDs"
.TP
\fIsystem\fR \fBunset\fR \fIbdd\fR
Forgets the value of the given BDD and makes its name undefined.


.SH "FUNCTIONS FOR FDDD SUPPORT"

One of the uses of the BDD package is to support an implementation of
Finite Domain Decision Diagrams (FDDD's). A few service functions are
provided for convenience to FDDD support and to aid in the management of
bulk data.
.TP
\fIsystem\fR \fBload\fR \fIbdd\fR \fIdescriptionList\fR \fIvalue\fR ?\fIvalue\fR...?
This call processes one set of finite-domain values into Boolean variable
assignments and OR's them into the given \fIbdd\fR. The \fIdescriptionList\fR
is a list containing a multiple of three elements, all of which are integers,
describing how the bits in the finite domain values are to be mapped to Boolean
variable assignments. For each triple in the list, the first element is the
number of a variable in the BDD (as created with \fBnthvar\fR or 
\fBnotnthvar\fR). The second element is the index within the \fIvalue\fR
parameters (0 representing the first of the parameters) of the source
of the corresponding bit, and the third element is the bit position (0 being
the least significant bit) of the bit within the specified \fIvalue\fR.
.IP
The variables in \fIdescriptionList\fR must appear in increasing order
by variable number. The corresponding bit positions in the \fIvalue\fR
parameters may be specified in any order.
No \fIvalue\fR may be greater than the maximum value of a \fBTcl_WideInt\fR.
.IP
It is expected that the \fBload\fR method may be useful to other code that
wishes to express Boolean functions by enumerating rows of their truth tables
or in "sum of products" form.
.TP
\fIsystem\fR \fBproject\fR \fIresultBdd\fR \fIvarList\fR \fIbdd\fR
This is a convenience method equivalent to [\fIsystem\fR \fBforall\fR],
except that the \fIvarList\fR argument contains a list of variable numbers,
rather than of variable names.
.TP
\fIsystem\fR \fBreplace\fR \fIresultBdd\fR \fIvarsToReplace\fR \fIreplacementVars\fR \fIbdd\fR
This is a convenience method equivalent to [\fIsystem\fR \fBcompose\fR]. In
this method, the \fIvarsToReplace\fR parameter is a list of variable
numbers to substitute, and \fIreplacementVars\fI is a list of the same length,
containing variable numbers that are to replace the variables
\fIvarsToReplace\fR. This method is used to rewrite a BDD, giving the same
expression over a different variable set.
.SH "MISCELLANEOUS FUNCTIONS"
.TP
\fIsystem\fR \fBgc\fR
Performs garbage collection on the memory representing the given system of
BDD's. When BDD's are overwritten, their memory is retained for a short 
while because other BDD's under construction often reconstruct exactly the
same node structure. This method arranges that all such memory is freed.
.SH "SEE ALSO"
Bdd(3), tclfddd(n), datalog(n)
.SH "KEYWORDS"
binary decision diagram, BDD, Boolean function, finite domain decision diagram,
FDDD, deduction, deductive database, logic programming
.SH "REFERENCES"
An accessible introduction to Binary Decision diagrams is available as:
.PP
Andersen, Henrik Reif. "An introduction to binary decision diagrams." 
Lecture notes, available online, IT University of Copenhagen (1997).
.br
http://aima.eecs.berkeley.edu/~russell/classes/cs289/f04/
readings/Andersen:1997.pdf 
.PP
The original reference to BDD's is:
.PP
Bryant, R.E., "Graph-Based Algorithms for Boolean Function Manipulation," 
\fIIEEE Transactions on Computers,\fR \fBC-35:\fR8 (August, 1986), pp. 677-691. 
http://dx.doi.org/10.1109/TC.1986.1676819
.SH "COPYRIGHT"
Copyright (c) 2014 by Kevin B. Kenny.
'\" Local Variables:
'\" mode: nroff
'\" End:
'\"