IT/Description/HolBdd.tex

88 The development of {\tt HolBddLib} has gone through two phases.  The
91 These are described in the paper {\it Reachability programming in HOL98 using BDDs\/} \cite{tphols2000-Gordon}. The first release of
104 The primitive inference rules for representation judgements are contained in the structure
136 engine. The interface from \Buddy{} to Moscow ML, called \Muddy, is
157 The derivation of `theorems' like \termbdd{a}{\rho}{t}{b} can be viewed
163 The structure \t{HolBddLib} currently contains two main structures: \t{PrimitiveBddRules}
174 The Voss system \cite{SegerVoss} has strongly influenced and inspired
178 The normal boolean operations $\neg$, $\wedge$, $\vee$, $\equiv$,
185 evaluation (STE) \cite{JoyceSeger}. The HOL-Voss system integrates HOL88
194 The early experiments with HOL-Voss suggested that a lighter theorem
212 metalanguage. The connection between symbolic trajectory evaluation
219 The combination of \HOL{} and \Buddy{} in Version~1 of
262 The current \HolBuddy{} system only uses \t{bdd} and so
268 The \Buddy{} package must be initialised before any BDD operations are done.
277 The library \t{HolBddLib} (Section~\ref{HolBddLib})
279 be 10000. The following is a quotation from the \Buddy{} documentation \cite{BuDDy}.
304 The initial number of nodes is not critical for any BDD operation
309 The function
318 The functions \t{init} and \t{done} should only be called once per session.
320 The function
330 The functions \t{init} and \t{done} should only be called once in a session.
346 The meaning of the values of the various named fields in the record returned by
365 The management of the node table and internal caches can be tuned
375 when doing an expansion of the nodetable should be $n$.  The previous maximum is returned.
383 The atomic BDDs representing the two truthvalues are bound to the ML
393 The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE.
411 The number of variables in use must be declared using
418 $1$, $\ldots$ , $n{-}1$ are available for use. The number of variables
420 with a larger number. The number of variables cannot be decreased
421 dynamically. The function
430 The function
456 of variables. The module  \t{bdd} provides a type \t{varSet} to represent such
465 The destructor \t{scanset} returns a vector of the variables in the
469 The following functions quantify BDDs with respect to sets of variables:
484 The operation \t{veccompose} performs the simultaneous substitution
485 of BDDs for variables in a BDD. The argument of \t{veccompose}
542 The exception \t{Domain} is raised if the argument to \t{satone} is unsatisfiable.
563 The functions \t{satone} and \t{findSat} do not necessarily find the
571 The structure \t{bdd} introduces a type \t{bddop}
573 The ML function
590 The function \t{appall} universally quantifies the result of the
631 The integer labelling a BDD node and the BDDs corresponding to the high
649 The entire \Buddy{} node table of a BDD can be copied into ML using
655 The integer returned as the first component of the pair is a pointer
661 ({\t{true}}) node. The first two nodes in the vector are special:
665 The number of nodes in a BDD is computed by the function
683 The number of assignments {\it to all variables in use in the current session\/} that satisfy a BDD (i.e.~make it true) is given by the ML
690 The answer is exact until the result is too big to be represented as a
694 The function
710 The
733 The ML function
763 The string argument is a file name.
770 The function
778 The functions for printing BDDs are;
837 See the \Buddy{} documentation \cite{BuDDy} for further details. The dynamic reordering
870 \subsection{The \Muddy{} structure \t{fdd}}\label{fdd}\index{HolBddLib!finite domains}
872 The structure \t{fdd} provides functions for manipulating values of finite domains.
897 \subsection{The \Muddy{} structure \t{bvec}}\label{bvec}\index{HolBddLib!BDD!vectors}
899 The structure \t{bvec} provides tools for encoding integers as arrays
948 The heart of the \Muddy{} package is mostly stub code that mirrors the
952 The most tricky part is to make the \mosml{} garbage collector cooperate
954 try to collect the other's garbage).  The cooperation is done by using
1024 \subsection{The structure \ml{Varmap}}\label{Varmap}\index{HolBddLib!termbdd@\ml{term\_bdd}!varmaps}
1026 The type \t{varmap} is defined by
1039 The following operations and predicates on varmaps are provided:
1078 \subsection{The structure \ml{PrintBdd}}\label{PrintBdd}\index{HolBddLib!termbdd@\ml{term\_bdd}!printing}
1095 the label being the string $label$. The BDD variables are printed as the numbers used by \Buddy{}.
1096 The \t{dot} program is then invoked to create
1097 a postscript file $file$\t{.ps}. The argument BDD is returned.
1111 of the term part of $tb$. The default labels
1116 \subsection{The structure \t{PrimitiveBddRules}}\label{PrimitiveBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!primitive rules}
1118 The structure \ml{PrimitiveBddRules} defines the type \termbddty{} by
1129 The constructor \t{TermBdd} is not exported, so the only way to construct
1184 The notation $a_1 \cup a_2$ denotes the union of $a_1$ and $a_2$
1188 The implementation is $a_1 \cup a_2~=~\t{HOLset.union}~a_1~a_2$.
1189 The empty set of assumptions is denoted by \emptyass, a set of
1461 (see Section~\ref{misc}). The exception
1737 $\hat{\t{F}}$ denotes \t{false}. The exception
1816 The exception
1851 The set $\{v_1=c_1,\ldots,v_p=c_p\}$ is a satisfying assignment for $t$
2017 \subsection{The structure \t{DerivedBddRules}}\label{DerivedBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!derived rules}
2259 previous term\_bdd tb and the current one tb'. The initial state