[Hol-checkins] SF.net SVN: hol: [5911] HOL/Manual/Description/HolBdd.tex

[<ha...@us...>]

Revision: 5911
          http://hol.svn.sourceforge.net/hol/?rev=5911&view=rev
Author:   hamjad
Date:     2008-04-29 07:17:24 -0700 (Tue, 29 Apr 2008)

Log Message:
-----------
Converted HolBdd.tex documentclass to article.

Modified Paths:
--------------
    HOL/Manual/Description/HolBdd.tex

Modified: HOL/Manual/Description/HolBdd.tex
===================================================================
--- HOL/Manual/Description/HolBdd.tex	2008-04-29 14:15:24 UTC (rev 5910)
+++ HOL/Manual/Description/HolBdd.tex	2008-04-29 14:17:24 UTC (rev 5911)
@@ -1,7 +1,7 @@
-\documentclass[12pt,fleqn]{book}
+\documentclass[12pt,fleqn]{article}
 \usepackage{makeidx}
 \usepackage{url}
-\usepackage{index}
+%\usepackage{index}
 \usepackage{multind}
 \usepackage{fancyvrb}
 \usepackage{latexsym}
@@ -14,7 +14,7 @@
 
 \input{../LaTeX/commands}
 
-\makeindex
+%\makeindex
 
 \newcommand{\hbc}[2]{
 \addtolength{\minipagewidth}{-10pt}
@@ -75,15 +75,15 @@
 %\parskip 1mm
 
 \setcounter{sessioncount}{0}
-%\title{HolBddLib}
-%\date{}
+\title{HolBddLib}
+\date{}
 \begin{document}
-\chapter{HolBddLib}
+\maketitle
 \index{HolBddLib|(}
 
-This section describes {\tt HolBddLib}, a \HOL{} interface to an external BDD engine.\index{binary decision diagrams|see {HolBddLib}}\index{BDDs|see {HolBddLib}}
+This document describes {\tt HolBddLib}, a \HOL{} interface to an external BDD engine.\index{binary decision diagrams|see {HolBddLib}}\index{BDDs|see {HolBddLib}}
 
-\subsection{Introduction}
+\section{Introduction}
 
 The development of {\tt HolBddLib} has gone through two phases.  The
 first phase consisted in experiments with different ways of linking
@@ -138,7 +138,7 @@
 {\tt HolBddLib} is built on top of \Muddy{} and
 is described in Section~\ref{HolBddLib}.
 
-\subsubsection{Overview}\index{HolBddLib!overview}
+\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
@@ -169,7 +169,7 @@
 and two small subsidiary structures \t{Varmap} and \t{PrintBdd}.
 
 
-\subsubsection{Relation to the Voss system}\label{related}\index{HolBddLib!Voss, relation to}
+\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
@@ -241,7 +241,7 @@
 
 
 
-\subsection{\Muddy}\label{muddy}
+\section{\Muddy}\label{muddy}
 
 \Muddy{} is the Moscow ML interface to \Buddy{}. It provides ML functions for constructing and
 manipulating BDDs via three structures:
@@ -263,7 +263,7 @@
 the documentation of \t{fdd} and \t{bvec} provided here is minimal
 (see Sections~\ref{fdd} and \ref{bvec} below).
 
-\subsubsection{Initialisation, termination and tuning sessions}\label{init}\index{HolBddLib!session!initialisation}\index{HolBddLib!session!termination}
+\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
@@ -378,7 +378,7 @@
 For example, if $n$ is $4$ then the internal caches will a quarter the size of the
 nodetable.
 
-\subsubsection{BDDs representing {\t{true}} and {\t{false}}}\index{HolBddLib!BDD!constants}
+\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}.
@@ -400,7 +400,7 @@
 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)}.
 
-\subsubsection{Variables}\index{HolBddLib!BDD!variables}
+\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
@@ -450,7 +450,7 @@
 greater than $n$.
 
 
-\subsubsection{Sets of variables and quantification}\label{varSet}\index{HolBddLib!BDD!quantification}
+\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
@@ -473,7 +473,7 @@
    exist  : varSet -> bdd -> bdd
 \end{verbatim}\index{HolBddLib!ML bindings!{forall}@\ml{forall}}\index{HolBddLib!ML bindings!{exist}@\ml{exist}}
 
-\subsubsection{Assignments, composition, replacement and restriction}\label{replace}\index{HolBddLib!BDD!assignments}\index{HolBddLib!BDD!composition}\index{HolBddLib!BDD!replacement}\index{HolBddLib!BDD!restriction}
+\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
@@ -531,7 +531,7 @@
 $\t{fromBool(}t_i\t{)}$ (for $1{\leq}i{\leq}n$). 
 
 
