\documentclass[12pt,fleqn]{article} \usepackage{makeidx} \usepackage{url} %\usepackage{index} %\usepackage{multind} \usepackage{fancyvrb} \usepackage{latexsym} %\usepackage{amsmath} \usepackage{amssymb} %\usepackage{amsbsy} \usepackage{alltt} \usepackage{../LaTeX/layout} \usepackage{graphicx} \input{../LaTeX/commands} %\makeindex \newcommand{\hbc}[2]{ \addtolength{\minipagewidth}{-10pt} \begin{minipage}{\minipagewidth} \begin{footnotesize} {\texttt{#1}} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} #2 \end{footnotesize} \end{minipage} } \renewcommand{\t}[1]{\mbox{\tt #1}} %\newcommand{\prev}[1]{#1} %\newcommand{\varord}[1]{#1} %\newcommand{\ma}[1]{{{$#1$}}} %\newcommand{\id}[1]{#1} \newcommand{\termbdd}[4]{\mbox{$#1~#2~#3~\mapsto~#4$}} \newcommand{\globtermbdd}[2]{\mbox{$#1\hspace{0.5mm}\mapsto\hspace{0.5mm}#2$}} \newcommand{\emptyass}{\mbox{\footnotesize$\{{}\}$}{}} \newcommand{\setass}[1]{\mbox{\footnotesize$\{#1\}$}{}} \newcommand\termbddty{\texttt{term\_bdd}{}} \newcommand{\mosml}{Moscow~ML{}} \newcommand{\Buddy}{BuDDy{}} \newcommand{\Muddy}{MuDDy{}} \newcommand\HolBuddy{\texttt{HolBddLib}{}} %\newcommand{\els}{\mid} %\newcommand{\Imp}{\Rightarrow} \renewcommand{\prod}{\mbox{\tt{*}}} %\newcommand{\SP}{~} %\newcommand{\SPP}{~} %\newcommand{\homedir}{\mbox{$\sim$}} \newcommand{\Turn}{\(\turn\)} \newcommand{\And}{\(\wedge\)} \newcommand{\Or}{\(\vee\)} \newcommand{\Not}{\(\neg\)} \newcommand{\Forall}{\(\forall\)} \newcommand{\Exists}{\(\exists\)} \newcommand{\Mapsto}{\(\mapsto\)} %\parindent 0mm %\parskip 1mm \setcounter{sessioncount}{0} \title{HolBddLib} \date{} \begin{document} \maketitle \index{HolBddLib|(} This document describes {\tt HolBddLib}, a \HOL{} interface to an external BDD engine.\index{binary decision diagrams|see {HolBddLib}}\index{BDDs|see {HolBddLib}} \section{Introduction} The development of {\tt HolBddLib} has gone through two phases. The first phase consisted in experiments with different ways of linking higher order logic (HOL) terms to binary decision diagrams (BDDs). These are described in the paper {\it Reachability programming in HOL98 using BDDs\/} \cite{tphols2000-Gordon}. The first release of \t{HolBddLib}, now called Version~1, consisted of an ad hoc collection of tools developed for these experiments. One of the approaches we experimented with was based on a protected type of `BDD representation judgements', analogous to the LCF protected type of theorems. Positive results of Hasan Amjad \cite{Amjad:TPHOLs2001} have lead us to narrow attention to just this approach. \t{HolBddLib} Version~2, which is described here, provides a set of representation judgement rules as core infrastructure for building `fully-expansive' or `LCF-style' combinations of HOL theorem proving and BDD-based symbolic calculation algorithms. All higher level tools, such as model checkers, are programmed in ML as `derived rules'. The primitive inference rules for representation judgements are contained in the structure {\tt{PrimitiveBddRules}}. Several useful and example derived rules are in the structure {\tt{DerivedBddRules}}. Version~1 of {\tt{HolBddLib}} was more elaborate than Version~2 because it mixed together code from a number of experiments. In Version~1 there was a function, called {\texttt{termToBdd}}, that tried to represent a \HOL{} term as a BDD using a dynamically extendable global table mapping \HOL{} terms to BDDs. $\t{TermToBdd}$ constructed the BDD of a term $t$ using any BDDs of subterms of $t$ that were stored in the global table. {\tt{HolBddLib}} Version~2 has jettisoned this imperative style in favour of purely functional rules. Some of the ideas of BDD tables are likely to return in the future, but as contexts, similar to HOL simpsets, that are passed functionally, rather than as a single global state held in references. {\tt{HolBddLib}} Version~1 only supported a single variable ordering, held in a global variable map. In Version~2, each representation judgement carries its own variable ordering, so that local scopes are possible. For convenience, {\tt{DerivedBddRules}} provides a way of storing a default variable ordering in a global variable, but this is just a derived facility, not part of the kernel. {\tt{HolBddLib}} Version~2 adds assumptions to representation judgements analogous to assumptions of HOL theorems. This enables Coudert, Berthet and Madre simplification to be represented as a primitive rule (see the rule \t{BddSimplify} in Section~\ref{term-bdd-rules}). It also allows the term part of a representation judgements to be simplified using equations with assumptions (see the rule \t{BddEqMp} in Section~\ref{BddEqMp}). {\tt HolBddLib} uses J{\o}rn Lind-Nielsen's \Buddy{} package as a BDD engine. The interface from \Buddy{} to Moscow ML, called \Muddy, is due to Ken Friis Larsen and Jakob Lichtenberg, and is described in Section~\ref{muddy}. {\tt HolBddLib} is built on top of \Muddy{} and is described in Section~\ref{HolBddLib}. \subsection{Overview}\index{HolBddLib!overview} In the fully expansive (or `LCF style') approach, theorems are represented by an abstract type whose primitive operations are the axioms and inference rules of a logic. Theorem proving tools are implemented by composing together the inference rules using ML programs. This idea can be generalised to computing valid judgements that represent other kinds of information. In particular, consider judgements $(a,\rho,t,b)$, where $a$ is a set of boolean terms (assumptions) that are assumed true, $\rho$ represents a variable order, $t$ is a boolean term all of whose free variables are boolean and $b$ is a BDD. Such a judgement is valid if under the assumptions $a$, the BDD representing $t$ with respect to $\rho$ is $b$, and we will write \termbdd{a}{\rho}{t}{b} when this is the case. The derivation of `theorems' like \termbdd{a}{\rho}{t}{b} can be viewed as `proof' in the style of LCF by defining an abstract type \termbddty{} that models judgements $\termbdd{a}{\rho}{t}{b}$ analogously to the way the type $\ty{thm}$ models theorems $\vdash t$. The structure \t{HolBddLib} currently contains two main structures: \t{PrimitiveBddRules} which defines a protected type \termbddty and rules for generating values of this type, and \t{DerivedBddRules} that contains derived rules for performing simple fixed-point calculations. There is also a theory \t{MachineTransitionTheory} containing the theorems on reachability and fixed points needed by the derived rules, and two small subsidiary structures \t{Varmap} and \t{PrintBdd}. \subsection{Relation to the Voss system}\label{related}\index{HolBddLib!Voss, relation to} The Voss system \cite{SegerVoss} has strongly influenced and inspired the ideas described here. Voss consists of a lazy ML-like functional language, called FL, with BDDs as a built-in datatype. Quantified boolean formulae can be input and are parsed to BDDs. The normal boolean operations $\neg$, $\wedge$, $\vee$, $\equiv$, $\forall$, $\exists$ are interpreted as BDD operations. Algorithms for model checking are easily programmed. Joyce and Seger interfaced an early HOL system (HOL88) to Voss and in a pioneering paper showed how to verify complex systems by a combination of theorem proving deduction and symbolic trajectory evaluation (STE) \cite{JoyceSeger}. The HOL-Voss system integrates HOL88 deduction with BDD computations. BDD tools are programmed in FL and can then be invoked by HOL-Voss tactics, which can make external calls into the Voss system, passing subgoals via a translation between the HOL88 and Voss term representations. In later work Lee, Seger and Greenstreet \cite{LeeGreenstreetSeger} showed how various optimised BDD algorithms could be programmed in FL. The early experiments with HOL-Voss suggested that a lighter theorem proving component was sufficient, since all that was really needed was a way of combining results obtained from STE. A system based on this idea, called VossProver, was developed by Carl Seger and his student Scott Hazelhurst. It provides operations in FL for combining assertions generated by Voss using proof rules corresponding to the laws of composition of the temporal logic assertions verified by STE \cite{hazelhurst-kropfbook-97}. VossProver was used to verify impressive integer and floating-point examples (see the DAC98 paper by Aagaard, Jones and Seger \cite{aagaard-dac-98} for further discussion and references). After Seger and Aagaard moved to Intel, the development of the Voss and VossProver systems evolved into a new system called Forte. Only partial details of this are in the public domain \cite{oleary-itj-99,aagaard-tphols-99}, but a key idea is that FL is used both as a specification language and as an LCF-style metalanguage. The connection between symbolic trajectory evaluation and proof is obtained via a tactic {\tt{Eval\_tac}} that converts the result of executing an FL program performing STE into a theorem in the logic. Theorem proving in Forte is used both to split goals into smaller subgoals that are tractable for model checking, and to transform formulae so that they can be checked more efficiently. The combination of \HOL{} and \Buddy{} in Version~1 of {\tt{HolBddLib}} provides a somewhat similar programming environment to Voss's FL (though with eager rather than lazy evaluation and no special support for STE). \Buddy{} provides BDD operations corresponding to $\neg$, $\wedge$, $\vee$, $\equiv$, $\forall$, $\exists$ and the \HOL{} term parser plus \ml{termToBdd} provides a way of using these to create BDDs from logical terms. Voss enables efficient computations on BDDs using functional programming. So does \ml{HolBddLib}. However, in addition it allows FL-like BDD programming in ML to be intimately mixed with \HOL{} deduction, so that, for example, theorem proving tools (e.g.~simplifiers) can be directly applied to terms to optimise them for BDD purposes (e.g.~disjunctive partitioning). This is in line with future developments discussed by Joyce and Seger \cite{JoyceSeger} and it appears that the Forte system has similar capabilities. {\tt{HolBddLib}} Version~2 provides a less developed interactive programming environment than Version~1. It is more oriented to providing a clean and simple API allowing implementers to create their own `fully-expansive' combinations of model checking and theorem proving. Such a combination could be a Voss-like verification platform. \section{\Muddy}\label{muddy} \Muddy{} is the Moscow ML interface to \Buddy{}. It provides ML functions for constructing and manipulating BDDs via three structures: \begin{itemize} \item \t{bdd} defines the ML type \t{bdd} representing BDDs and associated operations derived from \Buddy{}; \item \t{fdd} provides support for blocks of BDD variables used to encode values representing elements of finite domains; \item \t{bvec} provides support for Boolean vectors. \end{itemize} The current \HolBuddy{} system only uses \t{bdd} and so the documentation of \t{fdd} and \t{bvec} provided here is minimal (see Sections~\ref{fdd} and \ref{bvec} below). \subsection{Initialisation, termination and tuning sessions}\label{init}\index{HolBddLib!session!initialisation}\index{HolBddLib!session!termination} The \Buddy{} package must be initialised before any BDD operations are done. Initialisation is done with the ML function \begin{verbatim} init : int -> int -> unit \end{verbatim}\index{HolBddLib!ML bindings!{init}@\ml{init}} Evaluating $\t{init}~m~n$ initialises \Buddy{} with $m$ nodes in the nodetable and a cachesize of $n$. The library \t{HolBddLib} (Section~\ref{HolBddLib}) initialises the nodetable to 1000000 and cachesize to be 10000. The following is a quotation from the \Buddy{} documentation \cite{BuDDy}. \vspace*{-2mm} {\baselineskip8pt\begin{quote}\footnotesize Good initial values are \smallskip \begin{tabular}{lrr} {\bf Example} & {\bf nodenum} & {\bf cachesize} \\ Small test examples & 1000 & 100\\ Small examples & 10000 & 1000 \\ Medium sized examples & 100000 & 10000\\ Large examples & 1000000 & 10000 \end{tabular} \smallskip Too few nodes will only result in reduced performance and this increases the number of garbage collections needed. If the package needs more nodes, then it will automatically increase the size of the node table. \end{quote}} The initial number of nodes is not critical for any BDD operation as the table will be resized whenever there are too few nodes left after a garbage collection. But it does have some impact on the efficiency of the operations. The function \begin{verbatim} done : unit -> unit \end{verbatim}\index{HolBddLib!ML bindings!{done}@\ml{done}} frees all memory used by \Buddy{} and resets the package to its initial state. The functions \t{init} and \t{done} should only be called once per session. The function \begin{verbatim} isRunning : unit -> bool \end{verbatim}\index{HolBddLib!ML bindings!{isRunning}@\ml{isRunning}} tests whether \Buddy{} is running (i.e.~\t{init} has been called and \t{done} has not been called). It is useful for checking if initialialisation is needed. The functions \t{init} and \t{done} should only be called once in a session. Statistical information from \Buddy{} is available using the function \t{stats} \begin{verbatim} stats : unit -> {produced : int, nodenum : int, maxnodenum : int, freenodes : int, minfreenodes : int, varnum : int, cachesize : int, gbcnum : int} \end{verbatim}\index{HolBddLib!ML bindings!{stats}@\ml{stats}} The meaning of the values of the various named fields in the record returned by evaluating \t{stats()} are \medskip \begin{tabular}{|l|l|} \hline {\bf{Field name}}& {\bf{Meaning}} \\ \hline\hline \t{produced} & total number of new nodes ever produced \\ \hline \t{nodenum} & currently allocated number of BDD nodes \\ \hline \t{maxnodenum} & user defined maximum number of BDD nodes \\ \hline \t{freenodes} & number of currently free BDD nodes \\ \hline \t{minfreenodes} & minimum number of nodes left after a BDD garbage collection \\ \hline \t{varnum} & number of defined BDD variables \\ \hline \t{cachesize} & number of cache entries \\ \hline \t{gbcnum} & number of BDD garbage collections done \\ \hline \end{tabular} \medskip The management of the node table and internal caches can be tuned using the following functions \begin{verbatim} setMaxincrease : int -> int setCacheratio : int -> int \end{verbatim}\index{HolBddLib!ML bindings!{setMaxincrease}@\ml{setMaxincrease}}\index{HolBddLib!ML bindings!{setCacheratio}@\ml{setCacheratio}} Evaluating \t{setMaxincrease~$n$} tells \Buddy{} that the maximum of new nodes added when doing an expansion of the nodetable should be $n$. The previous maximum is returned. Evaluating \t{setCacheratio~$n$} sets the cache ratio to $n$. For example, if $n$ is $4$ then the internal caches will a quarter the size of the nodetable. \subsection{BDDs representing {\t{true}} and {\t{false}}}\index{HolBddLib!BDD!constants} The atomic BDDs representing the two truthvalues are bound to the ML identifiers \t{TRUE} and \t{FALSE}, both of type \t{bdd}. Functions for mapping from ML Booleans to BDDs and vice versa are, respectively \begin{verbatim} fromBool : bool -> bdd toBool : bdd -> bool \end{verbatim}\index{HolBddLib!ML bindings!{fromBool}@\ml{fromBool}}\index{HolBddLib!ML bindings!{toBool}@\ml{toBool}} The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE. It raises the exception \t{Domain} on non-atomic BDDs. \begin{verbatim} equal : bdd -> bdd -> bool \end{verbatim}\index{HolBddLib!ML bindings!{equal}@\ml{equal}} tests the equality of two BDDs. Thus \t{TRUE} is \t{equal} to \t{fromBool(true)} and \t{FALSE} is \t{equal} to \t{fromBool(false)}. \subsection{Variables}\index{HolBddLib!BDD!variables} In \Buddy{}, BDD variables are encoded as integers (type \t{int} in ML) and the BDD variable ordering is the numerical ordering. Thus to build a BDD to represent a \HOL{} term with a particular variable ordering it is necessary to map \HOL{} variables to integers so that the numerical order corresponds to the desired variable order. The number of variables in use must be declared using \begin{verbatim} setVarnum : int -> unit \end{verbatim}\index{HolBddLib!ML bindings!{setVarnum}@\ml{setVarnum}} Evaluating $\t{setVarnum}~n$ declares that the $n$ variables $0$, $1$, $\ldots$ , $n{-}1$ are available for use. The number of variables can be increased dynamically during a session by calling \t{setVarnum} with a larger number. The number of variables cannot be decreased dynamically. The function \begin{verbatim} getVarnum : unit -> int \end{verbatim}\index{HolBddLib!ML bindings!{getVarnum}@\ml{getVarnum}} returns the number of variables in use (i.e.~the argument of the last application of \t{setVarnum}). The function \begin{verbatim} ithvar : int -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{ithvar}@\ml{ithvar}} maps an ML integer to a BDD that consists of just the variable corresponding to the integer and \begin{verbatim} nithvar : int -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{nithvar}@\ml{nithvar}} maps an integer to the BDD representing the negation of the variable. Note that evaluating $\t{ithvar}~n$ or $\t{nithvar}~n$ will raise the exception \t{Fail} (with string argument \texttt{"Unknown variable"}) if $n$ has not been declared as in use, i.e.~if $\t{setVarnum}~m$ has not been previously evaluated for some $m$ greater than $n$. \subsection{Sets of variables and quantification}\label{varSet}\index{HolBddLib!BDD!quantification} \Buddy{} provides operations on BDDs for quantifying with respect to sets of variables. The module \t{bdd} provides a type \t{varSet} to represent such sets with, respectively, a constructor and two destructors: \begin{verbatim} makeset : int list -> varSet scanset : varSet -> int vector fromSet : varSet -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{makese}@\ml{makese}}\index{HolBddLib!ML bindings!{scanset}@\ml{scanset}}\index{HolBddLib!ML bindings!{fromSet}@\ml{fromSet}} The destructor \t{scanset} returns a vector of the variables in the set and the destructor \t{fromSet} returns a BDD representing the conjunction of the variables in the set. The following functions quantify BDDs with respect to sets of variables: \begin{verbatim} forall : varSet -> bdd -> bdd exist : varSet -> bdd -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{forall}@\ml{forall}}\index{HolBddLib!ML bindings!{exist}@\ml{exist}} \subsection{Assignments, composition, replacement and restriction}\label{replace}\index{HolBddLib!BDD!assignments}\index{HolBddLib!BDD!composition}\index{HolBddLib!BDD!replacement}\index{HolBddLib!BDD!restriction} \Muddy{} provides a function for general purpose simultaneous substitution of arbitrary BDDs for variables in a given BDD (\t{veccompose}). It also provides and three optimised special cases: substituting for a single variable (\t{compose}), renaming variables (\t{replace}) and substituting with boolean constants (\t{restrict}). The operation \t{veccompose} performs the simultaneous substitution of BDDs for variables in a BDD. The argument of \t{veccompose} is a value of type \t{composeSet}\index{HolBddLib!ML bindings!{composeSet}@\ml{composeSet}} (created with a constructor \t{composeSet}) that specifies a list if pairs \t[(($n_1$,$b_1$),$\ldots$,, where BDD variable $n$ is to be pre \begin{verbatim} composeSet : (int * bdd) list -> composeSet veccompose : composeSet -> bdd -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{veccompose}@\ml{veccompose}} A single variable can be replaced with a BDD using \begin{verbatim} compose : bdd -> bdd -> int -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{compose}@\ml{compose}} Evaluating \t{compose~$b_1$~$b_2$~$n$} substitutes $b_2$ for the variable $n$ in $b_1$. Variables can be renamed using the function \t{replace} that takes an argument of type \t{pairSet}\index{HolBddLib!ML bindings!{pairSet}@\ml{pairSet}} representing sets of pairs of variables (with constructor \t{makepairSet}) \begin{verbatim} makepairSet : (int * int)list -> pairSet replace : bdd -> pairSet -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{makepairSet}@\ml{makepairSet}}\index{HolBddLib!ML bindings!{replace}@\ml{replace}} Evaluating \t{makepairSet[($x_1$,$x_1'$), $\ldots$ , ($x_n$,$x_n'$)]} creates a set of pairs specifying that $x_i'$ be substituted for $x_i$ (for $1\leq i\leq n$). A renaming with \t{replace} will fail if it would result in distinct variables being identified (i.e.~if the shape of the BDD would change). BDDs can be restricted by instantiating variables to {\t{TRUE}} or {\t{FALSE}} using the function \t{restrict} that takes as argument a value of type \t{assignment}\index{HolBddLib!ML bindings!{assignment}@\ml{assignment}} (which has a constructor \t{assignment} and destructor \t{getAssignment}). \begin{verbatim} assignment : (int * bool)list -> assignment getAssignment : assignment -> (int * bool) list restrict : bdd -> assignment -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{restrict}@\ml{restrict}}\index{HolBddLib!ML bindings!{assignment}@\ml{assignment}}\index{HolBddLib!ML bindings!{getAssignment}@\ml{getAssignment}} \noindent Evaluating \t{assignment[($v_1$,$t_1$), $\ldots$ , ($v_n$,$t_n$)]} creates an assignment specifying that each $v_i$ be instantiated to $\t{fromBool(}t_i\t{)}$ (for $1{\leq}i{\leq}n$). \subsection{Finding satisfying assignments}\index{HolBddLib!BDD!satisfying assignments} An assignment satisfying a BDD can be computed via \Buddy{} using \begin{verbatim} satone : bdd -> assignment \end{verbatim}\index{HolBddLib!ML bindings!{makeset}@\ml{makeset}}\index{HolBddLib!ML bindings!{scanset}@\ml{scanset}}\index{HolBddLib!ML bindings!{fromSet}@\ml{fromSet}} The exception \t{Domain} is raised if the argument to \t{satone} is unsatisfiable. Alternatively, a model can be computed by an ML program such as: \begin{verbatim} val findSat = let fun findSatAux bdd = if bdd.equal bdd bdd.TRUE then [] else if bdd.equal bdd bdd.FALSE then raise Domain else ((bdd.var bdd,true) :: findSatAux(bdd.high bdd) handle Domain => (bdd.var bdd, false) :: findSatAux(bdd.low bdd)) in assignment o findSatAux end; \end{verbatim} The functions \t{satone} and \t{findSat} do not necessarily find the same satisfying assignment, if more than one exists. Also, \t{findSat} stops when it has found enough variable bindings to satisfy the BDD, so may not return an assignment giving values to all the variables. \subsection{Boolean operations on BDDs}\label{app}\index{HolBddLib!BDD!boolean operations} The structure \t{bdd} introduces a type \t{bddop} corresponding to Boolean operations on BDDs. The ML function \begin{verbatim} apply : bdd -> bdd -> bddop -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{apply}@\ml{apply}} applies a BDD operation to BDD values. \Buddy{} provides functions for calculating in a single step the result of performing a Boolean operation and then quantifying the result with respect to several variables. \begin{verbatim} appall : bdd -> bdd -> bddop -> varSet -> bdd appex : bdd -> bdd -> bddop -> varSet -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{appall}@\ml{appall}}\index{HolBddLib!ML bindings!{appex}@\ml{appex}} The function \t{appall} universally quantifies the result of the Boolean operation and \t{appex} existentially quantifies it. \Muddy{} provides ten operations of type \t{bddop} and for each of these an ML infix, pre-defined using \t{apply}, of type \t{bdd~*~bdd~->~bdd}. \begin{center} \begin{tabular}{|l||l|l|} \hline \t{bddop}\index{HolBddLib!ML bindings!{bddop}@\ml{bddop}} & \t{bdd~*~bdd~->~bdd} & Result of applying to $(b_1,b_2)$\\ \hline\hline \t{And}\index{HolBddLib!ML bindings!{And}@\ml{And}} & \t{AND} & $b_1\wedge b_2$ \\ \hline \t{Nand}\index{HolBddLib!ML bindings!{Nand}@\ml{Nand}} & \t{NAND} & $\neg(b_1\wedge b_2)$ \\ \hline \t{Or}\index{HolBddLib!ML bindings!{Or}@\ml{Or}} & \t{OR} & $b_1\vee b_2$ \\ \hline \t{Nor}\index{HolBddLib!ML bindings!{Nor}@\ml{Nor}} & \t{NOR} & $\neg(b_1\vee b_2)$ \\ \hline \t{Biimp}\index{HolBddLib!ML bindings!{Biimp}@\ml{Biimp}} & \t{BIIMP} & $b_1= b_2$ \\ \hline \t{Xor}\index{HolBddLib!ML bindings!{Xor}@\ml{Xor}} & \t{XOR} & $\neg(b_1=b_2)$ \\ \hline \t{Imp}\index{HolBddLib!ML bindings!{Imp}@\ml{Imp}} & \t{IMP} & $b_1\imp b_2$ \\ \hline \t{Invimp}\index{HolBddLib!ML bindings!{Invimp}@\ml{Invimp}} & \t{INVIMP} & $b_2\imp b_1$ \\ \hline \t{Lessth}\index{HolBddLib!ML bindings!{Lessth}@\ml{Lessth}} & \t{LESSTH} & $\neg b_1\wedge b_2$ \\ \hline \t{Diff}\index{HolBddLib!ML bindings!{Diff}@\ml{Diff}} & \t{DIFF} & $b_1\wedge \neg b_2$ \\ \hline \end{tabular}\label{bddops} \end{center} \Muddy{} also provides a unary negation operator and ternary conditional operator. \begin{verbatim} NOT : bdd -> bdd ITE : bdd -> bdd -> bdd -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{NOT}@\ml{NOT}}\index{HolBddLib!ML bindings!{ITE}@\ml{ITE}} $\t{NOT}~b$ is the BDD corresponding to `$\neg b$' and $\t{ITE}~b~b_1~b_2$ is the BDD corresponding to `$if~b~then~b_1~else~b_2$'. \subsection{Inspecting and counting nodes and states}\index{HolBddLib!BDD!nodes}\index{HolBddLib!BDD!states} The integer labelling a BDD node and the BDDs corresponding to the high (i.e.~{\t{true}}) and low (i.e.~{\t{false}}) nodes are obtained, respectively, with \begin{verbatim} var : bdd -> int high : bdd -> bdd low : bdd -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{var}@\ml{var}}\index{HolBddLib!ML bindings!{high}@\ml{high}}\index{HolBddLib!ML bindings!{low}@\ml{low}} Thus if $b$ is the BDD of ``${\it{if}}~x~{\it{then}}~t_1~{\it{else}}~t_2$'' then $\t{var}~b$ will return the number representing variable $x$, $\t{high}~b$ will return the BDD of $t_1$ and $\t{low}~b$ will return the BDD of $t_2$. Note that \t{var}, \t{high} and \t{low} raise an exception if applied to \t{TRUE} or \t{FALSE}. The entire \Buddy{} node table of a BDD can be copied into ML using \begin{verbatim} nodetable : bdd -> int * (int * int * int)vector \end{verbatim}\index{HolBddLib!ML bindings!{nodetable}@\ml{nodetable}} The integer returned as the first component of the pair is a pointer (starting from 0) into the second component, a vector of node descriptors. This pointer points to the root node. Each node descriptor is a triple of integers $(v,l,h)$, where $v$ is the node label (i.e.~a number representing a variable), $l$ points to the low ({\t{false}}) node in the vector and $h$ points to the high ({\t{true}}) node. The first two nodes in the vector are special: they represent {\t{true}} and {\t{false}}, respectively, and arbitrarily have the structure $(0,0,0)$. The number of nodes in a BDD is computed by the function \begin{verbatim} nodecount : bdd -> int \end{verbatim}\index{HolBddLib!ML bindings!{nodecount}@\ml{nodecount}} This could be defined by \begin{verbatim} fun nodecount bdd = Vector.length(snd(nodetable bdd)); \end{verbatim} However, \t{nodecount} defined this way is likely to run out of space on large BDDs (since it involves copying the argument BDD from \Buddy's representation into an ML vector). Thus the ML function provided by \Muddy{} invokes \Buddy's \t{nodecount} function directly and so is space-efficient. 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 function \begin{verbatim} satcount : bdd -> real \end{verbatim}\index{HolBddLib!ML bindings!{satcount}@\ml{satcount}} The answer is exact until the result is too big to be represented as a Moscow ML integer. Real numbers are used so that results can be returned when this happens. The function \begin{verbatim} support : bdd -> varSet \end{verbatim}\index{HolBddLib!ML bindings!{support}@\ml{support}} gives the variables that a BDD depends on. An application is to define a function that counts the number of valuations of a BDD using \t{satcount}. \begin{verbatim} statecount : bdd -> real \end{verbatim}\index{HolBddLib!ML bindings!{statecount}@\ml{statecount}} The definition of \t{statecount} is \begin{verbatim} fun statecount bdd = let val sat = satcount bdd val total = Real.fromInt(getVarnum()) val sup = scanset(support bdd) val numsup = Real.fromInt(Vector.length sup) val free = total - numsup in if equal bdd TRUE then 0.0 else sat / Math.pow(2.0, free) end \end{verbatim} % If a BDD is representing a set of states, then \t{statecount} gives the number of states in the set (hence the name). \subsection{Coudert, Berthet \& Madre simplification}\index{HolBddLib!BDD!simplification} The ML function \begin{verbatim} simplify : bdd -> bdd -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{simplify}@\ml{simplify}} simplifies its second argument under the assumption that the first argument is true. Thus evaluating \t{simplify~$b_1$~$b_2$} results in a BDD $b_2'$, hopefully simpler than $b_2$, such that $b_1 \Rightarrow (b_2 = b_2')$ or, equivalently, \mbox{$b_1 \wedge b_2 = b_1 \wedge b_2'$}. More precisely, the relationship between $b_1$, $b_2$ and $b_2'$ is that the BDD \t{IMP($b_1$,BIIMP($b_2$,$b_2'$))} is the BDD \t{TRUE} (or, equivalently, that \t{AND($b_1$,$b_2$)} and \t{AND($b_1$,$b_2'$)} are \t{equal}, i.e.~the same BDD). For more details see Henrik Reif Andersen's lecture notes on BDDs \cite{HenrikNotes}, where the algorithm underlying \t{simplify} is described and attributed to a paper by Coudert, Berthet and Madre \cite{CoudertBerthetMadre}. \subsection{Saving, hashing and printing BDDs}\label{printing}\index{HolBddLib!BDD!saving}\index{HolBddLib!BDD!hashing}\index{HolBddLib!BDD!printing} BDDs can be saved on disk with the functions \begin{verbatim} bddSave : string -> bdd -> unit bddLoad : string -> bdd \end{verbatim}\index{HolBddLib!ML bindings!{bddSave}@\ml{bddSave}}\index{HolBddLib!ML bindings!{bddLoad}@\ml{bddLoad}} The string argument is a file name. \Buddy{} provides two ways of printing BDDs: (i) as the set of paths from the root node to the {\it{true}} node and (ii) to the format used by the \t{dot} graph drawing program\footnote{\texttt{http://www.research.att.com/sw/tools/graphviz/}}. The function \begin{verbatim} hash : bdd -> int \end{verbatim}\index{HolBddLib!ML bindings!{hash}@\ml{hash}} hashes a bdd to an integer. The functions for printing BDDs are; \begin{verbatim} printset : bdd -> unit printdot : bdd -> unit fnprintset : string -> bdd -> unit fnprintdot : string -> bdd -> unit \end{verbatim}\index{HolBddLib!ML bindings!{printset}@\ml{printset}}\index{HolBddLib!ML bindings!{printdot}@\ml{printdot}}\index{HolBddLib!ML bindings!{fnprintset}@\ml{fnprintset}}\index{HolBddLib!ML bindings!{fnprintdot}@\ml{fnprintdot}} \t{printset} and \t{printdot} print to standard output, whilst \t{fnprintset} and \t{fnprintdot} print to a file with the supplied name. \t{printset} and \t{fnprintset} print out a sequence of paths, each one having the form \smallskip ~$\t{}}$ \smallskip where the $n_0$, $\ldots$ , $n_l$ after the colon (\t{:}) are \t{0} or \t{1} and indicate that the next node in the path is reached by following the low ({\t{false}}) or high ({\t{true}}) pointer, respectively. For example, evaluating \smallskip ~\t{printset~(AND(ithvar~0,~OR(ithvar~1,~NOT(ithvar~2))))} \smallskip results in \smallskip ~\t{<0:1,~1:0,~2:0><0:1,~1:1>} \smallskip which is best understood by looking at the diagram of the BDD drawn by \t{dot} that appears below. To illustrate printing to \t{dot} format, the same BDD can be printed to a file \t{ex} by evaluating \smallskip ~\t{fnprintdot~"ex"~(AND(ithvar~0,~OR(ithvar~1,~NOT(ithvar~2))))} \smallskip executing ~\t{dot~-Tps~ex~>~ex.ps} (in Unix) results in the following Postscript diagram of a BDD \begin{center} \includegraphics[width=3cm, height=5cm]{figs/ex} \end{center} \subsection{Dynamic variable reordering}\index{HolBddLib!BDD!dynamic reordering} \Buddy{} provides functions for dynamic variable reordering using a variety of methods. See the \Buddy{} documentation \cite{BuDDy} for further details. The dynamic reordering types and functions provided in ML via \Muddy{} are in the structure \t{bdd} and are \begin{verbatim} eqtype fixed FIXED : fixed FREE : fixed addvarblock : varnum -> varnum -> fixed -> unit clrvarblocks : unit -> unit eqtype method WIN2 : method WIN2ITE : method SIFT : method SIFTITE : method RANDOM : method REORDER_NONE : method reorder : method -> unit autoReorder : method -> method autoReorderTimes : method -> int -> method getMethod : unit -> method getTimes : unit -> int disableReorder : unit -> unit enableReorder : unit -> unit varToLevel : varnum -> int varAtLevel : int -> varnum \end{verbatim} \subsection{The \Muddy{} structure \t{fdd}}\label{fdd}\index{HolBddLib!finite domains} The structure \t{fdd} provides functions for manipulating values of finite domains. Functions are provided to allocate blocks of BDD variables to represent integer values instead of only Booleans. Encoding is done with the least significant bits first in the BDD ordering. For example, if variables $v_0, v_1, v_2, v_3$ are used to encode $12$, then the encoding would yield $v_0=0$, $v_1=0$, $v_2=1$ and $v_3=1$. See the \Buddy{} documentation \cite{BuDDy} for further details. See the ML structure \t{fdd} for the \Buddy{} facilities provides in ML via \Muddy: \begin{verbatim} type fddvar extDomain : int list -> fddvar list clearAll : unit -> unit domainNum : unit -> int domainSize : fddvar -> int varNum : fddvar -> int vars : fddvar -> bdd.varnum list ithSet : fddvar -> bdd.varSet domain : fddvar -> bdd.bdd setPairs : (fddvar * fddvar) list -> bdd.pairSet \end{verbatim} \subsection{The \Muddy{} structure \t{bvec}}\label{bvec}\index{HolBddLib!BDD!vectors} The structure \t{bvec} provides tools for encoding integers as arrays of BDDs, where each BDD represents one bit of an expression. See the \Buddy{} documentation \cite{BuDDy} for further details. See the ML structure \t{bvec} for the \Buddy{} facilities provides in ML via \Muddy{}. \begin{verbatim} type bvec bvectrue : fdd.precision -> bvec bvecfalse : fdd.precision -> bvec con : fdd.precision -> int -> bvec var : fdd.precision -> bdd.varnum -> int -> bvec varfdd : fdd.fddvar -> bvec coerce : fdd.precision -> bvec -> bvec isConst : bvec -> bool getConst : bvec -> int lookupConst : bvec -> int option add : bvec * bvec -> bvec sub : bvec * bvec -> bvec mul : bvec * bvec -> bvec mulfixed : bvec * int -> bvec div : bvec * bvec -> bvec * bvec divfixed : bvec * int -> bvec * bvec divi : bvec * bvec -> bvec divifixed : bvec * int -> bvec modu : bvec * bvec -> bvec modufixed : bvec * int -> bvec shl : bvec -> bvec -> bdd.bdd -> bvec shlfixed : bvec -> int -> bdd.bdd -> bvec shr : bvec -> bvec -> bdd.bdd -> bvec shrfixed : bvec -> int -> bdd.bdd -> bvec lth : bvec * bvec -> bdd.bdd lte : bvec * bvec -> bdd.bdd gth : bvec * bvec -> bdd.bdd gte : bvec * bvec -> bdd.bdd equ : bvec * bvec -> bdd.bdd neq : bvec * bvec -> bdd.bdd \end{verbatim} \subsection{Storage allocation and garbage collection}\index{HolBddLib!BDD!garbage collection} \label{sec:technical-details} The heart of the \Muddy{} package is mostly stub code that mirrors the \Buddy{} API and takes care of translating C values into SML values and vice versa. The most tricky part is to make the \mosml{} garbage collector cooperate with the \Buddy{} garbage collector (we don't want either collector to try to collect the other's garbage). The cooperation is done by using the \emph{finalized values} facility of the \mosml{} runtime system. That is, whenever a \texttt{bdd} value is returned from the \Buddy{} library, \Muddy{} register it as an external root (via \verb+bdd_addref+) and wraps it into a finalized value. A finalized value, in the \mosml{} runtime system, is a pair where the first component is the \emph{destructor} (a function pointer) and the second component is the \emph{data} (typicaly a pointer). When the \mosml{} collector collect a finalized value it apply the destructor on the data. In the case of the \Muddy{} package the destructor is \verb+bdd_delref+ and the data is the node-index returned by \Buddy{}. Output showing the activation of the \Buddy{} garbage collector can be generated using the function \begin{verbatim} verbosegc : (string * string) option -> unit \end{verbatim}\index{HolBddLib!ML bindings!{verbosegc}@\ml{verbosegc}} Evaluating \t{verbosegc(SOME($pregc$,$postgc$))} instructs BuDDy to print $pregc$ when a BuDDy GC is initiated and print $postgc$ when the \Buddy{} GC is completed. \section{\t{HolBddLib}}\label{HolBddLib} \t{HolBddLib} currently consists of five modules \begin{enumerate} \item \t{Varmap} defines the ML type \t{varmap} that represents mappings, often denoted by $\rho$, from HOL variables to BDD variables; \item \t{PrintBdd} provides some rudimentary facilities for printing BDDs with respect to a varmap; \item \t{PrimitiveBddRules} defines the protected type \termbddty representing BDD representation judgements \termbdd{a}{\rho}{t}{b} with the semantics that under assumptions $a$, term $t$ is represented by BDD $b$ with respect to varmap $\rho$; \item \t{DerivedBddRules} defines some derived rules for computing the representation of the reachable states of a transition system, and also for finding shortest paths to states satisfying a given property; \item \t{MachineTransitionTheory} contains HOL reachability and fixedpoint theorems needed for the derived rules in \t{DerivedBddRules}. \end{enumerate} Executing \vspace*{-2mm} \begin{verbatim} load "HolBddLib"; \end{verbatim} \vspace*{-2mm} loades these five modules and initialises \Buddy{} with a nodesize of 1000000 and cachesize of 10000. If you want to perform your own \Buddy{} initialisation with different values, then instead of loading \t{HolBddLib}, load \t{bdd} and then call \t{bdd.init} with the parameters you want (see Section~\ref{init}). \subsection{The structure \ml{Varmap}}\label{Varmap}\index{HolBddLib!termbdd@\ml{term\_bdd}!varmaps} The type \t{varmap} is defined by \vspace*{-2mm} \begin{verbatim} type varmap = (string, int) Binarymap.dict \end{verbatim}\index{HolBddLib!ML bindings!{varmap}@\ml{varmap}} \vspace*{-2mm} Strings are the names of HOL boolean variables and the integers associated with them are the corresponding BDD variables. The following operations and predicates on varmaps are provided: \begin{verbatim} empty : varmap insert : string * int -> varmap -> varmap remove : string -> varmap -> varmap peek : varmap -> string -> int option dest : varmap -> (string * int) list eq : varmap * varmap -> bool size : varmap -> int extends : varmap -> varmap -> bool unify : varmap -> varmap -> varmap \end{verbatim} \index{HolBddLib!ML bindings!{Varmap.empty}@\ml{Varmap.empty}} \index{HolBddLib!ML bindings!{Varmap.insert}@\ml{Varmap.insert}} \index{HolBddLib!ML bindings!{Varmap.remove}@\ml{Varmap.remove}} \index{HolBddLib!ML bindings!{Varmap.peek}@\ml{Varmap.peek}} \index{HolBddLib!ML bindings!{Varmap.dest}@\ml{Varmap.dest}} \index{HolBddLib!ML bindings!{Varmap.eq}@\ml{Varmap.eq}} \index{HolBddLib!ML bindings!{Varmap.size}@\ml{Varmap.size}} \index{HolBddLib!ML bindings!{Varmap.extends}@\ml{Varmap.extends}} \index{HolBddLib!ML bindings!{Varmap.unify}@\ml{Varmap.unify}} with the semantics \bigskip \begin{tabular}{|l|l|} \hline \t{Varmap.empty} & the empty varmap \\ \hline \t{Varmap.insert} & add an entry \\ \hline \t{Varmap.remove} & delete an entry for a variable \\ \hline \t{Varmap.peek} & lookup the value of a variable \\ \hline \t{Varmap.dest} & convert to a list of pairs \\ \hline \t{Varmap.eq} & pointer equality of varmaps ({\it not} general equality) \\ \hline \t{Varmap.size} & number of entries \\ \hline \t{Varmap.extends} & test if first argument included in second argument\\ \hline \t{Varmap.unify} & compute smallest varmap that extends both arguments\\ \hline \end{tabular} \subsection{The structure \ml{PrintBdd}}\label{PrintBdd}\index{HolBddLib!termbdd@\ml{term\_bdd}!printing} \t{PrintBdd} builds on top of \Muddy's support for drawing BDDs using the \t{dot} program (see Section~\ref{printing}). Three functions are provided. \begin{verbatim} dotBdd : string -> string -> bdd -> bdd dotLabelledTermBdd : string -> string -> term_bdd -> unit dotTermBdd : term_bdd -> unit \end{verbatim} \index{HolBddLib!ML bindings!{dotBdd}@\ml{dotBdd}} \index{HolBddLib!ML bindings!{dotLabelledTermBdd}@\ml{dotLabelledTermBdd}} \index{HolBddLib!ML bindings!{dotTermBdd}@\ml{dotTermBdd}} \begin{description} \item[$\t{dotBdd}~file~label~bdd$]\mbox{}\\ prints the BDD $bdd$ to $file$\t{.dot} with the label being the string $label$. The BDD variables are printed as the numbers used by \Buddy{}. The \t{dot} program is then invoked to create a postscript file $file$\t{.ps}. The argument BDD is returned. \item[$\t{dotLabelledTermBdd}~file~label~tb$]\mbox{}\\ prints the BDD part of \termbddty $tb$ with the nodes labelled with the variables specified in the varmap part of $tb$. A file $file$\t{.ps} is created, and the BDD is labelled with the string $label$. \item[$\t{dotTermBdd}~tb$]\mbox{}\\ prints the BDD part of \termbddty $tb$ with the nodes labelled with the variables specified in the varmap part of $tb$. A file \t{ScratchBdd.ps} is created, and the BDD is labelled by default with a representation of the term part of $tb$. The default labels can be suppressed (i.e. set to be always the empty string) by assigning \t{false} to the global reference \t{dotTermBddFlag}. \end{description} \subsection{The structure \t{PrimitiveBddRules}}\label{PrimitiveBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!primitive rules} The structure \ml{PrimitiveBddRules} defines the type \termbddty{} by \vspace*{-2mm} \begin{verbatim} type assums = term HOLset.set; datatype term_bdd = TermBdd of assums * varmap * term * bdd; \end{verbatim}\index{HolBddLib!ML bindings!termbdd@\ml{term\_bdd}}\index{HolBddLib!ML bindings!{assums}@\ml{assums}} \vspace*{-2mm} The constructor \t{TermBdd} is not exported, so the only way to construct values of type \termbddty is using the following inference rules (which are described in more detail in the rest of this section). \begin{verbatim} BddExtendVarmap : varmap->term_bdd->term_bdd BddFreevarsContractVarmap : term->term_bdd->term_bdd BddSupportContractVarmap : term->term_bdd->term_bdd BddVar : bool->varmap->term->term_bdd BddCon : bool->varmap->term_bdd BddNot : term_bdd->term_bdd BddIte : term_bdd*term_bdd*term_bdd->term_bdd BddOp : bddop*term_bdd*term_bdd->term_bdd BddForall : term list->term_bdd->term_bdd BddExists : term list->term_bdd->term_bdd BddAppall : term list->bddop*term_bdd*term_bdd->term_bdd BddAppex : term list->bddop*term_bdd*term_bdd->term_bdd BddCompose : term_bdd*term_bdd->term_bdd->term_bdd BddListCompose : (term_bdd*term_bdd)list->term_bdd->term_bdd BddRestrict : (term_bdd*term_bdd)list->term_bdd->term_bdd BddReplace : (term_bdd*term_bdd)list->term_bdd->term_bdd BddEqMp : thm->term_bdd->term_bdd BddSimplify : term_bdd*term_bdd->term_bdd BddFindModel : term_bdd->term_bdd \end{verbatim} Destructor functions \t{dest\_term\_bdd}, \t{getAssums}, \t{getVarmap}, \t{getTerm} and \t{getBdd} for values of type \termbddty are described in Section~\ref{misc} There is also a single oracle function \t{BddThmOracle} that derives the HOL theorem $a \vdash t$ from the representation judgement \termbdd{a}{\rho}{t}{\ml{TRUE}} (details are in Section~\ref{oracle}). Many of the rules assume that the varmaps in their \termbddty arguments are all equal. To apply these rules to hypotheses with different varmaps it may be possible to use \t{BddExtendVarmap}, \t{BddFreevarsContractVarmap} or \t{BddSupportContractVarmap} to make the varmaps equal. It is expected that derived rules to enable judgements with different varmaps to be combined will be implemented, however, as the soundness conditions for these are potentially subtle, such rules have not been included in the `trusted kernel'. Currently we have no formal treatment of notions of soundness or completeness for the rules in \t{PrimitiveBddRules}, though this is being thought about. We think the rules are `obviously sound', but such intuitions are known to be unreliable! Our intuition about completeness is weaker: it is probable that as more experience with derived rules is obtained, the need for additional primitive rules will appear. Support for `local scopes' (combining judgements with different variable orders) is an area that may reveal incompleteness in the current rules. \subsection{Rules for generating representation judgements}\label{term-bdd-rules} The notation $a_1 \cup a_2$ denotes the union of $a_1$ and $a_2$ Assumptions of representation judgements are identified up to $\alpha$-conversion (as are assumptions of HOL theorems). The implementation is $a_1 \cup a_2~=~\t{HOLset.union}~a_1~a_2$. The empty set of assumptions is denoted by \emptyass, a set of assumptions containing terms $t_1, \ldots ,t_n$ is denoted by $\setass{t_1, \ldots ,t_n}$ and $\termbdd{\emptyass}{\rho}{t}{b}$ is abbreviated to $\termbdd{}{\rho}{t}{b}$. \subsection{Extending and contracting the varmap} \newsavebox\BddExtendVarmap \begin{lrbox}\BddExtendVarmap \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddExtendVarmap : varmap -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} {\t{\footnotesize Varmap.extends}}~\rho_1~\rho_2 \qquad \termbdd{a}{\rho_1}{t}{b} \\ \hline \termbdd{a}{\rho_2}{t}{b} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddExtendVarmapError} if $\rho_2$ doesn not extend $\rho_1$ \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddExtendVarmap}}\index{HolBddLib!ML bindings!{BddExtendVarmap}@\ml{BddExtendVarmap}} \bigskip \newsavebox\BddFreevarsContractVarmap \noindent\begin{lrbox}\BddFreevarsContractVarmap \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddFreevarsContractVarmap : term -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a}{\rho}{t}{b} \qquad \mbox{$v$ not free in $t$} \\ \hline \termbdd{a}{({\texttt{\footnotesize{Varmap.remove~"}}}v{\texttt{\footnotesize{"}}}~\rho)}{t}{b} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddFreevarsContractVarmapError} if $v$ not free in $t$ \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddFreevarsContractVarmap}}\index{HolBddLib!ML bindings!{BddFreevarsContractVarmap}@\ml{BddFreevarsContractVarmap}} \bigskip \newsavebox\BddSupportContractVarmap \noindent\begin{lrbox}\BddSupportContractVarmap \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddSupportContractVarmap : term -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a}{\rho}{t}{b} \qquad \mbox{$\rho(v)$ doesn't occur in $b$} \\ \hline \termbdd{a}{({\texttt{\footnotesize{Varmap.remove~"}}}v{\texttt{\footnotesize{"}}}~\rho)}{t}{b} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddSupportContractVarmapError} if $\rho(v)$ not in the support of $b$ \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddSupportContractVarmap}}\index{HolBddLib!ML bindings!{BddSupportContractVarmap}@\ml{BddSupportContractVarmap}} \subsection{Variables and constants} \newsavebox\BddVar \begin{lrbox}\BddVar \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddVar : bool -> varmap -> term -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \begin{array}{c} \rho(v)=n \\ \hline \termbdd{}{\rho}{v}{{\t{\footnotesize ithvar}}~n} \end{array} ~{\t{\footnotesize BddVar~true}} \\[8mm] \begin{array}{c} \rho(v)=n \\ \hline \termbdd{}{\rho}{\neg v}{{\t{\footnotesize nithvar}}~n} \end{array}~ {\t{\footnotesize BddVar~false}} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddVarError} if $v$ not in the domain of $\rho$ \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddVar}}\index{HolBddLib!ML bindings!{BddVar}@\ml{BddVar}} \bigskip \newsavebox\BddCon \noindent\begin{lrbox}\BddCon \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddCon : bool -> varmap -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \begin{array}{c} \\ \hline \termbdd{}{\rho}{{\t{\footnotesize T}}}{{\t{\footnotesize TRUE}}} \end{array} ~{\t{\footnotesize BddCon~true}} \\[8mm] \begin{array}{c} \\ \hline \termbdd{}{\rho}{{\t{\footnotesize F}}}{{\t{\footnotesize FALSE}}} \end{array}~ {\t{\footnotesize BddCon~false}} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Always succeeds \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddCon}}\index{HolBddLib!ML bindings!{BddCon}@\ml{BddCon}} \subsection{Boolean operations} \newsavebox\BddNot \begin{lrbox}\BddNot \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddNot : term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a}{\rho}{t}{b} \\ \hline \termbdd{a}{\rho}{\neg t}{{\t{\footnotesize NOT}}~b} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Always succeeds \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddNot}}\index{HolBddLib!ML bindings!{BddNot}@\ml{BddNot}} \bigskip \newsavebox\BddIte \noindent\begin{lrbox}\BddIte \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddIte : term_bdd * term_bdd * term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a}{\rho}{t}{b} \qquad \termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2} \\ \hline \termbdd{a \cup a_1 \cup a_2}{\rho}{\mbox{\t{\footnotesize (if~$t$~then~$t_1$~else~$t_2$)}}}{{\t{\footnotesize ITE}}~b~b_1~b_2} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises {\t{\footnotesize BddIteError}} if the varmaps of the hypotheses are not all pointer equal \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddIte}}\index{HolBddLib!ML bindings!{BddIte}@\ml{BddIte}} \bigskip \newsavebox\BddOp \noindent\begin{lrbox}\BddOp \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddOp : bddop * term_bdd * term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2} \\ \hline \termbdd{a_1\cup a_2}{\rho}{{\t{\footnotesize (termApply}}~t_1~t_2~bddop{\t{\footnotesize )}}}{{\t{\footnotesize apply}}~b_1~b_2~bddop} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} \t{termApply~$t_1$~$t_2$~$bddop$} applies the HOL operation corresponding to the \Buddy{} BDD operation $bddop$ to terms $t_1$ and $t_2$ (see Section~\ref{misc}). The exception {\t{\footnotesize BddOpError}} is raised if the varmaps of the hypotheses are not pointer equal \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddOp}}\index{HolBddLib!ML bindings!{BddOp}@\ml{BddOp}} \subsection{Quantification} \newsavebox\BddForall \begin{lrbox}\BddForall \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddForall : term list -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a}{\rho}{t}{b} \qquad \rho(v_1)=n_1,~ $\ldots$~,~ \rho(v_i)=n_i \\ \hline \termbdd{a}{\rho}{({\scriptstyle\forall} v_1~\cdots~v_i.~t)}% {{\t{\footnotesize forall~(makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddForallError} if any of the terms in the term list argument are not boolean variables in the domain of $\rho$, or occur free in any assumption \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddForall}}\index{HolBddLib!ML bindings!{BddForall}@\ml{BddForall}} \bigskip \newsavebox\BddExists \noindent\begin{lrbox}\BddExists \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddExists : term list -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a}{\rho}{t}{b} \qquad \rho(v_1)=n_1,~ $\ldots$~,~ \rho(v_i)=n_i \\ \hline \termbdd{a}{\rho}{({\scriptstyle\exists} v_1~\cdots~v_i.~t)}% {{\t{\footnotesize exist~(makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddExistsError} if any of the terms in the term list argument are not boolean variables in the domain of $\rho$, or occur free in any assumption \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddExists}}\index{HolBddLib!ML bindings!{BddExists}@\ml{BddExists}} \bigskip \newsavebox\BddAppall \noindent\begin{lrbox}\BddAppall \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddAppall : term list -> bddop * term_bdd * term_bdd -> term_bdd+} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2} \qquad \rho(v_1)=n_1,~ $\ldots$~,~ \rho(v_i)=n_i \\ \hline \begin{array}{l} {a_1 \cup a_2}% ~{\rho}% ~{({\scriptstyle\forall} v_1~\cdots~v_i.~% {\t{\footnotesize termApply}}~t_1~t_2~bddop)}\\ \mapsto\\ {{\t{\footnotesize appall}}~b_1~b_2~bddop~% {\t{\footnotesize (makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b} \end{array} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddAppallError} if the varmaps in the hypotheses are not pointer equal, or if any of the terms in the term list argument are not boolean variables in the domain of $\rho$, or occur free in any assumption \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddAppall}}\index{HolBddLib!ML bindings!{BddAppall}@\ml{BddAppall}} \bigskip \newsavebox\BddAppex \noindent\begin{lrbox}\BddAppex \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddAppex : term list -> bddop * term_bdd * term_bdd -> term_bdd+} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2} \qquad \rho(v_1)=n_1,~ $\ldots$~,~ \rho(v_i)=n_i \\ \hline \begin{array}{l} {a_1 \cup a_2}% ~{\rho}% ~{({\scriptstyle\exists} v_1~\cdots~v_i.~% {\t{\footnotesize termApply}}~t_1~t_2~bddop)}\\ \mapsto\\ {{\t{\footnotesize appex}}~b_1~b_2~bddop~% {\t{\footnotesize (makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b} \end{array} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddAppexError} if the varmaps of the hypotheses are not pointer equal, or if any of the terms in the term list argument are not boolean variables in the domain of $\rho$, or occur free in any assumption \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddAppex}}\index{HolBddLib!ML bindings!{BddAppex}@\ml{BddAppex}} \subsection{Composition, repacement and restriction} \newsavebox\BddCompose \begin{lrbox}\BddCompose \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddCompose : term_bdd * term_bdd -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_2}{\rho}{t_1}{b_1'}) \qquad \termbdd{a}{\rho}{t}{b} \\ \hline \termbdd{a_1 \cup a_2 \cup a} {\rho} {(\mbox{\t{\footnotesize subst[$v_1$ |-> $t_1$] $t$}})} {\mbox{\t{\footnotesize compose(var $b_1$, $b_1'$) $b$}}} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddComposeError} if varmaps in the hypotheses are not pointer equal, or the term $v_1$ is not a variable \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddCompose}}\index{HolBddLib!ML bindings!{BddCompose}@\ml{BddCompose}} \bigskip \newsavebox\BddListCompose \noindent\begin{lrbox}\BddListCompose \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddListCompose : (term_bdd * term_bdd) list -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \begin{array}{l} {\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{t_1}{b_1'}), \\ \phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\ \phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{t_i}{b_i'}){\t{\footnotesize ]}} \qquad \termbdd{a}{\rho}{t}{b} \end{array} \\ \hline \begin{array}{l} {a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\ {\rho}\\ {\mbox{\t{\footnotesize subst[$v_1$ |-> $t_1$,~$\ldots$~,~$v_i$ |-> $t_i$] $t$}}}\\ \mapsto\\ {\mbox{\t{\footnotesize veccompose(composeSet[(var $b_1$, $b_1'$),~$\ldots$~,~(var $b_i$, $b_i'$)])$b$}}} \end{array} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddListComposeError} if the varmaps in the hypotheses are not all pointer equal, or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddListCompose}}\index{HolBddLib!ML bindings!{BddListCompose}@\ml{BddListCompose}} \bigskip \newsavebox\BddRestrict \noindent\begin{lrbox}\BddRestrict \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddRestrict : (term_bdd * term_bdd) list -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \begin{array}{l} {\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{c_1}{b_1'}), \\ \phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\ \phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{c_i}{b_i'}){\t{\footnotesize ]}} \qquad \termbdd{a}{\rho}{t}{b} \end{array} \\ \hline \begin{array}{l} {a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\ {\rho}\\ {\mbox{\t{\footnotesize subst[$v_1$ |-> $c_1$,~$\ldots$~,~$v_i$ |-> $c_i$] $t$}}}\\ \mapsto\\ {\mbox{\t{\footnotesize restrict~$b$~(assignment[(var $b_1$, $\hat{c_1}$),~$\ldots$~,~(var $b_i$, $\hat{c_i}$)])}}} \end{array} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Where each of $c_1,\ldots,c_i$ is either the constant \t{F} or the constant \t{F}, and $\hat{\t{T}}$ denotes the ML value \t{true} and $\hat{\t{F}}$ denotes \t{false}. The exception \t{BddRestrictError} is raised if the varmaps in the hypotheses are not all pointer equal, or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables, or if any of $c_1,\ldots,c_i$ are not equal to \t{T} or \t{F} \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddRestrict}}\index{HolBddLib!ML bindings!{BddRestrict}@\ml{BddRestrict}} \bigskip \newsavebox\BddReplace \noindent\begin{lrbox}\BddReplace \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddReplace : (term_bdd * term_bdd) list -> term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \begin{array}{l} {\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{v_1'}{b_1'}), \\ \phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\ \phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{v_i'}{b_i'}){\t{\footnotesize ]}} \qquad \termbdd{a}{\rho}{t}{b} \end{array} \\ \hline \begin{array}{l} {a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\ {\rho}\\ {\mbox{\t{\footnotesize subst[$v_1$ |-> $v_1'$,~$\ldots$~,~$v_i$ |-> $v_i'$] $t$}}}\\ \mapsto\\ {\mbox{\t{\footnotesize replace~$b$~(makepairSet[(var $b_1$, var $b_1'$),~$\ldots$~,~(var $b_i$, var $b_i'$)])}}} \end{array} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Raises \t{BddReplaceError} if the varmaps in the hypotheses are not all pointer equal, or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables, or if any of the terms $v_1',\ldots,v_i'$ are repeated or are not variables \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddReplace}}\index{HolBddLib!ML bindings!{BddReplace}@\ml{BddReplace}} \subsection{Coudert, Berthet \& Madre simplification}\label{BddSimplify} \vspace*{-1mm} \newsavebox\BddSimplify \begin{lrbox}\BddSimplify \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddSimplify : term_bdd * term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2} \\ \hline \termbdd{a_1\cup a_2\cup \setass{t_1}}{\rho}{t_2}{{\t{\footnotesize simplify}}~b_1~b_2} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} The exception {\t{\footnotesize BddSimplifyError}} is raised if the varmaps in the hypotheses are not pointer equal \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddSimplify}}\index{HolBddLib!ML bindings!{BddSimplify}@\ml{BddSimplify}} \vspace*{-2mm} \subsection{Finding a satisfying assignment}\label{BddFindModel} \vspace*{-1mm} \newsavebox\BddFindModel \begin{lrbox}\BddFindModel \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+BddFindModel : term_bdd -> term_bdd +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a}{\rho}{t}{b} \\ \hline \termbdd{a\cup \setass{v_1=c_1,\ldots,v_p=c_p}}{\rho}{t}{{\t{\footnotesize TRUE}}} \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} The set $\{v_1=c_1,\ldots,v_p=c_p\}$ is a satisfying assignment for $t$ ($c_i$ is \T{} or \F{} for $1\leq i \leq p$). Exception {\t{\footnotesize BddFindModelError}} is raised if {\t{\footnotesize satone}} can't find a satisfying assignment. \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddFindModel}}\index{HolBddLib!ML bindings!{BddFindModel}@\ml{BddFindModel}} \subsection{Linking representation judgements to theorems}\label{oracle}\index{HolBddLib!termbdd@\ml{term\_bdd}!linking to theorems} \noindent \newsavebox\BddThmOracle \begin{lrbox}\BddThmOracle \begin{minipage}{\minipagewidth} {\verb+BddThmOracle : term_bdd -> thm+} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} \termbdd{a}{\rho}{t}{\ml{TRUE}} \\ \hline \texttt{[oracles:~HolBdd]}~ a \vdash t \end{array}$$ \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Allows HOL theorems to be `proved' by BDD calculation using \Buddy{}. Such theorems, and any theorems deduced from them, are tagged with \t{HolBdd} and so can be easily identified. \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddThmOracle}}\index{HolBddLib!ML bindings!{BddThmOracle}@\ml{BddThmOracle}} \bigskip \noindent \newsavebox\BddEqMp \begin{lrbox}\BddEqMp \begin{minipage}{\minipagewidth} {\verb+BddEqMp : thm -> term_bdd -> term_bdd+} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{-2mm} $$\begin{array}{c} a_1 \vdash t_1=t_2 \qquad \termbdd{a_2}{\rho}{t_1}{b} \qquad \\ \hline \termbdd{a_1 \cup a_2}{\rho}{t_2}{b} \end{array}$$\label{BddEqMp} \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} Enables the term part of a representation judgement to be replaced by a logically equivalent term. Raises \t{BddEqMpError} if the left hand side of the equation isn't $\alpha$-convertable to the term part of the representation judgement \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\BddEqMp}}\index{HolBddLib!ML bindings!{BddEqMp}@\ml{BddEqMp}} \subsection{Miscellaneous functions}\label{misc} %\paragraph{\t{term\_bdd} destructors} \noindent \newsavebox\destructors \begin{lrbox}\destructors \begin{minipage}{\minipagewidth} \begin{footnotesize} \begin{verbatim} dest_term_bdd : term_bdd -> assums * varmap * term * bdd getAssums : term_bdd -> assums getVarmap : term_bdd -> varmap getTerm : term_bdd -> term getBdd : term_bdd -> bdd \end{verbatim} \end{footnotesize} \vspace*{-6mm} \noindent \rule\minipagewidth{0.1pt} \vspace*{1mm} \begin{footnotesize} \hspace*{-1.5mm}$\begin{array}{ll} \t{dest\_term\_bdd}~(\termbdd{a}{\rho}{t}{b})&=~(\rho, t, b)\\ \t{getVarmap}~(\termbdd{a}{\rho}{t}{b})&=~\rho\\ \t{getTerm}~(\termbdd{a}{\rho}{t}{b})&=~t\\ \t{getBdd}~(\termbdd{a}{\rho}{t}{b})&=~b \end{array}$ \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\destructors}}\index{HolBddLib!termbdd@\ml{term\_bdd}!destructors} \bigskip \noindent \newsavebox\inSupport \begin{lrbox}\inSupport \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+inSupport : int -> bdd -> bool +} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} \t{inSupport}~$n$~$b$ checks if the BDD variable $n$ occurs in the BDD $b$ \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\inSupport}}\index{HolBddLib!ML bindings!{inSupport}@\ml{inSupport}} \bigskip \noindent \newsavebox\termApply \begin{lrbox}\termApply \begin{minipage}{\minipagewidth} \begin{footnotesize} {\verb+termApply : term -> term -> bddop -> term+} \end{footnotesize} \vspace*{-3mm} \noindent \rule\minipagewidth{0.1pt} \begin{footnotesize} \t{termApply}~$t_1$~$t_2$~$bddop$ applies the HOL operation corresponding to $bddop$ to $t_1$ and $t_2$. \vspace*{-2mm} \begin{verbatim} fun termApply t1 t2 bddop = case bddop of And => mk_conj(t1,t2) | Biimp => mk_eq(t1,t2) | Diff => mk_conj(t1, mk_neg t2) | Imp => mk_imp(t1,t2) | Invimp => mk_imp(t2,t1) | Lessth => mk_conj(mk_neg t1, t2) | Nand => mk_neg(mk_conj(t1,t2)) | Nor => mk_neg(mk_disj(t1,t2)) | Or => mk_disj(t1,t2) | Xor => mk_neg(mk_eq(t1,t2)); \end{verbatim} \end{footnotesize} \end{minipage} \end{lrbox} \fbox{\usebox{\termApply}}\index{HolBddLib!ML bindings!{termApply}@\ml{termApply}} \subsection{The structure \t{DerivedBddRules}}\label{DerivedBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!derived rules} This section notes a few of the more commonly used functions available in the structure \texttt{DerivedBddRules}. \subsection{Varmaps} \bigskip \noindent \newsavebox\extendVarmap \begin{lrbox}\extendVarmap \hbc{extendVarmap : term list -> varmap -> varmap}{Extend a varmap with a list of variables (allocating new BDD variables, if necessary).} \end{lrbox} \fbox{\usebox{\extendVarmap}}\index{HolBddLib!ML bindings!{extendVarmap}@\ml{extendVarmap}} \bigskip \noindent \newsavebox\globalvarmap \begin{lrbox}\globalvarmap \hbc{global\_varmap : varmap ref}{Global assignable varmap.} \end{lrbox} \fbox{\usebox{\globalvarmap}}\index{HolBddLib!ML bindings!{global\_varmap}@\ml{global\_varmap}} \subsection{Tests} \bigskip \noindent \newsavebox\BddEqualTest \begin{lrbox}\BddEqualTest \hbc{BddEqualTest : \termbddty -> \termbddty -> bool}{Test equality of BDD component of two term\_bdds and return true or false} \end{lrbox} \fbox{\usebox{\BddEqualTest}}\index{HolBddLib!ML bindings!{BddEqualTest}@\ml{BddEqualTest}} \bigskip \noindent \newsavebox\isTRUE \begin{lrbox}\isTRUE \hbc{isTRUE : \termbddty -> bool}{Test if the BDD part is TRUE} \end{lrbox} \fbox{\usebox{\isTRUE}}\index{HolBddLib!ML bindings!{isTRUE}@\ml{isTRUE}} \bigskip \noindent \newsavebox\isFALSE \begin{lrbox}\isFALSE \hbc{isFALSE : \termbddty -> bool}{Test if the BDD part is FALSE} \end{lrbox} \fbox{\usebox{\isFALSE}}\index{HolBddLib!ML bindings!{isFALSE}@\ml{isFALSE}} \subsection{Conversion to terms} \bigskip \noindent \newsavebox\GenTermToTermBdd \begin{lrbox}\GenTermToTermBdd \hbc{GenTermToTermBdd : (term -> \termbddty) -> varmap -> term -> \termbddty}{Scan a term and construct a term\_bdd using the primitive operations when applicable, and a supplied function on leaves when all else fails.} \end{lrbox} \fbox{\usebox{\GenTermToTermBdd}}\index{HolBddLib!ML bindings!{GenTermToTermBdd}@\ml{GenTermToTermBdd}} \bigskip \noindent \newsavebox\failfn \begin{lrbox}\failfn \hbc{failfn : 'a -> 'b}{Function that always raises exception fail (useful as argument to GenTermToTermBdd).} \end{lrbox} \fbox{\usebox{\failfn}}\index{HolBddLib!ML bindings!{failfn}@\ml{failfn}} \bigskip \noindent \newsavebox\bddToTerm \begin{lrbox}\bddToTerm \hbc{bddToTerm : varmap -> bdd -> term}{Convert a BDD to a nested conditional term with respect to a varmap .} \end{lrbox} \fbox{\usebox{\bddToTerm}}\index{HolBddLib!ML bindings!{bddToTerm}@\ml{bddToTerm}} \bigskip \noindent \newsavebox\termToTermBdd \begin{lrbox}\termToTermBdd \hbc{termToTermBdd : term -> \termbddty}{Like \texttt{GenTermToTermBdd} but fails on non-boolean leaves.} \end{lrbox} \fbox{\usebox{\termToTermBdd}}\index{HolBddLib!ML bindings!{termToTermBdd}@\ml{termToTermBdd}} \bigskip \noindent \newsavebox\destBddOp \begin{lrbox}\destBddOp \hbc{dest\_BddOp : term -> bddop * term * term}{Destruct a term corresponding to a BuDDY BDD binary operation (bddop). Fails with\newline \texttt{dest\_BddOpError} if not such a term.} \end{lrbox} \fbox{\usebox{\destBddOp}}\index{HolBddLib!ML bindings!{dest\_BddOp}@\ml{dest\_BddOp}} \subsection{Extracting theorems} \bigskip \noindent \newsavebox\TermBddToEqThm \begin{lrbox}\TermBddToEqThm \hbc{TermBddToEqThm : \termbddty -> thm}{\[\frac{\termbdd{a}{\rho}{t}{b}} {a \turn t = (\mathtt{bddToTerm}\, \rho\, b)}\]} \end{lrbox} \fbox{\usebox{\TermBddToEqThm}}\index{HolBddLib!ML bindings!{TermBddToEqThm}@\ml{TermBddToEqThm}} \bigskip \noindent \newsavebox\BddRhsOracle \begin{lrbox}\BddRhsOracle \hbc{BddRhsOracle : (term -> \termbddty) -> varmap -> thm -> thm}{\[\frac{\turn\,t1=t2}{\turn t1}\] if the BDD of t2 (using \texttt{GenTermToTermBdd}) is \texttt{TRUE}.} \end{lrbox} \fbox{\usebox{\BddRhsOracle}}\index{HolBddLib!ML bindings!{BddRhsOracle}@\ml{BddRhsOracle}} \bigskip \noindent \newsavebox\findModel \begin{lrbox}\findModel \hbc{findModel : \termbddty -> thm} {If $t$ is satisfiable (i.e., $b$ is not \texttt{FALSE}) \[\frac{\termbdd{a}{\rho}{t}{b}}{a \cup \{v_1=c_1,\ldots,v_n=c_n\} \turn t}\] Similar to \texttt{BddFindModel} followed by \texttt{BddThmOracle}, but checks the assignment found by \texttt{satone} using proof, so is pure (i.e., result not tagged with \texttt{HolBdd}).} \end{lrbox} \fbox{\usebox{\findModel}}\index{HolBddLib!ML bindings!{findModel}@\ml{findModel}} \subsection{Manipulating term\_bdd's} \bigskip \noindent \newsavebox\BddApThm \begin{lrbox}\BddApThm \hbc{BddApThm : thm -> \termbddty -> \termbddty}{\[\frac{a1\,\turn\,t1=t2\qquad\termbdd{a2}{\rho}{t1'}{b}} {\termbdd{a1\cup a2}{\rho}{t2'}{b}}\] where t1 can be instantiated to t1' and t2' is the corresponding instance of t2.} \end{lrbox} \fbox{\usebox{\BddApThm}}\index{HolBddLib!ML bindings!{BddApThm}@\ml{BddApThm}} \bigskip \noindent \newsavebox\BddApReplace \begin{lrbox}\BddApReplace \hbc{BddApReplace : \termbddty -> term -> \termbddty}{\[\frac{\termbdd{a}{\rho}{t}{b}} {\termbdd{a}{\rho}{t'}{b'}}\] where boolean variables in t can be renamed to get t' and b' is the corresponding replacement of BDD variables in b.} \end{lrbox} \fbox{\usebox{\BddApReplace}}\index{HolBddLib!ML bindings!{BddApReplace}@\ml{BddApReplace}} \bigskip \noindent \newsavebox\BddApRestrict \begin{lrbox}\BddApRestrict \hbc{BddApRestrict : \termbddty -> term -> \termbddty}{\[\frac{\termbdd{a}{\rho}{t}{b}} {\termbdd{a}{\rho}{t'}{b'}}\] Generates the BDD of a supplied term if it can be obtained by restricting a given term\_bdd.} \end{lrbox} \fbox{\usebox{\BddApRestrict}}\index{HolBddLib!ML bindings!{BddApRestrict}@\ml{BddApRestrict}} \bigskip \noindent \newsavebox\BddSubst \begin{lrbox}\BddSubst \hbc{BddSubst : (\termbddty * \termbddty) list -> \termbddty -> \termbddty} {\[\frac{\begin{array}{c} [(\termbdd{a_1}{\rho}{v_1}{b_1},\termbdd{a_1'}{\rho}{t_1}{b_1'}) \\ \vdots\\ (\termbdd{a_i}{\rho}{v_i}{b_i},\termbdd{a_i'}{\rho}{t_i}{b_i'})] \\ \termbdd{a}{\rho}{t}{b} \\ \end{array}} {\termbdd{a\cup\bigcup_i {a_i\cup a_i'}}{\rho}{\mathtt{subst} [v_1\mapsto t_1,\ldots,v_i\mapsto t_i] t}{\langle\textup{BDD b after replace}\rangle}}\] BddSubst applies a substitution $[(vtb_1,newtb_1),...,(vtb_i,newtb_i)]$ to a term\_bdd, where $vtb_p$ ($1 \leq p \leq i$) must be of the form $\termbdd{a}{\rho}{v_p}{b_p}$ where $v_p$ is a variable, and the varmaps are distinct This preliminary version separates the substitution into a restriction (variables mapped to \texttt{T} or \texttt{F}) followed by a variable renaming (replacement). A more elaborate scheme will be implemented using BuDDy's bdd\_veccompose.} \end{lrbox} \fbox{\usebox{\BddSubst}}\index{HolBddLib!ML bindings!{BddSubst}@\ml{BddSubst}} \bigskip \noindent \newsavebox\BddApSubst \begin{lrbox}\BddApSubst \hbc{BddApSubst : \termbddty -> term -> \termbddty}{\[\frac{\termbdd{a}{\rho}{t}{b}} {\termbdd{a}{\rho}{t'}{b'}}\] where boolean variables in t can be instantiated to get t' and b' is the corresponding replacement of BDD variables in b.} \end{lrbox} \fbox{\usebox{\BddApSubst}}\index{HolBddLib!ML bindings!{BddApSubst}@\ml{BddApSubst}} \bigskip \noindent \newsavebox\eqToTermBdd \begin{lrbox}\eqToTermBdd \hbc{eqToTermBdd : (term -> \termbddty) -> varmap -> thm -> \termbddty}{\[\frac{a\,\turn\,t1=t2} {\termbdd{a}{\rho}{t1}{\langle\textup{BDD of t2}\rangle}}\] Fails if \texttt{GenTermToTermBdd} fails on $t2$ with the supplied leaf function.} \end{lrbox} \fbox{\usebox{\eqToTermBdd}}\index{HolBddLib!ML bindings!{eqToTermBdd}@\ml{eqToTermBdd}} \bigskip \noindent \newsavebox\BddApConv \begin{lrbox}\BddApConv \hbc{BddApConv : conv -> \termbddty -> \termbddty}{\[\frac{\termbdd{a}{\rho}{t}{b}\qquad \mathtt{conv}\, t = (a' \turn t = t')} {\termbdd{a\cup a'}{\rho}{t'}{b}}\]} \end{lrbox} \fbox{\usebox{\BddApConv}}\index{HolBddLib!ML bindings!{BddApConv}@\ml{BddApConv}} \bigskip \noindent \newsavebox\BddSatone \begin{lrbox}\BddSatone \hbc{BddSatone : \termbddty -> (\termbddty * \termbddty) list} {\[\frac{\termbdd{a}{\rho}{t}{b}} {\begin{array}{c} [(\termbdd{a_1}{\rho}{v_1}{b_1},\termbdd{a_1'}{\rho}{c_1}{b_1'}) \\ \vdots\\ (\termbdd{a_i}{\rho}{v_i}{b_i},\termbdd{a_i'}{\rho}{c_i}{b_i'})] \\ \end{array}}\] with the property that \[\mathtt{isTRUE} \left(\mathtt{BddRestrict}{\begin{array}{c} [(\termbdd{a_1}{\rho}{v_1}{b_1},\termbdd{a_1'}{\rho}{c_1}{b_1'}) \\ \vdots\\ (\termbdd{a_i}{\rho}{v_i}{b_i},\termbdd{a_i'}{\rho}{c_i}{b_i'})] \\ \end{array}} {\termbdd{a}{\rho}{t}{b}}\right) \] } \end{lrbox} \fbox{\usebox{\BddSatone}}\index{HolBddLib!ML bindings!{BddSatone}@\ml{BddSatone}} \subsection{Fixed points and traces} \bigskip \noindent \newsavebox\computeFixedpoint \begin{lrbox}\computeFixedpoint \hbc{computeFixedpoint : reportfn\_ty -> varmap -> thm * thm -> \termbddty} {\[\frac{\turn f\, 0\, s = \ldots s \ldots \qquad \turn \forall n. f (n+1) s = \ldots f\, n \ldots s \ldots} {(\termbdd{}{\rho}{f\, i\, s}{b_i},\termbdd{}{\rho}{f\, (i+1)\, s}{b_{i+1}})}\] where $i$ is the first number such that $\turn f\, (i+1)\, s = f\, i\, s$ and the function reportfn is applied to the iteration level and current term\_bdd and can be used for tracing. A state of the iteration is a pair (tb,tb') consisting of the previous term\_bdd tb and the current one tb'. The initial state is (somewhat arbitarily) taken to be (tb0,tb0). } \end{lrbox} \fbox{\usebox{\computeFixedpoint}}\index{HolBddLib!ML bindings!{computeFixedpoint}@\ml{computeFixedpoint}} \bigskip \noindent \newsavebox\computeTrace \begin{lrbox}\computeTrace \hbc{computeTrace : reportfn\_ty -> varmap -> thm -> thm*thm -> \termbddty list} {\[\frac{\turn p\ s = \ldots s \ldots \qquad \turn f\, 0\, s = \ldots s \ldots \qquad \turn f (n+1) s = \ldots f\, n \ldots s \ldots} {(\termbdd{}{\rho}{f\, i\, s}{b_i},\termbdd{}{\rho}{f\, 0\, s}{b_0})}\] where $i$ is the first number such that $\turn f\, i\, s = p\, s$. } \end{lrbox} \fbox{\usebox{\computeTrace}}\index{HolBddLib!ML bindings!{computeTrace}@\ml{computeTrace}} \bigskip \noindent \newsavebox\findTrace \begin{lrbox}\findTrace \hbc{findTrace : varmap -> thm -> thm -> thm -> thm * thm list * thm} {\[\frac{ \begin{array}{l} \turn R((v_1,\ldots,v_n),(v_1',\ldots,v_n')) \\ \turn P(v_1,\ldots,v_n) = \ldots \\ \turn Q(v_1,\ldots,v_n) = \ldots \\ \end{array}} {(\turn P s_0,[\turn R(s_0,s_1),\ldots,\turn R(s_{n-1},s_n))],\turn Q s_n)}\]} \end{lrbox} \fbox{\usebox{\findTrace}}\index{HolBddLib!ML bindings!{findTrace}@\ml{findTrace}} \bigskip \noindent \newsavebox\MakeSimpRecThm \begin{lrbox}\MakeSimpRecThm \hbc{MakeSimpRecThm : thm -> thm}{Perform disjunctive partitioning. Implemented by \[\mathtt{SIMP\_RULE\, bool\_ss\, [LEFT\_AND\_OVER\_OR,EXISTS\_OR\_THM]}\]} \end{lrbox} \fbox{\usebox{\MakeSimpRecThm}}\index{HolBddLib!ML bindings!{MakeSimpRecThm}@\ml{MakeSimpRecThm}} \index{HolBddLib|)} \bibliographystyle{plain} \bibliography{description} %\printindex \end{document}