IT/Description/HolBdd.tex

\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{}<m_0\t{:}n_0\t{,} \ldots \t{,} m_l\t{:}n_l\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}