-\subsubsection{Finding satisfying assignments}\index{HolBddLib!BDD!satisfying assignments}
+\subsection{Finding satisfying assignments}\index{HolBddLib!BDD!satisfying assignments}
 
 An assignment satisfying a BDD can be computed via \Buddy{} using
 
@@ -566,7 +566,7 @@
 satisfy the BDD, so may not return an assignment giving values to all
 the variables.
 
-\subsubsection{Boolean operations on BDDs}\label{app}\index{HolBddLib!BDD!boolean operations}
+\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. 
@@ -626,7 +626,7 @@
 
 
 
-\subsubsection{Inspecting and counting nodes and states}\index{HolBddLib!BDD!nodes}\index{HolBddLib!BDD!states}
+\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,
@@ -728,7 +728,7 @@
 the number of states in the set (hence the name).
 
 
-\subsubsection{Coudert, Berthet \& Madre simplification}\index{HolBddLib!BDD!simplification}
+\subsection{Coudert, Berthet \& Madre simplification}\index{HolBddLib!BDD!simplification}
 
 The ML function
 
@@ -751,7 +751,7 @@
 the algorithm underlying \t{simplify} is described and attributed to a paper by
 Coudert, Berthet and Madre \cite{CoudertBerthetMadre}.
 
-\subsubsection{Saving, hashing and printing BDDs}\label{printing}\index{HolBddLib!BDD!saving}\index{HolBddLib!BDD!hashing}\index{HolBddLib!BDD!printing}
+\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
 
@@ -831,7 +831,7 @@
 \includegraphics[width=3cm, height=5cm]{figs/ex}
 \end{center}
 
-\subsubsection{Dynamic variable reordering}\index{HolBddLib!BDD!dynamic reordering}
+\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
@@ -867,7 +867,7 @@
     varAtLevel       : int -> varnum
 \end{verbatim}
 
-\subsubsection{The \Muddy{} structure \t{fdd}}\label{fdd}\index{HolBddLib!finite domains}
+\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
@@ -894,7 +894,7 @@
    setPairs   : (fddvar * fddvar) list -> bdd.pairSet
 \end{verbatim}
 
-\subsubsection{The \Muddy{} structure \t{bvec}}\label{bvec}\index{HolBddLib!BDD!vectors}
+\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.
@@ -942,7 +942,7 @@
    neq         : bvec * bvec -> bdd.bdd
 \end{verbatim}
 
-\subsubsection{Storage allocation and garbage collection}\index{HolBddLib!BDD!garbage collection}
+\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
@@ -975,7 +975,7 @@
 $pregc$ when a BuDDy GC is initiated and print $postgc$ when the
 \Buddy{} GC is completed.
 
-\subsection{\t{HolBddLib}}\label{HolBddLib}
+\section{\t{HolBddLib}}\label{HolBddLib}
 
 \t{HolBddLib} currently consists of five modules
 
@@ -1021,7 +1021,7 @@
 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}).  
 
-\subsubsection{The structure \ml{Varmap}}\label{Varmap}\index{HolBddLib!termbdd@\ml{term\_bdd}!varmaps}
+\subsection{The structure \ml{Varmap}}\label{Varmap}\index{HolBddLib!termbdd@\ml{term\_bdd}!varmaps}
 
 The type \t{varmap} is defined by
 
@@ -1075,7 +1075,7 @@
 \t{Varmap.unify} &  compute smallest varmap that extends both arguments\\ \hline
 \end{tabular}
 
-\subsubsection{The structure \ml{PrintBdd}}\label{PrintBdd}\index{HolBddLib!termbdd@\ml{term\_bdd}!printing}
+\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.
@@ -1113,7 +1113,7 @@
 to the global reference \t{dotTermBddFlag}.
 \end{description}
 
-\subsubsection{The structure \t{PrimitiveBddRules}}\label{PrimitiveBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!primitive rules}
+\subsection{The structure \t{PrimitiveBddRules}}\label{PrimitiveBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!primitive rules}
 
 The structure \ml{PrimitiveBddRules} defines the type \termbddty{} by
 
@@ -1179,7 +1179,7 @@
 different variable orders) is an area that may reveal incompleteness
 in the current rules.
 
