1\documentclass[12pt,fleqn]{article} 2\usepackage{makeidx} 3\usepackage{url} 4%\usepackage{index} 5%\usepackage{multind} 6\usepackage{fancyvrb} 7\usepackage{latexsym} 8%\usepackage{amsmath} 9\usepackage{amssymb} 10%\usepackage{amsbsy} 11\usepackage{alltt} 12\usepackage{../LaTeX/layout} 13\usepackage{graphicx} 14 15\input{../LaTeX/commands} 16 17%\makeindex 18 19\newcommand{\hbc}[2]{ 20\addtolength{\minipagewidth}{-10pt} 21\begin{minipage}{\minipagewidth} 22\begin{footnotesize} 23{\texttt{#1}} 24\end{footnotesize} 25\vspace*{-3mm} 26 27\noindent \rule\minipagewidth{0.1pt} 28 29\begin{footnotesize} 30#2 31\end{footnotesize} 32\end{minipage} 33} 34 35\renewcommand{\t}[1]{\mbox{\tt #1}} 36%\newcommand{\prev}[1]{#1} 37 38%\newcommand{\varord}[1]{#1} 39 40%\newcommand{\ma}[1]{{{$#1$}}} 41%\newcommand{\id}[1]{#1} 42 43\newcommand{\termbdd}[4]{\mbox{$#1~#2~#3~\mapsto~#4$}} 44\newcommand{\globtermbdd}[2]{\mbox{$#1\hspace{0.5mm}\mapsto\hspace{0.5mm}#2$}} 45 46\newcommand{\emptyass}{\mbox{\footnotesize$\{{}\}$}{}} 47\newcommand{\setass}[1]{\mbox{\footnotesize$\{#1\}$}{}} 48 49\newcommand\termbddty{\texttt{term\_bdd}{}} 50 51\newcommand{\mosml}{Moscow~ML{}} 52\newcommand{\Buddy}{BuDDy{}} 53\newcommand{\Muddy}{MuDDy{}} 54\newcommand\HolBuddy{\texttt{HolBddLib}{}} 55 56%\newcommand{\els}{\mid} 57%\newcommand{\Imp}{\Rightarrow} 58 59\renewcommand{\prod}{\mbox{\tt{*}}} 60%\newcommand{\SP}{~} 61%\newcommand{\SPP}{~} 62 63%\newcommand{\homedir}{\mbox{$\sim$}} 64 65\newcommand{\Turn}{\(\turn\)} 66\newcommand{\And}{\(\wedge\)} 67\newcommand{\Or}{\(\vee\)} 68\newcommand{\Not}{\(\neg\)} 69\newcommand{\Forall}{\(\forall\)} 70\newcommand{\Exists}{\(\exists\)} 71\newcommand{\Mapsto}{\(\mapsto\)} 72 73 74%\parindent 0mm 75%\parskip 1mm 76 77\setcounter{sessioncount}{0} 78\title{HolBddLib} 79\date{} 80\begin{document} 81\maketitle 82\index{HolBddLib|(} 83 84This document describes {\tt HolBddLib}, a \HOL{} interface to an external BDD engine.\index{binary decision diagrams|see {HolBddLib}}\index{BDDs|see {HolBddLib}} 85 86\section{Introduction} 87 88The development of {\tt HolBddLib} has gone through two phases. The 89first phase consisted in experiments with different ways of linking 90higher order logic (HOL) terms to binary decision diagrams (BDDs). 91These are described in the paper {\it Reachability programming in HOL98 using BDDs\/} \cite{tphols2000-Gordon}. The first release of 92\t{HolBddLib}, now called Version~1, consisted of an ad hoc collection 93of tools developed for these experiments. One of the approaches we 94experimented with was based on a protected type of `BDD representation 95judgements', analogous to the LCF protected type of theorems. 96Positive results of Hasan Amjad \cite{Amjad:TPHOLs2001} have lead us 97to narrow attention to just this approach. \t{HolBddLib} Version~2, 98which is described here, provides a set of representation judgement 99rules as core infrastructure for building `fully-expansive' or 100`LCF-style' combinations of HOL theorem proving and BDD-based symbolic 101calculation algorithms. All higher level tools, such as model 102checkers, are programmed in ML as `derived rules'. 103 104The primitive inference rules for representation judgements are contained in the structure 105{\tt{PrimitiveBddRules}}. Several useful and example derived rules are in the 106structure {\tt{DerivedBddRules}}. 107 108Version~1 of {\tt{HolBddLib}} was more elaborate than Version~2 109because it mixed together code from a number of experiments. 110In Version~1 there was a function, called 111{\texttt{termToBdd}}, that tried to represent a \HOL{} term as a BDD 112using a dynamically extendable global table mapping \HOL{} terms to 113BDDs. $\t{TermToBdd}$ constructed the BDD of a term $t$ using any 114BDDs of subterms of $t$ that were stored in the global table. 115{\tt{HolBddLib}} Version~2 has jettisoned this imperative style 116in favour of purely functional rules. Some of 117the ideas of BDD tables are likely to return in the future, but as 118contexts, similar to HOL simpsets, that are passed functionally, 119rather than as a single global state held in references. 120 121{\tt{HolBddLib}} Version~1 only supported a single variable 122ordering, held in a global variable map. In Version~2, each 123representation judgement carries its own variable ordering, so that local 124scopes are possible. For convenience, {\tt{DerivedBddRules}} 125provides a way of storing a default variable ordering in a global 126variable, but this is just a derived facility, not part of the kernel. 127 128{\tt{HolBddLib}} Version~2 adds assumptions to representation judgements 129analogous to assumptions of HOL theorems. This enables 130Coudert, Berthet and Madre simplification to be represented as a primitive 131rule (see the rule \t{BddSimplify} in Section~\ref{term-bdd-rules}). It also allows the term part 132of a representation judgements to be simplified using equations with assumptions 133(see the rule \t{BddEqMp} in Section~\ref{BddEqMp}). 134 135{\tt HolBddLib} uses J{\o}rn Lind-Nielsen's \Buddy{} package as a BDD 136engine. The interface from \Buddy{} to Moscow ML, called \Muddy, is 137due to Ken Friis Larsen and Jakob Lichtenberg, and is described in Section~\ref{muddy}. 138{\tt HolBddLib} is built on top of \Muddy{} and 139is described in Section~\ref{HolBddLib}. 140 141\subsection{Overview}\index{HolBddLib!overview} 142 143In the fully expansive (or `LCF style') approach, theorems are represented by an abstract type 144whose primitive operations are the axioms and inference rules of a 145logic. Theorem proving tools are implemented by composing together 146the inference rules using ML programs. 147 148This idea can be generalised to computing valid judgements that 149represent other kinds of information. In particular, consider 150judgements $(a,\rho,t,b)$, where $a$ is a set of boolean terms 151(assumptions) that are assumed true, $\rho$ represents a variable 152order, $t$ is a boolean term all of whose free variables are boolean 153and $b$ is a BDD. Such a judgement is valid if under the assumptions 154$a$, the BDD representing $t$ with respect to $\rho$ is $b$, and we 155will write \termbdd{a}{\rho}{t}{b} when this is the case. 156 157The derivation of `theorems' like \termbdd{a}{\rho}{t}{b} can be viewed 158as `proof' in the style of LCF by defining an abstract type \termbddty{} 159that models 160judgements $\termbdd{a}{\rho}{t}{b}$ analogously 161to the way the type $\ty{thm}$ models theorems $\vdash t$. 162 163The structure \t{HolBddLib} currently contains two main structures: \t{PrimitiveBddRules} 164which defines a protected type \termbddty and rules for generating 165values of this type, and \t{DerivedBddRules} that contains derived 166rules for performing simple fixed-point calculations. There is also a 167theory \t{MachineTransitionTheory} containing the theorems on 168reachability and fixed points needed by the derived rules, 169and two small subsidiary structures \t{Varmap} and \t{PrintBdd}. 170 171 172\subsection{Relation to the Voss system}\label{related}\index{HolBddLib!Voss, relation to} 173 174The Voss system \cite{SegerVoss} has strongly influenced and inspired 175the ideas described here. Voss consists of a lazy 176ML-like functional language, called FL, with BDDs as a built-in datatype. 177Quantified boolean formulae can be input and are parsed to BDDs. 178The normal boolean operations $\neg$, $\wedge$, $\vee$, $\equiv$, 179$\forall$, $\exists$ are interpreted as BDD operations. 180Algorithms for model checking are easily programmed. 181 182Joyce and Seger interfaced an early HOL system (HOL88) to Voss and in 183a pioneering paper showed how to verify complex systems by a 184combination of theorem proving deduction and symbolic trajectory 185evaluation (STE) \cite{JoyceSeger}. The HOL-Voss system integrates HOL88 186deduction with BDD computations. BDD tools are programmed in FL and 187can then be invoked by HOL-Voss tactics, which can make external 188calls into the Voss system, passing subgoals via a translation between 189the HOL88 and Voss term representations. 190 191In later work Lee, Seger and Greenstreet \cite{LeeGreenstreetSeger} 192showed how various optimised BDD algorithms could be programmed in FL. 193 194The early experiments with HOL-Voss suggested that a lighter theorem 195proving component was sufficient, since all that was really needed was 196a way of combining results obtained from STE. A system based on this 197idea, called VossProver, was developed by Carl Seger and his student 198Scott Hazelhurst. It provides operations in FL for combining 199assertions generated by Voss using proof rules corresponding to the 200laws of composition of the temporal logic assertions verified by STE 201\cite{hazelhurst-kropfbook-97}. 202VossProver was used to verify 203impressive integer and floating-point examples (see the DAC98 204paper by Aagaard, Jones and Seger \cite{aagaard-dac-98} for further 205discussion and references). 206 207After Seger and Aagaard moved to Intel, the development of the Voss and 208VossProver systems evolved into a new system called Forte. Only partial details 209of this are in the public domain 210\cite{oleary-itj-99,aagaard-tphols-99}, but a key idea is that FL is 211used both as a specification language and as an LCF-style 212metalanguage. The connection between symbolic trajectory evaluation 213and proof is obtained via a tactic {\tt{Eval\_tac}} that converts the 214result of executing an FL program performing STE into a theorem in the 215logic. Theorem proving in Forte is used both to split goals into 216smaller subgoals that are tractable for model checking, and to 217transform formulae so that they can be checked more efficiently. 218 219The combination of \HOL{} and \Buddy{} in Version~1 of 220{\tt{HolBddLib}} provides a somewhat similar programming environment 221to Voss's FL (though with eager rather than lazy evaluation and no 222special support for STE). \Buddy{} provides BDD operations 223corresponding to $\neg$, $\wedge$, $\vee$, $\equiv$, $\forall$, 224$\exists$ and the \HOL{} term parser plus \ml{termToBdd} provides a 225way of using these to create BDDs from logical terms. Voss enables 226efficient computations on BDDs using functional programming. So does 227\ml{HolBddLib}. However, in addition it allows FL-like BDD programming 228in ML to be intimately mixed with \HOL{} deduction, so that, for 229example, theorem proving tools (e.g.~simplifiers) can be directly 230applied to terms to optimise them for BDD purposes (e.g.~disjunctive 231partitioning). This is in line with future developments discussed by 232Joyce and Seger \cite{JoyceSeger} and it appears that the Forte system 233has similar capabilities. 234 235{\tt{HolBddLib}} Version~2 provides a less developed interactive 236programming environment than Version~1. It is more oriented to 237providing a clean and simple API allowing implementers to create their 238own `fully-expansive' combinations of model checking and theorem 239proving. Such a combination could be a Voss-like verification 240platform. 241 242 243 244\section{\Muddy}\label{muddy} 245 246\Muddy{} is the Moscow ML interface to \Buddy{}. It provides ML functions for constructing and 247manipulating BDDs via three structures: 248 249\begin{itemize} 250 251\item \t{bdd} defines the ML type 252\t{bdd} representing BDDs and associated operations derived from \Buddy{}; 253 254 255\item \t{fdd} provides support for blocks of BDD variables 256used to encode values representing elements of finite domains; 257 258\item \t{bvec} provides support for Boolean vectors. 259 260\end{itemize} 261 262The current \HolBuddy{} system only uses \t{bdd} and so 263the documentation of \t{fdd} and \t{bvec} provided here is minimal 264(see Sections~\ref{fdd} and \ref{bvec} below). 265 266\subsection{Initialisation, termination and tuning sessions}\label{init}\index{HolBddLib!session!initialisation}\index{HolBddLib!session!termination} 267 268The \Buddy{} package must be initialised before any BDD operations are done. 269Initialisation is done with the ML function 270 271\begin{verbatim} 272 init : int -> int -> unit 273\end{verbatim}\index{HolBddLib!ML bindings!{init}@\ml{init}} 274 275Evaluating $\t{init}~m~n$ initialises \Buddy{} with $m$ nodes in the 276nodetable and a cachesize of $n$. 277The library \t{HolBddLib} (Section~\ref{HolBddLib}) 278initialises the nodetable to 1000000 and cachesize to 279be 10000. The following is a quotation from the \Buddy{} documentation \cite{BuDDy}. 280 281\vspace*{-2mm} 282 283{\baselineskip8pt\begin{quote}\footnotesize 284Good initial values are 285 286\smallskip 287 288\begin{tabular}{lrr} 289{\bf Example} & {\bf nodenum} & {\bf cachesize} \\ 290Small test examples & 1000 & 100\\ 291Small examples & 10000 & 1000 \\ 292Medium sized examples & 100000 & 10000\\ 293Large examples & 1000000 & 10000 294\end{tabular} 295 296\smallskip 297 298Too few nodes will only result in reduced performance and this 299increases the number of garbage collections needed. If the package 300needs more nodes, then it will automatically increase the size of the 301node table. 302\end{quote}} 303 304The initial number of nodes is not critical for any BDD operation 305as the table will be resized whenever there are too few nodes left 306after a garbage collection. But it does have some impact on the 307efficiency of the operations. 308 309The function 310 311\begin{verbatim} 312 done : unit -> unit 313\end{verbatim}\index{HolBddLib!ML bindings!{done}@\ml{done}} 314 315frees all memory used by \Buddy{} and resets the 316package to its initial state. 317 318The functions \t{init} and \t{done} should only be called once per session. 319 320The function 321 322\begin{verbatim} 323 isRunning : unit -> bool 324\end{verbatim}\index{HolBddLib!ML bindings!{isRunning}@\ml{isRunning}} 325 326tests whether 327\Buddy{} is running (i.e.~\t{init} has been called and \t{done} has not been called). It is 328useful for checking if initialialisation is needed. 329 330The functions \t{init} and \t{done} should only be called once in a session. 331 332Statistical information from \Buddy{} is available 333using the function \t{stats} 334 335\begin{verbatim} 336 stats : unit -> {produced : int, 337 nodenum : int, 338 maxnodenum : int, 339 freenodes : int, 340 minfreenodes : int, 341 varnum : int, 342 cachesize : int, 343 gbcnum : int} 344\end{verbatim}\index{HolBddLib!ML bindings!{stats}@\ml{stats}} 345 346The meaning of the values of the various named fields in the record returned by 347evaluating \t{stats()} are 348 349\medskip 350 351\begin{tabular}{|l|l|} \hline 352{\bf{Field name}}& {\bf{Meaning}} \\ \hline\hline 353\t{produced} & total number of new nodes ever produced \\ \hline 354\t{nodenum} & currently allocated number of BDD nodes \\ \hline 355\t{maxnodenum} & user defined maximum number of BDD nodes \\ \hline 356\t{freenodes} & number of currently free BDD nodes \\ \hline 357\t{minfreenodes} & minimum number of nodes left after a BDD garbage collection \\ \hline 358\t{varnum} & number of defined BDD variables \\ \hline 359\t{cachesize} & number of cache entries \\ \hline 360\t{gbcnum} & number of BDD garbage collections done \\ \hline 361\end{tabular} 362 363\medskip 364 365The management of the node table and internal caches can be tuned 366using the following functions 367 368 369\begin{verbatim} 370 setMaxincrease : int -> int 371 setCacheratio : int -> int 372\end{verbatim}\index{HolBddLib!ML bindings!{setMaxincrease}@\ml{setMaxincrease}}\index{HolBddLib!ML bindings!{setCacheratio}@\ml{setCacheratio}} 373 374Evaluating \t{setMaxincrease~$n$} tells \Buddy{} that the maximum of new nodes added 375when doing an expansion of the nodetable should be $n$. The previous maximum is returned. 376 377Evaluating \t{setCacheratio~$n$} sets the cache ratio to $n$. 378For example, if $n$ is $4$ then the internal caches will a quarter the size of the 379nodetable. 380 381\subsection{BDDs representing {\t{true}} and {\t{false}}}\index{HolBddLib!BDD!constants} 382 383The atomic BDDs representing the two truthvalues are bound to the ML 384identifiers \t{TRUE} and \t{FALSE}, both of type \t{bdd}. 385 386Functions for mapping from ML Booleans to BDDs and vice versa are, respectively 387 388\begin{verbatim} 389 fromBool : bool -> bdd 390 toBool : bdd -> bool 391\end{verbatim}\index{HolBddLib!ML bindings!{fromBool}@\ml{fromBool}}\index{HolBddLib!ML bindings!{toBool}@\ml{toBool}} 392 393The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE. 394It raises the exception \t{Domain} on non-atomic BDDs. 395 396\begin{verbatim} 397 equal : bdd -> bdd -> bool 398\end{verbatim}\index{HolBddLib!ML bindings!{equal}@\ml{equal}} 399 400tests the equality of two BDDs. Thus \t{TRUE} is \t{equal} to \t{fromBool(true)} and 401\t{FALSE} is \t{equal} to \t{fromBool(false)}. 402 403\subsection{Variables}\index{HolBddLib!BDD!variables} 404 405In \Buddy{}, BDD variables are encoded as integers (type \t{int} in ML) and the BDD variable ordering 406is the numerical ordering. Thus to build a BDD to represent a \HOL{} term with a 407particular variable ordering it is necessary to map \HOL{} variables to 408integers so that the numerical order corresponds to the desired 409variable order. 410 411The number of variables in use must be declared using 412 413\begin{verbatim} 414 setVarnum : int -> unit 415\end{verbatim}\index{HolBddLib!ML bindings!{setVarnum}@\ml{setVarnum}} 416 417Evaluating $\t{setVarnum}~n$ declares that the $n$ variables $0$, 418$1$, $\ldots$ , $n{-}1$ are available for use. The number of variables 419can be increased dynamically during a session by calling \t{setVarnum} 420with a larger number. The number of variables cannot be decreased 421dynamically. The function 422 423\begin{verbatim} 424 getVarnum : unit -> int 425\end{verbatim}\index{HolBddLib!ML bindings!{getVarnum}@\ml{getVarnum}} 426 427returns the number of variables in use (i.e.~the argument of the last 428application of \t{setVarnum}). 429 430The function 431 432\begin{verbatim} 433 ithvar : int -> bdd 434\end{verbatim}\index{HolBddLib!ML bindings!{ithvar}@\ml{ithvar}} 435 436maps an ML integer to a BDD that consists of just the variable 437corresponding to the integer and 438 439\begin{verbatim} 440 nithvar : int -> bdd 441\end{verbatim}\index{HolBddLib!ML bindings!{nithvar}@\ml{nithvar}} 442 443maps 444an integer to the BDD representing the negation of the variable. 445 446Note that evaluating $\t{ithvar}~n$ or $\t{nithvar}~n$ will raise the exception 447\t{Fail} (with string argument \texttt{"Unknown variable"}) 448if $n$ has not been declared as in use, i.e.~if 449$\t{setVarnum}~m$ has not been previously evaluated for some $m$ 450greater than $n$. 451 452 453\subsection{Sets of variables and quantification}\label{varSet}\index{HolBddLib!BDD!quantification} 454 455\Buddy{} provides operations on BDDs for quantifying with respect to sets 456of variables. The module \t{bdd} provides a type \t{varSet} to represent such 457sets with, respectively, a constructor and two destructors: 458 459\begin{verbatim} 460 makeset : int list -> varSet 461 scanset : varSet -> int vector 462 fromSet : varSet -> bdd 463\end{verbatim}\index{HolBddLib!ML bindings!{makese}@\ml{makese}}\index{HolBddLib!ML bindings!{scanset}@\ml{scanset}}\index{HolBddLib!ML bindings!{fromSet}@\ml{fromSet}} 464 465The destructor \t{scanset} returns a vector of the variables in the 466set and the destructor \t{fromSet} returns a BDD representing the 467conjunction of the variables in the set. 468 469The following functions quantify BDDs with respect to sets of variables: 470 471\begin{verbatim} 472 forall : varSet -> bdd -> bdd 473 exist : varSet -> bdd -> bdd 474\end{verbatim}\index{HolBddLib!ML bindings!{forall}@\ml{forall}}\index{HolBddLib!ML bindings!{exist}@\ml{exist}} 475 476\subsection{Assignments, composition, replacement and restriction}\label{replace}\index{HolBddLib!BDD!assignments}\index{HolBddLib!BDD!composition}\index{HolBddLib!BDD!replacement}\index{HolBddLib!BDD!restriction} 477 478\Muddy{} provides a function for general purpose simultaneous 479substitution of arbitrary BDDs for variables in a given BDD (\t{veccompose}). It also 480provides and three optimised special cases: substituting for a single 481variable (\t{compose}), renaming variables (\t{replace}) and 482substituting with boolean constants (\t{restrict}). 483 484The operation \t{veccompose} performs the simultaneous substitution 485of BDDs for variables in a BDD. The argument of \t{veccompose} 486is a value of type \t{composeSet}\index{HolBddLib!ML bindings!{composeSet}@\ml{composeSet}} 487(created with a constructor \t{composeSet}) 488that specifies a list if pairs \t[(($n_1$,$b_1$),$\ldots$,, where BDD variable $n$ is to be pre 489 490\begin{verbatim} 491 composeSet : (int * bdd) list -> composeSet 492 veccompose : composeSet -> bdd -> bdd 493\end{verbatim}\index{HolBddLib!ML bindings!{veccompose}@\ml{veccompose}} 494 495A single variable can be replaced with a BDD using 496 497\begin{verbatim} 498 compose : bdd -> bdd -> int -> bdd 499\end{verbatim}\index{HolBddLib!ML bindings!{compose}@\ml{compose}} 500 501Evaluating \t{compose~$b_1$~$b_2$~$n$} substitutes $b_2$ for the 502variable $n$ in $b_1$. 503 504Variables can be renamed using the function \t{replace} that takes 505an argument of type \t{pairSet}\index{HolBddLib!ML bindings!{pairSet}@\ml{pairSet}} representing sets of pairs of variables 506(with constructor \t{makepairSet}) 507 508\begin{verbatim} 509 makepairSet : (int * int)list -> pairSet 510 replace : bdd -> pairSet -> bdd 511\end{verbatim}\index{HolBddLib!ML bindings!{makepairSet}@\ml{makepairSet}}\index{HolBddLib!ML bindings!{replace}@\ml{replace}} 512 513Evaluating \t{makepairSet[($x_1$,$x_1'$), $\ldots$ , ($x_n$,$x_n'$)]} 514creates a set of pairs specifying that $x_i'$ be substituted for $x_i$ 515(for $1\leq i\leq n$). A renaming with \t{replace} will fail if it 516would result in distinct variables being identified (i.e.~if the shape of the BDD would change). 517 518BDDs can be restricted by instantiating variables to {\t{TRUE}} or 519{\t{FALSE}} using the function \t{restrict} that takes 520as argument a value of type \t{assignment}\index{HolBddLib!ML bindings!{assignment}@\ml{assignment}} 521(which has a constructor \t{assignment} and destructor \t{getAssignment}). 522 523\begin{verbatim} 524 assignment : (int * bool)list -> assignment 525 getAssignment : assignment -> (int * bool) list 526 restrict : bdd -> assignment -> bdd 527\end{verbatim}\index{HolBddLib!ML bindings!{restrict}@\ml{restrict}}\index{HolBddLib!ML bindings!{assignment}@\ml{assignment}}\index{HolBddLib!ML bindings!{getAssignment}@\ml{getAssignment}} 528 529\noindent Evaluating \t{assignment[($v_1$,$t_1$), $\ldots$ , ($v_n$,$t_n$)]} 530creates an assignment specifying that each $v_i$ be instantiated to 531$\t{fromBool(}t_i\t{)}$ (for $1{\leq}i{\leq}n$). 532 533 534\subsection{Finding satisfying assignments}\index{HolBddLib!BDD!satisfying assignments} 535 536An assignment satisfying a BDD can be computed via \Buddy{} using 537 538\begin{verbatim} 539 satone : bdd -> assignment 540\end{verbatim}\index{HolBddLib!ML bindings!{makeset}@\ml{makeset}}\index{HolBddLib!ML bindings!{scanset}@\ml{scanset}}\index{HolBddLib!ML bindings!{fromSet}@\ml{fromSet}} 541 542The exception \t{Domain} is raised if the argument to \t{satone} is unsatisfiable. 543 544Alternatively, a model can be computed by an ML program such as: 545 546\begin{verbatim} 547 val findSat = 548 let fun findSatAux bdd = 549 if bdd.equal bdd bdd.TRUE 550 then [] 551 else 552 if bdd.equal bdd bdd.FALSE 553 then raise Domain 554 else 555 ((bdd.var bdd,true) :: findSatAux(bdd.high bdd) 556 handle Domain => 557 (bdd.var bdd, false) :: findSatAux(bdd.low bdd)) 558 in 559 assignment o findSatAux 560 end; 561\end{verbatim} 562 563The functions \t{satone} and \t{findSat} do not necessarily find the 564same satisfying assignment, if more than one exists. Also, 565\t{findSat} stops when it has found enough variable bindings to 566satisfy the BDD, so may not return an assignment giving values to all 567the variables. 568 569\subsection{Boolean operations on BDDs}\label{app}\index{HolBddLib!BDD!boolean operations} 570 571The structure \t{bdd} introduces a type \t{bddop} 572corresponding to Boolean operations on BDDs. 573The ML function 574 575\begin{verbatim} 576 apply : bdd -> bdd -> bddop -> bdd 577\end{verbatim}\index{HolBddLib!ML bindings!{apply}@\ml{apply}} 578 579applies a BDD operation to BDD values. 580 581\Buddy{} provides functions for calculating in a single step the 582result of performing a Boolean operation and then quantifying the 583result with respect to several variables. 584 585\begin{verbatim} 586 appall : bdd -> bdd -> bddop -> varSet -> bdd 587 appex : bdd -> bdd -> bddop -> varSet -> bdd 588\end{verbatim}\index{HolBddLib!ML bindings!{appall}@\ml{appall}}\index{HolBddLib!ML bindings!{appex}@\ml{appex}} 589 590The function \t{appall} universally quantifies the result of the 591Boolean operation and \t{appex} existentially quantifies it. 592 593\Muddy{} provides ten operations of type \t{bddop} and for each of 594these an ML infix, pre-defined using \t{apply}, of type \t{bdd~*~bdd~->~bdd}. 595 596 597 598\begin{center} 599 600\begin{tabular}{|l||l|l|} \hline 601\t{bddop}\index{HolBddLib!ML bindings!{bddop}@\ml{bddop}} & \t{bdd~*~bdd~->~bdd} & Result of applying to $(b_1,b_2)$\\ \hline\hline 602\t{And}\index{HolBddLib!ML bindings!{And}@\ml{And}} & \t{AND} & $b_1\wedge b_2$ \\ \hline 603\t{Nand}\index{HolBddLib!ML bindings!{Nand}@\ml{Nand}} & \t{NAND} & $\neg(b_1\wedge b_2)$ \\ \hline 604\t{Or}\index{HolBddLib!ML bindings!{Or}@\ml{Or}} & \t{OR} & $b_1\vee b_2$ \\ \hline 605\t{Nor}\index{HolBddLib!ML bindings!{Nor}@\ml{Nor}} & \t{NOR} & $\neg(b_1\vee b_2)$ \\ \hline 606\t{Biimp}\index{HolBddLib!ML bindings!{Biimp}@\ml{Biimp}} & \t{BIIMP} & $b_1= b_2$ \\ \hline 607\t{Xor}\index{HolBddLib!ML bindings!{Xor}@\ml{Xor}} & \t{XOR} & $\neg(b_1=b_2)$ \\ \hline 608\t{Imp}\index{HolBddLib!ML bindings!{Imp}@\ml{Imp}} & \t{IMP} & $b_1\imp b_2$ \\ \hline 609\t{Invimp}\index{HolBddLib!ML bindings!{Invimp}@\ml{Invimp}} & \t{INVIMP} & $b_2\imp b_1$ \\ \hline 610\t{Lessth}\index{HolBddLib!ML bindings!{Lessth}@\ml{Lessth}} & \t{LESSTH} & $\neg b_1\wedge b_2$ \\ \hline 611\t{Diff}\index{HolBddLib!ML bindings!{Diff}@\ml{Diff}} & \t{DIFF} & $b_1\wedge \neg b_2$ \\ \hline 612\end{tabular}\label{bddops} 613 614\end{center} 615 616\Muddy{} also provides a unary negation operator and ternary conditional operator. 617 618\begin{verbatim} 619 NOT : bdd -> bdd 620 ITE : bdd -> bdd -> bdd -> bdd 621\end{verbatim}\index{HolBddLib!ML bindings!{NOT}@\ml{NOT}}\index{HolBddLib!ML bindings!{ITE}@\ml{ITE}} 622 623$\t{NOT}~b$ is the BDD corresponding to `$\neg b$' and $\t{ITE}~b~b_1~b_2$ is the BDD corresponding 624to `$if~b~then~b_1~else~b_2$'. 625 626 627 628 629\subsection{Inspecting and counting nodes and states}\index{HolBddLib!BDD!nodes}\index{HolBddLib!BDD!states} 630 631The integer labelling a BDD node and the BDDs corresponding to the high 632(i.e.~{\t{true}}) and low (i.e.~{\t{false}}) nodes are obtained, 633respectively, with 634 635\begin{verbatim} 636 var : bdd -> int 637 high : bdd -> bdd 638 low : bdd -> bdd 639\end{verbatim}\index{HolBddLib!ML bindings!{var}@\ml{var}}\index{HolBddLib!ML bindings!{high}@\ml{high}}\index{HolBddLib!ML bindings!{low}@\ml{low}} 640 641Thus if $b$ is the BDD of ``${\it{if}}~x~{\it{then}}~t_1~{\it{else}}~t_2$'' 642then $\t{var}~b$ will return the number representing variable $x$, 643$\t{high}~b$ will return the BDD of $t_1$ and $\t{low}~b$ will return 644the BDD of $t_2$. 645 646Note that \t{var}, \t{high} and \t{low} raise an exception if applied 647to \t{TRUE} or \t{FALSE}. 648 649The entire \Buddy{} node table of a BDD can be copied into ML using 650 651\begin{verbatim} 652 nodetable : bdd -> int * (int * int * int)vector 653\end{verbatim}\index{HolBddLib!ML bindings!{nodetable}@\ml{nodetable}} 654 655The integer returned as the first component of the pair is a pointer 656(starting from 0) into the second component, a vector of node 657descriptors. This pointer points to the root node. Each node 658descriptor is a triple of integers $(v,l,h)$, where $v$ is the node 659label (i.e.~a number representing a variable), $l$ points to the low 660({\t{false}}) node in the vector and $h$ points to the high 661({\t{true}}) node. The first two nodes in the vector are special: 662they represent {\t{true}} and {\t{false}}, respectively, and arbitrarily have 663the structure $(0,0,0)$. 664 665The number of nodes in a BDD is computed by the function 666 667\begin{verbatim} 668 nodecount : bdd -> int 669\end{verbatim}\index{HolBddLib!ML bindings!{nodecount}@\ml{nodecount}} 670 671This could be defined by 672 673\begin{verbatim} 674 fun nodecount bdd = Vector.length(snd(nodetable bdd)); 675\end{verbatim} 676 677However, \t{nodecount} defined this way is likely to run out of space 678on large BDDs (since it involves copying the argument BDD from 679\Buddy's representation into an ML vector). Thus the ML function 680provided by \Muddy{} invokes \Buddy's \t{nodecount} function directly 681and so is space-efficient. 682 683The 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 684function 685 686\begin{verbatim} 687 satcount : bdd -> real 688\end{verbatim}\index{HolBddLib!ML bindings!{satcount}@\ml{satcount}} 689 690The answer is exact until the result is too big to be represented as a 691Moscow ML integer. Real numbers are used so that results can be 692returned when this happens. 693 694The function 695 696\begin{verbatim} 697 support : bdd -> varSet 698\end{verbatim}\index{HolBddLib!ML bindings!{support}@\ml{support}} 699 700gives the variables that a BDD depends on. 701 702An application is to define 703a function that counts the number of valuations of a BDD using 704\t{satcount}. 705 706\begin{verbatim} 707 statecount : bdd -> real 708\end{verbatim}\index{HolBddLib!ML bindings!{statecount}@\ml{statecount}} 709 710The 711definition of \t{statecount} is 712 713\begin{verbatim} 714fun statecount bdd = 715 let val sat = satcount bdd 716 val total = Real.fromInt(getVarnum()) 717 val sup = scanset(support bdd) 718 val numsup = Real.fromInt(Vector.length sup) 719 val free = total - numsup 720 in 721 if equal bdd TRUE 722 then 0.0 723 else sat / Math.pow(2.0, free) 724 end 725\end{verbatim} 726% 727If a BDD is representing a set of states, then \t{statecount} gives 728the number of states in the set (hence the name). 729 730 731\subsection{Coudert, Berthet \& Madre simplification}\index{HolBddLib!BDD!simplification} 732 733The ML function 734 735\begin{verbatim} 736 simplify : bdd -> bdd -> bdd 737\end{verbatim}\index{HolBddLib!ML bindings!{simplify}@\ml{simplify}} 738 739simplifies its second argument under the assumption that the first 740argument is true. Thus evaluating 741\t{simplify~$b_1$~$b_2$} results in a BDD $b_2'$, hopefully simpler than $b_2$, such that 742$b_1 \Rightarrow (b_2 = b_2')$ or, equivalently, \mbox{$b_1 \wedge b_2 = b_1 \wedge b_2'$}. 743More precisely, 744the relationship between $b_1$, $b_2$ and $b_2'$ is that 745the BDD \t{IMP($b_1$,BIIMP($b_2$,$b_2'$))} is the BDD \t{TRUE} 746(or, equivalently, that \t{AND($b_1$,$b_2$)} and \t{AND($b_1$,$b_2'$)} 747are \t{equal}, i.e.~the same BDD). 748 749For more details see Henrik Reif Andersen's lecture 750notes on BDDs \cite{HenrikNotes}, where 751the algorithm underlying \t{simplify} is described and attributed to a paper by 752Coudert, Berthet and Madre \cite{CoudertBerthetMadre}. 753 754\subsection{Saving, hashing and printing BDDs}\label{printing}\index{HolBddLib!BDD!saving}\index{HolBddLib!BDD!hashing}\index{HolBddLib!BDD!printing} 755 756BDDs can be saved on disk with the functions 757 758\begin{verbatim} 759 bddSave : string -> bdd -> unit 760 bddLoad : string -> bdd 761\end{verbatim}\index{HolBddLib!ML bindings!{bddSave}@\ml{bddSave}}\index{HolBddLib!ML bindings!{bddLoad}@\ml{bddLoad}} 762 763The string argument is a file name. 764 765\Buddy{} provides two ways of printing BDDs: (i) as the set of paths from 766the root node to the {\it{true}} node and (ii) to the format used by 767the \t{dot} graph drawing 768program\footnote{\texttt{http://www.research.att.com/sw/tools/graphviz/}}. 769 770The function 771 772\begin{verbatim} 773 hash : bdd -> int 774\end{verbatim}\index{HolBddLib!ML bindings!{hash}@\ml{hash}} 775 776hashes a bdd to an integer. 777 778The functions for printing BDDs are; 779 780\begin{verbatim} 781 printset : bdd -> unit 782 printdot : bdd -> unit 783 fnprintset : string -> bdd -> unit 784 fnprintdot : string -> bdd -> unit 785\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}} 786 787\t{printset} and \t{printdot} print to standard output, whilst 788\t{fnprintset} and \t{fnprintdot} print to a file with the supplied 789name. 790 791\t{printset} and \t{fnprintset} print out a sequence of paths, each one having the form 792 793\smallskip 794 795~$\t{}<m_0\t{:}n_0\t{,} \ldots \t{,} m_l\t{:}n_l\t{>}$ 796 797\smallskip 798 799where the $n_0$, $\ldots$ , $n_l$ after the colon (\t{:}) are \t{0} or 800\t{1} and indicate that the next node in the path is reached by 801following the low ({\t{false}}) or high ({\t{true}}) pointer, 802respectively. 803 804For 805example, evaluating 806 807\smallskip 808~\t{printset~(AND(ithvar~0,~OR(ithvar~1,~NOT(ithvar~2))))} 809\smallskip 810 811results in 812 813\smallskip 814~\t{<0:1,~1:0,~2:0><0:1,~1:1>} 815\smallskip 816 817which is best understood by looking at the diagram of the BDD drawn by 818\t{dot} that appears below. 819 820To illustrate printing to \t{dot} format, the same BDD can be 821printed to a file \t{ex} by evaluating 822 823\smallskip 824~\t{fnprintdot~"ex"~(AND(ithvar~0,~OR(ithvar~1,~NOT(ithvar~2))))} 825\smallskip 826 827executing ~\t{dot~-Tps~ex~>~ex.ps} (in Unix) results in 828the following Postscript diagram of a BDD 829 830\begin{center} 831\includegraphics[width=3cm, height=5cm]{figs/ex} 832\end{center} 833 834\subsection{Dynamic variable reordering}\index{HolBddLib!BDD!dynamic reordering} 835 836\Buddy{} provides functions for dynamic variable reordering using a variety of methods. 837See the \Buddy{} documentation \cite{BuDDy} for further details. The dynamic reordering 838types and functions provided in ML via \Muddy{} are in the structure \t{bdd} and are 839 840\begin{verbatim} 841 eqtype fixed 842 FIXED : fixed 843 FREE : fixed 844 845 addvarblock : varnum -> varnum -> fixed -> unit 846 clrvarblocks : unit -> unit 847 848 eqtype method 849 WIN2 : method 850 WIN2ITE : method 851 SIFT : method 852 SIFTITE : method 853 RANDOM : method 854 REORDER_NONE : method 855 856 reorder : method -> unit 857 autoReorder : method -> method 858 autoReorderTimes : method -> int -> method 859 860 getMethod : unit -> method 861 getTimes : unit -> int 862 863 disableReorder : unit -> unit 864 enableReorder : unit -> unit 865 866 varToLevel : varnum -> int 867 varAtLevel : int -> varnum 868\end{verbatim} 869 870\subsection{The \Muddy{} structure \t{fdd}}\label{fdd}\index{HolBddLib!finite domains} 871 872The structure \t{fdd} provides functions for manipulating values of finite domains. 873Functions are provided to allocate blocks of BDD variables to represent integer values instead 874of only Booleans. 875 876Encoding is done with the least significant bits first in the BDD ordering. For example, if variables 877$v_0, v_1, v_2, v_3$ are used to encode $12$, then the encoding would yield 878$v_0=0$, $v_1=0$, $v_2=1$ and $v_3=1$. 879 880See the \Buddy{} documentation \cite{BuDDy} for further details. See the ML structure \t{fdd} 881for the \Buddy{} facilities provides in ML via \Muddy: 882 883\begin{verbatim} 884 type fddvar 885 886 extDomain : int list -> fddvar list 887 clearAll : unit -> unit 888 domainNum : unit -> int 889 domainSize : fddvar -> int 890 varNum : fddvar -> int 891 vars : fddvar -> bdd.varnum list 892 ithSet : fddvar -> bdd.varSet 893 domain : fddvar -> bdd.bdd 894 setPairs : (fddvar * fddvar) list -> bdd.pairSet 895\end{verbatim} 896 897\subsection{The \Muddy{} structure \t{bvec}}\label{bvec}\index{HolBddLib!BDD!vectors} 898 899The structure \t{bvec} provides tools for encoding integers as arrays 900of BDDs, where each BDD represents one bit of an expression. 901 902See the \Buddy{} documentation \cite{BuDDy} for further details. See the ML structure \t{bvec} 903for the \Buddy{} facilities provides in ML via \Muddy{}. 904 905 906\begin{verbatim} 907 type bvec 908 909 bvectrue : fdd.precision -> bvec 910 bvecfalse : fdd.precision -> bvec 911 con : fdd.precision -> int -> bvec 912 var : fdd.precision -> bdd.varnum -> int -> bvec 913 varfdd : fdd.fddvar -> bvec 914 915 coerce : fdd.precision -> bvec -> bvec 916 917 isConst : bvec -> bool 918 getConst : bvec -> int 919 lookupConst : bvec -> int option 920 921 add : bvec * bvec -> bvec 922 sub : bvec * bvec -> bvec 923 mul : bvec * bvec -> bvec 924 mulfixed : bvec * int -> bvec 925 div : bvec * bvec -> bvec * bvec 926 divfixed : bvec * int -> bvec * bvec 927 divi : bvec * bvec -> bvec 928 divifixed : bvec * int -> bvec 929 930 modu : bvec * bvec -> bvec 931 modufixed : bvec * int -> bvec 932 shl : bvec -> bvec -> bdd.bdd -> bvec 933 shlfixed : bvec -> int -> bdd.bdd -> bvec 934 shr : bvec -> bvec -> bdd.bdd -> bvec 935 shrfixed : bvec -> int -> bdd.bdd -> bvec 936 937 lth : bvec * bvec -> bdd.bdd 938 lte : bvec * bvec -> bdd.bdd 939 gth : bvec * bvec -> bdd.bdd 940 gte : bvec * bvec -> bdd.bdd 941 equ : bvec * bvec -> bdd.bdd 942 neq : bvec * bvec -> bdd.bdd 943\end{verbatim} 944 945\subsection{Storage allocation and garbage collection}\index{HolBddLib!BDD!garbage collection} 946\label{sec:technical-details} 947 948The heart of the \Muddy{} package is mostly stub code that mirrors the 949\Buddy{} API and takes care of translating C values into SML values and 950vice versa. 951 952The most tricky part is to make the \mosml{} garbage collector cooperate 953with the \Buddy{} garbage collector (we don't want either collector to 954try to collect the other's garbage). The cooperation is done by using 955the \emph{finalized values} facility of the \mosml{} runtime system. 956That is, whenever a \texttt{bdd} value is returned from the \Buddy{} 957library, \Muddy{} register it as an external root (via 958\verb+bdd_addref+) and wraps it into a finalized value. 959 960A finalized value, in the \mosml{} runtime system, is a pair where the 961first component is the \emph{destructor} (a function pointer) and the 962second component is the \emph{data} (typicaly a pointer). When the 963\mosml{} collector collect a finalized value it apply the destructor on 964the data. In the case of the \Muddy{} package the destructor is 965\verb+bdd_delref+ and the data is the node-index returned by \Buddy{}. 966 967Output showing the activation of the \Buddy{} garbage collector can be generated 968using the function 969 970\begin{verbatim} 971 verbosegc : (string * string) option -> unit 972\end{verbatim}\index{HolBddLib!ML bindings!{verbosegc}@\ml{verbosegc}} 973 974Evaluating \t{verbosegc(SOME($pregc$,$postgc$))} instructs BuDDy to print 975$pregc$ when a BuDDy GC is initiated and print $postgc$ when the 976\Buddy{} GC is completed. 977 978\section{\t{HolBddLib}}\label{HolBddLib} 979 980\t{HolBddLib} currently consists of five modules 981 982\begin{enumerate} 983\item \t{Varmap} defines the ML type \t{varmap} that represents mappings, 984often denoted by $\rho$, 985from HOL variables to BDD variables; 986 987\item \t{PrintBdd} provides some rudimentary facilities for printing 988BDDs with respect to a varmap; 989 990\item \t{PrimitiveBddRules} defines the protected type \termbddty 991representing BDD representation judgements \termbdd{a}{\rho}{t}{b} 992with the semantics that under assumptions $a$, term $t$ is represented by BDD $b$ with respect to 993varmap $\rho$; 994 995\item \t{DerivedBddRules} defines some derived rules for computing 996the representation of the reachable states of a transition system, 997and also for finding shortest paths to states satisfying a given property; 998 999\item \t{MachineTransitionTheory} contains HOL reachability and fixedpoint theorems needed 1000for the derived rules in \t{DerivedBddRules}. 1001 1002 1003\end{enumerate} 1004 1005 1006Executing 1007 1008\vspace*{-2mm} 1009 1010\begin{verbatim} 1011 load "HolBddLib"; 1012\end{verbatim} 1013 1014\vspace*{-2mm} 1015 1016loades these five modules and 1017initialises \Buddy{} with a nodesize of 1000000 1018and cachesize of 10000. 1019 1020If you want to perform your own \Buddy{} initialisation with different 1021values, then instead of loading \t{HolBddLib}, load \t{bdd} and then 1022call \t{bdd.init} with the parameters you want (see Section~\ref{init}). 1023 1024\subsection{The structure \ml{Varmap}}\label{Varmap}\index{HolBddLib!termbdd@\ml{term\_bdd}!varmaps} 1025 1026The type \t{varmap} is defined by 1027 1028\vspace*{-2mm} 1029 1030\begin{verbatim} 1031 type varmap = (string, int) Binarymap.dict 1032\end{verbatim}\index{HolBddLib!ML bindings!{varmap}@\ml{varmap}} 1033 1034\vspace*{-2mm} 1035 1036Strings are the names of HOL boolean variables and the integers associated with them 1037are the corresponding BDD variables. 1038 1039The following operations and predicates on varmaps are provided: 1040 1041\begin{verbatim} 1042 empty : varmap 1043 insert : string * int -> varmap -> varmap 1044 remove : string -> varmap -> varmap 1045 peek : varmap -> string -> int option 1046 dest : varmap -> (string * int) list 1047 eq : varmap * varmap -> bool 1048 size : varmap -> int 1049 extends : varmap -> varmap -> bool 1050 unify : varmap -> varmap -> varmap 1051\end{verbatim} 1052\index{HolBddLib!ML bindings!{Varmap.empty}@\ml{Varmap.empty}} 1053\index{HolBddLib!ML bindings!{Varmap.insert}@\ml{Varmap.insert}} 1054\index{HolBddLib!ML bindings!{Varmap.remove}@\ml{Varmap.remove}} 1055\index{HolBddLib!ML bindings!{Varmap.peek}@\ml{Varmap.peek}} 1056\index{HolBddLib!ML bindings!{Varmap.dest}@\ml{Varmap.dest}} 1057\index{HolBddLib!ML bindings!{Varmap.eq}@\ml{Varmap.eq}} 1058\index{HolBddLib!ML bindings!{Varmap.size}@\ml{Varmap.size}} 1059\index{HolBddLib!ML bindings!{Varmap.extends}@\ml{Varmap.extends}} 1060\index{HolBddLib!ML bindings!{Varmap.unify}@\ml{Varmap.unify}} 1061 1062with the semantics 1063 1064\bigskip 1065 1066\begin{tabular}{|l|l|} \hline 1067\t{Varmap.empty} & the empty varmap \\ \hline 1068\t{Varmap.insert} & add an entry \\ \hline 1069\t{Varmap.remove} & delete an entry for a variable \\ \hline 1070\t{Varmap.peek} & lookup the value of a variable \\ \hline 1071\t{Varmap.dest} & convert to a list of pairs \\ \hline 1072\t{Varmap.eq} & pointer equality of varmaps ({\it not} general equality) \\ \hline 1073\t{Varmap.size} & number of entries \\ \hline 1074\t{Varmap.extends} & test if first argument included in second argument\\ \hline 1075\t{Varmap.unify} & compute smallest varmap that extends both arguments\\ \hline 1076\end{tabular} 1077 1078\subsection{The structure \ml{PrintBdd}}\label{PrintBdd}\index{HolBddLib!termbdd@\ml{term\_bdd}!printing} 1079 1080\t{PrintBdd} builds on top of \Muddy's support for drawing BDDs using the \t{dot} 1081program (see Section~\ref{printing}). Three functions are provided. 1082 1083\begin{verbatim} 1084 dotBdd : string -> string -> bdd -> bdd 1085 dotLabelledTermBdd : string -> string -> term_bdd -> unit 1086 dotTermBdd : term_bdd -> unit 1087\end{verbatim} 1088\index{HolBddLib!ML bindings!{dotBdd}@\ml{dotBdd}} 1089\index{HolBddLib!ML bindings!{dotLabelledTermBdd}@\ml{dotLabelledTermBdd}} 1090\index{HolBddLib!ML bindings!{dotTermBdd}@\ml{dotTermBdd}} 1091 1092\begin{description} 1093\item[$\t{dotBdd}~file~label~bdd$]\mbox{}\\ 1094prints the BDD $bdd$ to $file$\t{.dot} with 1095the label being the string $label$. The BDD variables are printed as the numbers used by \Buddy{}. 1096The \t{dot} program is then invoked to create 1097a postscript file $file$\t{.ps}. The argument BDD is returned. 1098 1099\item[$\t{dotLabelledTermBdd}~file~label~tb$]\mbox{}\\ 1100prints the 1101BDD part of \termbddty $tb$ with the nodes labelled with 1102the variables specified in the varmap part of $tb$. A file $file$\t{.ps} 1103is created, and the BDD is labelled with the string $label$. 1104 1105 1106\item[$\t{dotTermBdd}~tb$]\mbox{}\\ 1107prints the 1108BDD part of \termbddty $tb$ with the nodes labelled with 1109the variables specified in the varmap part of $tb$. A file \t{ScratchBdd.ps} 1110is created, and the BDD is labelled by default with a representation 1111of the term part of $tb$. The default labels 1112can be suppressed (i.e.\ set to be always the empty string) by assigning \t{false} 1113to the global reference \t{dotTermBddFlag}. 1114\end{description} 1115 1116\subsection{The structure \t{PrimitiveBddRules}}\label{PrimitiveBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!primitive rules} 1117 1118The structure \ml{PrimitiveBddRules} defines the type \termbddty{} by 1119 1120\vspace*{-2mm} 1121 1122\begin{verbatim} 1123 type assums = term HOLset.set; 1124 datatype term_bdd = TermBdd of assums * varmap * term * bdd; 1125\end{verbatim}\index{HolBddLib!ML bindings!termbdd@\ml{term\_bdd}}\index{HolBddLib!ML bindings!{assums}@\ml{assums}} 1126 1127\vspace*{-2mm} 1128 1129The constructor \t{TermBdd} is not exported, so the only way to construct 1130values of type \termbddty is using the following inference rules 1131(which are described in more detail in the rest of this section). 1132 1133\begin{verbatim} 1134 BddExtendVarmap : varmap->term_bdd->term_bdd 1135 BddFreevarsContractVarmap : term->term_bdd->term_bdd 1136 BddSupportContractVarmap : term->term_bdd->term_bdd 1137 BddVar : bool->varmap->term->term_bdd 1138 BddCon : bool->varmap->term_bdd 1139 BddNot : term_bdd->term_bdd 1140 BddIte : term_bdd*term_bdd*term_bdd->term_bdd 1141 BddOp : bddop*term_bdd*term_bdd->term_bdd 1142 BddForall : term list->term_bdd->term_bdd 1143 BddExists : term list->term_bdd->term_bdd 1144 BddAppall : term list->bddop*term_bdd*term_bdd->term_bdd 1145 BddAppex : term list->bddop*term_bdd*term_bdd->term_bdd 1146 BddCompose : term_bdd*term_bdd->term_bdd->term_bdd 1147 BddListCompose : (term_bdd*term_bdd)list->term_bdd->term_bdd 1148 BddRestrict : (term_bdd*term_bdd)list->term_bdd->term_bdd 1149 BddReplace : (term_bdd*term_bdd)list->term_bdd->term_bdd 1150 BddEqMp : thm->term_bdd->term_bdd 1151 BddSimplify : term_bdd*term_bdd->term_bdd 1152 BddFindModel : term_bdd->term_bdd 1153\end{verbatim} 1154 1155Destructor functions \t{dest\_term\_bdd}, \t{getAssums}, \t{getVarmap}, \t{getTerm} 1156and \t{getBdd} for values of type \termbddty are described in Section~\ref{misc} 1157 1158There is also a single oracle function 1159\t{BddThmOracle} that derives the HOL theorem $a \vdash t$ 1160from the representation judgement \termbdd{a}{\rho}{t}{\ml{TRUE}} 1161(details are in Section~\ref{oracle}). 1162 1163Many of the rules assume that the varmaps in their \termbddty 1164arguments are all equal. To apply these rules to hypotheses with 1165different varmaps it may be possible to use \t{BddExtendVarmap}, 1166\t{BddFreevarsContractVarmap} or \t{BddSupportContractVarmap} to make 1167the varmaps equal. It is expected that derived rules to enable 1168judgements with different varmaps to be combined will be implemented, 1169however, as the soundness conditions for these are potentially subtle, 1170such rules have not been included in the `trusted kernel'. 1171 1172Currently we have no formal treatment of notions of soundness or 1173completeness for the rules in \t{PrimitiveBddRules}, though this is 1174being thought about. We think the rules are `obviously sound', but 1175such intuitions are known to be unreliable! Our intuition about 1176completeness is weaker: it is probable that as more experience with 1177derived rules is obtained, the need for additional primitive rules 1178will appear. Support for `local scopes' (combining judgements with 1179different variable orders) is an area that may reveal incompleteness 1180in the current rules. 1181 1182\subsection{Rules for generating representation judgements}\label{term-bdd-rules} 1183 1184The notation $a_1 \cup a_2$ denotes the union of $a_1$ and $a_2$ 1185Assumptions of 1186representation judgements are identified up to $\alpha$-conversion (as 1187are assumptions of HOL theorems). 1188The implementation is $a_1 \cup a_2~=~\t{HOLset.union}~a_1~a_2$. 1189The empty set of assumptions is denoted by \emptyass, a set of 1190assumptions containing terms $t_1, \ldots ,t_n$ is denoted by 1191$\setass{t_1, \ldots ,t_n}$ and 1192$\termbdd{\emptyass}{\rho}{t}{b}$ is abbreviated to 1193$\termbdd{}{\rho}{t}{b}$. 1194 1195 1196\subsection{Extending and contracting the varmap} 1197 1198\newsavebox\BddExtendVarmap 1199\begin{lrbox}\BddExtendVarmap 1200\begin{minipage}{\minipagewidth} 1201 1202\begin{footnotesize} 1203{\verb+BddExtendVarmap : varmap -> term_bdd -> term_bdd +} 1204\end{footnotesize} 1205\vspace*{-3mm} 1206 1207\noindent \rule\minipagewidth{0.1pt} 1208 1209\vspace*{-2mm} 1210 1211$$\begin{array}{c} 1212{\t{\footnotesize Varmap.extends}}~\rho_1~\rho_2 \qquad \termbdd{a}{\rho_1}{t}{b} 1213\\ \hline 1214\termbdd{a}{\rho_2}{t}{b} 1215\end{array}$$ 1216 1217\noindent \rule\minipagewidth{0.1pt} 1218 1219\begin{footnotesize} 1220Raises \t{BddExtendVarmapError} if $\rho_2$ doesn not extend $\rho_1$ 1221\end{footnotesize} 1222\end{minipage} 1223\end{lrbox} 1224\fbox{\usebox{\BddExtendVarmap}}\index{HolBddLib!ML bindings!{BddExtendVarmap}@\ml{BddExtendVarmap}} 1225 1226\bigskip 1227 1228\newsavebox\BddFreevarsContractVarmap 1229\noindent\begin{lrbox}\BddFreevarsContractVarmap 1230\begin{minipage}{\minipagewidth} 1231 1232\begin{footnotesize} 1233{\verb+BddFreevarsContractVarmap : term -> term_bdd -> term_bdd +} 1234\end{footnotesize} 1235\vspace*{-3mm} 1236 1237\noindent \rule\minipagewidth{0.1pt} 1238 1239\vspace*{-2mm} 1240 1241$$\begin{array}{c} 1242\termbdd{a}{\rho}{t}{b} \qquad \mbox{$v$ not free in $t$} 1243\\ \hline 1244\termbdd{a}{({\texttt{\footnotesize{Varmap.remove~"}}}v{\texttt{\footnotesize{"}}}~\rho)}{t}{b} 1245\end{array}$$ 1246 1247\noindent \rule\minipagewidth{0.1pt} 1248 1249\begin{footnotesize} 1250Raises \t{BddFreevarsContractVarmapError} if $v$ not free in $t$ 1251\end{footnotesize} 1252\end{minipage} 1253\end{lrbox} 1254\fbox{\usebox{\BddFreevarsContractVarmap}}\index{HolBddLib!ML bindings!{BddFreevarsContractVarmap}@\ml{BddFreevarsContractVarmap}} 1255 1256 1257 1258\bigskip 1259 1260\newsavebox\BddSupportContractVarmap 1261\noindent\begin{lrbox}\BddSupportContractVarmap 1262\begin{minipage}{\minipagewidth} 1263 1264\begin{footnotesize} 1265{\verb+BddSupportContractVarmap : term -> term_bdd -> term_bdd +} 1266\end{footnotesize} 1267\vspace*{-3mm} 1268 1269\noindent \rule\minipagewidth{0.1pt} 1270 1271\vspace*{-2mm} 1272 1273$$\begin{array}{c} 1274\termbdd{a}{\rho}{t}{b} \qquad \mbox{$\rho(v)$ doesn't occur in $b$} 1275\\ \hline 1276\termbdd{a}{({\texttt{\footnotesize{Varmap.remove~"}}}v{\texttt{\footnotesize{"}}}~\rho)}{t}{b} 1277\end{array}$$ 1278 1279\noindent \rule\minipagewidth{0.1pt} 1280 1281\begin{footnotesize} 1282Raises \t{BddSupportContractVarmapError} if $\rho(v)$ not in the support of $b$ 1283\end{footnotesize} 1284\end{minipage} 1285\end{lrbox} 1286\fbox{\usebox{\BddSupportContractVarmap}}\index{HolBddLib!ML bindings!{BddSupportContractVarmap}@\ml{BddSupportContractVarmap}} 1287 1288 1289\subsection{Variables and constants} 1290 1291\newsavebox\BddVar 1292\begin{lrbox}\BddVar 1293\begin{minipage}{\minipagewidth} 1294 1295\begin{footnotesize} 1296{\verb+BddVar : bool -> varmap -> term -> term_bdd +} 1297\end{footnotesize} 1298\vspace*{-3mm} 1299 1300\noindent \rule\minipagewidth{0.1pt} 1301 1302\vspace*{-2mm} 1303 1304$$\begin{array}{c} 1305\begin{array}{c} 1306\rho(v)=n 1307\\ \hline 1308\termbdd{}{\rho}{v}{{\t{\footnotesize ithvar}}~n} 1309\end{array} ~{\t{\footnotesize BddVar~true}} 1310 1311\\[8mm] 1312 1313\begin{array}{c} 1314\rho(v)=n 1315\\ \hline 1316\termbdd{}{\rho}{\neg v}{{\t{\footnotesize nithvar}}~n} 1317\end{array}~ {\t{\footnotesize BddVar~false}} 1318 1319\end{array}$$ 1320 1321\noindent \rule\minipagewidth{0.1pt} 1322 1323\begin{footnotesize} 1324Raises \t{BddVarError} if $v$ not in the domain of $\rho$ 1325\end{footnotesize} 1326\end{minipage} 1327\end{lrbox} 1328\fbox{\usebox{\BddVar}}\index{HolBddLib!ML bindings!{BddVar}@\ml{BddVar}} 1329 1330\bigskip 1331 1332\newsavebox\BddCon 1333\noindent\begin{lrbox}\BddCon 1334\begin{minipage}{\minipagewidth} 1335 1336\begin{footnotesize} 1337{\verb+BddCon : bool -> varmap -> term_bdd +} 1338\end{footnotesize} 1339\vspace*{-3mm} 1340 1341\noindent \rule\minipagewidth{0.1pt} 1342 1343\vspace*{-2mm} 1344 1345$$\begin{array}{c} 1346\begin{array}{c} 1347 1348\\ \hline 1349\termbdd{}{\rho}{{\t{\footnotesize T}}}{{\t{\footnotesize TRUE}}} 1350\end{array} ~{\t{\footnotesize BddCon~true}} 1351 1352\\[8mm] 1353 1354\begin{array}{c} 1355\\ \hline 1356\termbdd{}{\rho}{{\t{\footnotesize F}}}{{\t{\footnotesize FALSE}}} 1357\end{array}~ {\t{\footnotesize BddCon~false}} 1358 1359\end{array}$$ 1360 1361\noindent \rule\minipagewidth{0.1pt} 1362 1363\begin{footnotesize} 1364Always succeeds 1365\end{footnotesize} 1366\end{minipage} 1367\end{lrbox} 1368\fbox{\usebox{\BddCon}}\index{HolBddLib!ML bindings!{BddCon}@\ml{BddCon}} 1369 1370\subsection{Boolean operations} 1371 1372 1373 1374\newsavebox\BddNot 1375\begin{lrbox}\BddNot 1376\begin{minipage}{\minipagewidth} 1377 1378\begin{footnotesize} 1379{\verb+BddNot : term_bdd -> term_bdd +} 1380\end{footnotesize} 1381\vspace*{-3mm} 1382 1383\noindent \rule\minipagewidth{0.1pt} 1384 1385\vspace*{-2mm} 1386 1387$$\begin{array}{c} 1388\termbdd{a}{\rho}{t}{b} 1389\\ \hline 1390\termbdd{a}{\rho}{\neg t}{{\t{\footnotesize NOT}}~b} 1391\end{array}$$ 1392 1393\noindent \rule\minipagewidth{0.1pt} 1394 1395\begin{footnotesize} 1396Always succeeds 1397\end{footnotesize} 1398\end{minipage} 1399\end{lrbox} 1400\fbox{\usebox{\BddNot}}\index{HolBddLib!ML bindings!{BddNot}@\ml{BddNot}} 1401 1402\bigskip 1403 1404\newsavebox\BddIte 1405\noindent\begin{lrbox}\BddIte 1406\begin{minipage}{\minipagewidth} 1407 1408\begin{footnotesize} 1409{\verb+BddIte : term_bdd * term_bdd * term_bdd -> term_bdd +} 1410\end{footnotesize} 1411\vspace*{-3mm} 1412 1413\noindent \rule\minipagewidth{0.1pt} 1414 1415\vspace*{-2mm} 1416 1417$$\begin{array}{c} 1418\termbdd{a}{\rho}{t}{b} \qquad \termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2} 1419\\ \hline 1420\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} 1421\end{array}$$ 1422 1423\noindent \rule\minipagewidth{0.1pt} 1424 1425\begin{footnotesize} 1426Raises {\t{\footnotesize BddIteError}} if the varmaps of the hypotheses are not all 1427pointer equal 1428\end{footnotesize} 1429\end{minipage} 1430\end{lrbox} 1431\fbox{\usebox{\BddIte}}\index{HolBddLib!ML bindings!{BddIte}@\ml{BddIte}} 1432 1433 1434\bigskip 1435 1436\newsavebox\BddOp 1437\noindent\begin{lrbox}\BddOp 1438\begin{minipage}{\minipagewidth} 1439 1440\begin{footnotesize} 1441{\verb+BddOp : bddop * term_bdd * term_bdd -> term_bdd +} 1442\end{footnotesize} 1443\vspace*{-3mm} 1444 1445\noindent \rule\minipagewidth{0.1pt} 1446 1447\vspace*{-2mm} 1448 1449$$\begin{array}{c} 1450\termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2} 1451\\ \hline 1452\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} 1453\end{array}$$ 1454 1455\noindent \rule\minipagewidth{0.1pt} 1456 1457\begin{footnotesize} 1458\t{termApply~$t_1$~$t_2$~$bddop$} applies 1459the HOL operation 1460corresponding to the \Buddy{} BDD operation $bddop$ to terms $t_1$ and $t_2$ 1461(see Section~\ref{misc}). The exception 1462{\t{\footnotesize BddOpError}} is raised if the varmaps of the hypotheses are not pointer equal 1463\end{footnotesize} 1464\end{minipage} 1465\end{lrbox} 1466\fbox{\usebox{\BddOp}}\index{HolBddLib!ML bindings!{BddOp}@\ml{BddOp}} 1467 1468 1469\subsection{Quantification} 1470 1471\newsavebox\BddForall 1472\begin{lrbox}\BddForall 1473\begin{minipage}{\minipagewidth} 1474 1475\begin{footnotesize} 1476{\verb+BddForall : term list -> term_bdd -> term_bdd +} 1477\end{footnotesize} 1478\vspace*{-3mm} 1479 1480\noindent \rule\minipagewidth{0.1pt} 1481 1482\vspace*{-2mm} 1483 1484$$\begin{array}{c} 1485\termbdd{a}{\rho}{t}{b} \qquad \rho(v_1)=n_1,~ $\ldots$~,~ \rho(v_i)=n_i 1486\\ \hline 1487\termbdd{a}{\rho}{({\scriptstyle\forall} v_1~\cdots~v_i.~t)}% 1488{{\t{\footnotesize forall~(makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b} 1489\end{array}$$ 1490 1491\noindent \rule\minipagewidth{0.1pt} 1492 1493\begin{footnotesize} 1494Raises \t{BddForallError} if any of the terms in the term list argument 1495are not boolean variables in the domain of $\rho$, 1496or occur free in any assumption 1497\end{footnotesize} 1498\end{minipage} 1499\end{lrbox} 1500\fbox{\usebox{\BddForall}}\index{HolBddLib!ML bindings!{BddForall}@\ml{BddForall}} 1501 1502\bigskip 1503 1504 1505\newsavebox\BddExists 1506\noindent\begin{lrbox}\BddExists 1507\begin{minipage}{\minipagewidth} 1508 1509\begin{footnotesize} 1510{\verb+BddExists : term list -> term_bdd -> term_bdd +} 1511\end{footnotesize} 1512\vspace*{-3mm} 1513 1514\noindent \rule\minipagewidth{0.1pt} 1515 1516\vspace*{-2mm} 1517 1518$$\begin{array}{c} 1519\termbdd{a}{\rho}{t}{b} \qquad \rho(v_1)=n_1,~ $\ldots$~,~ \rho(v_i)=n_i 1520\\ \hline 1521\termbdd{a}{\rho}{({\scriptstyle\exists} v_1~\cdots~v_i.~t)}% 1522{{\t{\footnotesize exist~(makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b} 1523\end{array}$$ 1524 1525\noindent \rule\minipagewidth{0.1pt} 1526 1527\begin{footnotesize} 1528Raises \t{BddExistsError} if any of the terms in the term list argument 1529are not boolean variables in the domain of $\rho$, 1530or occur free in any assumption 1531\end{footnotesize} 1532\end{minipage} 1533\end{lrbox} 1534\fbox{\usebox{\BddExists}}\index{HolBddLib!ML bindings!{BddExists}@\ml{BddExists}} 1535 1536\bigskip 1537 1538 1539\newsavebox\BddAppall 1540\noindent\begin{lrbox}\BddAppall 1541\begin{minipage}{\minipagewidth} 1542 1543\begin{footnotesize} 1544{\verb+BddAppall : term list -> bddop * term_bdd * term_bdd -> term_bdd+} 1545\end{footnotesize} 1546\vspace*{-3mm} 1547 1548\noindent \rule\minipagewidth{0.1pt} 1549 1550\vspace*{-2mm} 1551 1552$$\begin{array}{c} 1553\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 1554\\ \hline 1555\begin{array}{l} 1556{a_1 \cup a_2}% 1557~{\rho}% 1558~{({\scriptstyle\forall} v_1~\cdots~v_i.~% 1559{\t{\footnotesize termApply}}~t_1~t_2~bddop)}\\ 1560\mapsto\\ 1561{{\t{\footnotesize appall}}~b_1~b_2~bddop~% 1562{\t{\footnotesize (makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b} 1563\end{array} 1564\end{array}$$ 1565 1566\noindent \rule\minipagewidth{0.1pt} 1567 1568\begin{footnotesize} 1569Raises \t{BddAppallError} if the varmaps in the hypotheses are not pointer equal, or 1570if any of the terms in the term list argument 1571are not boolean variables in the domain of $\rho$, 1572or occur free in any assumption 1573\end{footnotesize} 1574\end{minipage} 1575\end{lrbox} 1576\fbox{\usebox{\BddAppall}}\index{HolBddLib!ML bindings!{BddAppall}@\ml{BddAppall}} 1577 1578 1579\bigskip 1580 1581 1582\newsavebox\BddAppex 1583\noindent\begin{lrbox}\BddAppex 1584\begin{minipage}{\minipagewidth} 1585 1586\begin{footnotesize} 1587{\verb+BddAppex : term list -> bddop * term_bdd * term_bdd -> term_bdd+} 1588\end{footnotesize} 1589\vspace*{-3mm} 1590 1591\noindent \rule\minipagewidth{0.1pt} 1592 1593\vspace*{-2mm} 1594 1595$$\begin{array}{c} 1596\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 1597\\ \hline 1598\begin{array}{l} 1599{a_1 \cup a_2}% 1600~{\rho}% 1601~{({\scriptstyle\exists} v_1~\cdots~v_i.~% 1602{\t{\footnotesize termApply}}~t_1~t_2~bddop)}\\ 1603\mapsto\\ 1604{{\t{\footnotesize appex}}~b_1~b_2~bddop~% 1605{\t{\footnotesize (makeset[}}n_1,\ldots,n_i{\t{\footnotesize ])}}~b} 1606\end{array} 1607\end{array}$$ 1608 1609\noindent \rule\minipagewidth{0.1pt} 1610 1611\begin{footnotesize} 1612Raises \t{BddAppexError} if the varmaps of the hypotheses are not pointer equal, or 1613if any of the terms in the term list argument 1614are not boolean variables in the domain of $\rho$, 1615or occur free in any assumption 1616\end{footnotesize} 1617\end{minipage} 1618\end{lrbox} 1619\fbox{\usebox{\BddAppex}}\index{HolBddLib!ML bindings!{BddAppex}@\ml{BddAppex}} 1620 1621\subsection{Composition, repacement and restriction} 1622 1623 1624\newsavebox\BddCompose 1625\begin{lrbox}\BddCompose 1626\begin{minipage}{\minipagewidth} 1627 1628\begin{footnotesize} 1629{\verb+BddCompose : term_bdd * term_bdd -> term_bdd -> term_bdd +} 1630\end{footnotesize} 1631\vspace*{-3mm} 1632 1633\noindent \rule\minipagewidth{0.1pt} 1634 1635\vspace*{-2mm} 1636 1637$$\begin{array}{c} 1638(\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_2}{\rho}{t_1}{b_1'}) 1639\qquad \termbdd{a}{\rho}{t}{b} 1640\\ \hline 1641\termbdd{a_1 \cup a_2 \cup a} 1642{\rho} 1643{(\mbox{\t{\footnotesize subst[$v_1$ |-> $t_1$] $t$}})} 1644{\mbox{\t{\footnotesize compose(var $b_1$, $b_1'$) $b$}}} 1645\end{array}$$ 1646 1647\noindent \rule\minipagewidth{0.1pt} 1648 1649\begin{footnotesize} 1650Raises \t{BddComposeError} if varmaps in the hypotheses are not pointer equal, 1651or the term $v_1$ is not a variable 1652\end{footnotesize} 1653\end{minipage} 1654\end{lrbox} 1655\fbox{\usebox{\BddCompose}}\index{HolBddLib!ML bindings!{BddCompose}@\ml{BddCompose}} 1656 1657\bigskip 1658 1659\newsavebox\BddListCompose 1660\noindent\begin{lrbox}\BddListCompose 1661\begin{minipage}{\minipagewidth} 1662 1663\begin{footnotesize} 1664{\verb+BddListCompose : (term_bdd * term_bdd) list -> term_bdd -> term_bdd +} 1665\end{footnotesize} 1666\vspace*{-3mm} 1667 1668\noindent \rule\minipagewidth{0.1pt} 1669 1670\vspace*{-2mm} 1671 1672$$\begin{array}{c} 1673\begin{array}{l} 1674{\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{t_1}{b_1'}), \\ 1675\phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\ 1676\phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{t_i}{b_i'}){\t{\footnotesize ]}} 1677\qquad \termbdd{a}{\rho}{t}{b} 1678\end{array} 1679\\ \hline 1680\begin{array}{l} 1681{a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\ 1682{\rho}\\ 1683{\mbox{\t{\footnotesize subst[$v_1$ |-> $t_1$,~$\ldots$~,~$v_i$ |-> $t_i$] $t$}}}\\ 1684\mapsto\\ 1685{\mbox{\t{\footnotesize veccompose(composeSet[(var $b_1$, $b_1'$),~$\ldots$~,~(var $b_i$, $b_i'$)])$b$}}} 1686\end{array} 1687\end{array}$$ 1688 1689\noindent \rule\minipagewidth{0.1pt} 1690 1691\begin{footnotesize} 1692Raises \t{BddListComposeError} if the varmaps in the hypotheses are not all pointer equal, 1693or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables 1694\end{footnotesize} 1695\end{minipage} 1696\end{lrbox} 1697\fbox{\usebox{\BddListCompose}}\index{HolBddLib!ML bindings!{BddListCompose}@\ml{BddListCompose}} 1698 1699 1700\bigskip 1701 1702\newsavebox\BddRestrict 1703\noindent\begin{lrbox}\BddRestrict 1704\begin{minipage}{\minipagewidth} 1705 1706\begin{footnotesize} 1707{\verb+BddRestrict : (term_bdd * term_bdd) list -> term_bdd -> term_bdd +} 1708\end{footnotesize} 1709\vspace*{-3mm} 1710 1711\noindent \rule\minipagewidth{0.1pt} 1712 1713\vspace*{-2mm} 1714 1715$$\begin{array}{c} 1716\begin{array}{l} 1717{\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{c_1}{b_1'}), \\ 1718\phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\ 1719\phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{c_i}{b_i'}){\t{\footnotesize ]}} 1720\qquad \termbdd{a}{\rho}{t}{b} 1721\end{array} 1722\\ \hline 1723\begin{array}{l} 1724{a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\ 1725{\rho}\\ 1726{\mbox{\t{\footnotesize subst[$v_1$ |-> $c_1$,~$\ldots$~,~$v_i$ |-> $c_i$] $t$}}}\\ 1727\mapsto\\ 1728{\mbox{\t{\footnotesize restrict~$b$~(assignment[(var $b_1$, $\hat{c_1}$),~$\ldots$~,~(var $b_i$, $\hat{c_i}$)])}}} 1729\end{array} 1730\end{array}$$ 1731 1732\noindent \rule\minipagewidth{0.1pt} 1733 1734\begin{footnotesize} 1735Where each of $c_1,\ldots,c_i$ is either the constant \t{F} or the constant \t{F}, 1736and $\hat{\t{T}}$ denotes the ML value \t{true} and 1737$\hat{\t{F}}$ denotes \t{false}. The exception 1738\t{BddRestrictError} is raised if the varmaps in the hypotheses are not all pointer equal, 1739or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables, 1740or if any of $c_1,\ldots,c_i$ are not equal to \t{T} or \t{F} 1741\end{footnotesize} 1742\end{minipage} 1743\end{lrbox} 1744\fbox{\usebox{\BddRestrict}}\index{HolBddLib!ML bindings!{BddRestrict}@\ml{BddRestrict}} 1745 1746 1747\bigskip 1748 1749\newsavebox\BddReplace 1750\noindent\begin{lrbox}\BddReplace 1751\begin{minipage}{\minipagewidth} 1752 1753\begin{footnotesize} 1754{\verb+BddReplace : (term_bdd * term_bdd) list -> term_bdd -> term_bdd +} 1755\end{footnotesize} 1756\vspace*{-3mm} 1757 1758\noindent \rule\minipagewidth{0.1pt} 1759 1760\vspace*{-2mm} 1761 1762$$\begin{array}{c} 1763\begin{array}{l} 1764{\t{\footnotesize [}} (\termbdd{a_1}{\rho}{v_1}{b_1},~~ \termbdd{a_1'}{\rho}{v_1'}{b_1'}), \\ 1765\phantom{{\t{\footnotesize [}}(\termbdd{a_1}{\rho}{v_1}{b_1}} \vdots\\ 1766\phantom{{\t{\footnotesize [}}}(\termbdd{a_i}{\rho}{v_i}{b_i},~~~~ \termbdd{a_i'}{\rho}{v_i'}{b_i'}){\t{\footnotesize ]}} 1767\qquad \termbdd{a}{\rho}{t}{b} 1768\end{array} 1769\\ \hline 1770\begin{array}{l} 1771{a_1 \cup a_1'~\cup~\cdots~\cup~a_i \cup a_i' \cup a}\\ 1772{\rho}\\ 1773{\mbox{\t{\footnotesize subst[$v_1$ |-> $v_1'$,~$\ldots$~,~$v_i$ |-> $v_i'$] $t$}}}\\ 1774\mapsto\\ 1775{\mbox{\t{\footnotesize replace~$b$~(makepairSet[(var $b_1$, var $b_1'$),~$\ldots$~,~(var $b_i$, var $b_i'$)])}}} 1776\end{array} 1777\end{array}$$ 1778 1779\noindent \rule\minipagewidth{0.1pt} 1780 1781\begin{footnotesize} 1782Raises \t{BddReplaceError} if the varmaps in the hypotheses are not all pointer equal, 1783or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables, 1784or if any of the terms $v_1',\ldots,v_i'$ are repeated or are not variables 1785\end{footnotesize} 1786\end{minipage} 1787\end{lrbox} 1788\fbox{\usebox{\BddReplace}}\index{HolBddLib!ML bindings!{BddReplace}@\ml{BddReplace}} 1789 1790\subsection{Coudert, Berthet \& Madre simplification}\label{BddSimplify} 1791 1792\vspace*{-1mm} 1793 1794\newsavebox\BddSimplify 1795\begin{lrbox}\BddSimplify 1796\begin{minipage}{\minipagewidth} 1797 1798\begin{footnotesize} 1799{\verb+BddSimplify : term_bdd * term_bdd -> term_bdd +} 1800\end{footnotesize} 1801\vspace*{-3mm} 1802 1803\noindent \rule\minipagewidth{0.1pt} 1804 1805\vspace*{-2mm} 1806 1807$$\begin{array}{c} 1808\termbdd{a_1}{\rho}{t_1}{b_1} \qquad \termbdd{a_2}{\rho}{t_2}{b_2} 1809\\ \hline 1810\termbdd{a_1\cup a_2\cup \setass{t_1}}{\rho}{t_2}{{\t{\footnotesize simplify}}~b_1~b_2} 1811\end{array}$$ 1812 1813\noindent \rule\minipagewidth{0.1pt} 1814 1815\begin{footnotesize} 1816The exception 1817{\t{\footnotesize BddSimplifyError}} is raised if the varmaps in the hypotheses are not pointer equal 1818\end{footnotesize} 1819\end{minipage} 1820\end{lrbox} 1821\fbox{\usebox{\BddSimplify}}\index{HolBddLib!ML bindings!{BddSimplify}@\ml{BddSimplify}} 1822 1823\vspace*{-2mm} 1824 1825\subsection{Finding a satisfying assignment}\label{BddFindModel} 1826 1827\vspace*{-1mm} 1828 1829\newsavebox\BddFindModel 1830\begin{lrbox}\BddFindModel 1831\begin{minipage}{\minipagewidth} 1832 1833\begin{footnotesize} 1834{\verb+BddFindModel : term_bdd -> term_bdd +} 1835\end{footnotesize} 1836\vspace*{-3mm} 1837 1838\noindent \rule\minipagewidth{0.1pt} 1839 1840\vspace*{-2mm} 1841 1842$$\begin{array}{c} 1843\termbdd{a}{\rho}{t}{b} 1844\\ \hline 1845\termbdd{a\cup \setass{v_1=c_1,\ldots,v_p=c_p}}{\rho}{t}{{\t{\footnotesize TRUE}}} 1846\end{array}$$ 1847 1848\noindent \rule\minipagewidth{0.1pt} 1849 1850\begin{footnotesize} 1851The set $\{v_1=c_1,\ldots,v_p=c_p\}$ is a satisfying assignment for $t$ 1852($c_i$ is \T{} or \F{} for $1\leq i \leq p$). Exception 1853{\t{\footnotesize BddFindModelError}} is raised if {\t{\footnotesize satone}} 1854can't find a satisfying assignment. 1855\end{footnotesize} 1856\end{minipage} 1857\end{lrbox} 1858\fbox{\usebox{\BddFindModel}}\index{HolBddLib!ML bindings!{BddFindModel}@\ml{BddFindModel}} 1859 1860\subsection{Linking representation judgements to theorems}\label{oracle}\index{HolBddLib!termbdd@\ml{term\_bdd}!linking to theorems} 1861 1862\noindent \newsavebox\BddThmOracle 1863\begin{lrbox}\BddThmOracle 1864\begin{minipage}{\minipagewidth} 1865 1866{\verb+BddThmOracle : term_bdd -> thm+} 1867 1868\vspace*{-3mm} 1869 1870\noindent \rule\minipagewidth{0.1pt} 1871 1872\vspace*{-2mm} 1873 1874$$\begin{array}{c} 1875\termbdd{a}{\rho}{t}{\ml{TRUE}} 1876\\ \hline 1877\texttt{[oracles:~HolBdd]}~ a \vdash t 1878\end{array}$$ 1879 1880\noindent \rule\minipagewidth{0.1pt} 1881 1882\begin{footnotesize} 1883Allows HOL theorems to be `proved' by BDD calculation using \Buddy{}. 1884Such theorems, and any theorems deduced from them, are tagged with 1885\t{HolBdd} and so can be easily identified. 1886\end{footnotesize} 1887\end{minipage} 1888\end{lrbox} 1889\fbox{\usebox{\BddThmOracle}}\index{HolBddLib!ML bindings!{BddThmOracle}@\ml{BddThmOracle}} 1890 1891\bigskip 1892 1893 1894\noindent \newsavebox\BddEqMp 1895\begin{lrbox}\BddEqMp 1896\begin{minipage}{\minipagewidth} 1897 1898{\verb+BddEqMp : thm -> term_bdd -> term_bdd+} 1899 1900\vspace*{-3mm} 1901 1902\noindent \rule\minipagewidth{0.1pt} 1903 1904\vspace*{-2mm} 1905 1906$$\begin{array}{c} 1907a_1 \vdash t_1=t_2 \qquad \termbdd{a_2}{\rho}{t_1}{b} \qquad 1908\\ \hline 1909\termbdd{a_1 \cup a_2}{\rho}{t_2}{b} 1910\end{array}$$\label{BddEqMp} 1911 1912\noindent \rule\minipagewidth{0.1pt} 1913 1914\begin{footnotesize} 1915Enables the term part of a representation judgement to be replaced 1916by a logically equivalent term. Raises \t{BddEqMpError} 1917if the left hand side of the equation 1918isn't $\alpha$-convertable to the term part of the representation judgement 1919\end{footnotesize} 1920\end{minipage} 1921\end{lrbox} 1922\fbox{\usebox{\BddEqMp}}\index{HolBddLib!ML bindings!{BddEqMp}@\ml{BddEqMp}} 1923 1924\subsection{Miscellaneous functions}\label{misc} 1925 1926%\paragraph{\t{term\_bdd} destructors} 1927 1928\noindent \newsavebox\destructors 1929\begin{lrbox}\destructors 1930\begin{minipage}{\minipagewidth} 1931 1932\begin{footnotesize} 1933\begin{verbatim} 1934dest_term_bdd : term_bdd -> assums * varmap * term * bdd 1935getAssums : term_bdd -> assums 1936getVarmap : term_bdd -> varmap 1937getTerm : term_bdd -> term 1938getBdd : term_bdd -> bdd 1939\end{verbatim} 1940\end{footnotesize} 1941\vspace*{-6mm} 1942 1943\noindent \rule\minipagewidth{0.1pt} 1944 1945\vspace*{1mm} 1946 1947\begin{footnotesize} 1948\hspace*{-1.5mm}$\begin{array}{ll} 1949\t{dest\_term\_bdd}~(\termbdd{a}{\rho}{t}{b})&=~(\rho, t, b)\\ 1950\t{getVarmap}~(\termbdd{a}{\rho}{t}{b})&=~\rho\\ 1951\t{getTerm}~(\termbdd{a}{\rho}{t}{b})&=~t\\ 1952\t{getBdd}~(\termbdd{a}{\rho}{t}{b})&=~b 1953\end{array}$ 1954\end{footnotesize} 1955\end{minipage} 1956\end{lrbox} 1957\fbox{\usebox{\destructors}}\index{HolBddLib!termbdd@\ml{term\_bdd}!destructors} 1958 1959\bigskip 1960 1961\noindent \newsavebox\inSupport 1962\begin{lrbox}\inSupport 1963\begin{minipage}{\minipagewidth} 1964 1965\begin{footnotesize} 1966{\verb+inSupport : int -> bdd -> bool +} 1967\end{footnotesize} 1968\vspace*{-3mm} 1969 1970\noindent \rule\minipagewidth{0.1pt} 1971 1972\begin{footnotesize} 1973\t{inSupport}~$n$~$b$ checks if the BDD variable $n$ occurs in the BDD $b$ 1974\end{footnotesize} 1975\end{minipage} 1976\end{lrbox} 1977\fbox{\usebox{\inSupport}}\index{HolBddLib!ML bindings!{inSupport}@\ml{inSupport}} 1978 1979\bigskip 1980 1981\noindent \newsavebox\termApply 1982\begin{lrbox}\termApply 1983\begin{minipage}{\minipagewidth} 1984 1985\begin{footnotesize} 1986{\verb+termApply : term -> term -> bddop -> term+} 1987\end{footnotesize} 1988\vspace*{-3mm} 1989 1990\noindent \rule\minipagewidth{0.1pt} 1991 1992\begin{footnotesize} 1993\t{termApply}~$t_1$~$t_2$~$bddop$ applies the HOL operation 1994corresponding to $bddop$ to $t_1$ and $t_2$. 1995 1996\vspace*{-2mm} 1997 1998\begin{verbatim} 1999 fun termApply t1 t2 bddop = 2000 case bddop of 2001 And => mk_conj(t1,t2) 2002 | Biimp => mk_eq(t1,t2) 2003 | Diff => mk_conj(t1, mk_neg t2) 2004 | Imp => mk_imp(t1,t2) 2005 | Invimp => mk_imp(t2,t1) 2006 | Lessth => mk_conj(mk_neg t1, t2) 2007 | Nand => mk_neg(mk_conj(t1,t2)) 2008 | Nor => mk_neg(mk_disj(t1,t2)) 2009 | Or => mk_disj(t1,t2) 2010 | Xor => mk_neg(mk_eq(t1,t2)); 2011\end{verbatim} 2012\end{footnotesize} 2013\end{minipage} 2014\end{lrbox} 2015\fbox{\usebox{\termApply}}\index{HolBddLib!ML bindings!{termApply}@\ml{termApply}} 2016 2017\subsection{The structure \t{DerivedBddRules}}\label{DerivedBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!derived rules} 2018 2019This section notes a few of the more commonly used functions available in the structure \texttt{DerivedBddRules}. 2020 2021\subsection{Varmaps} 2022 2023\bigskip 2024 2025\noindent \newsavebox\extendVarmap 2026\begin{lrbox}\extendVarmap 2027\hbc{extendVarmap : term list -> varmap -> varmap}{Extend a varmap with a list of variables (allocating new BDD variables, if necessary).} 2028\end{lrbox} 2029\fbox{\usebox{\extendVarmap}}\index{HolBddLib!ML bindings!{extendVarmap}@\ml{extendVarmap}} 2030 2031 2032\bigskip 2033 2034\noindent \newsavebox\globalvarmap 2035\begin{lrbox}\globalvarmap 2036\hbc{global\_varmap : varmap ref}{Global assignable varmap.} 2037\end{lrbox} 2038\fbox{\usebox{\globalvarmap}}\index{HolBddLib!ML bindings!{global\_varmap}@\ml{global\_varmap}} 2039 2040\subsection{Tests} 2041 2042\bigskip 2043 2044\noindent \newsavebox\BddEqualTest 2045\begin{lrbox}\BddEqualTest 2046\hbc{BddEqualTest : \termbddty -> \termbddty -> bool}{Test equality of BDD component of two term\_bdds and return true or false} 2047\end{lrbox} 2048\fbox{\usebox{\BddEqualTest}}\index{HolBddLib!ML bindings!{BddEqualTest}@\ml{BddEqualTest}} 2049 2050\bigskip 2051 2052\noindent \newsavebox\isTRUE 2053\begin{lrbox}\isTRUE 2054\hbc{isTRUE : \termbddty -> bool}{Test if the BDD part is TRUE} 2055\end{lrbox} 2056\fbox{\usebox{\isTRUE}}\index{HolBddLib!ML bindings!{isTRUE}@\ml{isTRUE}} 2057 2058\bigskip 2059 2060\noindent \newsavebox\isFALSE 2061\begin{lrbox}\isFALSE 2062\hbc{isFALSE : \termbddty -> bool}{Test if the BDD part is FALSE} 2063\end{lrbox} 2064\fbox{\usebox{\isFALSE}}\index{HolBddLib!ML bindings!{isFALSE}@\ml{isFALSE}} 2065 2066\subsection{Conversion to terms} 2067 2068\bigskip 2069 2070\noindent \newsavebox\GenTermToTermBdd 2071\begin{lrbox}\GenTermToTermBdd 2072\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.} 2073\end{lrbox} 2074\fbox{\usebox{\GenTermToTermBdd}}\index{HolBddLib!ML bindings!{GenTermToTermBdd}@\ml{GenTermToTermBdd}} 2075 2076\bigskip 2077 2078\noindent \newsavebox\failfn 2079\begin{lrbox}\failfn 2080\hbc{failfn : 'a -> 'b}{Function that always raises exception fail (useful as argument to GenTermToTermBdd).} 2081\end{lrbox} 2082\fbox{\usebox{\failfn}}\index{HolBddLib!ML bindings!{failfn}@\ml{failfn}} 2083 2084\bigskip 2085 2086\noindent \newsavebox\bddToTerm 2087\begin{lrbox}\bddToTerm 2088\hbc{bddToTerm : varmap -> bdd -> term}{Convert a BDD to a nested conditional term with respect to a varmap .} 2089\end{lrbox} 2090\fbox{\usebox{\bddToTerm}}\index{HolBddLib!ML bindings!{bddToTerm}@\ml{bddToTerm}} 2091 2092\bigskip 2093 2094\noindent \newsavebox\termToTermBdd 2095\begin{lrbox}\termToTermBdd 2096\hbc{termToTermBdd : term -> \termbddty}{Like \texttt{GenTermToTermBdd} but fails on non-boolean leaves.} 2097\end{lrbox} 2098\fbox{\usebox{\termToTermBdd}}\index{HolBddLib!ML bindings!{termToTermBdd}@\ml{termToTermBdd}} 2099\bigskip 2100 2101\noindent \newsavebox\destBddOp 2102\begin{lrbox}\destBddOp 2103\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.} 2104\end{lrbox} 2105\fbox{\usebox{\destBddOp}}\index{HolBddLib!ML bindings!{dest\_BddOp}@\ml{dest\_BddOp}} 2106 2107\subsection{Extracting theorems} 2108 2109\bigskip 2110 2111\noindent \newsavebox\TermBddToEqThm 2112\begin{lrbox}\TermBddToEqThm 2113\hbc{TermBddToEqThm : \termbddty -> thm}{\[\frac{\termbdd{a}{\rho}{t}{b}} 2114 {a \turn t = (\mathtt{bddToTerm}\, \rho\, b)}\]} 2115\end{lrbox} 2116\fbox{\usebox{\TermBddToEqThm}}\index{HolBddLib!ML bindings!{TermBddToEqThm}@\ml{TermBddToEqThm}} 2117 2118\bigskip 2119 2120\noindent \newsavebox\BddRhsOracle 2121\begin{lrbox}\BddRhsOracle 2122\hbc{BddRhsOracle : (term -> \termbddty) -> varmap -> thm -> thm}{\[\frac{\turn\,t1=t2}{\turn t1}\] 2123 if the BDD of t2 (using \texttt{GenTermToTermBdd}) is \texttt{TRUE}.} 2124\end{lrbox} 2125\fbox{\usebox{\BddRhsOracle}}\index{HolBddLib!ML bindings!{BddRhsOracle}@\ml{BddRhsOracle}} 2126 2127\bigskip 2128 2129\noindent \newsavebox\findModel 2130\begin{lrbox}\findModel 2131\hbc{findModel : \termbddty -> thm} 2132{If $t$ is satisfiable (i.e., $b$ is not \texttt{FALSE}) 2133\[\frac{\termbdd{a}{\rho}{t}{b}}{a \cup \{v_1=c_1,\ldots,v_n=c_n\} \turn t}\] 2134 Similar to \texttt{BddFindModel} followed by \texttt{BddThmOracle}, but checks the 2135 assignment found by \texttt{satone} using proof, so is pure 2136 (i.e., result not tagged with \texttt{HolBdd}).} 2137\end{lrbox} 2138\fbox{\usebox{\findModel}}\index{HolBddLib!ML bindings!{findModel}@\ml{findModel}} 2139 2140\subsection{Manipulating term\_bdd's} 2141 2142\bigskip 2143 2144\noindent \newsavebox\BddApThm 2145\begin{lrbox}\BddApThm 2146\hbc{BddApThm : thm -> \termbddty -> \termbddty}{\[\frac{a1\,\turn\,t1=t2\qquad\termbdd{a2}{\rho}{t1'}{b}} 2147 {\termbdd{a1\cup a2}{\rho}{t2'}{b}}\] 2148where t1 can be instantiated to t1' and t2' is the corresponding instance of t2.} 2149\end{lrbox} 2150\fbox{\usebox{\BddApThm}}\index{HolBddLib!ML bindings!{BddApThm}@\ml{BddApThm}} 2151 2152\bigskip 2153 2154\noindent \newsavebox\BddApReplace 2155\begin{lrbox}\BddApReplace 2156\hbc{BddApReplace : \termbddty -> term -> \termbddty}{\[\frac{\termbdd{a}{\rho}{t}{b}} 2157 {\termbdd{a}{\rho}{t'}{b'}}\] 2158where boolean variables in t can be renamed to get t' and b' is the corresponding replacement of BDD variables in b.} 2159\end{lrbox} 2160\fbox{\usebox{\BddApReplace}}\index{HolBddLib!ML bindings!{BddApReplace}@\ml{BddApReplace}} 2161 2162\bigskip 2163 2164\noindent \newsavebox\BddApRestrict 2165\begin{lrbox}\BddApRestrict 2166\hbc{BddApRestrict : \termbddty -> term -> \termbddty}{\[\frac{\termbdd{a}{\rho}{t}{b}} 2167 {\termbdd{a}{\rho}{t'}{b'}}\] 2168Generates the BDD of a supplied term if it can be obtained by restricting a given term\_bdd.} 2169\end{lrbox} 2170\fbox{\usebox{\BddApRestrict}}\index{HolBddLib!ML bindings!{BddApRestrict}@\ml{BddApRestrict}} 2171 2172\bigskip 2173 2174\noindent \newsavebox\BddSubst 2175\begin{lrbox}\BddSubst 2176\hbc{BddSubst : (\termbddty * \termbddty) list -> \termbddty -> \termbddty} 2177{\[\frac{\begin{array}{c} 2178 [(\termbdd{a_1}{\rho}{v_1}{b_1},\termbdd{a_1'}{\rho}{t_1}{b_1'}) \\ 2179 \vdots\\ 2180 (\termbdd{a_i}{\rho}{v_i}{b_i},\termbdd{a_i'}{\rho}{t_i}{b_i'})] \\ 2181 \termbdd{a}{\rho}{t}{b} \\ 2182 \end{array}} 2183 {\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}}\] 2184 BddSubst applies a substitution $[(vtb_1,newtb_1),...,(vtb_i,newtb_i)]$ 2185 to a term\_bdd, where $vtb_p$ ($1 \leq p \leq i$) must be of the form 2186 $\termbdd{a}{\rho}{v_p}{b_p}$ where $v_p$ is a variable, and the varmaps are distinct 2187 2188 This preliminary version separates the substitution into a 2189 restriction (variables mapped to \texttt{T} or \texttt{F}) followed by a variable 2190 renaming (replacement). A more elaborate scheme will be implemented 2191 using BuDDy's bdd\_veccompose.} 2192\end{lrbox} 2193\fbox{\usebox{\BddSubst}}\index{HolBddLib!ML bindings!{BddSubst}@\ml{BddSubst}} 2194 2195\bigskip 2196 2197\noindent \newsavebox\BddApSubst 2198\begin{lrbox}\BddApSubst 2199\hbc{BddApSubst : \termbddty -> term -> \termbddty}{\[\frac{\termbdd{a}{\rho}{t}{b}} 2200 {\termbdd{a}{\rho}{t'}{b'}}\] 2201where boolean variables in t can be instantiated to get t' and b' is the corresponding replacement of BDD variables in b.} 2202\end{lrbox} 2203\fbox{\usebox{\BddApSubst}}\index{HolBddLib!ML bindings!{BddApSubst}@\ml{BddApSubst}} 2204 2205\bigskip 2206 2207\noindent \newsavebox\eqToTermBdd 2208\begin{lrbox}\eqToTermBdd 2209\hbc{eqToTermBdd : (term -> \termbddty) -> varmap -> thm -> \termbddty}{\[\frac{a\,\turn\,t1=t2} 2210 {\termbdd{a}{\rho}{t1}{\langle\textup{BDD of t2}\rangle}}\] 2211Fails if \texttt{GenTermToTermBdd} fails on $t2$ with the supplied leaf function.} 2212\end{lrbox} 2213\fbox{\usebox{\eqToTermBdd}}\index{HolBddLib!ML bindings!{eqToTermBdd}@\ml{eqToTermBdd}} 2214 2215\bigskip 2216 2217\noindent \newsavebox\BddApConv 2218\begin{lrbox}\BddApConv 2219\hbc{BddApConv : conv -> \termbddty -> \termbddty}{\[\frac{\termbdd{a}{\rho}{t}{b}\qquad \mathtt{conv}\, t = (a' \turn t = t')} 2220 {\termbdd{a\cup a'}{\rho}{t'}{b}}\]} 2221\end{lrbox} 2222\fbox{\usebox{\BddApConv}}\index{HolBddLib!ML bindings!{BddApConv}@\ml{BddApConv}} 2223 2224\bigskip 2225 2226\noindent \newsavebox\BddSatone 2227\begin{lrbox}\BddSatone 2228\hbc{BddSatone : \termbddty -> (\termbddty * \termbddty) list} 2229{\[\frac{\termbdd{a}{\rho}{t}{b}} 2230 {\begin{array}{c} 2231 [(\termbdd{a_1}{\rho}{v_1}{b_1},\termbdd{a_1'}{\rho}{c_1}{b_1'}) \\ 2232 \vdots\\ 2233 (\termbdd{a_i}{\rho}{v_i}{b_i},\termbdd{a_i'}{\rho}{c_i}{b_i'})] \\ 2234 \end{array}}\] 2235with the property that 2236\[\mathtt{isTRUE} \left(\mathtt{BddRestrict}{\begin{array}{c} 2237 [(\termbdd{a_1}{\rho}{v_1}{b_1},\termbdd{a_1'}{\rho}{c_1}{b_1'}) \\ 2238 \vdots\\ 2239 (\termbdd{a_i}{\rho}{v_i}{b_i},\termbdd{a_i'}{\rho}{c_i}{b_i'})] \\ 2240 \end{array}} {\termbdd{a}{\rho}{t}{b}}\right) \] 2241} 2242\end{lrbox} 2243\fbox{\usebox{\BddSatone}}\index{HolBddLib!ML bindings!{BddSatone}@\ml{BddSatone}} 2244 2245\subsection{Fixed points and traces} 2246 2247\bigskip 2248 2249\noindent \newsavebox\computeFixedpoint 2250\begin{lrbox}\computeFixedpoint 2251\hbc{computeFixedpoint : reportfn\_ty -> varmap -> thm * thm -> \termbddty} 2252{\[\frac{\turn f\, 0\, s = \ldots s \ldots \qquad \turn \forall n. f (n+1) s = \ldots f\, n \ldots s \ldots} 2253 {(\termbdd{}{\rho}{f\, i\, s}{b_i},\termbdd{}{\rho}{f\, (i+1)\, s}{b_{i+1}})}\] 2254 where $i$ is the first number such that $\turn f\, (i+1)\, s = f\, i\, s$ 2255and the function reportfn is applied to the iteration level and current 2256term\_bdd and can be used for tracing. 2257 2258A state of the iteration is a pair (tb,tb') consisting of the 2259previous term\_bdd tb and the current one tb'. The initial state 2260is (somewhat arbitarily) taken to be (tb0,tb0). } 2261\end{lrbox} 2262\fbox{\usebox{\computeFixedpoint}}\index{HolBddLib!ML bindings!{computeFixedpoint}@\ml{computeFixedpoint}} 2263 2264\bigskip 2265 2266\noindent \newsavebox\computeTrace 2267\begin{lrbox}\computeTrace 2268\hbc{computeTrace : reportfn\_ty -> varmap -> thm -> thm*thm -> \termbddty list} 2269{\[\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} 2270 {(\termbdd{}{\rho}{f\, i\, s}{b_i},\termbdd{}{\rho}{f\, 0\, s}{b_0})}\] 2271 where $i$ is the first number such that $\turn f\, i\, s = p\, s$. } 2272\end{lrbox} 2273\fbox{\usebox{\computeTrace}}\index{HolBddLib!ML bindings!{computeTrace}@\ml{computeTrace}} 2274 2275\bigskip 2276 2277\noindent \newsavebox\findTrace 2278\begin{lrbox}\findTrace 2279\hbc{findTrace : varmap -> thm -> thm -> thm -> thm * thm list * thm} 2280{\[\frac{ 2281 \begin{array}{l} 2282 \turn R((v_1,\ldots,v_n),(v_1',\ldots,v_n')) \\ 2283 \turn P(v_1,\ldots,v_n) = \ldots \\ 2284 \turn Q(v_1,\ldots,v_n) = \ldots \\ 2285 \end{array}} 2286 {(\turn P s_0,[\turn R(s_0,s_1),\ldots,\turn R(s_{n-1},s_n))],\turn Q s_n)}\]} 2287\end{lrbox} 2288\fbox{\usebox{\findTrace}}\index{HolBddLib!ML bindings!{findTrace}@\ml{findTrace}} 2289 2290\bigskip 2291 2292\noindent \newsavebox\MakeSimpRecThm 2293\begin{lrbox}\MakeSimpRecThm 2294\hbc{MakeSimpRecThm : thm -> thm}{Perform disjunctive partitioning. Implemented by \[\mathtt{SIMP\_RULE\, bool\_ss\, [LEFT\_AND\_OVER\_OR,EXISTS\_OR\_THM]}\]} 2295\end{lrbox} 2296\fbox{\usebox{\MakeSimpRecThm}}\index{HolBddLib!ML bindings!{MakeSimpRecThm}@\ml{MakeSimpRecThm}} 2297 2298\index{HolBddLib|)} 2299\bibliographystyle{plain} 2300\bibliography{description} 2301 2302%\printindex 2303 2304\end{document} 2305