tclbdd

Check-in [780b74afbb]
Login

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

Overview
Comment:Begin writing a man page for tclbdd, and make some comments truthful
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:780b74afbb42af34db3a585a25ddeb2e832b26d7
User & Date: kbk 2014-07-01 03:26:17
Context
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
2014-01-14
00:35
added != to datalog, and extended tclfddd to support it. check-in: bd3c0053ea user: kbk tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Added doc/tclbdd.n.

            1  +'\" bdd.n --
            2  +'\" 
            3  +'\"     Documentation for the 'bdd' package
            4  +'\" 
            5  +'\" Copyright (c) 2014 by Kevin B. Kenny
            6  +'\" 
            7  +'\" See the file "license.terms" for information on usage and redistribution of
            8  +'\" this file, and for a DISCLAIMER OF ALL WARRANTIES.
            9  +'\" .so man.macros
           10  +'\" IGNORE
           11  +.if t .wh -1.3i ^B
           12  +.nr ^l \n(.l
           13  +.ad b
           14  +'\"	# BS - start boxed text
           15  +'\"	# ^y = starting y location
           16  +'\"	# ^b = 1
           17  +.de BS
           18  +.br
           19  +.mk ^y
           20  +.nr ^b 1u
           21  +.if n .nf
           22  +.if n .ti 0
           23  +.if n \l'\\n(.lu\(ul'
           24  +.if n .fi
           25  +..
           26  +'\"	# BE - end boxed text (draw box now)
           27  +.de BE
           28  +.nf
           29  +.ti 0
           30  +.mk ^t
           31  +.ie n \l'\\n(^lu\(ul'
           32  +.el \{\
           33  +'\"	Draw four-sided box normally, but don't draw top of
           34  +'\"	box if the box started on an earlier page.
           35  +.ie !\\n(^b-1 \{\
           36  +\h'-1.5n'\L'|\\n(^yu-1v'\l'\\n(^lu+3n\(ul'\L'\\n(^tu+1v-\\n(^yu'\l'|0u-1.5n\(ul'
           37  +.\}
           38  +.el \}\
           39  +\h'-1.5n'\L'|\\n(^yu-1v'\h'\\n(^lu+3n'\L'\\n(^tu+1v-\\n(^yu'\l'|0u-1.5n\(ul'
           40  +.\}
           41  +.\}
           42  +.fi
           43  +.br
           44  +.nr ^b 0
           45  +..
           46  +'\" END IGNORE
           47  +.TH "bdd" n 0.1 TclBDD "Tcl Binary Decision Diagram library"
           48  +.BS
           49  +.SH "NAME"
           50  +bdd \- Binary Decision Diagram (BDD) library
           51  +.SH "SYNOPSIS"
           52  +.nf
           53  +package require \fBtclbdd 0.1\fR
           54  +\fBbdd::system create \fIsystem\fR ?\fIinitSize\fR
           55  +\fBbdd::system new ?\fIinitSize\fR
           56  +
           57  +\fIsystem\fR \fB:=\fR \fIresultBdd\fR \fIbdd\fR
           58  +\fIsystem\fR \fB===\fR \fIbdd\fR \fIbdd2\fR
           59  +\fIsystem\fR \fB~\fR \fIresultBdd\fR \fIbdd\fR
           60  +\fIsystem\fR \fBbeadcount\fR \fIbdd\fR
           61  +\fIsystem\fR \fBbeadindex\fR \fIbdd\fR
           62  +\fIsystem\fR \fBcompose\fR \fIresultBdd\fR \fIbdd\fR ?\fIvarName bdd2\fR?...
           63  +\fIsystem\fR \fBdump\fR \fIbdd\fR
           64  +\fIsystem\fR \fBexists\fR \fIresultBdd\fR \fIvarList\fR \fIbdd\fR
           65  +\fIsystem\fR \fBforall\fR \fIresultBdd\fR \fIvarList\fR \fIbdd\fR
           66  +\fIsystem\fR \fBforeach_sat\fR \fItclVarName\fR \fIbdd\fR \fIscript\fR
           67  +\fIsystem\fR \fBgc\fR
           68  +\fIsystem\fR \fBnotnthvar\fR \fIresultBdd\fR \fIindex\fR
           69  +\fIsystem\fR \fBnthvar\fR \fIresultBdd\fR \fIindex\fR
           70  +\fIsystem\fR \fBprofile\fR \fIbdd\fR
           71  +\fIsystem\fR \fBrestrict\fR \fIresultBdd\fR \fIbdd\fR ?\fIliteral\fR,,,?
           72  +\fIsystem\fR \fBsatcount\fR \fIbdd\fR
           73  +\fIsystem\fR \fBsatisfiable\fR \fIbdd\fR
           74  +\fIsystem\fR \fBsimplify\fR \fIresultBdd\fR \fIbdd1\fR \fIbdd2\fR 
           75  +\fIsystem\fR \fBsupport\fR \fIbdd\fR
           76  +\fIsystem\fR \fBtautology\fR \fIbdd\fR
           77  +\fIsystem\fR \fBunset\fR \fIbdd\fR
           78  +
           79  +\fIsystem\fR \fIbinop\fR \fIresultBdd\fR \fIbdd1\fR \fIbdd2\fR
           80  +\fIsystem\fR \fBexists_\fR\fIbinop\fR \fIresultBdd\fR \fIvarList\fR \fIbdd1\fR \fIbdd2\fR
           81  +\fIsystem\fR \fBforall_\fR\fIbinop\fR \fIresultBdd\fR \fIvarList\fR \fIbdd1\fR \fIbdd2\fR
           82  +
           83  +\fIsystem\fR \fIternop\fR \fIresultBdd\fR \fIbdd1\fR \fIbdd2\fR \fIbdd3\fR
           84  +
           85  +\fIsystem\fR \fBload\fR \fIresultBdd\fR \fImapping\fR \fIvalue...\fR
           86  +\fIsystem\fR \fBproject\fR \fBresultBdd\fR \fIindexList\fR \fBbdd\fR
           87  +\fIsystem\fR \fBreplace\fR \fBresultBdd\fR \fIindexList\fR \fIindexList2\fR \fIbdd\fR
           88  +
           89  +\fBbdd::foreach_fullsat\fR \fItclVar\fB \fIvarlist\fR \fIterm\fR \fIscript\fR
           90  +.fi
           91  +.SH "ARGUMENTS"
           92  +.TP
           93  +\fIbdd\fR, \fIbdd2\fR, \fIbdd3\fR...
           94  +Names of binary decision diagrams in \fIsystem\fR.
           95  +.TP
           96  +\fIbinop\fR
           97  +A binary operation, one of '!=', '&', '<', '<=', '==', '>', '>=', '^',
           98  +'nand', 'nor', or '|'. See \fBINARY OPERATIONS\fR for the descriptions of these.
           99  +.TP
          100  +\fIindex\fR
          101  +An unsigned integer index of a variable within the set of variables known
          102  +to the BDD system. Variable indices start at 0 and increment arbitrarily. 
          103  +Indices may be any number up to 2**31-1.
          104  +.TP
          105  +\fIindexList\fR, \fIindexList2\fR
          106  +A list of integer indices designating variables in \fIsystem\fR that the
          107  +command is to act on in a batch.
          108  +.TP
          109  +\fIliteral\fR
          110  +The name of a BDD within \fIsystem\R. The name must designate a BDD 
          111  +representing either a single variable or its negation.
          112  +.TP
          113  +\fImapping\fR
          114  +A list of integers giving a mapping between the bits of the input tuple 
          115  +and the variables in the BDD. See \fBFINITE DOMAIN DIAGRAM SUPPORT\fI for
          116  +the details of this argument, which appears only in the \fBload\fR method.
          117  +.TP
          118  +\fIresultBdd\fR
          119  +Name of a binary decision diagram that will be created in \fIsystem\fR by
          120  +the operation of a method. If the diagram already exists, it will be 
          121  +overwritten.
          122  +.TP
          123  +\fIscript\fR
          124  +Tcl script to evaluate once per iteration over a result set.
          125  +.TP
          126  +\fItclVarName\fR
          127  +Name of a Tcl variable in the caller's scope that will receive one element
          128  +of a result set when iterating over the results.
          129  +.TP
          130  +\fIternop\fR
          131  +A ternary operator, one of '&3', '^3', '?:', 'borrow', 'concur3', 'differ3',
          132  +'even3', 'median', 'nand3', 'nor3', 'oneof3', 'twoof3', or 'or3'. See
          133  +\fBTERNARY OPERATORS\fR for a description of these operators.
          134  +.TP
          135  +\fIvarList\fR
          136  +A Tcl list containing the names of binary decision diagrams in \fIsystem\fR. 
          137  +Each name in the list must designate a single variable (not negated).
          138  +.TP
          139  +\fIvarName\fR
          140  +Name of a binary decision diagram in \fIsystem\fR that designates a single 
          141  +variable (not negated).
          142  +.BE
          143  +.SH "DESCRIPTION"
          144  +.PP
          145  +Binary Decision Diagrams (BDD's) are a compact way to represent arbitrary
          146  +functions of Boolean variables. They are capable of evaluating quickly, and 
          147  +with limited memory, functions that give problems to other representations.
          148  +For instance, parity trees, which grow exponentially in may other 
          149  +representations of Boolean functions (such as sum-of-products or
          150  +product-of-sums), can be managed in linear space and time on BDD's.
          151  +.PP
          152  +The \fBbdd::system\fR class provides a means for Tcl programs to manage
          153  +sets of BDD's. A program can name variables, create Boolean formulas
          154  +involving those variables, test satisfiability, and enumerate satisfying
          155  +variable assignments. 
          156  +.SH "CONSTRUCTING A BDD SYSTEM"
          157  +.PP
          158  +The program constructs a BDD system using the constructor of the \fBbdd::system\fI class.
          159  +.PP
          160  +.nf
          161  +\fBbdd::system create \fIsystem\fR ?\fIinitSize\fR
          162  +\fBbdd::system new ?\fIinitSize\fR
          163  +.fi
          164  +.PP
          165  +The \fIinitSize\fR parameter gives the number of nodes to be preallocated
          166  +for the BDD system. In most cases, this parameter may be omitted without
          167  +harm.
          168  +.SH "CREATING BDD'S"
          169  +.PP
          170  +The program creates a BDD in a system by creating one that represents a named
          171  +variable, or the negation of a named variable.
          172  +.PP
          173  +.nf
          174  +\fIsystem\fR \fBnthvar\fR \fIresultBdd\fR \fIindex\fR
          175  +\fIsystem\fR \fBnotnthvar\fR \fIresultBdd\fR \fIindex\fR
          176  +.fi
          177  +.PP
          178  +In these methods, \fIindex\fR is a zero-based index of the variable number 
          179  +within the system. The programmer is given control over the assignment of
          180  +variable indices because correct variable ordering is sometimes critical to
          181  +performance.
          182  +.PP
          183  +In addition to the BDD's representing variables, two predefined BDD's are
          184  +always available: \fB0\fR is the BDD whose value is always false and \fB1\fR
          185  +is the BDD whose value is always true.
          186  +.SH "COPYING AND NEGATING"
          187  +.PP
          188  +A BDD name may be assigned to another BDD, or to its logical complement, by
          189  +the \fB:=\fR and \fB~\fR methods:
          190  +.PP
          191  +.nf
          192  +\fIsystem\fR \fB:=\fR \fIresultBdd\fR \fIbdd\fR
          193  +\fIsystem\fR \fB~\fR \fIresultBdd\fR \fIbdd\fR
          194  +.fi
          195  +.PP
          196  +After these methods execute, \fIresultBdd\fR will designate either the same
          197  +Boolean function as \fIbdd\fR, or its logical negation.
          198  +.SH "BINARY OPERATORS"
          199  +.PP
          200  +Pairs of BDD's may be combined with binary operators. The resulting function
          201  +is assigned a new name (overwriting any other function of the same name 
          202  +in  \fIsystem\fR). The available operators are;
          203  +.TP
          204  +\fIsystem\fR \fB!=\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          205  +The value of the function will be TRUE for those variable assignments that
          206  +make \fIbdd1\fR and \fIbdd2\fR have different values. This is the same function
          207  +as \fB^\fR, the EXCLUSIVE OR operation.
          208  +.TP
          209  +\fIsystem\fR \fB&\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          210  +The value of the function will be the logical AND of the two input functions.
          211  +.TP
          212  +\fIsystem\fR \fB<\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          213  +The value of the function will be TRUE for those variable assignments where
          214  +the value of \fIbdd\fR is FALSE and the value of \fIbdd2\fR is TRUE. 
          215  +(FALSE < TRUE just as 0 < 1). 
          216  +.TP
          217  +\fIsystem\fR \fB<=\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          218  +The value of the function will be TRUE for those variable assignments where
          219  +the value of \fIbdd\fR is FALSE the value of \fIbdd2\fR is TRUE.
          220  +In addition to being a "less than or equal" comparison, this operator
          221  +is also "logical implication", \fIbdd\fR->\fIbdd2\fR.
          222  +.TP
          223  +\fIsystem\fR \fB==\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          224  +The value of the function will be TRUE for those variable assignments
          225  +where the values of \fIbdd\fR and \fIbdd2\fR are equal. This operation is
          226  +the negation of "exclusive OR".
          227  +.TP
          228  +\fIsystem\fR \fB<\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          229  +The value of the function will be TRUE for those variable assignments where
          230  +the value of \fIbdd\fR is TRUE and the value of \fIbdd2\fR is FALSE. 
          231  +(TRUE > FALSE just as 1 > 0).
          232  +.TP
          233  +\fIsystem\fR \fB>=\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          234  +The value of the function will be TRUE for those variable assignments where
          235  +the value of \fIbdd\fR is TRUE the value of \fIbdd2\fR is FALSE.
          236  +In addition to being a "greater than or equal" comparison, this operator
          237  +is also "logical implication", \fIbdd2\fR->\fIbdd\fR.
          238  +.TP
          239  +\fIsystem\fR \fB^\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          240  +The value of the result is the EXCLUSIVE OR of the values of the two input
          241  +functions.
          242  +.TP
          243  +\fIsystem\fR \fBnand\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          244  +The value of the result is the NAND of the values of the two input functions.
          245  +.TP
          246  +\fIsystem\fR \fBnor\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          247  +The value of the result is the NOR of the values of the two input functions.
          248  +.TP
          249  +\fIsystem\fR \fB|\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR
          250  +The value of the result is the logical OR of the values of the two input 
          251  +functions.
          252  +.SH "TERNARY OPERATORS"
          253  +BDD's may also be constructed by applying ternary operations to three
          254  +functions:
          255  +.TP
          256  +\fIsystem\fR \fB&3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          257  +The resulting function will be the logical AND of three input BDD's.
          258  +.TP
          259  +\fIsystem\fR \fB^3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          260  +The logical EXCLUSIVE OR of three input BDD's. The resulting function is
          261  +true over those variable assignments that make an odd number (1 or 3) of
          262  +the input functions true.
          263  +.TP
          264  +\fIsystem\fR \fB?:\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          265  +The resulting function will have the same value as \fIbdd2\fR on
          266  +those variable assignments that make \fIbdd\fR true, and the same value
          267  +as \fIbdd3\fR on those variable assignments that make \fIbdd\fR false.
          268  +.TP
          269  +\fIsystem\fR \fBborrow\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          270  +This operation is used to implement subtraction in Finite Domain Decision
          271  +Diagram (FDDD) systems. If true==1 and false==0, then the 'borrow'
          272  +operation is true for those input variable assigments that cause the
          273  +calculation of \fIbdd\fR\-\fIbdd2\fR\-\-\fIbdd3\fR to return a value less
          274  +than zero (that is, to borrow from the next column). 
          275  +.TP
          276  +\fIsystem\fR \fBconcur3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          277  +The resulting function will be true only for those variable assignments
          278  +for which \fIbdd\fR, \fIbdd2\fR, and \fIbdd3\fR return the same value (either
          279  +all are false or all are true).
          280  +.TP
          281  +\fIsystem\fR \fBdiffer3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          282  +The resulting function will be true only for those variable assignments
          283  +for which \fIbdd\fR, \fIbdd2\fR, and \fIbdd3\fR are not all equal.
          284  +.TP
          285  +\fIsystem\fR \fBeven3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          286  +The resulting function will be true only for those variable assignments
          287  +for which an even number of \fIbdd\fR, \fIbdd2\fR, and \fIbdd3\fR are true.
          288  +.TP
          289  +\fIsystem\fR \fBmedian\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          290  +The resulting function will be the median value of \fIbdd\fR, \fIbdd2\fR, 
          291  +and \fIbdd3\fR. This operation may be used to describe "majority voting".
          292  +If the values of 0 or 1 of the input functions are true, the value of the
          293  +result function will be false. If the values of 2 or 3 of the input functions
          294  +are true, the result will be true.
          295  +.TP
          296  +\fIsystem\fR \fBnand3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          297  +The resulting function will be the logical NAND of three input BDD's.
          298  +.TP
          299  +\fIsystem\fR \fBnor3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          300  +The resulting function will be the logical NOR of three input BDD's.
          301  +.TP
          302  +\fIsystem\fR \fBoneof3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          303  +The resulting function will be true only for those variable assignments
          304  +for which exactly one of \fIbdd\fR, \fIbdd2\fR, and \fIbdd3\fR are true.
          305  +.TP
          306  +\fIsystem\fR \fBtwoof3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          307  +The resulting function will be true only for those variable assignments
          308  +for which exactly two of \fIbdd\fR, \fIbdd2\fR, and \fIbdd3\fR are true.
          309  +.TP
          310  +\fIsystem\fR \fB|3\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR \fIbdd3\fR
          311  +The resulting function will be the logical OR of three input BDD's.
          312  +.SH "QUANTIFIED FORMULAS"
          313  +A family of quantification functions exist to remove variables from BDD's by
          314  +quantificaton: that is, return a formula representing the condition where
          315  +a given formula is satisfied for at least one, or for all, values of a set of 
          316  +variables.
          317  +.TP
          318  +\fIsystem\fR \fBexists\fR \fIresultBdd\fR \fIvarList\fR \fIbdd\fR
          319  +The resulting function will represent the condition needed to make the given 
          320  +function true for at least one combination of values for the variables
          321  +whose names appear in 'varList'. The variables in 'varList' will not appear
          322  +in the result.
          323  +.TP
          324  +\fIsystem\fR \fBforall\fR \fIresultBdd\fR \fIvarList\fR \fIbdd\fR
          325  +The resulting function will represent the condition needed to make the given
          326  +function true for all combinations of values of the variables whose names
          327  +appear in 'varList'. The variables in 'varList' will not appear in the result.
          328  +.TP
          329  +\fIsystem\fR \fBexists_\fR\fIbinop\fR \fIresultBdd\fR \fIvarList\fR \fIbdd1\fR \fIbdd2\fR
          330  +This method is a combination of a binary operator and the \fBexists\fR
          331  +quantifier. It first computes the value of 
          332  +the given binary operation applied to \fIbdd1\fR
          333  +and \fIbdd2\fR. It then eliminates the variables in \fIvarList\fR by
          334  +setting \fIresultBdd\fR to a Boolean formula which is true only for free 
          335  +variable combinations that make the value true for at least one combination 
          336  +of values of the variables in \fIvarList\fR.
          337  +.PP
          338  +The evaluation of both the binary operator and the quanitifier is done in the
          339  +same pass.
          340  +.PP
          341  +The binary operator may be any of the eleven operators, \fB!=\fR, \fB&\fR,
          342  +\fB<\fR, \fB<=\fR, \fB==\fR, \fB>\fR, \fB>=\fR, \fB^\fR, \fBnand\fR,
          343  +\fBnor\fR, and \fB|\fR.
          344  +.TP
          345  +\fIsystem\fR \fBforall_\fR\fIbinop\fR \fIresultBdd\fR \fIvarList\fR \fIbdd1\fR \fIbdd2\fR
          346  +This method is a combination of a binary operator and the \fBforall\fR
          347  +quantifier. It first computes the value of 
          348  +the given binary operation applied to \fIbdd1\fR
          349  +and \fIbdd2\fR. It then eliminates the variables in \fIvarList\fR by
          350  +setting \fIresultBdd\fR to a Boolean formula which is true only for free 
          351  +variable combinations that make the value true for every possible combination 
          352  +of values of the variables in \fIvarList\fR.
          353  +.PP
          354  +The evaluation of both the binary operator and the quanitifier is done in the
          355  +same pass.
          356  +.PP
          357  +The binary operator may be any of the eleven operators, \fB!=\fR, \fB&\fR,
          358  +\fB<\fR, \fB<=\fR, \fB==\fR, \fB>\fR, \fB>=\fR, \fB^\fR, \fBnand\fR,
          359  +\fBnor\fR, and \fB|\fR.
          360  +.SH "VARIABLE AND EXPRESSION SUBSTITUTION IN BDDs"
          361  +Three methods are provided that allow BDD's to be rewritten with changes of
          362  +variables or with restrictive assumptions.
          363  +.TP
          364  +\fIsystem\fR \fBcompose\fR \fIresultBdd\fR \fIbdd\fR ?\fIvarName bdd2\fR?...
          365  +This method rewrites the Boolean expression \fIbdd\fR, replacing each of the
          366  +variables given by the \fIvarName\fR arguments with the corresponding
          367  +expression \fIbdd2\fR. Substitution proceeds entirely simultaneously. For
          368  +example, it is legal to interchange two variables in a BDD by writing
          369  +.CS
          370  +$system compose newBdd oldBdd a b b a
          371  +.CE
          372  +.TP
          373  +\fIsystem\fR \fBrestrict\fR \fIresultBdd\fR \fIbdd\fR ?\fIliteral\fR,,,?
          374  +This method is a much simpler (and faster) alternative to \fIcompose\fR
          375  +for the case where all the variables are to be replaced with constants.
          376  +The resulting BDD gets the simplification of \fIbdd\fR. Each of 
          377  +the \fIliteral\fR arguments is either a variable or the negation of a variable.
          378  +.TP
          379  +\fIsystem\fR \fBsimplify\fR \fIresultBdd\fR \fIbdd\fR \fIbdd2\fR 
          380  +This method attempts to find a simpler expression for \fIbdd\fR assuming
          381  +that \fIbdd2\fR is true. The \fIresultBdd\fR will have the same values 
          382  +as \fIbdd\fR in that circumstance. This method is often used to try to simplify
          383  +BDD's in the presence of 'don't care' conditions.
          384  +.SH "EXAMINING BDDs"
          385  +A number of methods are provided to obtain information about BDD's once
          386  +they are constructed.
          387  +.TP
          388  +\fIsystem\fR \fB===\fR \fIbdd\fR \fIbdd2\fR
          389  +Returns 1 if the two BDD's return the same output value for all variable
          390  +assignments and 0 otherwise, running in constant time. Note that this is
          391  +not the same as the \fB==\fR method, which constructs a BDD whose value is
          392  +1 for those variable assignments over which the two input BDD's are equal.
          393  +.TP
          394  +\fIsystem\fR \fBbeadindex\fR \fIbdd\fR
          395  +Returns the ordinal number of the bead making the first decision in the
          396  +given BDD. This function is used chiefly for debugging the BDD library itself.
          397  +.TP
          398  +\fIsystem\fR \fBdump\fR \fIbdd\fr
          399  +Returns a representation of the given BDD as a Tcl list. This method is
          400  +intended only for testing the BDD library.
          401  +.TP
          402  +\fIsystem\fR \fBprofile\fR \fIbdd\fR
          403  +Computes the number of nodes at each level of the given BDD. This function
          404  +returns a list of integers. The nth element of the list is the number of nodes
          405  +at level n (equivalently, testing the value of variable number n).
          406  +.PP
          407  +This function is provided so that the programmer can test whether the order
          408  +of variables chosen to represent a given formula yields a compact representation
          409  +as a BDD, in order to choose among possible variable orderings. (Choice of
          410  +variable order, in some cases, may yield a BDD whose size grows exponentially
          411  +while in others it yields a BDD whose size grows only linearly.)
          412  +.TP
          413  +\fIsystem\fR \fBsatcount\fR \fIbdd\fR
          414  +Returns an integer which is the number of combinations of variables in \fIsystem\fR (whether they appear in the given BDD or not) that yield a true value for the given BDD. This number is expected to grow exponentially with the number of variables, but can be computed in reasonable time.
          415  +.TP
          416  +\fIsystem\fR \fBsatisfiable\fR \fIbdd\fR
          417  +Returns 1 if any combination of variable values satisfies the given BDD,
          418  +that is, makes it true. Returns 0 if the given BDD is always false. This method
          419  +runs in constant time.
          420  +.TP
          421  +\fIsystem\fR \fBsupport\fR \fIbdd\fR
          422  +Returns a list of variable indices corresponding to the variables
          423  +that appear in the given BDD. The indices present in the returned list are
          424  +exactly the indices for which the result of
          425  +.CS
          426  +$system profile $bdd
          427  +.CE
          428  +is nonzero.
          429  +.TP
          430  +\fIsystem\fR \fBsatisfiable\fR \fIbdd\fR
          431  +Returns 1 if the given BDD is a tautology, that is, if it is true for every
          432  +combination of variable values.
          433  +Returns 0 if the given BDD is sometimes false. This method
          434  +runs in constant time.
          435  +.SH "DELETING BDDs"
          436  +.TP
          437  +\fIsystem\fR \fBunset\fR \fIbdd\fR
          438  +Forgets the value of the given BDD and makes its name undefined.
          439  +.SH "ENUMERATING SATISFYING VARIABLE ASSIGNMENTS"
          440  +'\" foreach_sat and bdd::foreach_fullsat
          441  +.SH "FUNCTIONS FOR FDDD SUPPORT"
          442  +'\" load, project, replace
          443  +.SH "MISCELLANEOUS FUNCTIONS"
          444  +.TP
          445  +\fIsystem\fR \fBgc\fR
          446  +Performs garbage collection on the memory representing the given system of
          447  +BDD's. When BDD's are overwritten, their memory is retained for a short 
          448  +while because other BDD's under construction often reconstruct exactly the
          449  +same node structure. This method arranges that all such memory is freed.
          450  +.SH "SEE ALSO"
          451  +.SH "KEYWORDS"
          452  +.SH "REFERENCES"
          453  +.SH "COPYRIGHT"
          454  +Copyright (c) 2014 by Kevin B. Kenny.
          455  +'\" Local Variables:
          456  +'\" mode: nroff
          457  +'\" End:
          458  +'\"

Changes to generic/tclBdd.c.

  1985   1985    *-----------------------------------------------------------------------------
  1986   1986    *
  1987   1987    * BddSystemReplaceMethod --
  1988   1988    *
  1989   1989    *	Replaces a set of variables in a BDD with other variables.
  1990   1990    *
  1991   1991    * Usage:
  1992         - *	$system project result vars vars2 expr
         1992  + *	$system replace result vars vars2 expr
  1993   1993    *
  1994   1994    * Parameters:
  1995   1995    *	system - System of BDD's
  1996   1996    *	result - Name of a BDD that will receive the result
  1997   1997    *	vars - List of integers giving positions of variables to replace
  1998   1998    *	vars2 - List of integers giving positions of variables that will
  1999   1999    *              replace vars. The two lists must have the same length.
................................................................................
  2001   2001    *
  2002   2002    * Results:
  2003   2003    *	Returns a standard Tcl result
  2004   2004    *
  2005   2005    * Side effects:
  2006   2006    *	Creates the named expression if successful
  2007   2007    *
  2008         - * This is the same operation as existential quantification. It is provided
  2009         - * for the convenience of Finite Domain Decision Diagrams, where it exists
  2010         - * as the relational 'project' operator.
         2008  + * This is the same operation as composition. It is provided for the
         2009  + * convenience of Finite Domain Decision Diagrams, where it exists as
         2010  + * the relational 'replace' operator.
  2011   2011    *
  2012   2012    *-----------------------------------------------------------------------------
  2013   2013    */
  2014   2014   static int
  2015   2015   BddSystemReplaceMethod(
  2016   2016       ClientData clientData,	/* Operation to perform */
  2017   2017       Tcl_Interp* interp,		/* Tcl interpreter */
................................................................................
  2147   2147    *                  expressions representing a single, possibly negated,
  2148   2148    *		    literal.
  2149   2149    *
  2150   2150    * Results:
  2151   2151    *	None
  2152   2152    *
  2153   2153    * Side effects:
  2154         - *	Assigns the negation of the given variable to the new name
         2154  + *	Assigns the result of the restriction to the new name.
  2155   2155    *
  2156   2156    *-----------------------------------------------------------------------------
  2157   2157    */
  2158   2158   
  2159   2159   static int
  2160   2160   BddSystemRestrictMethod(
  2161   2161       ClientData clientData,	/* Operation to perform */
................................................................................
  2289   2289    *	Simplifies a BDD with a respect to a domain. (Coudert and Madre's
  2290   2290    *	Restrict function).
  2291   2291    *
  2292   2292    * Usage:
  2293   2293    *	$system simplify a f domain
  2294   2294    *
  2295   2295    * Parameters:
  2296         - *	OP - One of the binary operators nor, <, >, !=, ^, nand, &,
  2297         - *           ==, <=, >=, |
  2298   2296    *	a - Name of the result expression
  2299   2297    *	f - Name of the expression to simplify
  2300   2298    *	domain - Name of the expression describing the domain of interest
  2301   2299    *
  2302   2300    * Results:
  2303   2301    *	None
  2304   2302    *