-\subsubsection{Rules for generating representation judgements}\label{term-bdd-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
@@ -1193,7 +1193,7 @@
 $\termbdd{}{\rho}{t}{b}$.
 
 
-\subsubsection*{Extending and contracting the varmap}
+\subsection{Extending and contracting the varmap}
 
 \newsavebox\BddExtendVarmap
 \begin{lrbox}\BddExtendVarmap
@@ -1286,7 +1286,7 @@
 \fbox{\usebox{\BddSupportContractVarmap}}\index{HolBddLib!ML bindings!{BddSupportContractVarmap}@\ml{BddSupportContractVarmap}}
 
 
-\subsubsection*{Variables and constants}
+\subsection{Variables and constants}
 
 \newsavebox\BddVar
 \begin{lrbox}\BddVar
@@ -1367,7 +1367,7 @@
 \end{lrbox}
 \fbox{\usebox{\BddCon}}\index{HolBddLib!ML bindings!{BddCon}@\ml{BddCon}}
 
-\subsubsection*{Boolean operations}
+\subsection{Boolean operations}
 
 
 
@@ -1466,7 +1466,7 @@
 \fbox{\usebox{\BddOp}}\index{HolBddLib!ML bindings!{BddOp}@\ml{BddOp}}
 
 
-\subsubsection*{Quantification}
+\subsection{Quantification}
 
 \newsavebox\BddForall
 \begin{lrbox}\BddForall
@@ -1618,7 +1618,7 @@
 \end{lrbox}
 \fbox{\usebox{\BddAppex}}\index{HolBddLib!ML bindings!{BddAppex}@\ml{BddAppex}}
 
-\subsubsection*{Composition, repacement and restriction}
+\subsection{Composition, repacement and restriction}
 
 
 \newsavebox\BddCompose
@@ -1787,7 +1787,7 @@
 \end{lrbox}
 \fbox{\usebox{\BddReplace}}\index{HolBddLib!ML bindings!{BddReplace}@\ml{BddReplace}}
 
-\subsubsection*{Coudert, Berthet \& Madre simplification}\label{BddSimplify}
+\subsection{Coudert, Berthet \& Madre simplification}\label{BddSimplify}
 
 \vspace*{-1mm}
 
@@ -1822,7 +1822,7 @@
 
 \vspace*{-2mm}
 
-\subsubsection*{Finding a satisfying assignment}\label{BddFindModel}
+\subsection{Finding a satisfying assignment}\label{BddFindModel}
 
 \vspace*{-1mm}
 
@@ -1857,7 +1857,7 @@
 \end{lrbox}
 \fbox{\usebox{\BddFindModel}}\index{HolBddLib!ML bindings!{BddFindModel}@\ml{BddFindModel}}
 
-\subsubsection{Linking representation judgements to theorems}\label{oracle}\index{HolBddLib!termbdd@\ml{term\_bdd}!linking to theorems}
+\subsection{Linking representation judgements to theorems}\label{oracle}\index{HolBddLib!termbdd@\ml{term\_bdd}!linking to theorems}
 
 \noindent \newsavebox\BddThmOracle
 \begin{lrbox}\BddThmOracle
@@ -1921,7 +1921,7 @@
 \end{lrbox}
 \fbox{\usebox{\BddEqMp}}\index{HolBddLib!ML bindings!{BddEqMp}@\ml{BddEqMp}}
 
-\subsubsection{Miscellaneous functions}\label{misc}
+\subsection{Miscellaneous functions}\label{misc}
 
 %\paragraph{\t{term\_bdd} destructors}
 
@@ -2014,11 +2014,11 @@
 \end{lrbox}
 \fbox{\usebox{\termApply}}\index{HolBddLib!ML bindings!{termApply}@\ml{termApply}}
 
-\subsubsection{The structure \t{DerivedBddRules}}\label{DerivedBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!derived rules}
+\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}.
 
-\subsubsection*{Varmaps}
+\subsection{Varmaps}
 
 \bigskip 
 
@@ -2037,7 +2037,7 @@
 \end{lrbox}             
 \fbox{\usebox{\globalvarmap}}\index{HolBddLib!ML bindings!{global\_varmap}@\ml{global\_varmap}}
 
-\subsubsection*{Tests}
+\subsection{Tests}
 
 \bigskip
 
@@ -2063,7 +2063,7 @@
 \end{lrbox}
 \fbox{\usebox{\isFALSE}}\index{HolBddLib!ML bindings!{isFALSE}@\ml{isFALSE}}
 
-\subsubsection*{Conversion to terms}
+\subsection{Conversion to terms}
 
 \bigskip 
 
@@ -2104,7 +2104,7 @@
 \end{lrbox}
 \fbox{\usebox{\destBddOp}}\index{HolBddLib!ML bindings!{dest\_BddOp}@\ml{dest\_BddOp}}
 
-\subsubsection*{Extracting theorems}
+\subsection{Extracting theorems}
 
 \bigskip 
 
@@ -2137,7 +2137,7 @@
 \end{lrbox}             
 \fbox{\usebox{\findModel}}\index{HolBddLib!ML bindings!{findModel}@\ml{findModel}}
 
-\subsubsection*{Manipulating term\_bdd's}
+\subsection{Manipulating term\_bdd's}
 
 \bigskip 
 
@@ -2242,7 +2242,7 @@
 \end{lrbox}             
 \fbox{\usebox{\BddSatone}}\index{HolBddLib!ML bindings!{BddSatone}@\ml{BddSatone}}
 
-\subsubsection*{Fixed points and traces}
+\subsection{Fixed points and traces}
 
 \bigskip 
 


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.